X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Frun.ml;h=53cecb4fd01ce2229caea09671952a95cd8bcd50;hp=9c8203bd305059d7e93918445e90ef0b6379f53a;hb=a601c67e92d85f7096db693e4fde86950be598c6;hpb=2d9352c1cd8cd3f73c60d0b7c50981f9b42ceb57

diff --git a/src/run.ml b/src/run.ml
index 9c8203b..53cecb4 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -299,7 +299,7 @@ DEFINE AND_(t1,t2) =
     let cache2 = run.cache2 in
     let cache5 = run.cache5 in
     let unstable = run.unstable in
-    let init_todo = StateSet.diff  (Ata.get_states auto)  (Ata.get_starting_states auto) in
+    let init_todo = StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto) 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
@@ -445,23 +445,29 @@ DEFINE AND_(t1,t2) =
         (fun q -> Hashtbl.add res_mapper q [])
         (Ata.get_selecting_states auto)
     in
+    let dummy = [ T.nil ] in
+    let res_mapper = Cache.N1.create dummy in
+    let () =
+      StateSet.iter
+        (fun q -> Cache.N1.add res_mapper (q :> int) [])
+        (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
         StateSet.iter
           (fun q ->
-            try
-              let acc = Hashtbl.find res_mapper q in
-              Hashtbl.replace res_mapper q (node::acc)
-            with
-              Not_found -> ())
+            let res = Cache.N1.find res_mapper (q :> int) in
+            if res != dummy then
+              Cache.N1.add res_mapper (q :> int) (node::res)
+          )
           cache.(T.preorder tree node).NodeStatus.node.sat
     in
     loop (T.root tree);
-    StateSet.fold
-      (fun q acc -> (q, Hashtbl.find res_mapper q)::acc)
-      (Ata.get_selecting_states auto) []
+    (StateSet.fold_right
+       (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
+       (Ata.get_selecting_states auto) [])
 
   let prepare_run run list =
     let tree = run.tree in
@@ -497,7 +503,6 @@ DEFINE AND_(t1,t2) =
     if full then `Full (get_full_results run)
     else `Normal (get_results run)
 
-
   let full_eval auto tree nodes =
     match eval true auto tree nodes with
       `Full l -> l