Remove some unneeded code that was slowing down the run function.

[tatoo.git] / src / run.ml

diff --git a/src/run.ml b/src/run.ml
index 31eb26c..7677af1 100644 (file)
--- a/src/run.ml
+++ b/src/run.ml
@@ -132,8 +132,6 @@ module Make (T : Tree.S) =
      (* The automaton to be run *)
      status : NodeStatus.t array;
      (* A mapping from node preorders to NodeStatus *)
-     unstable : Bitvector.t;
-     (* A bitvector remembering whether a subtree is stable *)
      mutable redo : bool;
      (* A boolean indicating whether the run is incomplete *)
      mutable pass : int;
@@ -157,7 +155,6 @@ module Make (T : Tree.S) =
        tree = tree;
        auto = auto;
        status = Array.create len dummy_status;
-       unstable = Bitvector.create ~init:true len;
        redo = true;
        pass = 0;
        cache2 = Cache.N2.create dummy_form;
@@ -330,7 +327,6 @@ DEFINE AND_(t1,t2) =
     let status = run.status in
     let cache2 = run.cache2 in
     let cache5 = run.cache5 in
-    let unstable = run.unstable 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
@@ -339,8 +335,7 @@ DEFINE AND_(t1,t2) =
     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
-      else begin
+      if node != T.nil then begin
         let parent = T.parent tree node in
         let fc = T.first_child tree node in
         let fc_id = T.preorder tree fc in
@@ -348,7 +343,6 @@ DEFINE AND_(t1,t2) =
         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
@@ -370,7 +364,6 @@ DEFINE AND_(t1,t2) =
               }
           else c
         in
-        IFTRACE(html tree node _i status0 "Entering node");
         (* 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
@@ -380,14 +373,13 @@ DEFINE AND_(t1,t2) =
           if status0.NodeStatus.node.todo == StateSet.empty then status0
           else begin
             let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in
-            IFTRACE(html tree node _i status1 "Updating transitions");
           (* update the cache if the status of the node changed *)
             if status1 != status0 then status.(node_id) <- status1;
             status1
           end
         in
         (* recursively traverse the first child *)
-        let unstable_left = loop fc in
+        let () = loop 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
@@ -403,60 +395,34 @@ DEFINE AND_(t1,t2) =
           if status1.NodeStatus.node.todo == StateSet.empty then status1
           else begin
             let status2 = eval_trans auto cache2 cache5 tag fcs1 nss ps status1 in
-            IFTRACE(html tree node _i status2
-                      "Updating transitions (after first-child)");
             if status2 != status1 then status.(node_id) <- status2;
             status2
           end
         in
-        let unstable_right = loop ns in
+        let () = loop ns in
         let nss1 = unsafe_get_status status ns_id in
-        let status3 =
-          if status2.NodeStatus.node.todo == StateSet.empty then status2
-          else begin
-            let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in
-            IFTRACE(html tree node _i status3
-                      "Updating transitions (after next-sibling)");
-          if status3 != status2 then status.(node_id) <- status3;
-          status3
-        end
-        in
-        let unstable_self =
-          (* if either our left or right child is unstable or if we
-             still have transitions pending, the current node is
-             unstable *)
-          unstable_left
-          || unstable_right
-          || StateSet.empty != status3.NodeStatus.node.todo
-        in
-        Bitvector.unsafe_set unstable node_id unstable_self;
-        IFTRACE((if not unstable_self then
-            Html.finalize_node
-              node_id
-              _i
-              Ata.(StateSet.intersect status3.NodeStatus.node.sat
-                     (get_selecting_states auto))));
-        unstable_self
+        if status2.NodeStatus.node.todo != StateSet.empty then
+          let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in
+          if status3 != status2 then status.(node_id) <- status3
       end
     in
-    run.redo <- loop (T.root tree);
-    run.pass <- run.pass + 1
+    loop (T.root tree)
 
 
   let get_results run =
     let cache = run.status 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 Ata.(
-          StateSet.intersect
-            cache.(T.preorder tree node).NodeStatus.node.sat
-            (get_selecting_states auto)) then node::acc1
+        if StateSet.intersect
+          cache.(T.preorder tree node).NodeStatus.node.sat
+          sel_states then node::acc1
         else acc1
     in
     loop (T.root tree) []
@@ -530,7 +496,8 @@ DEFINE AND_(t1,t2) =
     let run = make auto tree in
     prepare_run run nodes;
     for i = 0 to Ata.get_max_rank auto do
-      top_down run
+      top_down run;
+      run.pass <- run.pass + 1
     done;
     pass := Ata.get_max_rank auto + 1;
     IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree);