+
+(* Begin Lucca Hirschi *)
+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