Abstract result sets beind a Node_list interface.
[tatoo.git] / src / run.ml
index 0e4e0b3..8eb58f9 100644 (file)
@@ -18,6 +18,7 @@ INCLUDE "debug.ml"
 
 open Format
 open Misc
+open Bigarray
 
 type stats = { run : int;
                tree_size : int;
@@ -38,151 +39,85 @@ let reset_stat_counters () =
   eval_trans_cache_access := 0
 
 
-module Make (T : Tree.S) =
- struct
-
-   module NodeSummary =
-   struct
+module NodeSummary =
+struct
      (* Pack into an integer the result of the is_* and has_ predicates
         for a given node *)
-     type t = int
-     let dummy = -1
-    (*
-      333333333333333210
-      3333 -> kind
-      2 -> has_right
-      1 -> has_left
-      0 -> is_left/is_right
-    *)
-     let is_left (s : t) : bool =
-       s land 1 == 1
-
-     let is_right (s : t) : bool =
-       s land 1 == 0
-
-     let has_left (s : t) : bool =
-       (s lsr 1) land 1 == 1
-
-     let has_right (s : t) : bool =
-       (s lsr 2) land 1 == 1
-
-     let kind (s : t) : Tree.NodeKind.t =
-       Obj.magic (s lsr 3)
-
-     let make is_left has_left has_right kind =
-       (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)
+  type t = int
+  let dummy = -1
+     (*
+       ...44443210
+       ...4444 -> kind
+       3 -> has_right
+       2 -> has_left
+       1 -> is_right
+       0 -> is_left
+     *)
+  let is_left (s : t) : bool =
+    s land 1 != 0
+
+  let is_right (s : t) : bool =
+    s land 0b10 != 0
+
+  let has_left (s : t) : bool =
+    s land 0b100 != 0
+
+  let has_right (s : t) : bool =
+       s land 0b1000 != 0
+
+  let kind (s : t) : Tree.NodeKind.t =
+    Obj.magic (s lsr 4)
+
+  let make is_left is_right has_left has_right kind =
+    (int_of_bool is_left) lor
+      ((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
 
-   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_set = StateSet.singleton State.dummy
 
-   let dummy_status =
-     NodeStatus.make {
-       rank = -1;
-       sat = StateSet.empty;
-       todo = StateSet.empty;
-       summary = NodeSummary.dummy;
-     }
 
 
-   type run = {
-     tree : T.t ;
+IFDEF HTMLTRACE
+THEN
+   type sat_array = StateSet.t array list
+   DEFINE IFHTML(a,b) = (a)
+ELSE
+   type sat_array = StateSet.t array
+   DEFINE IFHTML(a,b) = (b)
+END
+
+   let unsafe_get a i =
+     if i < 0 then StateSet.empty else
+       Array.unsafe_get (IFHTML(List.hd a, a)) i
+
+   let unsafe_set a i v old_v =
+     if v != old_v then
+       Array.unsafe_set (IFHTML(List.hd a, a)) i v
+
+   type 'a run = {
+     tree : 'a ;
      (* The argument of the run *)
      auto : Ata.t;
      (* The automaton to be run *)
-     status : NodeStatus.t array;
-     (* A mapping from node preorders to NodeStatus *)
+     mutable sat: sat_array;
+     (* A mapping from node preorders to states satisfied at that node *)
      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 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 len = T.size tree in
-     {
-       tree = tree;
-       auto = auto;
-       status = Array.create len dummy_status;
-       pass = 0;
-       fetch_trans_cache = Cache.N2.create dummy_form;
-       td_cache = Cache.N5.create dummy_status;
-       bu_cache = Cache.N5.create dummy_status;
-     }
-
-   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;
@@ -201,295 +136,180 @@ 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
-           | 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) ->
-                         let down, ({ NodeStatus.node = n_sum; _ } as sum) =
+                       b && StateSet.mem q (
                            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
-           | 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
 
 
-   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 trans_cache tag summary fcs nss ps sat todo  =
+     StateSet.fold (fun q (a_sat) ->
+       let phi =
+         get_form 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 trans_cache tag summary fcs nss ps sat todo  =
+     let new_sat =
+       eval_trans_aux auto trans_cache tag summary fcs nss ps sat todo
      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 trans_cache tag summary fcs nss ps new_sat todo
 
 
-   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 summary fcs nss ps ss todo =
+     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 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;
-     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 summary fcs nss ps ss todo
+          in
+          Cache.N6.add eval_cache tagid summary ssid fcsid nssid psid new_sat;
+          new_sat
+
+
+module Make (T : Tree.S) (L : Node_list.S with type node = T.node) =
+ struct
 
-  let top_down run =
+   let make auto tree =
+     let len = T.size tree in
+     {
+       tree = tree;
+       auto = auto;
+       sat = (let a = Array.create len StateSet.empty in
+             IFHTML([a], a));
+       pass = 0;
+       fetch_trans_cache = Cache.N2.create dummy_form;
+       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 top_down run =
     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
+    let bu_todo =
+      if i == Array.length states_by_rank - 1 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 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
-        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_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 *)
+            in
+            run.node_summaries.{node_id} <- s; s
         in
+        let status0 = unsafe_get run.sat node_id 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 *)
-        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
-        in
-        let () = Logger.msg `STATS "Run %i, Node %a, %a@\n"
-          (i) QName.print tag NodeStatus.print status0
+        let status1 =
+          eval_trans
+            auto run.fetch_trans_cache run.td_cache tag
+            summary
+            (unsafe_get run.sat (T.preorder tree fc))
+            (unsafe_get run.sat (T.preorder tree ns))
+            parent_sat
+            status0 td_todo
         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
-          in
-
-          if status1 != status0 then status.(node_id) <- status1;
-        end;
-        (* recursively traverse the first child *)
-        loop_td_only fc;
-        loop_td_only ns
-      end
+        (* 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
+          if bu_todo == StateSet.empty then begin
+            unsafe_set run.sat node_id status1 status0; (* write the td_states *)
+            loop_td_and_bu ns node status1 (* tail call *)
+          end else
+            let nss1 = loop_td_and_bu ns node status1 in
+            let status2 =
+              eval_trans auto run.fetch_trans_cache run.bu_cache tag
+                summary fcs1
+                nss1
+                parent_sat
+                status1 bu_todo
+            in
+            unsafe_set run.sat node_id status2 status0;
+            status2
+        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 dummy_set in
+    run.pass <- run.pass + 2
 
 
   let get_results run =
-    let cache = run.status in
+    let cache = IFHTML((List.hd run.sat), run.sat) in
     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).NodeStatus.node.sat
-          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 =
-    let cache = run.status in
+    let cache = IFHTML((List.hd run.sat), run.sat) in
     let auto = run.auto in
     let tree = run.tree in
     let res_mapper = Hashtbl.create MED_H_SIZE in
@@ -498,24 +318,26 @@ DEFINE AND_(t1,t2) =
         (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).NodeStatus.node.sat
+          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
@@ -526,29 +348,25 @@ DEFINE AND_(t1,t2) =
   let prepare_run run list =
     let tree = run.tree in
     let auto = run.auto in
-    let status = run.status 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 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 sat = IFHTML((List.hd run.sat), run.sat) in
+    let sat0 = Ata.get_starting_states auto in
+    L.iter (fun node ->
       let node_id = T.preorder tree node in
-      status.(node_id) <- status0) list
+      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;
@@ -556,13 +374,14 @@ DEFINE AND_(t1,t2) =
     prepare_run run nodes;
     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;
+      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;
     done;
+    IFHTML((run.sat <- List.tl run.sat), ());
     pass := Ata.get_max_rank auto + 1;
-    IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree);
-
+    IFHTML(Html_trace.gen_trace auto run.sat (module T : Tree.S with type t = T.t) tree ,());
     run
 
   let full_eval auto tree nodes =
@@ -571,7 +390,8 @@ DEFINE AND_(t1,t2) =
 
   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;