Adds a blocking clause to the solver.
Removes all learnt clauses fromt the solver.
Discards the current model (meant to be used when iterating on models of a formula).
Force timeout to expire.
Success(model)
the currently set timeout value in seconds.
the currently set timeout value in milliseconds.
True iff DB simplification is allowed.
True iff the solver is kept hot between check-sats.
Lifts the negation of the current model to a clause (to be used as a blocking clause when enumerating models), optionally projecting the model over the given set of literals.
Lifts the negation of the current model to a clause (to be used as a blocking clause when enumerating models), optionally projecting the model over the given set of literals.
A list of literals on which to restrict the clause
Success(clause)
Lifts the current model to a cube, optionally projecting the model over the given set of literals.
Lifts the current model to a cube, optionally projecting the model over the given set of literals.
A list of literals on which to restrict the cube
Success(cube)
Resets the solver to a clean state.
Enable/disable clause DB simplification.
Enable/disable the "keep solver hot" feature.
Sets a timeout expressed in seconds.
Sets a timeout expressed in seconds.
timeout duration in seconds.
Sets a timeout expressed in milliseconds.
Sets a timeout expressed in milliseconds.
timeout duration in milliseconds.
Sets a timeout expressed as a number of conflicts.
Sets a timeout expressed as a number of conflicts.
timeout duration in number of conflicts reached.
Returns a clause explaning the unsat state of the constraints (must follow a call to ProblemLike.isSatisfiable that returned false.
Returns a clause explaning the unsat state of the constraints (must follow a call to ProblemLike.isSatisfiable that returned false.
Success(clause)
A builder for dimacs models, returning a result of type R.