|
def | __init__ (self, ctx=None) |
|
def | __deepcopy__ (self, memo={}) |
|
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 (self, arg, weight="1", id=None) |
|
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 | use_pp (self) |
|
Optimize API provides methods for solving using objective functions and weighted soft constraints
Definition at line 7380 of file z3py.py.
◆ __init__()
def __init__ |
( |
|
self, |
|
|
|
ctx = None |
|
) |
| |
Definition at line 7383 of file z3py.py.
7383 def __init__(self, ctx=None):
7384 self.ctx = _get_ctx(ctx)
◆ __del__()
Definition at line 7391 of file z3py.py.
7392 if self.optimize
is not None and self.ctx.ref()
is not None:
◆ __deepcopy__()
def __deepcopy__ |
( |
|
self, |
|
|
|
memo = {} |
|
) |
| |
Definition at line 7388 of file z3py.py.
7388 def __deepcopy__(self, memo={}):
7389 return Optimize(self.optimize, self.ctx)
◆ __iadd__()
def __iadd__ |
( |
|
self, |
|
|
|
fml |
|
) |
| |
Definition at line 7425 of file z3py.py.
7425 def __iadd__(self, fml):
◆ __repr__()
Return a formatted string with all added rules and constraints.
Definition at line 7552 of file z3py.py.
7553 """Return a formatted string with all added rules and constraints."""
◆ add()
Assert constraints as background axioms for the optimize solver. Alias for assert_expr.
Definition at line 7421 of file z3py.py.
7421 def add(self, *args):
7422 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7423 self.assert_exprs(*args)
Referenced by Optimize.__iadd__().
◆ add_soft()
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 7458 of file z3py.py.
7458 def add_soft(self, arg, weight = "1", id = None):
7459 """Add soft constraint with optional weight and optional identifier.
7460 If no weight is supplied, then the penalty for violating the soft constraint
7462 Soft constraints are grouped by identifiers. Soft constraints that are
7463 added without identifiers are grouped by default.
7466 weight =
"%d" % weight
7467 elif isinstance(weight, float):
7468 weight =
"%f" % weight
7469 if not isinstance(weight, str):
7470 raise Z3Exception(
"weight should be a string or an integer")
7475 return OptimizeObjective(self, v,
False)
◆ assert_and_track()
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 7429 of file z3py.py.
7429 def assert_and_track(self, a, p):
7430 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7432 If `p` is a string, it will be automatically converted into a Boolean constant.
7437 >>> s.assert_and_track(x > 0, 'p1')
7438 >>> s.assert_and_track(x != 1, 'p2')
7439 >>> s.assert_and_track(x < 0, p3)
7440 >>> print(s.check())
7442 >>> c = s.unsat_core()
7452 if isinstance(p, str):
7453 p =
Bool(p, self.ctx)
7454 _z3_assert(isinstance(a, BoolRef),
"Boolean expression expected")
7455 _z3_assert(isinstance(p, BoolRef)
and is_const(p),
"Boolean expression expected")
◆ assert_exprs()
def assert_exprs |
( |
|
self, |
|
|
* |
args |
|
) |
| |
Assert constraints as background axioms for the optimize solver.
Definition at line 7409 of file z3py.py.
7409 def assert_exprs(self, *args):
7410 """Assert constraints as background axioms for the optimize solver."""
7411 args = _get_args(args)
7414 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
Referenced by Optimize.add().
◆ assertions()
Return an AST vector containing all added constraints.
Definition at line 7544 of file z3py.py.
7544 def assertions(self):
7545 """Return an AST vector containing all added constraints."""
◆ check()
def check |
( |
|
self, |
|
|
* |
assumptions |
|
) |
| |
Check satisfiability while optimizing objective functions.
Definition at line 7493 of file z3py.py.
7493 def check(self, *assumptions):
7494 """Check satisfiability while optimizing objective functions."""
7495 assumptions = _get_args(assumptions)
7496 num = len(assumptions)
7497 _assumptions = (Ast * num)()
7498 for i
in range(num):
7499 _assumptions[i] = assumptions[i].as_ast()
7500 return CheckSatResult(
Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
◆ from_file()
def from_file |
( |
|
self, |
|
|
|
filename |
|
) |
| |
Parse assertions and objectives from a file
Definition at line 7536 of file z3py.py.
7536 def from_file(self, filename):
7537 """Parse assertions and objectives from a file"""
◆ from_string()
def from_string |
( |
|
self, |
|
|
|
s |
|
) |
| |
Parse assertions and objectives from a string
Definition at line 7540 of file z3py.py.
7540 def from_string(self, s):
7541 """Parse assertions and objectives from a string"""
◆ help()
Display a string describing all available options.
Definition at line 7401 of file z3py.py.
7402 """Display a string describing all available options."""
◆ lower()
Definition at line 7516 of file z3py.py.
7516 def lower(self, obj):
7517 if not isinstance(obj, OptimizeObjective):
7518 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
◆ lower_values()
def lower_values |
( |
|
self, |
|
|
|
obj |
|
) |
| |
Definition at line 7526 of file z3py.py.
7526 def lower_values(self, obj):
7527 if not isinstance(obj, OptimizeObjective):
7528 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7529 return obj.lower_values()
◆ maximize()
def maximize |
( |
|
self, |
|
|
|
arg |
|
) |
| |
Add objective function to maximize.
Definition at line 7477 of file z3py.py.
7477 def maximize(self, arg):
7478 """Add objective function to maximize."""
7479 return OptimizeObjective(self,
Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
True)
◆ minimize()
def minimize |
( |
|
self, |
|
|
|
arg |
|
) |
| |
Add objective function to minimize.
Definition at line 7481 of file z3py.py.
7481 def minimize(self, arg):
7482 """Add objective function to minimize."""
7483 return OptimizeObjective(self,
Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
False)
◆ model()
Return a model for the last check().
Definition at line 7506 of file z3py.py.
7507 """Return a model for the last check()."""
7511 raise Z3Exception(
"model is not available")
Referenced by FuncInterp.translate().
◆ objectives()
returns set of objective functions
Definition at line 7548 of file z3py.py.
7548 def objectives(self):
7549 """returns set of objective functions"""
◆ param_descrs()
Return the parameter description set.
Definition at line 7405 of file z3py.py.
7405 def param_descrs(self):
7406 """Return the parameter description set."""
◆ pop()
restore to previously created backtracking point
Definition at line 7489 of file z3py.py.
7490 """restore to previously created backtracking point"""
◆ push()
create a backtracking point for added rules, facts and assertions
Definition at line 7485 of file z3py.py.
7486 """create a backtracking point for added rules, facts and assertions"""
◆ reason_unknown()
def reason_unknown |
( |
|
self | ) |
|
Return a string that describes why the last `check()` returned `unknown`.
Definition at line 7502 of file z3py.py.
7502 def reason_unknown(self):
7503 """Return a string that describes why the last `check()` returned `unknown`."""
◆ set()
def set |
( |
|
self, |
|
|
* |
args, |
|
|
** |
keys |
|
) |
| |
Set a configuration option. The method `help()` return a string containing all available options.
Definition at line 7395 of file z3py.py.
7395 def set(self, *args, **keys):
7396 """Set a configuration option. The method `help()` return a string containing all available options.
◆ sexpr()
Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
Definition at line 7556 of file z3py.py.
7557 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
Referenced by Optimize.__repr__().
◆ statistics()
Return statistics for the last check`.
Definition at line 7561 of file z3py.py.
7561 def statistics(self):
7562 """Return statistics for the last check`.
◆ unsat_core()
Definition at line 7513 of file z3py.py.
7513 def unsat_core(self):
◆ upper()
Definition at line 7521 of file z3py.py.
7521 def upper(self, obj):
7522 if not isinstance(obj, OptimizeObjective):
7523 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
◆ upper_values()
def upper_values |
( |
|
self, |
|
|
|
obj |
|
) |
| |
Definition at line 7531 of file z3py.py.
7531 def upper_values(self, obj):
7532 if not isinstance(obj, OptimizeObjective):
7533 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7534 return obj.upper_values()
◆ ctx
Definition at line 7384 of file z3py.py.
Referenced by Probe.__call__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), Optimize.from_file(), Optimize.from_string(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Optimize.param_descrs(), Tactic.param_descrs(), Optimize.pop(), Optimize.push(), Optimize.reason_unknown(), Optimize.set(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Optimize.statistics(), and Optimize.unsat_core().
◆ optimize
Definition at line 7385 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.sexpr(), Optimize.statistics(), and Optimize.unsat_core().
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
Assert tracked hard constraint to the optimization context.
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d)
Retrieve a string that describes the last status returned by Z3_optimize_check.
expr range(expr const &lo, expr const &hi)
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives....
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)
Return objectives on the optimization context. If the objective function is a max-sat objective it is...
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)
Return the set of asserted formulas on the optimization context.
Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o)
Return the parameter description set for the given optimize object.
def to_symbol(s, ctx=None)
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives....
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)
Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
def args2params(arguments, keywords, ctx=None)
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.