.

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index be8bbeb..da50753 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -21,6 +21,7 @@ open Misc
 open Bigarray
 
 type stats = { mutable pass : int;
+               auto : Uid.t;
                tree_size : int;
                mutable fetch_trans_cache_access : int;
                mutable fetch_trans_cache_hit : int;
@@ -219,7 +220,8 @@ struct
       bu_cache = Cache.N6.create dummy_set;
       node_summaries = ba;
       stats = {
-        pass = 0;
+          pass = 0;
+          auto = Ata.uid auto;
         tree_size = len;
         fetch_trans_cache_access = 0;
         fetch_trans_cache_hit = 0;
@@ -242,6 +244,8 @@ struct
       else
         states_by_rank.(i+1)
     in
+    let td_only = bu_todo == StateSet.empty in
+    let root = T.root tree in
     let last_run = i >= Array.length states_by_rank - 2 in
     let rec loop_td_and_bu node parent parent_sat =
       if node == T.nil then StateSet.empty
@@ -256,12 +260,16 @@ struct
           let s = Array1.unsafe_get run.node_summaries node_id in
           if  s != 0 then s else
             let s =
-              NodeSummary.make
-                (node == (T.first_child tree parent)) (*is_left *)
-                (node == (T.next_sibling tree parent)) (*is_right *)
-                (fc != T.nil) (* has_left *)
-                (ns != T.nil) (* has_right *)
-                (T.kind tree node) (* kind *)
+              if node == root then
+                NodeSummary.make false false (fc != T.nil) (ns != T.nil) (T.kind tree node)
+              else
+                let is_left = node == T.first_child tree parent in
+                NodeSummary.make
+                  is_left
+                  (not is_left)
+                  (fc != T.nil) (* has_left *)
+                  (ns != T.nil) (* has_right *)
+                  (T.kind tree node) (* kind *)
             in
             run.node_summaries.{node_id} <- s; s
         in
@@ -279,7 +287,7 @@ struct
         in
           (* update the cache if the status of the node changed
              unsafe_set run.sat node_id status1 status0;*)
-        if bu_todo == StateSet.empty then begin
+        if td_only then begin
           unsafe_set run.sat node_id status1 status0; (* write the td_states *)
           update_res false status1 node;
           let _ = loop_td_and_bu fc node status1 in
@@ -372,22 +380,22 @@ struct
     run
 
 
-  let last_stats = ref None
+  let last_stats = ref []
 
   let full_eval auto tree nodes =
     let update_full,get_full = mk_update_full_result auto in
     let run = compute_run auto tree nodes update_full in
-    last_stats := Some run.stats;
+    last_stats :=  run.stats :: !last_stats;
     get_full ()
 
   let eval auto tree nodes =
     let update_res,get_res = mk_update_result auto in
     let run = compute_run auto tree nodes update_res in
-    last_stats := Some run.stats;
+    last_stats :=  run.stats :: !last_stats;
     get_res ()
 
   let stats () = match !last_stats with
-      Some s -> s.nodes_per_run <- List.rev s.nodes_per_run;s
-    | None -> failwith "Missing stats"
+      _ :: _ as l -> List.iter (fun s -> s.nodes_per_run <- List.rev s.nodes_per_run) l; List.rev l
+    | [] -> failwith "Missing stats"
 
 end