Package com.microsoft.z3

Class Optimize.Handle<R extends Sort>

java.lang.Object

com.microsoft.z3.Optimize.Handle<R>

Enclosing class:

Optimize

public static class Optimize.Handle<R extends Sort>
extends Object

Handle to objectives returned by objective functions.

Method Summary

Modifier and Type	Method	Description
Expr<R>	getLower()	Retrieve a lower bound for the objective handle.
Expr<?>[]	getLowerAsVector()
Expr<R>	getUpper()	Retrieve an upper bound for the objective handle.
Expr<?>[]	getUpperAsVector()
Expr<R>	getValue()	Retrieve the value of an objective.
String	toString()	Print a string representation of the handle.

Methods inherited from class java.lang.Object

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

Method Details

getLower

public Expr<R> getLower()

Retrieve a lower bound for the objective handle.

getUpper

public Expr<R> getUpper()

Retrieve an upper bound for the objective handle.

getUpperAsVector

public Expr<?>[] getUpperAsVector()

Returns:

a triple representing the upper bound of the objective handle. The triple contains values inf, value, eps, where the objective value is unbounded iff inf is non-zero, and otherwise is represented by the expression value + eps * EPSILON, where EPSILON is an arbitrarily small real number.

getLowerAsVector

public Expr<?>[] getLowerAsVector()

Returns:

a triple representing the upper bound of the objective handle.

See getUpperAsVector() for triple semantics.

getValue

public Expr<R> getValue()

Retrieve the value of an objective.

toString

public String toString()

Print a string representation of the handle.

Overrides:

toString in class Object