From: Kim Nguyễn <kn@lri.fr>
Date: Wed, 7 Aug 2013 10:34:51 +0000 (+0200)
Subject: Improve performance of parallel run by replacing standard hashtable with
X-Git-Tag: v0.1~50
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=d9e3bea94223a9d8f47ca0f0724b43aa102abf1e

Improve performance of parallel run by replacing standard hashtable with
Cache.N1 array.
---

diff --git a/src/run.ml b/src/run.ml
index bd60264..e356128 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -445,22 +445,28 @@ 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);
     List.rev (StateSet.fold
-                (fun q acc -> (q, Hashtbl.find res_mapper q)::acc)
+                (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
                 (Ata.get_selecting_states auto) [])
 
   let prepare_run run list =
@@ -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