Package org.sosy_lab.java_smt.api

Interface OptimizationProverEnvironment

All Superinterfaces:

AutoCloseable, BasicProverEnvironment<Void>

All Known Implementing Classes:

DebuggingOptimizationProverEnvironment

public interface OptimizationProverEnvironment
extends BasicProverEnvironment<Void>, AutoCloseable

Interface for optimization modulo SMT.

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static class	OptimizationProverEnvironment.OptStatus	Status of the optimization problem.

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

BasicProverEnvironment.AllSatCallback<R>

Field Summary

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

NO_MODEL_HELP

Method Summary

Modifier and Type	Method	Description
OptimizationProverEnvironment.OptStatus	check()	Optimize the objective function subject to the previously imposed constraints.
Model	getModel()	Get a satisfying assignment.
Optional<Rational>	lower(int handle, Rational epsilon)
int	maximize(Formula objective)	Add the maximization objective.
int	minimize(Formula objective)	Add minimization objective.
Optional<Rational>	upper(int handle, Rational epsilon)

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

Method Detail

maximize

int maximize(Formula objective)

Add the maximization objective.

Note: push/pop may be used for switching objectives

Returns:

Objective handle, to be used for retrieving the value.

minimize

int minimize(Formula objective)

Add minimization objective.

Note: push/pop may be used for switching objectives

Returns:

Objective handle, to be used for retrieving the value.

check

OptimizationProverEnvironment.OptStatus check()
                                       throws InterruptedException,
                                              SolverException

Optimize the objective function subject to the previously imposed constraints.

Returns:

Status of the optimization problem.

Throws:

InterruptedException

SolverException

upper

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

Parameters:

epsilon - Value to substitute for the epsilon.

Returns:

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

lower

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

Parameters:

epsilon - Value to substitute for the epsilon.

Returns:

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

getModel

Model getModel()
        throws SolverException

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.

Please note that the prover is allowed to use standard numbers for any real variable in the model after a sat-query returned OptimizationProverEnvironment.OptStatus.OPT. For integer formulas, we expect the optimal assignment.

Example 1: For the constraint 'x<10' with a real x, the upper bound of x is '10-epsilon' (epsilon can even be set to zero). The model can return the assignment x=9. To get an optimal assignment, query the solver with an additional constraint 'x == 10-epsilon'.

Example 2: For the constraint 'x<10' with an integer x, the upper bound of x is '9' (epsilon is irrelevant here and can be zero). The model returns the optimal assignment x=9.

Specified by:

getModel in interface BasicProverEnvironment<Void>

Throws:

SolverException