X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fformula.ml;h=f3decb0100d75934d17a1cc1b66f820b4540008f;hb=3c05557d22d07e447ae8efae3bfe38619c14c2a9;hp=2d9893cd223cd2d1d808a169728a2eee98c82ac0;hpb=0223b78baf156e7b8de86e334a4648fb2c3819e8;p=tatoo.git

diff --git a/src/formula.ml b/src/formula.ml
index 2d9893c..f3decb0 100644
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -25,7 +25,7 @@ type 'hcons expr =
 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 *)
 }
 
@@ -73,28 +73,94 @@ 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 num_call = ref 0
+let num_miss = ref 0
+let num_call_i = ref 0
+let num_miss_i = ref 0
+let () = at_exit(fun () -> Format.fprintf Format.err_formatter
+  "Num: call %d, Num Miss: %d\n%!" (!num_call) (!num_miss);
+  Format.fprintf Format.err_formatter
+    "Num: call_i %d, Num Miss_i: %d\n%!" (!num_call_i) (!num_miss_i))
+
+let rec eval_form (q,qf,qn) f hashEval =
+  incr num_call;
+  try HashEval.find hashEval (q,qf,qn,f)
+  with _ ->
+    incr num_miss;  
+  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 =
+  incr num_call_i;
+  try HashInfer.find hashInfer (sq,sqf,sqn,f)
+  with _ ->
+  incr num_miss_i;
+  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 =
@@ -141,27 +207,28 @@ let cons pos neg s1 s2 size1 size2 =
     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
-    | `Self -> si, StateSet.empty       (* TODO WHAT? *)
+    | `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