|
Z3
|
|
|
Z3
|
|
Inheritance diagram for Optimize:Public Member Functions | |
| def | __init__ |
| def | __deepcopy__ |
| def | __del__ (self) |
| def | set (self, args, keys) |
| def | help (self) |
| def | param_descrs (self) |
| def | assert_exprs (self, args) |
| def | add (self, args) |
| def | __iadd__ (self, fml) |
| def | assert_and_track (self, a, p) |
| def | add_soft |
| def | maximize (self, arg) |
| def | minimize (self, arg) |
| def | push (self) |
| def | pop (self) |
| def | check (self, assumptions) |
| def | reason_unknown (self) |
| def | model (self) |
| def | unsat_core (self) |
| def | lower (self, obj) |
| def | upper (self, obj) |
| def | lower_values (self, obj) |
| def | upper_values (self, obj) |
| def | from_file (self, filename) |
| def | from_string (self, s) |
| def | assertions (self) |
| def | objectives (self) |
| def | __repr__ (self) |
| def | sexpr (self) |
| def | statistics (self) |
| def | set_on_model (self, on_model) |
| Public Member Functions inherited from Z3PPObject | |
| def | use_pp (self) |
Data Fields | |
| ctx | |
| optimize | |
Optimize API provides methods for solving using objective functions and weighted soft constraints
| def __init__ | ( | self, | |
ctx = None |
|||
| ) |
| def __del__ | ( | self | ) |
| def __deepcopy__ | ( | self, | |
memo = {} |
|||
| ) |
Definition at line 7760 of file z3py.py.
| def __repr__ | ( | self | ) |
| def add | ( | self, | |
| args | |||
| ) |
Assert constraints as background axioms for the optimize solver. Alias for assert_expr.
Definition at line 7796 of file z3py.py.
Referenced by Optimize.__iadd__().
| def add_soft | ( | self, | |
| arg, | |||
weight = "1", |
|||
id = None |
|||
| ) |
Add soft constraint with optional weight and optional identifier. If no weight is supplied, then the penalty for violating the soft constraint is 1. Soft constraints are grouped by identifiers. Soft constraints that are added without identifiers are grouped by default.
Definition at line 7833 of file z3py.py.
| def assert_and_track | ( | self, | |
| a, | |||
| p | |||
| ) |
Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
If `p` is a string, it will be automatically converted into a Boolean constant.
>>> x = Int('x')
>>> p3 = Bool('p3')
>>> s = Optimize()
>>> s.assert_and_track(x > 0, 'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0, p3)
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True
Definition at line 7804 of file z3py.py.
| def assert_exprs | ( | self, | |
| args | |||
| ) |
Assert constraints as background axioms for the optimize solver.
Definition at line 7784 of file z3py.py.
Referenced by Optimize.add().
| def assertions | ( | self | ) |
Return an AST vector containing all added constraints.
Definition at line 7932 of file z3py.py.
| def check | ( | self, | |
| assumptions | |||
| ) |
Check satisfiability while optimizing objective functions.
Definition at line 7881 of file z3py.py.
| def from_file | ( | self, | |
| filename | |||
| ) |
Parse assertions and objectives from a file
Definition at line 7924 of file z3py.py.
| def from_string | ( | self, | |
| s | |||
| ) |
Parse assertions and objectives from a string
Definition at line 7928 of file z3py.py.
| def help | ( | self | ) |
| def maximize | ( | self, | |
| arg | |||
| ) |
| def minimize | ( | self, | |
| arg | |||
| ) |
| def model | ( | self | ) |
Return a model for the last check().
Definition at line 7894 of file z3py.py.
Referenced by FuncInterp.translate().
| def objectives | ( | self | ) |
returns set of objective functions
Definition at line 7936 of file z3py.py.
| def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 7780 of file z3py.py.
| def pop | ( | self | ) |
| def push | ( | self | ) |
| def reason_unknown | ( | self | ) |
| def set | ( | self, | |
| args, | |||
| keys | |||
| ) |
| def set_on_model | ( | self, | |
| on_model | |||
| ) |
Register a callback that is invoked with every incremental improvement to objective values. The callback takes a model as argument. The life-time of the model is limited to the callback so the model has to be (deep) copied if it is to be used after the callback
Definition at line 7955 of file z3py.py.
| def sexpr | ( | self | ) |
Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
Definition at line 7944 of file z3py.py.
Referenced by Optimize.__repr__().
| def statistics | ( | self | ) |
| def unsat_core | ( | self | ) |
Definition at line 7901 of file z3py.py.
| ctx |
Definition at line 7755 of file z3py.py.
Referenced by Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.model(), Optimize.objectives(), Optimize.param_descrs(), Tactic.param_descrs(), Optimize.set(), Optimize.set_on_model(), Tactic.solver(), Optimize.statistics(), and Optimize.unsat_core().
| optimize |
Definition at line 7756 of file z3py.py.
Referenced by Optimize.__deepcopy__(), Optimize.__del__(), Optimize.add_soft(), Optimize.assert_and_track(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), Optimize.from_file(), Optimize.from_string(), Optimize.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Optimize.param_descrs(), Optimize.pop(), Optimize.push(), Optimize.reason_unknown(), Optimize.set(), Optimize.set_on_model(), Optimize.sexpr(), Optimize.statistics(), and Optimize.unsat_core().
1.8.10