Optimize.
More...
Optimize.
Definition at line 7890 of file z3py.py.
◆ __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
◆ __str__()
Definition at line 7918 of file z3py.py.
7918 def __str__(self):
7919 return "%s:%s" % (self._value, self._is_max)
7920
7921
◆ lower()
Definition at line 7896 of file z3py.py.
7896 def lower(self):
7897 opt = self._opt
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()
Definition at line 7904 of file z3py.py.
7904 def lower_values(self):
7905 opt = self._opt
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()
Definition at line 7900 of file z3py.py.
7900 def upper(self):
7901 opt = self._opt
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()
Definition at line 7908 of file z3py.py.
7908 def upper_values(self):
7909 opt = self._opt
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()
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().
◆ _is_max
◆ _opt
◆ _value