package minisat

  1. Overview
  2. Docs
Bindings to the SAT solver Minisat, with the solver included.

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (6)

Authors

  1. S
    simon.cruanes.2007@m4x.org

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

minisat-0.6.tbz
sha256=e407a60be9c495d449be8a0ad955941ac1639515bad19fdbacd4a15d5aaf6605
sha512=17a5eafd2afb2cb3e829a0b7eb32c14de5ebeeaed12ecfc4f58410c9b582918595c6c31facbbda126e9fd394d3846e14f961cab529d41ac82b0775930246e5fa

doc/minisat/Minisat/index.html

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
Sourceval create : unit -> t

Create a fresh solver state.

Sourceval okay : t -> bool

true if the solver isn't known to be in an unsat state

  • since 0.6
Sourceexception Unsat
Sourceval ensure_lit_exists : t -> Lit.t -> unit

Make sure the solver decides this literal.

  • since 0.6
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 value_at_level_0 : t -> Lit.t -> value

Returns the assignment level for this literal at level 0, if assigned there, or V_undef. If lit is not assigned at level 0, this returns V_undef even when the literal has a value in the current model.

  • since 0.6
Sourceval unsat_core : t -> Lit.t array

Returns the subset of assumptions of a solver that returned "unsat" when called with solve ~assumptions s.

  • since 0.6
Sourceval set_verbose : t -> int -> unit

Verbose mode.

Sourceval interrupt : t -> unit

Interrupt the solver, typically from another thread.

  • since 0.6
Sourceval clear_interrupt : t -> unit

Clear interrupt flag so that we can use the solver again.

  • since 0.6
Sourceval n_clauses : t -> int
  • since 0.6
Sourceval n_vars : t -> int
  • since 0.6
Sourceval n_conflicts : t -> int
  • since 0.6
Sourcemodule Debug : sig ... end