Z3
 
Loading...
Searching...
No Matches
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 = opt
 
 _value = value
 
 _is_max = is_max
 

Detailed Description

Optimize.

Definition at line 7890 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
opt,
value,
is_max )

Definition at line 7891 of file z3py.py.

7891 def __init__(self, opt, value, is_max):
7892 self._opt = opt
7893 self._value = value
7894 self._is_max = is_max
7895

Member Function Documentation

◆ __str__()

__str__ ( self)

Definition at line 7918 of file z3py.py.

7918 def __str__(self):
7919 return "%s:%s" % (self._value, self._is_max)
7920
7921

◆ lower()

lower ( self)

Definition at line 7896 of file z3py.py.

7896 def lower(self):
7897 opt = self._opt
7898 return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7899
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.

◆ lower_values()

lower_values ( self)

Definition at line 7904 of file z3py.py.

7904 def lower_values(self):
7905 opt = self._opt
7906 return AstVector(Z3_optimize_get_lower_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7907
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 7900 of file z3py.py.

7900 def upper(self):
7901 opt = self._opt
7902 return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7903
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.

◆ upper_values()

upper_values ( self)

Definition at line 7908 of file z3py.py.

7908 def upper_values(self):
7909 opt = self._opt
7910 return AstVector(Z3_optimize_get_upper_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
7911
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 7912 of file z3py.py.

7912 def value(self):
7913 if self._is_max:
7914 return self.upper()
7915 else:
7916 return self.lower()
7917

Referenced by FuncEntry.as_list().

Field Documentation

◆ _is_max

_is_max = is_max
protected

Definition at line 7894 of file z3py.py.

◆ _opt

_opt = opt
protected

Definition at line 7892 of file z3py.py.

◆ _value

_value = value
protected

Definition at line 7893 of file z3py.py.