+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 *)
+