let apply_split_right (state: state) (literal: literal) (context_unifier: subst)
(clause: clause) (clause_vars: Subst.var list) (clause_index: int) (clause_value: unit -> unit)
(context_literals: literal array)
: unit =
let active =
active_choice_point state
in
let literal_info =
create_literal_info literal SplitRight active
context_unifier clause clause_vars context_literals clause_index clause_value None
in
active.cp_right_splits <- literal :: active.cp_right_splits;
LiteralTable.add state.st_literal_info literal literal_info