Module type SatSolver.S

module type S = sig .. end

type var 

type lit 

val reset : unit -> unit

val restart : unit -> unit

val new_var : unit -> var

val pos_lit : var -> lit

val neg_lit : var -> lit

val is_eliminated : var -> bool

val lookahead : unit -> int option

val add_clause : lit list -> unit

val add_quantifier : bool -> var list -> unit

val solve : ?simplify:bool -> lit list -> SatSolver.solution

val solve_cnf : int list list -> SatSolver.solution * int list

val value_of : var -> SatSolver.value

val set_timeout : float -> unit