Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Minisat
SourceBindings to Minisat.
An instance of minisat (stateful)
Add a clause (as a list of literals) to the solver state.
Add a clause (as an array of literals) to the solver state.
Perform simplifications on the solver state. Speeds up later manipulations on the solver state, e.g. calls to solve
.
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.
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
.