Module type Solver_intf.E

External solver interface.

type t
type var
val pp_var : Ppx_deriving_runtime.Format.formatter -> var -> Ppx_deriving_runtime.unit
val show_var : var -> Ppx_deriving_runtime.string
type lit
val pp_lit : Ppx_deriving_runtime.Format.formatter -> lit -> Ppx_deriving_runtime.unit
val show_lit : lit -> Ppx_deriving_runtime.string
val create : unit -> t
val set_verbosity : t -> int -> unit
val add_clause : t -> lit list -> unit
val add_clause_empty : t -> unit
val add_clause_unit : t -> lit -> unit
val add_clause_binary : t -> lit -> lit -> unit
val add_clause_ternary : t -> lit -> lit -> lit -> unit
val add_clause_quaternary : t -> lit -> lit -> lit -> lit -> unit
val add_at_most : t -> lit list -> int -> unit
val add_at_least : t -> lit list -> int -> unit
val add_exactly : t -> lit list -> int -> unit
val new_var : t -> var
val okay : t -> bool
val simplify : t -> unit
val solve : t -> solution
val solve_all : t -> var list -> var list list
val value_of : t -> var -> value
val get_stats : t -> stats
val cpu_time : unit -> float

Cumulative user CPU time (seconds) for the process, as measured by the solver's C layer. Monotonic; not reset per solve.

val positive_lit : var -> lit

Cumulative user CPU time (seconds) for the process, as measured by the solver's C layer. Monotonic; not reset per solve.

val negative_lit : var -> lit
val negate : lit -> lit