sig
  type solver
  val new_solver : unit -> Cc_core.solver
  val fresh_variable : Cc_core.solver -> Cc_literal.Variable.t
  val proxy_app :
    Cc_core.solver ->
    Cc_literal.Variable.t -> Cc_literal.Variable.t -> Cc_literal.Variable.t
  val proxy_u :
    Cc_core.solver ->
    Cc_literal.Variable.t ->
    Cc_literal.Variable.t -> Cc_literal.Variable.t -> Cc_literal.Variable.t
  val proxy_k :
    Cc_core.solver -> Cc_literal.Variable.t -> Cc_literal.Variable.t
  val add_interface_literal :
    Cc_core.solver -> Cc_literal.Variable.t * Cc_literal.Variable.t -> unit
  val decision_level : Cc_core.solver -> int
  val inference_possible : Cc_core.solver -> bool
  val conflict_detected : Cc_core.solver -> bool
  val is_true : Cc_core.solver -> Cc_literal.literal -> bool
  val is_inferred : Cc_core.solver -> Cc_literal.literal -> bool
  val infer : Cc_core.solver -> unit
  val final_check : Cc_core.solver -> unit
  val set_literal : Cc_core.solver -> Cc_literal.literal -> unit
  val get_literal_possible : Cc_core.solver -> bool
  val get_literal : Cc_core.solver -> Cc_literal.literal
  val get_lemma_possible : Cc_core.solver -> bool
  val get_lemma : Cc_core.solver -> Cc_literal.lemma
  val literal_explanation :
    Cc_core.solver -> Cc_literal.literal -> Cc_literal.literal list
  val increment_level : Cc_core.solver -> unit
  val backjump : Cc_core.solver -> int -> unit
  val restart : Cc_core.solver -> unit
  val conflict_clause : Cc_core.solver -> Cc_literal.literal list
end

---

Hosted by the ^* web site.
^*Other names and brands may be claimed as the property of others.