From: Kim Nguyễn <kn@lri.fr>
Date: Wed, 13 Mar 2013 17:54:21 +0000 (+0100)
Subject: Replace the Hashtbl.t used for mapping nodes to state-sets by an
X-Git-Tag: v0.1~124
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=9b3611f8b650edf4183169a9c2c4317e13be536d;hp=738218592e41da4ceb46f4dba41f292a60ba1f7b

Replace the Hashtbl.t used for mapping nodes to state-sets by an
array indexed by pre-order.
---

diff --git a/src/auto/eval.ml b/src/auto/eval.ml
index 5c346d0..cc9ed71 100644
--- a/src/auto/eval.ml
+++ b/src/auto/eval.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-13 18:27:13 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-13 18:54:08 CET by Kim Nguyen>
 *)
 
 INCLUDE "utils.ml"
@@ -27,12 +27,10 @@ module Make (T : Tree.Sig.S) :
   end
  = struct
 
-  type cache = (int, StateSet.t) Hashtbl.t
-  let get c t n =
-    try Hashtbl.find c (T.preorder t n)
-    with Not_found -> StateSet.empty
+  type cache = StateSet.t Cache.N1.t
+  let get c t n = Cache.N1.find c (T.preorder t n)
 
-  let set c t n v = Hashtbl.replace c (T.preorder t n) v
+  let set c t n v = Cache.N1.add c (T.preorder t n) v
 
   module Info = struct
     type t = { is_left : bool;
@@ -95,7 +93,7 @@ module Make (T : Tree.Sig.S) :
               (acct, StateSet.add q accs)
             else
               (Ata.TransList.cons trs acct, accs)
-        ) ltrs (Ata.TransList.nil, ss) 
+        ) ltrs (Ata.TransList.nil, ss)
       in
       Cache.N6.add cache i j k l m n res; res
     else
@@ -176,7 +174,7 @@ module Make (T : Tree.Sig.S) :
     loop node []
 
   let eval auto tree node =
-    let cache = Hashtbl.create 511 in
+    let cache = Cache.N1.create (T.size tree) StateSet.empty in
     let redo = ref true in
     let iter = ref 0 in
     while !redo do
diff --git a/src/tree/naive.ml b/src/tree/naive.ml
index 0885bad..fa14d93 100644
--- a/src/tree/naive.ml
+++ b/src/tree/naive.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-13 10:33:17 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-13 18:47:18 CET by Kim Nguyen>
 *)
 open Utils
 
@@ -54,6 +54,7 @@ let rec dummy = {
 
 type t = {
   root : node;
+  size : int;
   (* TODO add other intersting stuff *)
 }
 
@@ -211,7 +212,9 @@ struct
        match ctx.stack with
          [ root ] ->
            root.next_sibling <- nil;
-           { root = root }
+           { root = root;
+             size = ctx.current_preorder
+           }
        | _ -> raise (Expat.Expat_error Expat.UNCLOSED_TOKEN)
     )
 
@@ -299,6 +302,7 @@ let print_xml out tree_ node =
   let nnode =  { node with next_sibling = nil } in print_xml out tree_ nnode
 
 let root t = t.root
+let size t = t.size
 let first_child _ n = n.first_child
 let next_sibling _ n = n.next_sibling
 let parent _ n = n.parent
diff --git a/src/tree/sig.ml b/src/tree/sig.ml
index aba5917..e2db1d1 100644
--- a/src/tree/sig.ml
+++ b/src/tree/sig.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-11 00:12:27 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-13 18:46:18 CET by Kim Nguyen>
 *)
 
 (** Implementation of documents as binary trees *)
@@ -27,6 +27,9 @@ sig
   type t
   (** The type of trees *)
 
+  val size : t -> int
+  (** Return the number of nodes *)
+
   val nil : node
   (** Nil node, denoting the first/second child of a leaf or the parent of
       the root *)