projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Lowlevel optimizations in the Ptset module, replace some function
[tatoo.git]
/
src
/
run.ml
diff --git
a/src/run.ml
b/src/run.ml
index
9c8203b
..
bd60264
100644
(file)
--- a/
src/run.ml
+++ b/
src/run.ml
@@
-299,7
+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 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
@@
-459,9
+459,9
@@
DEFINE AND_(t1,t2) =
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) []
+
List.rev (
StateSet.fold
+
(fun q acc -> (q, Hashtbl.find res_mapper q)::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