Preliminary work for multiple starters evaluation.

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 38b7e45..d7d5177 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -159,6 +159,16 @@ END
        (Ata.TransList.print ~sep:"<br/>") config.todo i
 
 
+   let debug msg tree node i config =
+     let config = config.NodeStatus.node in
+     eprintf
+       "DEBUG:%s node: %i\nsat: %a\nunsat: %a\ntodo: %around: %i\n"
+       msg
+       (T.preorder tree node)
+       StateSet.print config.sat
+       StateSet.print config.unsat
+       (Ata.TransList.print ~sep:"\n") config.todo i
+
 
    let get_trans cache2 auto tag states =
      let trs =
@@ -262,7 +272,7 @@ END
 
 
 
-  let top_down node run =
+  let top_down run =
     let tree = run.tree in
     let auto = run.auto in
     let status = run.status in
@@ -285,7 +295,8 @@ END
           if c == dummy_status then
             (* first time we visit the node *)
             NodeStatus.make
-              { c.NodeStatus.node with
+              { sat = StateSet.empty;
+                unsat = Ata.get_starting_states auto;
                 todo = get_trans cache2 auto tag (Ata.get_states auto);
                 summary = NodeSummary.make
                   (node == T.first_child tree parent) (* is_left *)
@@ -346,7 +357,7 @@ END
         unstable_self
       end
     in
-    run.redo <- loop node;
+    run.redo <- loop (T.root tree);
     run.pass <- run.pass + 1
 
 (*
@@ -405,9 +416,40 @@ END
     in
     loop (T.root tree) []
 
+  let prepare_run run list =
+    let tree = run.tree in
+    let auto = run.auto in
+    let status = run.status in
+    let cache2 = run.cache2 in
+    List.iter (fun node ->
+      let parent = T.parent tree node in
+      let fc = T.first_child tree node in
+      let ns = T.next_sibling tree node in
+      let tag = T.tag tree node in
+
+      let status0 =
+        NodeStatus.make
+          { sat = Ata.get_starting_states auto;
+            unsat = StateSet.empty;
+            todo = get_trans cache2 auto tag (Ata.get_states auto);
+            summary = 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 *)
+          }
+      in
+      let node_id = T.preorder tree node in
+      status.(node_id) <- status0) list
+
 
-  let eval auto tree node =
+
+  let eval auto tree nodes =
     let run = make auto tree in
-    while run.redo do top_down node run done;
+    prepare_run run nodes;
+    while run.redo do
+      top_down run;
+    done;
     get_results run
 end