projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Add fold_left/right functions to the set interface (iterate in
[tatoo.git]
/
src
/
run.ml
diff --git
a/src/run.ml
b/src/run.ml
index
f6812e4
..
53cecb4
100644
(file)
--- a/
src/run.ml
+++ b/
src/run.ml
@@
-299,6
+299,7
@@
DEFINE AND_(t1,t2) =
let cache2 = run.cache2 in
let cache5 = run.cache5 in
let unstable = run.unstable in
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 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
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
@@
-316,9
+317,7
@@
DEFINE AND_(t1,t2) =
(* first time we visit the node *)
NodeStatus.make
{ sat = StateSet.empty;
(* first time we visit the node *)
NodeStatus.make
{ sat = StateSet.empty;
- todo = StateSet.diff
- (Ata.get_states auto)
- (Ata.get_starting_states auto);
+ todo = init_todo;
summary = NodeSummary.make
(node == T.first_child tree parent) (* is_left *)
(node == T.next_sibling tree parent) (* is_right *)
summary = NodeSummary.make
(node == T.first_child tree parent) (* is_left *)
(node == T.next_sibling tree parent) (* is_right *)
@@
-446,23
+445,29
@@
DEFINE AND_(t1,t2) =
(fun q -> Hashtbl.add res_mapper q [])
(Ata.get_selecting_states auto)
in
(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 ->
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);
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
let prepare_run run list =
let tree = run.tree in
@@
-498,7
+503,6
@@
DEFINE AND_(t1,t2) =
if full then `Full (get_full_results run)
else `Normal (get_results run)
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
let full_eval auto tree nodes =
match eval true auto tree nodes with
`Full l -> l