sig
  type var = Var.var
  type literal = Term.literal
  type clause = Term.clause
  type subst = Subst.subst
  type choice_point = State.choice_point
  type state = State.state
  type 'a stack = 'a Stack.stack
  type candidate_type = Close | Assert | Split | CloseAssert | All
  type context_partner = private {
    cp_element : Context.element;
    cp_partial_context_unifier : Context_unifier.subst option;
    cp_empty_remainder : bool;
  }
  type context_partners = Context_unifier.context_partner array
  type input_partner = private {
    ip_index : int;
    ip_literal : Context_unifier.literal;
    ip_vars : Subst.var list;
    mutable ip_context_partners :
      Context_unifier.context_partner Context_unifier.stack;
    mutable ip_resolved : Context_unifier.context_partner option;
  }
  type context_unifier_space = private {
    cus_id : int;
    cus_clause : Context_unifier.clause;
    cus_lemma : bool;
    mutable cus_lemma_learned : int;
    cus_vars : Subst.var list;
    cus_shared_vars : Subst.var list;
    cus_local_vars : Subst.var list;
    cus_input_partners : Context_unifier.input_partner array;
    cus_input_partners_ordering : int array;
    cus_process_close_candidate : Context_unifier.raw_context_unifier -> unit;
    cus_process_assert_candidate :
      Context_unifier.raw_context_unifier -> bool;
    cus_process_split_candidate : Context_unifier.raw_context_unifier -> unit;
    cus_is_element_incomplete_assert : Context.element -> bool;
    cus_is_element_incomplete_split : Context.element -> bool;
    cus_utility : int Pervasives.ref;
  }
  and raw_context_unifier = private {
    rcu_space : Context_unifier.context_unifier_space;
    rcu_context_partners : Context_unifier.context_partners;
    rcu_exceeding_complexity : bool;
  }
  exception UNSATISFIABLE
  exception CLOSE of Context_unifier.raw_context_unifier
  val null_partner : Context_unifier.context_partner
  val assert_partner : Context_unifier.context_partner
  val null_context_unifier : Context_unifier.raw_context_unifier
  val create_context_unifier :
    Context_unifier.context_unifier_space ->
    Context_unifier.context_partners ->
    bool -> Context_unifier.raw_context_unifier
  val create_context_partner :
    Context.element ->
    Context_unifier.subst option -> bool -> Context_unifier.context_partner
  val create_input_partner :
    int ->
    Context_unifier.literal ->
    Subst.var list -> Context_unifier.input_partner
  val create_space :
    int ->
    Context_unifier.clause ->
    Subst.var list ->
    Subst.var list ->
    Subst.var list ->
    Context_unifier.input_partner array ->
    int array ->
    (Context_unifier.raw_context_unifier -> unit) ->
    (Context_unifier.raw_context_unifier -> bool) ->
    (Context_unifier.raw_context_unifier -> unit) ->
    (Context.element -> bool) ->
    (Context.element -> bool) ->
    bool -> Context_unifier.context_unifier_space
  val set_resolved :
    Context_unifier.input_partner ->
    Context_unifier.context_partner option -> unit
  val increase_lemma_learned : Context_unifier.context_unifier_space -> unit
  val is_raw_context_unifier_invalid :
    Context_unifier.raw_context_unifier -> bool
  val extend_partial_context_unifier :
    recompute:bool ->
    p_preserving:bool ->
    Context_unifier.subst ->
    Context_unifier.input_partner ->
    Context_unifier.context_partner -> Context_unifier.subst
  val recompute_unifier :
    recompute:bool ->
    Context_unifier.raw_context_unifier -> Context_unifier.subst
  val recompute_full_unifier :
    recompute:bool ->
    Context_unifier.raw_context_unifier -> Context_unifier.subst
  val is_remainder : Context_unifier.subst -> Context.element -> int -> bool
  val is_remainder' : Context_unifier.subst -> bool
  val compute_remainder_states :
    Context_unifier.raw_context_unifier ->
    Context_unifier.subst -> bool array
  val generation_of_candidate : Context_unifier.context_partners -> int
  val get_context_literals :
    Context_unifier.context_partners -> Context_unifier.literal array
  val get_creation_choice_point :
    Context_unifier.context_partners -> Context_unifier.choice_point
  val creating_context_element :
    Context_unifier.raw_context_unifier -> Context.element
  val is_permanently_blocking :
    Context.element -> Context_unifier.context_partners -> bool
  val create_space_utility_inc :
    Context_unifier.context_unifier_space -> unit -> unit
  val compare_context_unifiers :
    different:bool ->
    Context_unifier.raw_context_unifier ->
    Context_unifier.raw_context_unifier -> int
  val raw_context_unifier_to_string :
    Context_unifier.raw_context_unifier -> string
  val context_unifier_to_string :
    Context_unifier.context_unifier_space ->
    Context_unifier.context_partners -> string
end