package minisat

  1. Overview
  2. Docs
package minisat
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module MinisatSource

Bindings to Minisat.

Sourcetype t

An instance of minisat (stateful)

Sourcetype 'a printer = Format.formatter -> 'a -> unit
Sourcemodule Lit : sig ... end
Sourcetype assumptions = Lit.t array
Sourcemodule Raw : sig ... end
Sourceval create : unit -> t

Create a fresh solver state.

Sourceexception Unsat
Sourceval 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.

Sourceval 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.

Sourceval pp_clause : Lit.t list printer
Sourceval 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.

Sourceval 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.

Sourcetype value =
  1. | V_undef
  2. | V_true
  3. | V_false
Sourceval string_of_value : value -> string
  • since 0.5
Sourceval pp_value : value printer
  • since 0.5
Sourceval 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.

Sourceval set_verbose : t -> int -> unit