OptimizeObjective Class Reference

Optimize. More...

Public Member Functions
	__init__ (self, opt, value, is_max)
	lower (self)
	upper (self)
	lower_values (self)
	upper_values (self)
	value (self)
	__str__ (self)

Protected Attributes
	_opt
	_value
	_is_max

Detailed Description

Optimize.

Definition at line 7883 of file z3py.py.

Constructor & Destructor Documentation

__init__()

__init__	(		self,
			opt,
			value,
			is_max
	)

Definition at line 7884 of file z3py.py.

    def __init__(self, opt, value, is_max):
        self._opt = opt
        self._value = value
        self._is_max = is_max
 

Member Function Documentation

__str__()

__str__

(

self

)

Definition at line 7911 of file z3py.py.

    def __str__(self):
        return "%s:%s" % (self._value, self._is_max)
 
 

lower()

lower

(

self

)

Definition at line 7889 of file z3py.py.

    def lower(self):
        opt = self._opt
        return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
 

Referenced by OptimizeObjective.value().

lower_values()

lower_values

(

self

)

Definition at line 7897 of file z3py.py.

    def lower_values(self):
        opt = self._opt
        return AstVector(Z3_optimize_get_lower_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
 

upper()

upper

(

self

)

Definition at line 7893 of file z3py.py.

    def upper(self):
        opt = self._opt
        return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
 

Referenced by OptimizeObjective.value().

upper_values()

upper_values

(

self

)

Definition at line 7901 of file z3py.py.

    def upper_values(self):
        opt = self._opt
        return AstVector(Z3_optimize_get_upper_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
 

value()

value

(

self

)

Definition at line 7905 of file z3py.py.

    def value(self):
        if self._is_max:
            return self.upper()
        else:
            return self.lower()
 

Referenced by FuncEntry.as_list().

Field Documentation

_is_max

_is_max

protected

Definition at line 7887 of file z3py.py.

Referenced by OptimizeObjective.__str__(), and OptimizeObjective.value().

_opt

_opt

protected

Definition at line 7885 of file z3py.py.

Referenced by OptimizeObjective.lower(), OptimizeObjective.lower_values(), OptimizeObjective.upper(), and OptimizeObjective.upper_values().

_value

_value

protected

Definition at line 7886 of file z3py.py.

Referenced by OptimizeObjective.__str__(), OptimizeObjective.lower(), OptimizeObjective.lower_values(), OptimizeObjective.upper(), and OptimizeObjective.upper_values().