- 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 auto run.fetch_trans_cache 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
+ action node node_id fc ns
+ end
+
+ and td_action_builder parent_sat summary tag status1 =
+ let update_res = mk_update_res false status1 in
+ match NodeSummary.(has_left summary, has_right summary) with
+ false, false ->
+ (fun node node_id fc ns ->
+ unsafe_set run_sat node_id status1;
+ update_res node;
+ StateSet.empty)
+ | true, false ->
+ (fun node node_id fc ns ->
+ unsafe_set run_sat node_id status1;
+ update_res node;
+ loop_td fc node status1)
+ | false, true ->
+ (fun node node_id fc ns ->
+ unsafe_set run_sat node_id status1;
+ update_res node;
+ loop_td ns node status1)
+ | _ ->
+ (fun node node_id fc ns ->
+ unsafe_set run_sat node_id status1; (* write the td_states *)
+ update_res node;
+ ignore (loop_td fc node status1);
+ loop_td ns node status1 (* tail call *)
+ )
+ and td_and_bu_action_builder parent_sat summary tag status1 node node_id fc ns =
+ let fcs1 = loop_td_and_bu fc node status1 in
+ let nss1 = loop_td_and_bu ns node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary fcs1 nss1 parent_sat status1 bu_todo bu_action_builder
+ in
+ action node node_id
+ and bu_action_builder parent_sat summary tag status2 node node_id =
+ unsafe_set run_sat node_id status2;
+ status2
+ and td_and_bu_last_action_builder parent_sat summary tag status1 node node_id fc ns =
+ let nss1 = loop_td_and_bu_last ns node status1 in
+ let fcs1 = loop_td_and_bu_last fc node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary fcs1 nss1 parent_sat status1 bu_todo bu_last_action_builder
+ in
+ action node node_id
+ and bu_last_action_builder parent_sat summary tag status2 =
+ let update_res = mk_update_res true status2 in
+ (fun node node_id ->
+ unsafe_set run_sat node_id status2;
+ update_res node;
+ status2)
+ and loop_td node parent parent_sat =
+ common node parent parent_sat td_action_builder
+ and loop_td_and_bu node parent parent_sat =
+ common node parent parent_sat td_and_bu_action_builder
+ and loop_td_and_bu_last node parent parent_sat =
+ common node parent parent_sat td_and_bu_last_action_builder
+ in
+ let _ =
+ if bu_todo == StateSet.empty then
+ loop_td (Tree.root tree) Tree.nil dummy_set
+ else if last_run then
+ loop_td_and_bu_last (Tree.root tree) Tree.nil dummy_set
+ else
+ loop_td_and_bu (Tree.root tree) Tree.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 = ResultSet.create () in
+ (fun prepend sat ->
+ if StateSet.intersect sat sel_states then
+ if prepend then (fun n -> ResultSet.push_front n res)
+ else (fun n -> ResultSet.push_back n res)
+ else (fun _ -> ())),
+ (fun () -> res)
+
+
+ let mk_update_full_result auto =
+ let sel_states = Ata.get_selecting_states auto in
+ let res_mapper =
+ StateSet.fold_right (fun q acc -> (q, ResultSet.create())::acc) sel_states []