projects
/
tatoo.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
45ca692
)
Refine the run to have a different set of states to satisfy while going td/bu.
author
Kim Nguyễn
<kn@lri.fr>
Sat, 30 Nov 2013 18:27:49 +0000
(19:27 +0100)
committer
Kim Nguyễn
<kn@lri.fr>
Sat, 30 Nov 2013 18:27:49 +0000
(19:27 +0100)
src/ata.ml
patch
|
blob
|
history
src/run.ml
patch
|
blob
|
history
diff --git
a/src/ata.ml
b/src/ata.ml
index
f55452e
..
565dfc8
100644
(file)
--- a/
src/ata.ml
+++ b/
src/ata.ml
@@
-490,7
+490,6
@@
let compute_rank auto =
done;
let by_rank = Hashtbl.create 17 in
List.iter (fun (r,s) ->
done;
let by_rank = Hashtbl.create 17 in
List.iter (fun (r,s) ->
- let r = r/2 in
let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
auto.ranked_states <-
let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
auto.ranked_states <-
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