From d9e3bea94223a9d8f47ca0f0724b43aa102abf1e Mon Sep 17 00:00:00 2001
From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= <kn@lri.fr>
Date: Wed, 7 Aug 2013 12:34:51 +0200
Subject: [PATCH] Improve performance of parallel run by replacing standard
 hashtable with Cache.N1 array.

---
 src/run.ml | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

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
-- 
2.17.1