Package org.sosy_lab.java_smt.delegate.debugging

Class DebuggingOptimizationProverEnvironment

java.lang.Object

org.sosy_lab.java_smt.delegate.debugging.DebuggingOptimizationProverEnvironment

All Implemented Interfaces:

AutoCloseable, BasicProverEnvironment<Void>, OptimizationProverEnvironment

public class DebuggingOptimizationProverEnvironment
extends Object
implements OptimizationProverEnvironment

Nested Class Summary

Nested classes/interfaces inherited from interface org.sosy_lab.java_smt.api.BasicProverEnvironment

BasicProverEnvironment.AllSatCallback<R>

Nested classes/interfaces inherited from interface org.sosy_lab.java_smt.api.OptimizationProverEnvironment

OptimizationProverEnvironment.OptStatus

Field Summary

Fields inherited from interface org.sosy_lab.java_smt.api.BasicProverEnvironment

NO_MODEL_HELP

Method Summary

Modifier and Type	Method	Description
@Nullable T	addConstraint(BooleanFormula constraint)	Add a constraint to the latest backtracking point.
<R> R	allSat(BasicProverEnvironment.AllSatCallback<R> callback, List<BooleanFormula> important)	Get all satisfying assignments of the current environment with regard to a subset of terms, and create a region representing all those models.
OptimizationProverEnvironment.OptStatus	check()	Optimize the objective function subject to the previously imposed constraints.
void	close()	Closes the prover environment.
Model	getModel()	Get a satisfying assignment.
List<BooleanFormula>	getUnsatCore()	Get an unsat core.
boolean	isUnsat()	Check whether the conjunction of all formulas on the stack is unsatisfiable.
boolean	isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)	Check whether the conjunction of all formulas on the stack together with the list of assumptions is satisfiable.
Optional<Rational>	lower(int handle, Rational epsilon)
int	maximize(Formula objective)	Add the maximization objective.
int	minimize(Formula objective)	Add minimization objective.
void	pop()	Remove one backtracking point/level from the current stack.
void	push()	Create a new backtracking point, i.e., a new level on the assertion stack.
int	size()	Get the number of backtracking points/levels on the current stack.
Optional<List<BooleanFormula>>	unsatCoreOverAssumptions(Collection<BooleanFormula> assumptions)	Returns an UNSAT core (if it exists, otherwise Optional.empty()), over the chosen assumptions.
Optional<Rational>	upper(int handle, Rational epsilon)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.sosy_lab.java_smt.api.BasicProverEnvironment

addConstraint, allSat, close, getEvaluator, getModelAssignments, getStatistics, getUnsatCore, isUnsat, isUnsatWithAssumptions, pop, push, push, registerUserPropagator, size, unsatCoreOverAssumptions

Methods inherited from interface org.sosy_lab.java_smt.api.OptimizationProverEnvironment

getModel

Method Detail

maximize

public int maximize(Formula objective)

Description copied from interface: OptimizationProverEnvironment

Add the maximization objective.

Note: push/pop may be used for switching objectives

Specified by:

maximize in interface OptimizationProverEnvironment

Returns:

Objective handle, to be used for retrieving the value.

minimize

public int minimize(Formula objective)

Description copied from interface: OptimizationProverEnvironment

Add minimization objective.

Note: push/pop may be used for switching objectives

Specified by:

minimize in interface OptimizationProverEnvironment

Returns:

Objective handle, to be used for retrieving the value.

check

public OptimizationProverEnvironment.OptStatus check()
                                              throws InterruptedException,
                                                     SolverException

Description copied from interface: OptimizationProverEnvironment

Optimize the objective function subject to the previously imposed constraints.

Specified by:

check in interface OptimizationProverEnvironment

Returns:

Status of the optimization problem.

Throws:

InterruptedException

SolverException

upper

public Optional<Rational> upper(int handle,
                                Rational epsilon)

Specified by:

upper in interface OptimizationProverEnvironment

epsilon - Value to substitute for the epsilon.

Returns:

Upper approximation of the optimized value, or absent optional if the objective is unbounded.

lower

public Optional<Rational> lower(int handle,
                                Rational epsilon)

Specified by:

lower in interface OptimizationProverEnvironment

epsilon - Value to substitute for the epsilon.

Returns:

Lower approximation of the optimized value, or absent optional if the objective is unbounded.

pop

public void pop()

Description copied from interface: BasicProverEnvironment

Remove one backtracking point/level from the current stack. This removes the latest level including all of its formulas, i.e., all formulas that were added for this backtracking point.

Specified by:

pop in interface BasicProverEnvironment<T>

addConstraint

public @Nullable T addConstraint(BooleanFormula constraint)
                          throws InterruptedException

Description copied from interface: BasicProverEnvironment

Add a constraint to the latest backtracking point.

Specified by:

addConstraint in interface BasicProverEnvironment<T>

Throws:

InterruptedException

push

public void push()
          throws InterruptedException

Description copied from interface: BasicProverEnvironment

Create a new backtracking point, i.e., a new level on the assertion stack. Each level can hold several asserted formulas.

If formulas are added before creating the first backtracking point, they can not be removed via a POP-operation.

Specified by:

push in interface BasicProverEnvironment<T>

Throws:

InterruptedException

size

public int size()

Description copied from interface: BasicProverEnvironment

Get the number of backtracking points/levels on the current stack.

Caution: This is the number of PUSH-operations, and not necessarily equal to the number of asserted formulas. On any level there can be an arbitrary number of asserted formulas. Even with size of 0, formulas can already be asserted (at bottom level).

Specified by:

size in interface BasicProverEnvironment<T>

isUnsat

public boolean isUnsat()
                throws SolverException,
                       InterruptedException

Description copied from interface: BasicProverEnvironment

Check whether the conjunction of all formulas on the stack is unsatisfiable.

Specified by:

isUnsat in interface BasicProverEnvironment<T>

Throws:

SolverException

InterruptedException

isUnsatWithAssumptions

public boolean isUnsatWithAssumptions(Collection<BooleanFormula> assumptions)
                               throws SolverException,
                                      InterruptedException

Description copied from interface: BasicProverEnvironment

Check whether the conjunction of all formulas on the stack together with the list of assumptions is satisfiable.

Specified by:

isUnsatWithAssumptions in interface BasicProverEnvironment<T>

Parameters:

assumptions - A list of literals.

Throws:

SolverException

InterruptedException

getModel

public Model getModel()
               throws SolverException

Description copied from interface: BasicProverEnvironment

Get a satisfying assignment. This method should be called only immediately after an BasicProverEnvironment.isUnsat() call that returned false. The returned model is guaranteed to stay constant and valid as long as the solver context is available, even if constraints are added to, pushed or popped from the prover stack.

A model might contain additional symbols with their evaluation, if a solver uses its own temporary symbols. There should be at least a value-assignment for each free symbol.

Specified by:

getModel in interface BasicProverEnvironment<T>

Throws:

SolverException

getUnsatCore

public List<BooleanFormula> getUnsatCore()

Description copied from interface: BasicProverEnvironment

Get an unsat core. This should be called only immediately after an BasicProverEnvironment.isUnsat() call that returned false.

Specified by:

getUnsatCore in interface BasicProverEnvironment<T>

unsatCoreOverAssumptions

public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(Collection<BooleanFormula> assumptions)
                                                        throws SolverException,
                                                               InterruptedException

Description copied from interface: BasicProverEnvironment

Returns an UNSAT core (if it exists, otherwise Optional.empty()), over the chosen assumptions. Does NOT require the SolverContext.ProverOptions.GENERATE_UNSAT_CORE option to work.

Specified by:

unsatCoreOverAssumptions in interface BasicProverEnvironment<T>

Parameters:

assumptions - Selected assumptions

Returns:

Empty optional if the constraints with assumptions are satisfiable, subset of assumptions which is unsatisfiable with the original constraints otherwise.

Throws:

SolverException

InterruptedException

close

public void close()

Description copied from interface: BasicProverEnvironment

Closes the prover environment. The object should be discarded, and should not be used after closing. The first call of this method will close the prover instance, further calls are ignored.

Specified by:

close in interface AutoCloseable

Specified by:

close in interface BasicProverEnvironment<T>

allSat

public <R> R allSat(BasicProverEnvironment.AllSatCallback<R> callback,
                    List<BooleanFormula> important)
             throws InterruptedException,
                    SolverException

Description copied from interface: BasicProverEnvironment

Get all satisfying assignments of the current environment with regard to a subset of terms, and create a region representing all those models.

Specified by:

allSat in interface BasicProverEnvironment<T>

important - A set of (positive) variables appearing in the asserted queries. Only these variables will appear in the region.

Returns:

A region representing all satisfying models of the formula.

Throws:

InterruptedException

SolverException