Speed-up the run function by keeping only the set of node to be satified for each...

diff --git a/src/run.ml b/src/run.ml
index 0e4e0b3..1824aeb 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -48,95 +48,58 @@ module Make (T : Tree.S) =
      type t = int
      let dummy = -1
     (*
      type t = int
      let dummy = -1
     (*

-      333333333333333210
-      3333 -> kind
-      2 -> has_right
-      1 -> has_left
-      0 -> is_left/is_right
+      ...44443210
+      ...4444 -> kind
+      3 -> has_right
+      2 -> has_left
+      1 -> is_right
+      0 -> is_left

     *)
      let is_left (s : t) : bool =
     *)
      let is_left (s : t) : bool =

-       s land 1 == 1
+       s land 1 != 0

 
      let is_right (s : t) : bool =
 
      let is_right (s : t) : bool =

-       s land 1 == 0
+       s land 0b10 != 0

 
      let has_left (s : t) : bool =
 
      let has_left (s : t) : bool =

-       (s lsr 1) land 1 == 1
+       s land 0b100 != 0

 
      let has_right (s : t) : bool =
 
      let has_right (s : t) : bool =

-       (s lsr 2) land 1 == 1
+       s land 0b1000 != 0

 
      let kind (s : t) : Tree.NodeKind.t =
 
      let kind (s : t) : Tree.NodeKind.t =

-       Obj.magic (s lsr 3)
+       Obj.magic (s lsr 4)

 
 

-     let make is_left has_left has_right kind =
+     let make is_left is_right has_left has_right kind =

        (int_of_bool is_left) lor
        (int_of_bool is_left) lor

-         ((int_of_bool has_left) lsl 1) lor
-         ((int_of_bool has_right) lsl 2) lor
-         ((Obj.magic kind) lsl 3)
+         ((int_of_bool is_right) lsl 1) lor
+         ((int_of_bool has_left) lsl 2) lor
+         ((int_of_bool has_right) lsl 3) lor
+         ((Obj.magic kind) lsl 4)

    end
 
    end
 

-   type node_status = {
-     rank : int;
-     sat : StateSet.t;  (* States that are satisfied at the current node *)
-     todo : StateSet.t; (* States that remain to be proven *)
-     (* For every node_status and automaton a,
-        a.states - (sat U todo) = unsat *)
-     summary : NodeSummary.t; (* Summary of the shape of the node *)
-   }
-(* Describe what is kept at each node for a run *)
-
-   module NodeStatus =
-     struct
-       include Hcons.Make(struct
-         type t = node_status
-         let equal c d =
-           c == d ||
-             c.rank == d.rank &&
-             c.sat == d.sat &&
-             c.todo == d.todo &&
-             c.summary == d.summary
-
-         let hash c =
-           HASHINT4(c.rank,
-                    (c.sat.StateSet.id :> int),
-                    (c.todo.StateSet.id :> int),
-                    c.summary)
-       end
-       )
-       let print ppf s =
-         fprintf ppf
-           "{ rank: %i; sat: %a; todo: %a; summary: _ }"
-           s.node.rank
-           StateSet.print s.node.sat
-           StateSet.print s.node.todo
-     end
-
-   let dummy_status =
-     NodeStatus.make {
-       rank = -1;
-       sat = StateSet.empty;
-       todo = StateSet.empty;
-       summary = NodeSummary.dummy;
-     }
-
-
+   let dummy_set = StateSet.singleton State.dummy
+   open Bigarray

    type run = {
      tree : T.t ;
      (* The argument of the run *)
      auto : Ata.t;
      (* The automaton to be run *)
    type run = {
      tree : T.t ;
      (* The argument of the run *)
      auto : Ata.t;
      (* The automaton to be run *)

-     status : NodeStatus.t array;
-     (* A mapping from node preorders to NodeStatus *)
+     sat: StateSet.t array;
+     (* A mapping from node preorders to states satisfied at that node *)

      mutable pass : int;
      mutable pass : int;

+     (* Number of run we have performed *)

      mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t;
      (* A cache from states * label to list of transitions *)
      mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t;
      (* A cache from states * label to list of transitions *)

-     mutable td_cache : NodeStatus.t Cache.N5.t;
-     mutable bu_cache : NodeStatus.t Cache.N5.t;
+     mutable td_cache : StateSet.t Cache.N6.t;
+     mutable bu_cache : StateSet.t Cache.N6.t;
+     (* Two 6-way caches used during the top-down and bottom-up phase
+        label * self-set * fc-set * ns-set * parent-set * node-shape -> self-set
+     *)
+     node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t;

    }
 
 
    }
 
 

-

    let dummy_form = Ata.Formula.stay State.dummy
 
    let make auto tree =
    let dummy_form = Ata.Formula.stay State.dummy
 
    let make auto tree =


@@ -144,45 +107,15 @@ module Make (T : Tree.S) =
      {
        tree = tree;
        auto = auto;
      {
        tree = tree;
        auto = auto;

-       status = Array.create len dummy_status;
+       sat = Array.create len StateSet.empty;

        pass = 0;
        fetch_trans_cache = Cache.N2.create dummy_form;
        pass = 0;
        fetch_trans_cache = Cache.N2.create dummy_form;

-       td_cache = Cache.N5.create dummy_status;
-       bu_cache = Cache.N5.create dummy_status;
+       td_cache = Cache.N6.create dummy_set;
+       bu_cache = Cache.N6.create dummy_set;
+       node_summaries = let ba = Array1.create int16_unsigned c_layout len in
+                        Array1.fill ba 0; ba

      }
 
      }
 

-   let get_status a i =
-     if i < 0 then dummy_status else Array.get a i
-
-   let unsafe_get_status a i =
-     if i < 0 then dummy_status else Array.unsafe_get a i
-
-IFDEF HTMLTRACE
-  THEN
-DEFINE IFTRACE(e) = (e)
-  ELSE
-DEFINE IFTRACE(e) = ()
-END
-
-   let html tree node i config msg =
-     let config = config.NodeStatus.node in
-     Html.trace ~msg:msg
-       (T.preorder tree node) i
-       config.todo
-       config.sat
-
-
-
-   let debug msg tree node i config =
-     let config = config.NodeStatus.node in
-     eprintf
-       "DEBUG:%s node: %i\nsat: %a\ntodo: %a\nround: %i\n"
-       msg
-       (T.preorder tree node)
-       StateSet.print config.sat
-       StateSet.print config.todo
-       i
-

    let get_form fetch_trans_cache auto tag q =
      let phi =
        incr fetch_trans_cache_access;
    let get_form fetch_trans_cache auto tag q =
      let phi =
        incr fetch_trans_cache_access;


@@ -201,276 +134,137 @@ END
        phi
      end
 
        phi
      end
 

-   type trivalent = False | True | Unknown
-   let of_bool = function false -> False | true -> True
-   let or_ t1 t2 =
-     match t1 with
-       False -> t2
-     | True -> True
-     | Unknown -> if t2 == True then True else Unknown
-
-   let and_ t1 t2 =
-     match t1 with
-       False -> False
-     | True -> t2
-     | Unknown -> if t2 == False then False else Unknown
-
- (* Define as macros to get lazyness *)
-DEFINE OR_(t1,t2) =
-     match t1 with
-       False -> (t2)
-     | True -> True
-     | Unknown -> if (t2) == True then True else Unknown
-
-DEFINE AND_(t1,t2) =
-     match t1 with
-       False -> False
-     | True -> (t2)
-     | Unknown -> if (t2) == False then False else Unknown
-

 
    let eval_form phi fcs nss ps ss summary =
      let open Ata in
          let rec loop phi =
            begin match Formula.expr phi with
 
    let eval_form phi fcs nss ps ss summary =
      let open Ata in
          let rec loop phi =
            begin match Formula.expr phi with

-           | Boolean.False -> False
-           | Boolean.True -> True
+           | Boolean.False -> false
+           | Boolean.True -> true

            | Boolean.Atom (a, b) ->
                begin
                  let open NodeSummary in
                      match a.Atom.node with
                      | Move (m, q) ->
            | Boolean.Atom (a, b) ->
                begin
                  let open NodeSummary in
                      match a.Atom.node with
                      | Move (m, q) ->

-                         let down, ({ NodeStatus.node = n_sum; _ } as sum) =
+                       b && StateSet.mem q (

                            match m with
                            match m with

-                             `First_child -> true, fcs
-                           | `Next_sibling -> true, nss
-                           | `Parent | `Previous_sibling -> false, ps
-                           | `Stay -> false, ss
-                         in
-                         if sum == dummy_status
-                           (*|| (down && n_sum.rank < ss.NodeStatus.node.rank) *)
-                           || StateSet.mem q n_sum.todo then
-                           Unknown
-                         else
-                           of_bool (b == StateSet.mem q n_sum.sat)
-                     | Is_first_child -> of_bool (b == is_left summary)
-                     | Is_next_sibling -> of_bool (b == is_right summary)
-                     | Is k -> of_bool (b == (k == kind summary))
-                     | Has_first_child -> of_bool (b == has_left summary)
-                     | Has_next_sibling -> of_bool (b == has_right summary)
+                             `First_child -> fcs
+                           | `Next_sibling -> nss
+                           | `Parent | `Previous_sibling ->  ps
+                           | `Stay ->  ss
+                       )
+                     | Is_first_child -> b == is_left summary
+                     | Is_next_sibling -> b == is_right summary
+                     | Is k -> b == (k == kind summary)
+                     | Has_first_child -> b == has_left summary
+                     | Has_next_sibling -> b == has_right summary

                end
                end

-           | Boolean.And(phi1, phi2) -> AND_ (loop phi1, loop phi2)
-           | Boolean.Or (phi1, phi2) -> OR_ (loop phi1, loop phi2)
+           | Boolean.And(phi1, phi2) -> loop phi1 && loop phi2
+           | Boolean.Or (phi1, phi2) -> loop phi1 || loop phi2

            end
          in
          loop phi
 
 
            end
          in
          loop phi
 
 

-   let eval_trans_aux auto fetch_trans_cache tag fcs nss ps old_status =
-     let { sat = old_sat;
-           todo = old_todo;
-           summary = old_summary } as os_node = old_status.NodeStatus.node
-     in
-     let sat, todo =
-       StateSet.fold (fun q ((a_sat, a_todo) as acc) ->
-         let phi =
-           get_form fetch_trans_cache auto tag q
-         in
-
-         let v = eval_form phi fcs nss ps old_status old_summary in
-         match v with
-           True -> StateSet.add q a_sat, a_todo
-         | False -> acc
-         | Unknown -> a_sat, StateSet.add q a_todo
-       ) old_todo (old_sat, StateSet.empty)
-     in
-     if old_sat != sat || old_todo != todo then
-       NodeStatus.make { os_node with sat; todo }
-     else old_status
+   let eval_trans_aux auto fetch_trans_cache tag fcs nss ps sat todo summary =
+     StateSet.fold (fun q (a_sat) ->
+       let phi =
+         get_form fetch_trans_cache auto tag q
+       in
+       if eval_form phi fcs nss ps a_sat summary then
+         StateSet.add q a_sat
+       else a_sat
+     ) todo sat

 
 
 
 

-   let rec eval_trans_fix auto fetch_trans_cache tag fcs nss ps old_status =
-     let new_status =
-       eval_trans_aux auto fetch_trans_cache tag fcs nss ps old_status
+   let rec eval_trans_fix auto fetch_trans_cache tag fcs nss ps sat todo summary =
+     let new_sat =
+       eval_trans_aux auto fetch_trans_cache tag fcs nss ps sat todo summary

      in
      in

-     if new_status == old_status then old_status else
-       eval_trans_fix auto fetch_trans_cache tag fcs nss ps new_status
+     if new_sat == sat then sat else
+       eval_trans_fix auto fetch_trans_cache tag fcs nss ps new_sat todo summary

 
 
 
 

-   let eval_trans auto fetch_trans_cache td_cache tag fcs nss ps ss =
-     let fcsid = (fcs.NodeStatus.id :> int) in
-     let nssid = (nss.NodeStatus.id :> int) in
-     let psid = (ps.NodeStatus.id :> int) in
-     let ssid = (ss.NodeStatus.id :> int) in
+   let eval_trans auto fetch_trans_cache eval_cache tag fcs nss ps ss todo summary =
+     let fcsid = (fcs.StateSet.id :> int) in
+     let nssid = (nss.StateSet.id :> int) in
+     let psid = (ps.StateSet.id :> int) in
+     let ssid = (ss.StateSet.id :> int) in

      let tagid = (tag.QName.id :> int) in
      let tagid = (tag.QName.id :> int) in

-     let res = Cache.N5.find td_cache tagid ssid fcsid nssid psid in
+     let res = Cache.N6.find eval_cache tagid summary ssid fcsid nssid psid in

      incr eval_trans_cache_access;
      incr eval_trans_cache_access;

-     if res != dummy_status then begin incr eval_trans_cache_hit; res end
-     else let new_status = eval_trans_fix auto fetch_trans_cache tag fcs nss ps ss in
-          Cache.N5.add td_cache tagid ssid fcsid nssid psid new_status;
-          new_status
+     if res != dummy_set then begin incr eval_trans_cache_hit; res end
+     else let new_sat =
+            eval_trans_fix auto fetch_trans_cache tag fcs  nss ps ss todo summary
+          in
+          Cache.N6.add eval_cache tagid summary ssid fcsid nssid psid new_sat;
+          new_sat
+

 
 

-  let top_down run =
+   let unsafe_get a i = if i < 0 then StateSet.empty else Array.unsafe_get a i
+
+   let top_down run =

     let i = run.pass in
     let tree = run.tree in
     let auto = run.auto in
     let i = run.pass in
     let tree = run.tree in
     let auto = run.auto in

-    let status = run.status in
-    let fetch_trans_cache = run.fetch_trans_cache in
-    let td_cache = run.td_cache in
-    let bu_cache = run.bu_cache in

     let states_by_rank = Ata.get_states_by_rank auto 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 states_by_rank = Ata.get_states_by_rank auto 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_td_and_bu node =
-      if node == T.nil then () else begin
+    let rec loop_td_and_bu node parent parent_sat =
+      if node == T.nil then StateSet.empty else begin

         let node_id = T.preorder tree node in
         let node_id = T.preorder tree node in

-        let parent = T.parent tree node in

         let fc = T.first_child tree node in
         let fc = T.first_child tree node in

-        let fc_id = T.preorder tree fc in

         let ns = T.next_sibling tree node in
         let ns = T.next_sibling tree node in

-        let ns_id = T.preorder tree ns in

         let tag = T.tag tree node in
         (* We enter the node from its parent *)
         let tag = T.tag tree node in
         (* We enter the node from its parent *)

-        let status0 =
-          let c = unsafe_get_status status node_id in
-          if c.NodeStatus.node.rank < i then
-            (* first time we visit the node during this run *)
-            NodeStatus.make
-              { rank = i;
-                sat = c.NodeStatus.node.sat;
-                todo = td_todo;
-                summary =
-                  let summary = c.NodeStatus.node.summary in
-                  if summary != NodeSummary.dummy then summary
-                  else
-                    NodeSummary.make
-                      (node != T.next_sibling tree parent)
-                      (fc != T.nil) (* has_left *)
-                      (ns != T.nil) (* has_right *)
-                      (T.kind tree node) (* kind *)
-              }
-          else c
-        in
-        let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
-          i QName.print tag NodeStatus.print status0
+        let summary =
+          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 *)
+            in
+            run.node_summaries.{node_id} <- s; s

         in
         in

+        let status0 = unsafe_get run.sat node_id in

         (* get the node_statuses for the first child, next sibling and parent *)
         (* get the node_statuses for the first child, next sibling and parent *)

-        let ps = unsafe_get_status status (T.preorder tree parent) in
-        let fcs = unsafe_get_status status fc_id in
-        let nss = unsafe_get_status status ns_id in
+        let fcs = unsafe_get run.sat (T.preorder tree fc) in
+        let nss = unsafe_get run.sat (T.preorder tree ns) in

         (* evaluate the transitions with all this statuses *)
         let status1 =
         (* evaluate the transitions with all this statuses *)
         let status1 =

-          if status0.NodeStatus.node.todo == StateSet.empty then status0
-          else begin
-            let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in
-          (* update the cache if the status of the node changed *)
-            if status1 != status0 then status.(node_id) <- status1;
-            status1
-          end
-        in
-        let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
-          i QName.print tag NodeStatus.print status1
-        in
-        (* recursively traverse the first child *)
-        let () = loop_td_and_bu fc in
-        (* here we re-enter the node from its first child,
-           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+1 then
-            NodeStatus.make { status1.NodeStatus.node with
-              rank = i+1;
-              todo = bu_todo }
-          else
-            status1
-        in
-        let status2 =
-          if status1.NodeStatus.node.todo == StateSet.empty then status1
-          else begin
-            let status2 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss ps status1 in
-            if status2 != status1 then status.(node_id) <- status2;
-            status2
-          end
-        in
-        let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
-          (i+1) QName.print tag NodeStatus.print status2
-        in
-        let () = loop_td_and_bu ns in
-        let nss1 = unsafe_get_status status ns_id in
-        if status2.NodeStatus.node.todo != StateSet.empty then
-          let status3 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss1 ps status2 in
-          let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
-            (i+1) QName.print tag NodeStatus.print status3
-          in
-
-          if status3 != status2 then status.(node_id) <- status3
-      end
-    and loop_td_only node =
-      if node == T.nil then () else begin
-        let node_id = T.preorder tree node in
-        let parent = T.parent tree node in
-        let fc = T.first_child tree node in
-        let fc_id = T.preorder tree fc in
-        let ns = T.next_sibling tree node in
-        let ns_id = T.preorder tree ns in
-        let tag = T.tag tree node in
-        (* We enter the node from its parent *)
-        let status0 =
-          let c = unsafe_get_status status node_id in
-          if c.NodeStatus.node.rank < i then
-            (* first time we visit the node during this run *)
-            NodeStatus.make
-              { rank = i;
-                sat = c.NodeStatus.node.sat;
-                todo = td_todo;
-                summary =
-                  let summary = c.NodeStatus.node.summary in
-                  if summary != NodeSummary.dummy then summary
-                  else
-                    NodeSummary.make
-                      (node != T.next_sibling tree parent)
-                      (fc != T.nil) (* has_left *)
-                      (ns != T.nil) (* has_right *)
-                      (T.kind tree node) (* kind *)
-              }
-          else c
+          eval_trans auto run.fetch_trans_cache run.td_cache tag fcs nss
+            parent_sat
+            status0 td_todo summary

         in
         in

-        let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
-          (i) QName.print tag NodeStatus.print status0
-        in
-
-        (* get the node_statuses for the first child, next sibling and parent *)
-        let ps = unsafe_get_status status (T.preorder tree parent) in
-        let fcs = unsafe_get_status status fc_id in
-        let nss = unsafe_get_status status ns_id in
-        (* evaluate the transitions with all this statuses *)
-        if status0.NodeStatus.node.todo != StateSet.empty then begin
-          let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in
-          (* update the cache if the status of the node changed *)
-          let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
-            (i) QName.print tag NodeStatus.print status1
+        (* update the cache if the status of the node changed *)
+        if status1 != status0 then run.sat.(node_id) <- status1;
+        let fcs1 = loop_td_and_bu fc node status1 in
+        if bu_todo == StateSet.empty then
+          loop_td_and_bu ns node status1 (* tail call *)
+        else
+          let nss1 = loop_td_and_bu ns node status1 in
+          let status2 =
+            eval_trans auto run.fetch_trans_cache run.bu_cache tag fcs1 nss1
+              parent_sat
+              status1 bu_todo summary

           in
           in

-
-          if status1 != status0 then status.(node_id) <- status1;
-        end;
-        (* recursively traverse the first child *)
-        loop_td_only fc;
-        loop_td_only ns
+          if status2 != status1 then run.sat.(node_id) <- status2;
+          status2

       end
     in
       end
     in

-    if bu_todo == StateSet.empty then
-      let () = loop_td_only (T.root tree) in
-      run.pass <- run.pass + 1
-    else
-      let () = loop_td_and_bu (T.root tree) in
-      run.pass <- run.pass + 2
+    let _ = loop_td_and_bu (T.root tree) T.nil StateSet.empty in
+    run.pass <- run.pass + 2

 
 
   let get_results run =
 
 
   let get_results run =

-    let cache = run.status in
+    let cache = run.sat in

     let auto = run.auto in
     let tree = run.tree in
     let sel_states = Ata.get_selecting_states auto in
     let auto = run.auto in
     let tree = run.tree in
     let sel_states = Ata.get_selecting_states auto in


@@ -481,7 +275,7 @@ DEFINE AND_(t1,t2) =
         let acc1 = loop (T.first_child tree node) acc0 in
 
         if StateSet.intersect
         let acc1 = loop (T.first_child tree node) acc0 in
 
         if StateSet.intersect

-          cache.(T.preorder tree node).NodeStatus.node.sat
+          cache.(T.preorder tree node)(* NodeStatus.node.sat *)

           sel_states then node::acc1
         else acc1
     in
           sel_states then node::acc1
         else acc1
     in


@@ -489,7 +283,7 @@ DEFINE AND_(t1,t2) =
 
 
   let get_full_results run =
 
 
   let get_full_results run =

-    let cache = run.status in
+    let cache = run.sat(*tatus*) in

     let auto = run.auto in
     let tree = run.tree in
     let res_mapper = Hashtbl.create MED_H_SIZE in
     let auto = run.auto in
     let tree = run.tree in
     let res_mapper = Hashtbl.create MED_H_SIZE in


@@ -515,7 +309,7 @@ DEFINE AND_(t1,t2) =
             if res != dummy then
               Cache.N1.add res_mapper (q :> int) (node::res)
           )
             if res != dummy then
               Cache.N1.add res_mapper (q :> int) (node::res)
           )

-          cache.(T.preorder tree node).NodeStatus.node.sat
+          cache.(T.preorder tree node)(* NodeStatus.node.sat *)

     in
     loop (T.root tree);
     (StateSet.fold_right
     in
     loop (T.root tree);
     (StateSet.fold_right


@@ -526,26 +320,10 @@ DEFINE AND_(t1,t2) =
   let prepare_run run list =
     let tree = run.tree in
     let auto = run.auto in
   let prepare_run run list =
     let tree = run.tree in
     let auto = run.auto in

-    let status = run.status in
+    let sat0 = Ata.get_starting_states auto in

     List.iter (fun node ->
     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 status0 =
-        NodeStatus.make
-          { rank = 0;
-            sat = Ata.get_starting_states auto;
-            todo =
-              StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto);
-            summary = NodeSummary.make
-              (node != T.next_sibling tree parent) (* is_left *)
-              (fc != T.nil) (* has_left *)
-              (ns != T.nil) (* has_right *)
-              (T.kind tree node) (* kind *)
-          }
-      in

       let node_id = T.preorder tree node in
       let node_id = T.preorder tree node in

-      status.(node_id) <- status0) list
+      run.sat.(node_id) <- sat0) list

 
   let tree_size = ref 0
   let pass = ref 0
 
   let tree_size = ref 0
   let pass = ref 0


@@ -557,11 +335,10 @@ DEFINE AND_(t1,t2) =
     let rank = Ata.get_max_rank auto in
     while run.pass <= rank do
       top_down run;
     let rank = Ata.get_max_rank auto in
     while run.pass <= rank do
       top_down run;

-      run.td_cache <- Cache.N5.create dummy_status;
-      run.bu_cache <- Cache.N5.create dummy_status;
+      run.td_cache <- Cache.N6.create dummy_set;
+      run.bu_cache <- Cache.N6.create dummy_set;

     done;
     pass := Ata.get_max_rank auto + 1;
     done;
     pass := Ata.get_max_rank auto + 1;

-    IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree);

 
     run
 
 
     run