INCLUDE "utils.ml"
open Format
-type move = [ `Left | `Right ]
+type move = [ `Left | `Right | `Self ]
type 'hcons expr =
| False | True
| Or of 'hcons * 'hcons
type 'hcons node = {
pos : 'hcons expr;
mutable neg : 'hcons;
- st : StateSet.t * StateSet.t;
+ st : StateSet.t * StateSet.t * StateSet.t;
size: int; (* Todo check if this is needed *)
}
| Or _ -> 1
(* Begin Lucca Hirschi *)
-let rec eval_form ss f = match expr f with
- | False -> false
- | True -> true
- | And(f1,f2) -> eval_form ss f1 && eval_form ss f2
- | Or(f1,f2) -> eval_form ss f1 || eval_form ss f2
- | Atom(dir, b, s) ->
- let set = match dir with |`Left -> fst ss | `Right -> snd ss in
- StateSet.mem s set
-(* End *)
+module type HcEval =
+sig
+ type t = StateSet.t*StateSet.t*StateSet.t*Node.t
+ val equal : t -> t -> bool
+ val hash : t -> int
+end
+
+type dStateS = StateSet.t*StateSet.t
+module type HcInfer =
+sig
+ type t = dStateS*dStateS*dStateS*Node.t
+ val equal : t -> t -> bool
+ val hash : t -> int
+end
+
+module HcEval : HcEval = struct
+ type t =
+ StateSet.t*StateSet.t*StateSet.t*Node.t
+ let equal (s,l,r,f) (s',l',r',f') = StateSet.equal s s' &&
+ StateSet.equal l l' && StateSet.equal r r' && Node.equal f f'
+ let hash (s,l,r,f) =
+ HASHINT4(StateSet.hash s, StateSet.hash l, StateSet.hash r, Node.hash f)
+end
+
+let dequal (x,y) (x',y') = StateSet.equal x x' && StateSet.equal y y'
+let dhash (x,y) = HASHINT2(StateSet.hash x, StateSet.hash y)
+module HcInfer : HcInfer = struct
+ type t = dStateS*dStateS*dStateS*Node.t
+ let equal (s,l,r,f) (s',l',r',f') = dequal s s' &&
+ dequal l l' && dequal r r' && Node.equal f f'
+ let hash (s,l,r,f) =
+ HASHINT4(dhash s, dhash l, dhash r, Node.hash f)
+end
+module HashEval = Hashtbl.Make(HcEval)
+module HashInfer = Hashtbl.Make(HcInfer)
+type hcEval = bool Hashtbl.Make(HcEval).t
+type hcInfer = bool Hashtbl.Make(HcInfer).t
+
+let rec eval_form (q,qf,qn) f hashEval =
+try HashEval.find hashEval (q,qf,qn,f)
+with _ ->
+ let res = match expr f with
+ | False -> false
+ | True -> true
+ | And(f1,f2) -> eval_form (q,qf,qn) f1 hashEval &&
+ eval_form (q,qf,qn) f2 hashEval
+ | Or(f1,f2) -> eval_form (q,qf,qn) f1 hashEval ||
+ eval_form (q,qf,qn) f2 hashEval
+ | Atom(dir, b, s) ->
+ let set = match dir with
+ |`Left -> qf | `Right -> qn | `Self -> q in
+ if b then StateSet.mem s set
+ else not (StateSet.mem s set) in
+ HashEval.add hashEval (q,qf,qn,f) res;
+ res
+
+let rec infer_form sq sqf sqn f hashInfer =
+try HashInfer.find hashInfer (sq,sqf,sqn,f)
+with _ ->
+ let res = match expr f with
+ | False -> false
+ | True -> true
+ | And(f1,f2) -> infer_form sq sqf sqn f1 hashInfer &&
+ infer_form sq sqf sqn f2 hashInfer
+ | Or(f1,f2) -> infer_form sq sqf sqn f1 hashInfer ||
+ infer_form sq sqf sqn f2 hashInfer
+ | Atom(dir, b, s) ->
+ let setq, setr = match dir with
+ | `Left -> sqf | `Right -> sqn | `Self -> sq in
+ (* WG: WE SUPPOSE THAT Q^r and Q^q are disjoint ! *)
+ let mem = StateSet.mem s setq || StateSet.mem s setr in
+ if b then mem else not mem in
+ HashInfer.add hashInfer (sq,sqf,sqn,f) res;
+ res
+(* End *)
+
let rec print ?(parent=false) ppf f =
if parent then fprintf ppf "(";
let _ = match expr f with
match dir with
| `Left -> Pretty.down_arrow, Pretty.subscript 1
| `Right -> Pretty.down_arrow, Pretty.subscript 2
+ | `Self -> Pretty.down_arrow, Pretty.subscript 0
in
fprintf fmt "%s%s" a_str d_str;
State.print fmt s;
pnode,nnode
-let empty_pair = StateSet.empty, StateSet.empty
-let true_,false_ = cons True False empty_pair empty_pair 0 0
+let empty_triple = StateSet.empty, StateSet.empty, StateSet.empty
+let true_,false_ = cons True False empty_triple empty_triple 0 0
let atom_ d p s =
let si = StateSet.singleton s in
let ss = match d with
- | `Left -> si, StateSet.empty
- | `Right -> StateSet.empty, si
+ | `Left -> StateSet.empty, si, StateSet.empty
+ | `Right -> StateSet.empty, StateSet.empty, si
+ | `Self -> si, StateSet.empty, StateSet.empty
in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
let not_ f = f.Node.node.neg
-let union_pair (l1,r1) (l2, r2) =
+let union_triple (s1,l1,r1) (s2,l2, r2) =
+ StateSet.union s1 s2,
StateSet.union l1 l2,
StateSet.union r1 r2
let merge_states f1 f2 =
let sp =
- union_pair (st f1) (st f2)
+ union_triple (st f1) (st f2)
and sn =
- union_pair (st (not_ f1)) (st (not_ f2))
+ union_triple (st (not_ f1)) (st (not_ f2))
in
sp,sn