sig
  exception Sat
  exception Unsat of Solver_types.clause list
  module Make :
    functor (Dummy : sig  end->
      sig
        type state
        val solve : unit -> unit
        val assume : Literal.LT.t list list -> cnumber:int -> unit
        val clear : unit -> unit
        val save : unit -> Solver.Make.state
        val restore : Solver.Make.state -> unit
      end
end