X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=8eb58f9867c8f96445c6e005b7829ded57874822;hp=fb9f81d751099ed5ed496464ba9d6c91ced8f553;hb=3406b26f1ea26a997d7f194c547439891c108ce6;hpb=b6dc15847ef86e61c0d242bc7ae025c1763f8a77

diff --git a/src/run.ml b/src/run.ml
index fb9f81d..8eb58f9 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -203,7 +203,7 @@ END
           new_sat
 
 
-module Make (T : Tree.S) =
+module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
  struct
 
    let make auto tree =
@@ -245,8 +245,8 @@ module Make (T : Tree.S) =
           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 *)
+                (node_id == T.preorder tree (T.first_child tree parent)) (*is_left *)
+                (node_id ==  T.preorder tree (T.next_sibling tree parent))(*is_right *)
                 (fc != T.nil) (* has_left *)
                 (ns != T.nil) (* has_right *)
                 (T.kind tree node) (* kind *)
@@ -266,6 +266,7 @@ module Make (T : Tree.S) =
             parent_sat
             status0 td_todo
         in
+
         (* update the cache if the status of the node changed
            unsafe_set run.sat node_id status1 status0;*)
           let fcs1 = loop_td_and_bu fc node status1 in
@@ -294,16 +295,17 @@ module Make (T : Tree.S) =
     let auto = run.auto in
     let tree = run.tree in
     let sel_states = Ata.get_selecting_states auto in
-    let rec loop node acc =
-      if node == T.nil  then acc
-      else
-        let acc0 = loop (T.next_sibling tree node) acc in
-        let acc1 = loop (T.first_child tree node) acc0 in
-        if StateSet.intersect cache.(T.preorder tree node)
-          sel_states then node::acc1
-        else acc1
+    let res = ref (L.create ()) in
+    let rec loop node =
+      if node != T.nil  then begin
+        if StateSet.intersect sel_states cache.(T.preorder tree node) then
+          res := L.add node !res;
+        loop (T.first_child tree node);
+        loop (T.next_sibling tree node)
+      end
     in
-    loop (T.root tree) []
+    loop (T.root tree);
+    !res
 
 
   let get_full_results run =
@@ -316,24 +318,26 @@ module Make (T : Tree.S) =
         (fun q -> Hashtbl.add res_mapper q [])
         (Ata.get_selecting_states auto)
     in
-    let dummy = [ T.nil ] in
+    let dummy = L.create () in
+
     let res_mapper = Cache.N1.create dummy in
     let () =
       StateSet.iter
-        (fun q -> Cache.N1.add res_mapper (q :> int) [])
+        (fun q -> Cache.N1.add res_mapper (q :> int) (L.create()))
         (Ata.get_selecting_states auto)
     in
     let rec loop node =
-      if node != T.nil then
-        let () = loop (T.next_sibling tree node) in
-        let () = loop (T.first_child tree node) in
+      if node != T.nil then begin
         StateSet.iter
           (fun q ->
             let res = Cache.N1.find res_mapper (q :> int) in
             if res != dummy then
-              Cache.N1.add res_mapper (q :> int) (node::res)
+              Cache.N1.add res_mapper (q :> int) (L.add node res)
           )
-          cache.(T.preorder tree node)
+          cache.(T.preorder tree node);
+        loop (T.first_child tree node);
+        loop (T.next_sibling tree node)
+      end
     in
     loop (T.root tree);
     (StateSet.fold_right
@@ -346,12 +350,23 @@ module Make (T : Tree.S) =
     let auto = run.auto in
     let sat = IFHTML((List.hd run.sat), run.sat) in
     let sat0 = Ata.get_starting_states auto in
-    List.iter (fun node ->
+    L.iter (fun node ->
       let node_id = T.preorder tree node in
       sat.(node_id) <- sat0) list
 
   let tree_size = ref 0
   let pass = ref 0
+
+let time f arg msg =
+  let t1 = Unix.gettimeofday () in
+  let r = f arg in
+  let t2 = Unix.gettimeofday () in
+  let time = (t2 -. t1) *. 1000. in
+  Printf.eprintf "%s: %fms%!" msg time;
+  r
+
+
+
   let compute_run auto tree nodes =
     pass := 0;
     tree_size := T.size tree;
@@ -359,7 +374,7 @@ module Make (T : Tree.S) =
     prepare_run run nodes;
     let rank = Ata.get_max_rank auto in
     while run.pass <= rank do
-      top_down run;
+      time top_down run ("Timing run number " ^ string_of_int run.pass ^ "/" ^ string_of_int (Ata.get_max_rank auto + 1));
       IFHTML((run.sat <- (Array.copy (List.hd run.sat)) :: run.sat), ());
       run.td_cache <- Cache.N6.create dummy_set;
       run.bu_cache <- Cache.N6.create dummy_set;
@@ -375,7 +390,8 @@ module Make (T : Tree.S) =
 
   let eval auto tree nodes =
     let r = compute_run auto tree nodes in
-    get_results r
+    let nl = get_results r in
+    nl
 
   let stats () = {
     tree_size = !tree_size;