- 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 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
+ )