sig
  type value = int
  type solution = SAT | UNSAT | TIMEOUT
  val string_of_value : SatSolver.value -> string
  module type S =
    sig
      type var
      type lit
      val reset : unit -> unit
      val restart : unit -> unit
      val new_var : unit -> SatSolver.S.var
      val pos_lit : SatSolver.S.var -> SatSolver.S.lit
      val neg_lit : SatSolver.S.var -> SatSolver.S.lit
      val is_eliminated : SatSolver.S.var -> bool
      val lookahead : unit -> int option
      val add_clause : SatSolver.S.lit list -> unit
      val add_quantifier : bool -> SatSolver.S.var list -> unit
      val solve :
        ?simplify:bool -> SatSolver.S.lit list -> SatSolver.solution
      val solve_cnf : int list list -> SatSolver.solution * int list
      val value_of : SatSolver.S.var -> SatSolver.value
      val set_timeout : float -> unit
    end
  val solver : string Pervasives.ref
  val get_solver : unit -> (module SatSolver.S)
  val delete_dimacs_files : bool Pervasives.ref
end