match m with
`First_child -> fcs
| `Next_sibling -> nss
- | `Parent | `Previous_sibling -> ps
- | `Stay -> ss
+ | `Parent | `Previous_sibling -> ps
+ | `Stay -> ss
)
| Is_first_child -> b == is_left summary
| Is_next_sibling -> b == is_right summary
let rec loop_td_and_bu node parent parent_sat =
if node == T.nil then StateSet.empty
else begin
+ let tag = T.tag tree node in
let node_id = T.preorder tree node in
let fc = T.first_child tree node in
let ns = T.next_sibling tree node in
if s != 0 then s else
let s =
NodeSummary.make
- (node_id == T.preorder tree (T.first_child tree parent)) (*is_left *)
- (node_id == T.preorder tree (T.next_sibling tree parent))(*is_right *)
+ (node == (T.first_child tree parent)) (*is_left *)
+ (node == (T.next_sibling tree parent))(*is_right *)
(fc != T.nil) (* has_left *)
(ns != T.nil) (* has_right *)
(T.kind tree node) (* kind *)
let status0 = unsafe_get run.sat node_id in
(* get the node_statuses for the first child, next sibling and parent *)
(* evaluate the transitions with all this statuses *)
- let tag = T.tag tree node in
let status1 =
eval_trans
auto run.fetch_trans_cache run.td_cache tag
parent_sat
status0 td_todo
in
-
- (* update the cache if the status of the node changed
- unsafe_set run.sat node_id status1 status0;*)
+ if status1 == StateSet.empty && status0 != StateSet.empty
+ then StateSet.empty else
+ (* update the cache if the status of the node changed
+ unsafe_set run.sat node_id status1 status0;*)
if bu_todo == StateSet.empty then begin
unsafe_set run.sat node_id status1 status0; (* write the td_states *)
update_res false status1 node;
status1 bu_todo
in
unsafe_set run.sat node_id status2 status0;
- if last_run then update_res true status2 node;
+ if last_run && status2 != StateSet.empty then update_res true status2 node;
status2
end
in