An instance of minisat (stateful)

Create a fresh solver state.

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

• since 0.6

Make sure the solver decides this literal.

• since 0.6

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

• raises Unsat

  if the problem is unsat.

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

• raises Unsat

  if the problem is unsat.

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.

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.

• since 0.5

• since 0.5

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.

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

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

• since 0.6

Verbose mode.

Interrupt the solver, typically from another thread.

• since 0.6

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

• since 0.6

• since 0.6

• since 0.6

• since 0.6