Evaluation anf inference of formulas are now hconsed (in Formula).

[tatoo.git] / src / formula.ml

diff --git a/src/formula.ml b/src/formula.ml
index 225440f..6c98118 100644 (file)
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -73,28 +73,81 @@ let prio f =
     | Or _ -> 1
       
 (* Begin Lucca Hirschi *)
-let rec eval_form (q,qf,qn) f = match expr f with
-  | False -> false
-  | True -> true
-  | And(f1,f2) -> eval_form (q,qf,qn) f1 && eval_form (q,qf,qn) f2
-  | Or(f1,f2) -> eval_form (q,qf,qn) f1 || eval_form (q,qf,qn) f2
-  | 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)
-
-let rec infer_form sq sqf sqn f = match expr f with
-  | False -> false
-  | True -> true
-  | And(f1,f2) -> infer_form sq sqf sqn f1 && infer_form sq sqf sqn f2
-  | Or(f1,f2) -> infer_form sq sqf sqn f1 || infer_form sq sqf sqn f2
-  | Atom(dir, b, s) -> 
-    let setq, setr = match dir with
-      | `Left -> sqf | `Right -> sqn | `Self -> sq in
+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
+      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 =