package minisat
Legend:
Library
Module
Module type
Parameter
Class
Class type

Bindings to Minisat

type t

An instance of minisat (stateful)

type 'a printer = Format.formatter -> 'a -> unit
module Lit : sig ... end
type assumptions = Lit.t array
module Raw : sig ... end
val create : unit -> t
exception Unsat
val add_clause_l : t -> Lit.t list -> unit
  • raises Unsat

    if the problem is unsat

val add_clause_a : t -> Lit.t array -> unit
  • raises Unsat

    if the problem is unsat

val pp_clause : Lit.t list printer
val simplify : t -> unit
  • raises Unsat

    if the problem is unsat

val solve : ?assumptions:assumptions -> t -> unit
  • raises Unsat

    if the problem is unsat

type value =
| V_undef
| V_true
| V_false
val value : t -> Lit.t -> value
val set_verbose : t -> int -> unit