projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Refine the run to have a different set of states to satisfy while going td/bu.
[tatoo.git]
/
src
/
run.ml
diff --git
a/src/run.ml
b/src/run.ml
index
b51daf9
..
31eb26c
100644
(file)
--- a/
src/run.ml
+++ b/
src/run.ml
@@
-253,15
+253,15
@@
DEFINE AND_(t1,t2) =
let open NodeSummary in
match a.Atom.node with
| Move (m, q) ->
let open NodeSummary in
match a.Atom.node with
| Move (m, q) ->
- let
{ NodeStatus.node = n_sum; _ } as sum
=
+ let
down, ({ NodeStatus.node = n_sum; _ } as sum)
=
match m with
match m with
- `First_child -> fcs
- | `Next_sibling -> nss
- | `Parent | `Previous_sibling -> ps
- | `Stay -> ss
+ `First_child ->
true,
fcs
+ | `Next_sibling ->
true,
nss
+ | `Parent | `Previous_sibling ->
false,
ps
+ | `Stay ->
false,
ss
in
if sum == dummy_status
in
if sum == dummy_status
- ||
n_sum.rank < ss.NodeStatus.node.rank
+ ||
(down && n_sum.rank < ss.NodeStatus.node.rank)
|| StateSet.mem q n_sum.todo then
Unknown
else
|| StateSet.mem q n_sum.todo then
Unknown
else
@@
-332,7
+332,11
@@
DEFINE AND_(t1,t2) =
let cache5 = run.cache5 in
let unstable = run.unstable in
let states_by_rank = Ata.get_states_by_rank auto in
let cache5 = run.cache5 in
let unstable = run.unstable in
let states_by_rank = Ata.get_states_by_rank auto in
- let init_todo = states_by_rank.(i) in
+ let td_todo = states_by_rank.(i) in
+ let bu_todo = if i + 1 = Array.length states_by_rank then StateSet.empty
+ else
+ states_by_rank.(i+1)
+ 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
let rec loop node =
let node_id = T.preorder tree node in
if node == T.nil (*|| not (Bitvector.get unstable node_id)*) then false
@@
-352,7
+356,7
@@
DEFINE AND_(t1,t2) =
NodeStatus.make
{ rank = i;
sat = c.NodeStatus.node.sat;
NodeStatus.make
{ rank = i;
sat = c.NodeStatus.node.sat;
- todo =
init
_todo;
+ todo =
td
_todo;
summary = let summary = c.NodeStatus.node.summary
in
if summary != NodeSummary.dummy then summary
summary = let summary = c.NodeStatus.node.summary
in
if summary != NodeSummary.dummy then summary
@@
-388,6
+392,13
@@
DEFINE AND_(t1,t2) =
get the new status of the first child *)
let fcs1 = unsafe_get_status status fc_id in
(* update the status *)
get the new status of the first child *)
let fcs1 = unsafe_get_status status fc_id in
(* update the status *)
+ let status1 = if status1.NodeStatus.node.rank < i then
+ NodeStatus.make { status1.NodeStatus.node with
+ rank = i;
+ todo = bu_todo }
+ else
+ status1
+ in
let status2 =
if status1.NodeStatus.node.todo == StateSet.empty then status1
else begin
let status2 =
if status1.NodeStatus.node.todo == StateSet.empty then status1
else begin