sig
  type config = Config.config
  type statistic = Statistic.statistic
  type bound = Bound.bound
  type literal = Term.literal
  type clause = Term.clause
  type state = State.state
  type context_unifier_space = Context_unifier.context_unifier_space
  type raw_context_unifier = Context_unifier.raw_context_unifier
  type problem_literals = Problem_literals.problem_literals
  type space_registry
  val create :
    Context_unifier_space.config ->
    Context_unifier_space.bound -> Context_unifier_space.space_registry
  val create_space :
    ?register:bool ->
    Context_unifier_space.space_registry ->
    Context_unifier_space.problem_literals ->
    Context_unifier_space.clause ->
    (Context_unifier_space.raw_context_unifier -> unit) ->
    (Context_unifier_space.raw_context_unifier -> bool) ->
    (Context_unifier_space.raw_context_unifier -> unit) ->
    (Context.element -> bool) ->
    (Context.element -> bool) ->
    bool -> Context_unifier_space.context_unifier_space
  val get_id : Context_unifier_space.space_registry -> int
  val backtrack : Context_unifier_space.context_unifier_space -> unit
end