Public Member Functions | |
__init__ (self, optimize=None, ctx=None) | |
__deepcopy__ (self, memo={}) | |
__del__ (self) | |
set (self, *args, **keys) | |
help (self) | |
param_descrs (self) | |
assert_exprs (self, *args) | |
add (self, *args) | |
__iadd__ (self, fml) | |
assert_and_track (self, a, p) | |
add_soft (self, arg, weight="1", id=None) | |
set_initial_value (self, var, value) | |
maximize (self, arg) | |
minimize (self, arg) | |
push (self) | |
pop (self) | |
check (self, *assumptions) | |
reason_unknown (self) | |
model (self) | |
unsat_core (self) | |
lower (self, obj) | |
upper (self, obj) | |
lower_values (self, obj) | |
upper_values (self, obj) | |
from_file (self, filename) | |
from_string (self, s) | |
assertions (self) | |
objectives (self) | |
__repr__ (self) | |
sexpr (self) | |
statistics (self) | |
set_on_model (self, on_model) | |
![]() | |
use_pp (self) | |
Data Fields | |
ctx = _get_ctx(ctx) | |
optimize = Z3_mk_optimize(self.ctx.ref()) | |
Protected Attributes | |
_on_models_id = None | |
Additional Inherited Members | |
![]() | |
_repr_html_ (self) | |
Optimize API provides methods for solving using objective functions and weighted soft constraints
__init__ | ( | self, | |
optimize = None, | |||
ctx = None ) |
Definition at line 7936 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 7948 of file z3py.py.
__deepcopy__ | ( | self, | |
memo = {} ) |
__iadd__ | ( | self, | |
fml ) |
__repr__ | ( | self | ) |
add | ( | self, | |
* | args ) |
Assert constraints as background axioms for the optimize solver. Alias for assert_expr.
Definition at line 7981 of file z3py.py.
Referenced by Solver.__iadd__().
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 8018 of file z3py.py.
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 7989 of file z3py.py.
assert_exprs | ( | self, | |
* | args ) |
Assert constraints as background axioms for the optimize solver.
Definition at line 7969 of file z3py.py.
Referenced by Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.insert(), and Solver.insert().
assertions | ( | self | ) |
Return an AST vector containing all added constraints.
Definition at line 8124 of file z3py.py.
check | ( | self, | |
* | assumptions ) |
Check consistency and produce optimal values.
Definition at line 8073 of file z3py.py.
from_file | ( | self, | |
filename ) |
Parse assertions and objectives from a file
Definition at line 8116 of file z3py.py.
from_string | ( | self, | |
s ) |
Parse assertions and objectives from a string
Definition at line 8120 of file z3py.py.
help | ( | self | ) |
Display a string describing all available options.
Definition at line 7961 of file z3py.py.
lower | ( | self, | |
obj ) |
lower_values | ( | self, | |
obj ) |
maximize | ( | self, | |
arg ) |
Add objective function to maximize.
Definition at line 8049 of file z3py.py.
minimize | ( | self, | |
arg ) |
Add objective function to minimize.
Definition at line 8057 of file z3py.py.
model | ( | self | ) |
Return a model for the last check().
Definition at line 8086 of file z3py.py.
Referenced by ModelRef.__del__(), ModelRef.__getitem__(), ModelRef.__len__(), ModelRef.decls(), ModelRef.eval(), ModelRef.get_interp(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), ModelRef.sexpr(), ModelRef.translate(), and ModelRef.update_value().
objectives | ( | self | ) |
returns set of objective functions
Definition at line 8128 of file z3py.py.
param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 7965 of file z3py.py.
pop | ( | self | ) |
restore to previously created backtracking point
Definition at line 8069 of file z3py.py.
Referenced by Solver.__exit__().
push | ( | self | ) |
create a backtracking point for added rules, facts and assertions
Definition at line 8065 of file z3py.py.
Referenced by Solver.__enter__().
reason_unknown | ( | self | ) |
Return a string that describes why the last `check()` returned `unknown`.
Definition at line 8082 of file z3py.py.
set | ( | self, | |
* | args, | ||
** | keys ) |
Set a configuration option. The method `help()` return a string containing all available options.
Definition at line 7954 of file z3py.py.
set_initial_value | ( | self, | |
var, | |||
value ) |
initialize the solver's state by setting the initial value of var to value
Definition at line 8042 of file z3py.py.
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 8147 of file z3py.py.
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 8136 of file z3py.py.
statistics | ( | self | ) |
Return statistics for the last check`.
Definition at line 8142 of file z3py.py.
unsat_core | ( | self | ) |
upper | ( | self, | |
obj ) |
upper_values | ( | self, | |
obj ) |
ctx = _get_ctx(ctx) |
Definition at line 7937 of file z3py.py.
Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), AstRef.__deepcopy__(), AstVector.__deepcopy__(), Datatype.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), Goal.__deepcopy__(), ModelRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), ParamsRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), AstRef.__del__(), AstVector.__del__(), Context.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), Goal.__del__(), ModelRef.__del__(), ParamDescrsRef.__del__(), ParamsRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), Solver.__del__(), Statistics.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstMap.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstMap.__len__(), AstVector.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), BoolRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), AstMap.__repr__(), ParamDescrsRef.__repr__(), ParamsRef.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstMap.__setitem__(), AstVector.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), AstVector.push(), Solver.push(), QuantifierRef.qid(), ArraySortRef.range(), FuncDeclRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), ParamsRef.set(), Solver.set(), AstVector.sexpr(), Goal.sexpr(), ModelRef.sexpr(), Goal.size(), ParamDescrsRef.size(), QuantifierRef.skolem_id(), AstRef.translate(), AstVector.translate(), Goal.translate(), ModelRef.translate(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
optimize = Z3_mk_optimize(self.ctx.ref()) |