let create (config: config) : state =
let root_choice_point = {
cp_id = 0;
cp_split_literal = Term.null_literal;
cp_right_splits = [];
cp_valid = true;
}
in
let state =
{
st_config = config;
st_id = Counter.create_with 0;
st_root_choice_point = root_choice_point;
st_branch = [root_choice_point];
st_literal_info = LiteralTable.create 1024;
}
in
let root_branch_node = {
li_literal = Term.null_literal;
li_type = Propagation;
li_choice_point = root_choice_point;
li_context_unifier = Subst.empty;
li_clause = [];
li_clause_vars = [];
li_clause_utility = (fun () -> ());
li_clause_index = -2;
li_context_literals = [| |];
li_explanation = Some [];
}
in
LiteralTable.add state.st_literal_info Term.assert_literal root_branch_node;
LiteralTable.add state.st_literal_info (Config.default_v state.st_config) root_branch_node;
LiteralTable.add state.st_literal_info Term.null_literal root_branch_node;
state