Library

Module

Module type

Parameter

Class

Class type

Legend:

Library

Module

Module type

Parameter

Class

Class type

Library

Module

Module type

Parameter

Class

Class type

Bindings to Minisat.

`type 'a printer = Format.formatter -> 'a -> unit`

`module Lit : sig ... end`

`type assumptions = Lit.t array`

`val create : unit -> t`

Create a fresh solver state.

`val okay : t -> bool`

`true`

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

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

`val simplify : t -> unit`

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

.

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

`val string_of_value : value -> string`

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.

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

.

`val set_verbose : t -> int -> unit`

Verbose mode.

`val interrupt : t -> unit`

Interrupt the solver, typically from another thread.

`val clear_interrupt : t -> unit`

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

`val n_clauses : t -> int`

`val n_vars : t -> int`

`val n_conflicts : t -> int`

`module Debug : sig ... end`

sectionYPositions = computeSectionYPositions($el), 10)" x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)">