Z3
 
Loading...
Searching...
No Matches
Public Member Functions | Protected Attributes
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 7815 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__init__ (   self,
  opt,
  value,
  is_max 
)

Definition at line 7816 of file z3py.py.

7816 def __init__(self, opt, value, is_max):
7817 self._opt = opt
7818 self._value = value
7819 self._is_max = is_max
7820

Member Function Documentation

◆ __str__()

__str__ (   self)

Definition at line 7843 of file z3py.py.

7843 def __str__(self):
7844 return "%s:%s" % (self._value, self._is_max)
7845
7846

◆ lower()

lower (   self)

Definition at line 7821 of file z3py.py.

7821 def lower(self):
7822 opt = self._opt
7823 return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7824
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective.

Referenced by OptimizeObjective.value().

◆ lower_values()

lower_values (   self)

Definition at line 7829 of file z3py.py.

7829 def lower_values(self):
7830 opt = self._opt
7831 return AstVector(Z3_optimize_get_lower_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7832
Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective. The returned vector ...

◆ upper()

upper (   self)

Definition at line 7825 of file z3py.py.

7825 def upper(self):
7826 opt = self._opt
7827 return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7828
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.

Referenced by OptimizeObjective.value().

◆ upper_values()

upper_values (   self)

Definition at line 7833 of file z3py.py.

7833 def upper_values(self):
7834 opt = self._opt
7835 return AstVector(Z3_optimize_get_upper_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7836
Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.

◆ value()

value (   self)

Definition at line 7837 of file z3py.py.

7837 def value(self):
7838 if self._is_max:
7839 return self.upper()
7840 else:
7841 return self.lower()
7842

Referenced by FuncEntry.as_list().

Field Documentation

◆ _is_max

_is_max
protected

Definition at line 7819 of file z3py.py.

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

◆ _opt

_opt
protected

◆ _value

_value
protected