X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=0d0e7e95cb8d3f8ec60e106eab68e1097c9d48fa;hp=887eb35cdeb2f44588923714608c64c4f89e50a2;hb=84751fead39221a8e01d20a4692faf0b63a7c996;hpb=b73ad7605777c49c65673e34f6f9ee635053db13

diff --git a/src/run.ml b/src/run.ml
index 887eb35..0d0e7e9 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -103,7 +103,8 @@ type 'a run = {
      (* 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;
+  (*node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t; *)
+  node_summaries: Bytes.t;
   stats : stats;
 }
 
@@ -193,7 +194,7 @@ let eval_trans run trans_cache tag summary fcs nss ps ss todo =
   stats.eval_trans_cache_access <- 1 + stats.eval_trans_cache_access;
   if res != dummy_set then
     res
-  else let new_sat =
+  else let new_sat = if todo == StateSet.empty then ss else
              eval_trans_fix run tag summary fcs nss ps ss todo
     in
     stats.eval_trans_cache_miss <- 1 + stats.eval_trans_cache_miss;
@@ -201,13 +202,18 @@ let eval_trans run trans_cache tag summary fcs nss ps ss todo =
     new_sat
 
 
-module Make (T : Tree.S) (L : Deque.S with type elem = T.node) =
+module Make (T : Tree.S)  =
 struct
+  module Tree : Tree.S with type node = T.node = T
+  module ResultSet : Deque.S with type elem = Tree.node =
+    Deque.Make (struct type t = Tree.node end)
+
 
   let make auto tree =
-    let len = T.size tree in
-    let ba = Array1.create int16_unsigned c_layout len in
-    Array1.fill ba 0;
+    let len = Tree.size tree in
+    (* let ba = Array1.create int16_unsigned c_layout len in
+       Array1.fill ba 0; *)
+    let ba = Bytes.make len '\000' in
     {
       tree = tree;
       auto = auto;
@@ -230,7 +236,7 @@ struct
     }
 
 
-  let top_down run update_res =
+  let top_down2 run update_res =
     let num_visited = ref 0 in
     let i = run.pass in
     let tree = run.tree in
@@ -242,95 +248,137 @@ struct
       else
         states_by_rank.(i+1)
     in
+    let run_sat = run.sat in
     let last_run = i >= Array.length states_by_rank - 2 in
-    let rec loop_td_and_bu node parent parent_sat =
-      if node == T.nil then StateSet.empty
+    let rec common node parent parent_sat kont =
+      if node == Tree.nil then StateSet.empty
       else begin
         incr num_visited;
-        let tag = T.tag tree node in
-        let node_id = T.preorder tree node in
-        let fc = T.first_child tree node in
-        let ns = T.next_sibling tree node in
-         (* We enter the node from its parent *)
+        let tag = Tree.tag tree node in
+        let node_id = Tree.preorder tree node in
+        let fc = Tree.first_child tree node in
+        let ns = Tree.next_sibling tree node in
+        (* We enter the node from its parent *)
         let summary =
-          let s = Array1.unsafe_get run.node_summaries node_id in
+          let s = Char.code (Bytes.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 *)
+                (node == (Tree.first_child tree parent)) (*is_left *)
+                (node == (Tree.next_sibling tree parent)) (*is_right *)
+                (fc != Tree.nil) (* has_left *)
+                (ns != Tree.nil) (* has_right *)
+                (Tree.kind tree node) (* kind *)
             in
-            run.node_summaries.{node_id} <- s; s
+            Bytes.unsafe_set run.node_summaries node_id (Char.chr s); s
         in
-        let status0 = unsafe_get run.sat node_id in
+        let status0 = unsafe_get run_sat node_id in
         (* get the node_statuses for the first child, next sibling and parent *)
         (* evaluate the transitions with all this statuses *)
         let status1 =
           eval_trans run
             run.td_cache tag
             summary
-            (unsafe_get run.sat (T.preorder tree fc))
-            (unsafe_get run.sat (T.preorder tree ns))
+            (unsafe_get run_sat (Tree.preorder tree fc))
+            (unsafe_get run_sat (Tree.preorder tree ns))
             parent_sat
             status0 td_todo
         in
-          (* update the cache if the status of the node changed
-             unsafe_set run.sat node_id status1 status0;*)
-        if bu_todo == StateSet.empty then begin
-          unsafe_set run.sat node_id status1 status0; (* write the td_states *)
-          update_res false status1 node;
-          let _ = loop_td_and_bu fc node status1 in
-          loop_td_and_bu ns node status1 (* tail call *)
-        end else
-          let fcs1, nss1 =
-            if last_run then
-              let nss1 = loop_td_and_bu ns node status1 in
-              let fcs1 = loop_td_and_bu fc node status1 in
-              fcs1, nss1
-            else
-              let fcs1 = loop_td_and_bu fc node status1 in
-              let nss1 = loop_td_and_bu ns node status1 in
-              fcs1, nss1
-          in
-          let status2 =
-            eval_trans run run.bu_cache tag
-              summary fcs1
-              nss1
-              parent_sat
-              status1 bu_todo
-          in
-          unsafe_set run.sat node_id status2 status0;
-          if last_run && status2 != StateSet.empty then update_res true status2 node;
-          status2
+        kont summary tag parent_sat status0 status1 fc ns node node_id
       end
+
+    and kont_pure_td summary tag parent_sat status0 status1 fc ns node node_id =
+      unsafe_set run_sat node_id status1 status0; (* write the td_states *)
+      update_res false status1 node;
+      if fc != Tree.nil then ignore (loop_td fc node status1);
+      if ns == Tree.nil then StateSet.empty else loop_td ns node status1 (* tail call *)
+    and kont_td_and_bu summary tag parent_sat status0 status1 fc ns node node_id =
+      let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu fc node status1 in
+      let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu ns node status1 in
+      let status2 =
+        eval_trans run run.bu_cache tag
+          summary fcs1
+          nss1
+          parent_sat
+          status1 bu_todo
+      in
+      unsafe_set run_sat node_id status2 status0;
+      status2
+    and kont_td_and_bu_last summary tag parent_sat status0 status1 fc ns node node_id =
+      let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu_last ns node status1 in
+      let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu_last fc node status1 in
+      let status2 =
+        eval_trans run run.bu_cache tag
+          summary fcs1
+          nss1
+          parent_sat
+          status1 bu_todo
+      in
+      unsafe_set run_sat node_id status2 status0;
+      if status2 != StateSet.empty then update_res true status2 node;
+      status2
+    and loop_td node parent parent_sat =
+      common node parent parent_sat kont_pure_td
+    and loop_td_and_bu node parent parent_sat =
+      common node parent parent_sat kont_td_and_bu
+    and loop_td_and_bu_last node parent parent_sat =
+      common node parent parent_sat kont_td_and_bu_last
+    in
+
+    let _ =
+      if bu_todo == StateSet.empty then
+        loop_td (Tree.root tree) Tree.nil dummy_set
+      else if last_run then
+        loop_td_and_bu_last (Tree.root tree) Tree.nil dummy_set
+      else
+        loop_td_and_bu (Tree.root tree) Tree.nil dummy_set
     in
-    let _ = loop_td_and_bu (T.root tree) T.nil dummy_set in
     run.pass <- run.pass + 2;
     run.stats.pass <- run.stats.pass + 1;
     run.stats.nodes_per_run <- !num_visited :: run.stats.nodes_per_run
 
 
+  type res_op = Dummy | Prepend | Append | Nothing
 
   let mk_update_result auto =
     let sel_states = Ata.get_selecting_states auto in
-    let res = L.create () in
+    let res = ResultSet.create () in
+    let cache = Cache.N2.create Dummy in
     (fun prepend sat node ->
+       let sat_id = (sat.StateSet.id :> int) in
+       let prep_id : int = Obj.magic prepend in
+       let op = Cache.N2.find cache prep_id sat_id in
+       let op =
+         if op == Dummy then
+           let op =
+             if StateSet.intersect sel_states sat then
+               if prepend then
+                 Prepend
+               else Append
+             else Nothing
+           in
+           let () = Cache.N2.add cache prep_id sat_id op in
+           op
+         else op
+       in
+       match op with
+         Dummy | Nothing -> ()
+       | Prepend -> ResultSet.push_front node res
+       | Append -> ResultSet.push_back node res
+                     (*
       if StateSet.intersect sel_states sat then begin
         if prepend then L.push_front node res else
           L.push_back node res
-      end),
+      end*)),
     (fun () -> res)
 
 
   let mk_update_full_result auto =
-    let dummy = L.create () in
+    let dummy = ResultSet.create () in
     let res_mapper = Cache.N1.create dummy in
     let () =
       StateSet.iter
-        (fun q -> Cache.N1.add res_mapper (q :> int) (L.create()))
+        (fun q -> Cache.N1.add res_mapper (q :> int) (ResultSet.create()))
         (Ata.get_selecting_states auto)
     in
     (fun prepend sat node ->
@@ -338,8 +386,8 @@ struct
         (fun q ->
           let res = Cache.N1.find res_mapper (q :> int) in
           if res != dummy then begin
-            if prepend then L.push_front node res
-            else L.push_back node res
+            if prepend then ResultSet.push_front node res
+            else ResultSet.push_back node res
           end
         ) sat),
     (fun () ->
@@ -352,8 +400,8 @@ struct
     let auto = run.auto 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
+   ResultSet.iter (fun node ->
+      let node_id = Tree.preorder tree node in
       sat.(node_id) <- sat0) list
 
 
@@ -362,13 +410,13 @@ struct
     prepare_run run nodes;
     let rank = Ata.get_max_rank auto in
     while run.pass <= rank do
-      top_down run update_res;
+      top_down2 run update_res;
       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), ());
-    IFHTML(Html_trace.gen_trace auto run.sat (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 = Tree.t) tree ,());
     run