Refine the run to have a different set of states to satisfy while going td/bu.

diff --git a/src/ata.ml b/src/ata.ml
index f55452e..565dfc8 100644 (file)
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -490,7 +490,6 @@ let compute_rank auto =
   done;
   let by_rank = Hashtbl.create 17 in
   List.iter (fun (r,s) ->
-    let r = r/2 in
     let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
     Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
   auto.ranked_states <-

diff --git a/src/run.ml b/src/run.ml
index b51daf9..31eb26c 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -253,15 +253,15 @@ DEFINE AND_(t1,t2) =
                  let open NodeSummary in
                      match a.Atom.node with
                      | Move (m, q) ->
-                         let { NodeStatus.node = n_sum; _ } as sum =
+                         let down, ({ NodeStatus.node = n_sum; _ } as sum) =
                            match m with
-                             `First_child -> fcs
-                           | `Next_sibling -> nss
-                           | `Parent | `Previous_sibling -> ps
-                           | `Stay -> ss
+                             `First_child -> true, fcs
+                           | `Next_sibling -> true, nss
+                           | `Parent | `Previous_sibling -> false, ps
+                           | `Stay -> false, ss
                          in
                          if sum == dummy_status
-                           || n_sum.rank < ss.NodeStatus.node.rank
+                           || (down && n_sum.rank < ss.NodeStatus.node.rank)
                            || StateSet.mem q n_sum.todo then
                            Unknown
                          else
@@ -332,7 +332,11 @@ DEFINE AND_(t1,t2) =
     let cache5 = run.cache5 in
     let unstable = run.unstable in
     let states_by_rank = Ata.get_states_by_rank auto in
-    let init_todo = states_by_rank.(i) in
+    let td_todo = states_by_rank.(i) in
+    let bu_todo = if i + 1 = Array.length states_by_rank then StateSet.empty
+      else
+        states_by_rank.(i+1)
+    in
     let rec loop node =
       let node_id = T.preorder tree node in
       if node == T.nil (*|| not (Bitvector.get unstable node_id)*) then false
@@ -352,7 +356,7 @@ DEFINE AND_(t1,t2) =
             NodeStatus.make
               { rank = i;
                 sat = c.NodeStatus.node.sat;
-                todo = init_todo;
+                todo = td_todo;
                 summary = let summary = c.NodeStatus.node.summary
                           in
                           if summary != NodeSummary.dummy then summary
@@ -388,6 +392,13 @@ DEFINE AND_(t1,t2) =
            get the new status of the first child *)
         let fcs1 = unsafe_get_status status fc_id in
         (* update the status *)
+        let status1 = if status1.NodeStatus.node.rank < i then
+            NodeStatus.make { status1.NodeStatus.node with
+              rank = i;
+              todo = bu_todo }
+          else
+            status1
+        in
         let status2 =
           if status1.NodeStatus.node.todo == StateSet.empty then status1
           else begin