sig
  type proof_step = Logtk.Proof.Step.t
  type proof = Logtk.Proof.t
  type result = Sat | Unsat of proof
  exception WrongState of string
  module type S =
    sig
      module Lit = BBox.Lit
      exception UndecidedLit
      type clause = Lit.t list
      val add_clause : proof:proof_step -> Lit.t list -> unit
      val add_clauses : proof:proof_step -> Lit.t list list -> unit
      val add_clause_seq : proof:proof_step -> Lit.t list Sequence.t -> unit
      val check : full:bool -> unit -> result
      val last_result : unit -> result
      val valuation : Lit.t -> bool
      val valuation_level : Lit.t -> bool * int
      val proved_at_0 : Lit.t -> bool option
      val all_proved : unit -> Lit.Set.t
      val set_printer : Lit.t CCFormat.printer -> unit
      val get_proof : unit -> proof
      val get_proof_opt : unit -> proof option
      val get_proof_of_lit : Lit.t -> proof
      val setup : unit -> unit
    end
  module Make : functor (Dummy : sig  end) -> S
  val set_compact : bool -> unit
end