+ 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 =
+ match NodeSummary.(has_left summary, has_right summary) with
+ false, false ->
+ (fun node node_id fc ns ->
+ let action =
+ eval_trans run run.bu_cache tag summary StateSet.empty StateSet.empty
+ parent_sat status1 bu_todo bu_action_builder
+ in
+ action node node_id)
+ | true, false ->
+ (fun node node_id fc ns ->
+ let fcs1 = loop_td_and_bu fc node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary fcs1 StateSet.empty
+ parent_sat status1 bu_todo bu_action_builder
+ in
+ action node node_id
+ )
+ | false, true ->
+ (fun node node_id fc ns ->
+ let nss1 = loop_td_and_bu ns node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary StateSet.empty nss1
+ parent_sat status1 bu_todo bu_action_builder
+ in
+ action node node_id
+ )
+ | _ ->
+ (fun 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 =
+ match NodeSummary.(has_left summary, has_right summary) with
+ false, false ->
+ (fun node node_id fc ns ->
+ let action =
+ eval_trans run run.bu_cache tag summary StateSet.empty StateSet.empty
+ parent_sat status1 bu_todo bu_last_action_builder
+ in
+ action node node_id)
+ | true, false ->
+ (fun node node_id fc ns ->
+ let fcs1 = loop_td_and_bu_last fc node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary fcs1 StateSet.empty
+ parent_sat status1 bu_todo bu_last_action_builder
+ in
+ action node node_id
+ )
+ | false, true ->
+ (fun node node_id fc ns ->
+ let nss1 = loop_td_and_bu_last ns node status1 in
+ let action =
+ eval_trans run run.bu_cache tag summary StateSet.empty nss1
+ parent_sat status1 bu_todo bu_last_action_builder
+ in
+ action node node_id
+ )
+ | _ ->
+ (fun 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