sig
  type config = Config.config
  type statistic = Statistic.statistic
  type counter = Counter.counter
  type var = Var.var
  type symbol = Symbol.symbol
  type term = Term.term
  type literal = Term.literal
  type clause = Term.clause
  type choice_point = State.choice_point
  type state = State.state
  type problem = Problem.problem
  type bound = Bound.bound
  type finite_domain = Finite_domain.finite_domain
  type element = private {
    el_id : int;
    el_literal : Context.literal;
    el_choice_point : Context.choice_point;
    el_pars : Context.var list;
    el_generation : int;
    el_is_fd_incomplete : bool;
    mutable el_compacted : int;
  }
  type context
  val create :
    Context.config -> Context.statistic -> Context.state -> Context.context
  val from_file :
    string ->
    Context.config -> Context.statistic -> Context.state -> Context.context
  val null_element : Context.element
  val assert_element : Context.element
  val plus_v_element : Context.element
  val minus_v_element : Context.element
  val add :
    Context.context -> Context.literal -> int -> bool -> Context.element
  val is_universal : Context.context -> bool
  val element_equal : Context.element -> Context.element -> bool
  val element_for_literal :
    Context.context -> Context.literal -> Context.element option
  val most_recent_element : Context.context -> Context.element
  val is_more_recent : Context.element -> Context.element -> bool
  val iter : (Context.element -> unit) -> Context.context -> unit
  val fold : ('a -> Context.element -> 'a) -> 'a -> Context.context -> 'a
  val check_contradictory :
    Context.context -> Context.literal -> Context.element option
  val check_subsumed :
    Context.context -> Context.literal -> Context.element option
  val check_productive :
    Context.context ->
    Context.literal -> Context.literal -> Context.element option
  val is_true : Context.context -> Context.literal -> bool
  val find_all_unifiable :
    Context.context -> Context.literal -> Context.element list
  val find_all_subsuming :
    Context.context -> Context.literal -> Context.element list
  val element_to_string : Context.element -> string
  val print_context : Context.context -> Pervasives.out_channel -> unit
  val print_DIG :
    Context.context -> Pervasives.out_channel -> Context.problem -> unit
  val print_tptp_model :
    Context.context ->
    Pervasives.out_channel ->
    Context.problem -> Context.finite_domain option -> Context.bound -> unit
  val print_multiplication_tables :
    Context.context ->
    Pervasives.out_channel -> Context.problem -> Context.bound -> unit
  val print_max_size : Context.context -> unit
  val backtrack : Context.context -> unit
end