- let status1 = eval_trans cache4 fcs nss ps status0 in
-
- TRACE(html tree node _i config1 "Updating transitions");
-
- (* update the cache if the status of the node changed *)
-
- if status1 != status0 then status.(node_id) <- status1;
- (* recursively traverse the first child *)
- let unstable_left = loop fc in
- (* here we re-enter the node from its first child,
- get the new status of the first child *)
- let fcs1 = unsafe_get_status status fc_id in
- (* update the status *)
- let status2 = eval_trans cache4 fcs1 nss ps status1 in
-
- TRACE(html tree node _i config2 "Updating transitions (after first-child)");
-
- if status2 != status1 then status.(node_id) <- status2;
- let unstable_right = loop ns in
- let nss1 = unsafe_get_status status ns_id in
- let status3 = eval_trans cache4 fcs1 nss1 ps status2 in
+ let status1 =
+ eval_trans run
+ run.td_cache tag
+ summary
+ (unsafe_get run.sat (T.preorder tree fc))
+ (unsafe_get run.sat (T.preorder tree ns))
+ parent_sat
+ status0 td_todo
+ in
+ 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;
+ let _ = loop_td_and_bu fc node status1 in
+ loop_td_and_bu ns node status1 (* tail call *)
+ end else
+ let fcs1, nss1 =
+ if last_run then
+ let nss1 = loop_td_and_bu ns node status1 in
+ let fcs1 = loop_td_and_bu fc node status1 in
+ fcs1, nss1
+ else
+ let fcs1 = loop_td_and_bu fc node status1 in
+ let nss1 = loop_td_and_bu ns node status1 in
+ fcs1, nss1
+ in
+ let status2 =
+ eval_trans run run.bu_cache tag
+ summary fcs1
+ nss1
+ parent_sat
+ status1 bu_todo
+ in
+ unsafe_set run.sat node_id status2 status0;
+ if last_run && status2 != StateSet.empty then update_res true status2 node;
+ status2
+ end
+ in
+ let _ = loop_td_and_bu (T.root tree) T.nil dummy_set in
+ run.pass <- run.pass + 2;
+ run.stats.pass <- run.stats.pass + 1;
+ run.stats.nodes_per_run <- !num_visited :: run.stats.nodes_per_run
+
+
+
+ let mk_update_result auto =
+ let sel_states = Ata.get_selecting_states auto in
+ let res = L.create () in
+ (fun prepend sat node ->
+ if StateSet.intersect sel_states sat then begin
+ if prepend then L.push_front node res else
+ L.push_back node res
+ end),
+ (fun () -> res)
+
+
+ let mk_update_full_result auto =
+ let dummy = L.create () in
+ let res_mapper = Cache.N1.create dummy in
+ let () =
+ StateSet.iter
+ (fun q -> Cache.N1.add res_mapper (q :> int) (L.create()))
+ (Ata.get_selecting_states auto)
+ in
+ (fun prepend sat node ->
+ StateSet.iter
+ (fun q ->
+ let res = Cache.N1.find res_mapper (q :> int) in
+ if res != dummy then begin
+ if prepend then L.push_front node res
+ else L.push_back node res
+ end
+ ) sat),
+ (fun () ->
+ StateSet.fold_right
+ (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
+ (Ata.get_selecting_states auto) [])