Add a counter for eval/infer.

diff --git a/src/formula.ml b/src/formula.ml
index 6c98118..f3decb0 100644 (file)
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -112,27 +112,40 @@ 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 =
-try HashEval.find hashEval (q,qf,qn,f)
-with _ ->
+  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
-
+      | 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 _ ->
+  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