loop phi
- let eval_trans_aux auto cache2 cache4 tag fcs nss ps old_status =
+ let eval_trans_aux auto cache2 tag fcs nss ps old_status =
let { sat = old_sat;
todo = old_todo;
summary = old_summary } as os_node = old_status.NodeStatus.node
let eval_trans auto cache2 cache5 tag fcs nss ps ss =
+ let rec loop old_status =
+ let new_status =
+ eval_trans_aux auto cache2 tag fcs nss ps old_status
+ in
+ if new_status == old_status then old_status else loop new_status
+ in
let fcsid = (fcs.NodeStatus.id :> int) in
let nssid = (nss.NodeStatus.id :> int) in
let psid = (ps.NodeStatus.id :> int) in
+ let ssid = (ss.NodeStatus.id :> int) in
let tagid = (tag.QName.id :> int) in
- let rec loop old_status =
- let oid = (old_status.NodeStatus.id :> int) in
- let res =
- let res = Cache.N5.find cache5 tagid oid fcsid nssid psid in
- if res != dummy_status then res
- else
- let new_status =
- eval_trans_aux auto cache2 cache5 tag fcs nss ps old_status
- in
- Cache.N5.add cache5 tagid oid fcsid nssid psid new_status;
- new_status
- in
- if res == old_status then res else loop res
- in
- loop ss
-
+ let res = Cache.N5.find cache5 tagid ssid fcsid nssid psid in
+ if res != dummy_status then res
+ else let new_status = loop ss in
+ Cache.N5.add cache5 tagid ssid fcsid nssid psid new_status;
+ new_status
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
(* 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 *)