Optimize.
More...
Optimize.
Definition at line 8534 of file z3py.py.
◆ __init__()
| __init__ |
( |
|
self, |
|
|
|
opt, |
|
|
|
value, |
|
|
|
is_max |
|
) |
| |
Definition at line 8535 of file z3py.py.
8535 def __init__(self, opt, value, is_max):
8536 self._opt = opt
8537 self._value = value
8538 self._is_max = is_max
8539
◆ __str__()
Definition at line 8562 of file z3py.py.
8562 def __str__(self):
8563 return "%s:%s" % (self._value, self._is_max)
8564
8565
◆ lower()
Definition at line 8540 of file z3py.py.
8540 def lower(self):
8541 opt = self._opt
8543
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 8548 of file z3py.py.
8548 def lower_values(self):
8549 opt = self._opt
8551
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 8544 of file z3py.py.
8544 def upper(self):
8545 opt = self._opt
8547
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 8552 of file z3py.py.
8552 def upper_values(self):
8553 opt = self._opt
8555
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 8556 of file z3py.py.
8556 def value(self):
8557 if self._is_max:
8558 return self.upper()
8559 else:
8560 return self.lower()
8561
Referenced by FuncEntry.as_list().
◆ _is_max
◆ _opt
◆ _value