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