let create (config: config) (bound: bound) (statistic: statistic) (state: state) (context: context)
(clauses: clause list) (lemmas: clause list) (initial_interpretation: literal list)
(guiding_path: guiding_path) : selection =
let problem_literals =
Problem_literals.create config bound statistic state context
in
let space_registry =
Context_unifier_space.create config bound
in
let selection_assert =
Selection_assert.create config bound statistic state context problem_literals
and selection_split =
Selection_split.create config bound statistic state context problem_literals space_registry
in
let best_closing =
ref None
in
let process_close_candidate (candidate: raw_context_unifier) : unit =
process_close_candidate state best_closing candidate
and process_assert_candidate (candidate: raw_context_unifier) : bool =
Selection_assert.add selection_assert candidate
and process_split_candidate (candidate: raw_context_unifier) : unit =
Selection_split.add selection_split candidate
and is_element_incomplete_assert (element: Context.element) : bool =
Selection_assert.is_element_incomplete selection_assert element
and is_element_incomplete_split (element: Context.element) : bool =
Selection_split.is_element_incomplete selection_split element
in
let clause_spaces, unit_asserts =
create_spaces space_registry statistic problem_literals
process_close_candidate process_assert_candidate process_split_candidate
is_element_incomplete_assert is_element_incomplete_split
clauses false
in
let lemmas_propositional =
Lemma_propositional.create config state context selection_assert process_close_candidate process_assert_candidate space_registry
in
let lemma_spaces, lemma_asserts =
match Config.lemma config with
| Flags.LM_Propositional ->
List.iter
(fun lemma ->
Lemma_propositional.add_lemma lemmas_propositional lemma true
)
lemmas;
[], []
| Flags.LM_None
| Flags.LM_Grounded
| Flags.LM_Lifted ->
let lemma_spaces, lemma_asserts =
create_spaces space_registry statistic problem_literals
process_close_candidate process_assert_candidate process_split_candidate
is_element_incomplete_assert is_element_incomplete_split
lemmas true
in
let lemma_spaces =
List.map (fun lemma -> (lemma, true)) lemma_spaces
in
lemma_spaces, lemma_asserts
in
let initial_interpretation' =
List.map
(fun literal ->
let new_context_unifier_space : context_unifier_space =
Context_unifier_space.create_space ~register:false
space_registry
problem_literals
[Term.init_literal]
process_close_candidate
process_assert_candidate
process_split_candidate
is_element_incomplete_assert
is_element_incomplete_split
false
in
let raw_context_unifier =
Context_unifier.create_context_unifier
new_context_unifier_space [| Context_unifier.assert_partner |] false
in
(literal, raw_context_unifier)
)
initial_interpretation
in
let sorted_unit_asserts =
List.sort
(fun (x, _) (y, _) ->
compare
(Term_attributes.weight_of_literal x)
(Term_attributes.weight_of_literal y)
)
(initial_interpretation' @ lemma_asserts @ unit_asserts)
in
let selection = {
sel_config = config;
sel_bound = bound;
sel_statistic = statistic;
sel_state = state;
sel_context = context;
sel_problem_literals = problem_literals;
sel_space_registry = space_registry;
sel_clause_spaces = Array.of_list clause_spaces;
sel_lemma_spaces = lemma_spaces;
sel_best_closing = best_closing;
sel_unit_asserts = sorted_unit_asserts;
sel_assert = selection_assert;
sel_split = selection_split;
sel_no_splits_yet = true;
sel_process_close = process_close_candidate;
sel_process_assert = process_assert_candidate;
sel_process_split = process_split_candidate;
sel_is_element_incomplete_assert = is_element_incomplete_assert;
sel_is_element_incomplete_split = is_element_incomplete_split;
sel_decay_counter = ref 0;
sel_guiding_path = guiding_path;
sel_lemmas_propositional = lemmas_propositional;
}
in
selection