let apply_split_left (state: state) (literal: literal) (context_unifier: subst)
(clause: clause) (clause_vars: Subst.var list) (clause_index: int) (clause_value: unit -> unit)
: choice_point =
let id =
try
Counter.next state.st_id
with
| Counter.OVERFLOW ->
raise (Const.NO_SOLUTION "State.apply_split_left: state id overflow")
in
let new_choice_point = {
cp_id = id;
cp_split_literal = literal;
cp_right_splits = [];
cp_valid = true;
}
in
let branch_node =
create_literal_info literal SplitLeft new_choice_point
context_unifier clause clause_vars [| |] clause_index clause_value (Some ([new_choice_point]))
in
LiteralTable.add state.st_literal_info literal branch_node;
state.st_branch <- new_choice_point :: state.st_branch;
new_choice_point