- and kont_pure_td summary tag parent_sat status0 status1 fc ns node node_id =
- unsafe_set run_sat node_id status1 status0; (* write the td_states *)
- update_res false status1 node;
- if fc != Tree.nil then ignore (loop_td fc node status1);
- if ns == Tree.nil then StateSet.empty else loop_td ns node status1 (* tail call *)
- and kont_td_and_bu summary tag parent_sat status0 status1 fc ns node node_id =
- let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu fc node status1 in
- let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu ns node status1 in
- let status2 =
- eval_trans run run.bu_cache tag
- summary fcs1
- nss1
- parent_sat
- status1 bu_todo
+ 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