Adds a blocking clause to the solver.
Adds a blocking clause to the solver.
Removes all learnt clauses fromt the solver.
Removes all learnt clauses fromt the solver.
Discards the current model (meant to be used when iterating on models of a formula).
Discards the current model (meant to be used when iterating on models of a formula).
Force timeout to expire.
Force timeout to expire.
Checks the problem for satisfiability
Checks the problem for satisfiability
a set of literals to assert during the check.
Succes(m)
Checks the problem for satisfiability
Success(model)
the currently set timeout value in seconds.
the currently set timeout value in milliseconds.
True iff DB simplification is allowed.
True iff DB simplification is allowed.
Checks the problem for satisfiability.
Checks the problem for satisfiability.
set of literals to assert during the check.
true iff the problem is satisfiable under the given assumptions.
Checks the problem for satisfiability.
Checks the problem for satisfiability.
if true, the timeout counter will not reset between each call.
true iff the problem is satisfiable.
Checks the problem for satisfiability.
Checks the problem for satisfiability.
a set of literals to assert during the check.
if true, timeout counter will not be reset between call.
true iff the problem is satisfiable under the given assumptions.
Checks the problem for satisfiability.
Checks the problem for satisfiability.
true iff the problem is satisfiable.
True iff the solver is kept hot between check-sats.
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)
Success(m)
Checks if the given literal is part of the prime implicant computed using the previous call to primeImplicant.
Checks if the given literal is part of the prime implicant computed using the previous call to primeImplicant.
Success(b)
Generates a prime implicant of the problem if some exists.
Generates a prime implicant of the problem if some exists.
Success(pi)
Resets the solver to a clean state.
Resets the solver to a clean state.
Enable/disable clause DB simplification.
Enable/disable clause DB simplification.
Enable/disable the "keep solver hot" feature.
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.