sig
  module Lit = BBox.Lit
  exception UndecidedLit
  type clause = Lit.t list
  val add_clause : proof:Sat_solver_intf.proof_step -> Lit.t list -> unit
  val add_clauses :
    proof:Sat_solver_intf.proof_step -> Lit.t list list -> unit
  val add_clause_seq :
    proof:Sat_solver_intf.proof_step -> Lit.t list Sequence.t -> unit
  val check : unit -> Sat_solver_intf.result
  val last_result : unit -> Sat_solver_intf.result
  val valuation : Lit.t -> bool
  val valuation_level : Lit.t -> bool * int
  val proved_at_0 : Lit.t -> bool option
  val set_printer : Lit.t CCFormat.printer -> unit
  val get_proof : unit -> Sat_solver_intf.proof
  val get_proof_of_lit : Lit.t -> Sat_solver_intf.proof
  val setup : unit -> unit
  type save_level
  val root_save_level : Sat_solver_intf.S.save_level
  val save : unit -> Sat_solver_intf.S.save_level
  val restore : Sat_solver_intf.S.save_level -> unit
end