let create_space ?(register: bool = true) (space_registry: space_registry)
(problem_literals: problem_literals)
(clause: clause)
(process_close_candidate: raw_context_unifier -> unit)
(process_assert_candidate: raw_context_unifier -> bool)
(process_split_candidate: raw_context_unifier -> unit)
(is_element_incomplete_assert: Context.element -> bool)
(is_element_incomplete_split: Context.element -> bool)
(is_lemma: bool)
: context_unifier_space =
match clause with
| [] ->
failwith "Context_unifier_space.create"
| _ ->
create_space' ~register:register space_registry problem_literals
process_close_candidate process_assert_candidate process_split_candidate
is_element_incomplete_assert is_element_incomplete_split
clause is_lemma