package minisat

You can search for identifiers within the package.

in-package search v0.2.0

package minisat

minisat
- Minisat
  - Lit
  - Raw

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

Create a fresh solver state.

exception Unsat

val add_clause_l : t -> Lit.t list -> unit

Add a clause (as a list of literals) to the solver state.

raises Unsat
if the problem is unsat.

val add_clause_a : t -> Lit.t array -> unit

Add a clause (as an array of literals) to the solver state.

raises Unsat
if the problem is unsat.

val pp_clause : Lit.t list printer

val simplify : t -> unit

Perform simplifications on the solver state. Speeds up later manipulations on the solver state, e.g. calls to solve.

raises Unsat
if the problem is unsat.

val solve : ?assumptions:assumptions -> t -> unit

Check whether the current solver state is satisfiable, additionally assuming that the literals provided in assumptions are assigned to true. After solve terminates (raising Unsat or not), the solver state is unchanged: the literals in assumptions are only considered to be true for the duration of the query.

raises Unsat
if the problem is unsat.

type value =

| V_undef
| V_true
| V_false

val string_of_value : value -> string

since 0.5

val pp_value : value printer

since 0.5

val value : t -> Lit.t -> value

Returns the assignation of a literal in the solver state. This must only be called after a call to solve that returned successfully without raising Unsat.

val set_verbose : t -> int -> unit