Fixpoint in BU_over_max is now hconsed (37% better).

diff --git a/res b/res
index 19e73f9..cf46161 100644 (file)
--- a/res
+++ b/res
@@ -7,4 +7,12 @@ sys     0m0.395s
 real    0m17.625s
 user    0m17.202s
 sys     0m0.395s
+(~0% better)
 
+## With hconsed fixpoint in BU_Oracle and BU_Over_approx
+eal     0m12.884s
+user    0m12.504s
+sys     0m0.356s
+(37% better)
+
+## With hconsed fixpoint in BU_Oracle, BU_Over_approx and TP_Max
\ No newline at end of file

diff --git a/src/run.ml b/src/run.ml
index 8529d9b..b5dbc84 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -107,7 +107,7 @@ let rec bu_oracle asta run tree tnode hashOracle=
         try HashOracle.find hashOracle (set_i, qfr, qnr, list_tr, t)
         with _ -> 
           let set,flag = result set_i qfr qnr 0 list_tr in
-          HashOracle.add hashOracle (set_i,qfr,qnr,list_tr,t) (set);
+          HashOracle.add hashOracle (set_i,qfr,qnr,list_tr,t) (set); (* todo: Think about this position *)
           if flag = 0
           then set
           else fix_point set qfr qnr list_tr t in
@@ -143,17 +143,22 @@ let rec bu_over_max asta run tree tnode hashRun =
       let list_tr,_ = Asta.transitions_lab asta lab (* only take query st. *)
       and _,resultr = try NodeHash.find run node
         with _ -> raise Over_max_fail in      
-      let rec result set flag = function
-        | [] -> if flag = 0 then set else result set 0 list_tr
+      let rec result set qf qn flag list_tr = function 
+        | [] -> if flag = 0 then set else result set qf qn 0 list_tr list_tr
         | (q,form) :: tl ->
           if StateSet.mem q set
-          then result set 0 tl
+          then result set qf qn 0 list_tr tl
           else if Formula.infer_form (set,resultr) qf qn form
-               then result (StateSet.add q set) 1 tl
-               else result set 0 tl in
-      let result_set = result StateSet.empty 0 list_tr in
+          then result (StateSet.add q set) qf qn 1 list_tr tl
+          else result set qf qn 0 list_tr tl in
+      let result_set () =
+        try HashRun.find hashRun ((StateSet.empty,resultr),qf,qn,list_tr,lab)
+        with _ -> let res = result StateSet.empty qf qn 0 list_tr list_tr in
+                  HashRun.add hashRun
+                    ((StateSet.empty,resultr), qf,qn,list_tr,lab) res;
+                  res in
       (* we keep the old recognizing states set *)
-      NodeHash.replace run node (result_set, resultr)
+      NodeHash.replace run node (result_set(), resultr)
     end