projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Replace the Hashtbl.t used for mapping nodes to state-sets by an
[tatoo.git]
/
src
/
auto
/
eval.ml
diff --git
a/src/auto/eval.ml
b/src/auto/eval.ml
index
5c346d0
..
cc9ed71
100644
(file)
--- 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"
*)
INCLUDE "utils.ml"
@@
-27,12
+27,10
@@
module Make (T : Tree.Sig.S) :
end
= struct
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;
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)
(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
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 =
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
let redo = ref true in
let iter = ref 0 in
while !redo do