Add a generic deque module.

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 0ae25f9..887eb35 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -23,9 +23,9 @@ open Bigarray
 type stats = { mutable pass : int;
                tree_size : int;
                mutable fetch_trans_cache_access : int;
 type stats = { mutable pass : int;
                tree_size : int;
                mutable fetch_trans_cache_access : int;

-               mutable fetch_trans_cache_hit : int;
+               mutable fetch_trans_cache_miss : int;

                mutable eval_trans_cache_access : int;
                mutable eval_trans_cache_access : int;

-               mutable eval_trans_cache_hit : int;
+               mutable eval_trans_cache_miss : int;

                mutable nodes_per_run : int list;
              }
 
                mutable nodes_per_run : int list;
              }
 


@@ -120,15 +120,15 @@ let get_form run tag (q : State.t) =
   if phi == dummy_form then
     let phi = Ata.get_form auto tag q in
     let () =
   if phi == dummy_form then
     let phi = Ata.get_form auto tag q in
     let () =

+      stats.fetch_trans_cache_miss <- stats.fetch_trans_cache_miss + 1;

       Cache.N2.add
         fetch_trans_cache
         (tag.QName.id :> int)
         (q :> int) phi
     in phi
       Cache.N2.add
         fetch_trans_cache
         (tag.QName.id :> int)
         (q :> int) phi
     in phi

-  else begin
-    stats.fetch_trans_cache_hit <- stats.fetch_trans_cache_hit + 1;
+  else

     phi
     phi

-  end
+

 
 
 let eval_form phi fcs nss ps ss summary =
 
 
 let eval_form phi fcs nss ps ss summary =


@@ -191,17 +191,17 @@ let eval_trans run trans_cache tag summary fcs nss ps ss todo =
 
   let res = Cache.N6.find trans_cache tagid summary ssid fcsid nssid psid in
   stats.eval_trans_cache_access <- 1 + stats.eval_trans_cache_access;
 
   let res = Cache.N6.find trans_cache tagid summary ssid fcsid nssid psid in
   stats.eval_trans_cache_access <- 1 + stats.eval_trans_cache_access;

-  if res != dummy_set then begin
-    stats.eval_trans_cache_hit <- 1 + stats.eval_trans_cache_hit;
+  if res != dummy_set then

     res
     res

-  end else let new_sat =
+  else let new_sat =

              eval_trans_fix run tag summary fcs nss ps ss todo
              eval_trans_fix run tag summary fcs nss ps ss todo

-           in
-           Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_sat;
-           new_sat
+    in
+    stats.eval_trans_cache_miss <- 1 + stats.eval_trans_cache_miss;
+    Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_sat;
+    new_sat

 
 
 
 

-module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
+module Make (T : Tree.S) (L : Deque.S with type elem = T.node) =

 struct
 
   let make auto tree =
 struct
 
   let make auto tree =


@@ -222,9 +222,9 @@ struct
         pass = 0;
         tree_size = len;
         fetch_trans_cache_access = 0;
         pass = 0;
         tree_size = len;
         fetch_trans_cache_access = 0;

-        fetch_trans_cache_hit = 0;
+        fetch_trans_cache_miss = 0;

         eval_trans_cache_access = 0;
         eval_trans_cache_access = 0;

-        eval_trans_cache_hit = 0;
+        eval_trans_cache_miss = 0;

         nodes_per_run = [];
       }
     }
         nodes_per_run = [];
       }
     }