|
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 7414 of file z3py.py.
◆ __init__()
def __init__ |
( |
|
self, |
|
|
|
ctx = None |
|
) |
| |
Definition at line 7417 of file z3py.py.
7418 self.ctx = _get_ctx(ctx)
◆ __del__()
Definition at line 7425 of file z3py.py.
7426 if self.optimize
is not None and self.ctx.ref()
is not None:
◆ __deepcopy__()
def __deepcopy__ |
( |
|
self, |
|
|
|
memo = {} |
|
) |
| |
Definition at line 7422 of file z3py.py.
7422 def __deepcopy__(self, memo={}):
7423 return Optimize(self.optimize, self.ctx)
◆ __iadd__()
def __iadd__ |
( |
|
self, |
|
|
|
fml |
|
) |
| |
Definition at line 7459 of file z3py.py.
7459 def __iadd__(self, fml):
◆ __repr__()
Return a formatted string with all added rules and constraints.
Definition at line 7586 of file z3py.py.
7587 """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 7455 of file z3py.py.
7455 def add(self, *args):
7456 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7457 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 7492 of file z3py.py.
7492 def add_soft(self, arg, weight = "1", id = None):
7493 """Add soft constraint with optional weight and optional identifier.
7494 If no weight is supplied, then the penalty for violating the soft constraint
7496 Soft constraints are grouped by identifiers. Soft constraints that are
7497 added without identifiers are grouped by default.
7500 weight =
"%d" % weight
7501 elif isinstance(weight, float):
7502 weight =
"%f" % weight
7503 if not isinstance(weight, str):
7504 raise Z3Exception(
"weight should be a string or an integer")
7509 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 7463 of file z3py.py.
7463 def assert_and_track(self, a, p):
7464 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7466 If `p` is a string, it will be automatically converted into a Boolean constant.
7471 >>> s.assert_and_track(x > 0, 'p1')
7472 >>> s.assert_and_track(x != 1, 'p2')
7473 >>> s.assert_and_track(x < 0, p3)
7474 >>> print(s.check())
7476 >>> c = s.unsat_core()
7486 if isinstance(p, str):
7487 p =
Bool(p, self.ctx)
7488 _z3_assert(isinstance(a, BoolRef),
"Boolean expression expected")
7489 _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 7443 of file z3py.py.
7443 def assert_exprs(self, *args):
7444 """Assert constraints as background axioms for the optimize solver."""
7445 args = _get_args(args)
7448 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
Referenced by Optimize.add().
◆ assertions()
Return an AST vector containing all added constraints.
Definition at line 7578 of file z3py.py.
7578 def assertions(self):
7579 """Return an AST vector containing all added constraints."""
◆ check()
def check |
( |
|
self, |
|
|
* |
assumptions |
|
) |
| |
Check satisfiability while optimizing objective functions.
Definition at line 7527 of file z3py.py.
7527 def check(self, *assumptions):
7528 """Check satisfiability while optimizing objective functions."""
7529 assumptions = _get_args(assumptions)
7530 num = len(assumptions)
7531 _assumptions = (Ast * num)()
7532 for i
in range(num):
7533 _assumptions[i] = assumptions[i].as_ast()
7534 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 7570 of file z3py.py.
7570 def from_file(self, filename):
7571 """Parse assertions and objectives from a file"""
◆ from_string()
def from_string |
( |
|
self, |
|
|
|
s |
|
) |
| |
Parse assertions and objectives from a string
Definition at line 7574 of file z3py.py.
7574 def from_string(self, s):
7575 """Parse assertions and objectives from a string"""
◆ help()
Display a string describing all available options.
Definition at line 7435 of file z3py.py.
7436 """Display a string describing all available options."""
◆ lower()
Definition at line 7550 of file z3py.py.
7550 def lower(self, obj):
7551 if not isinstance(obj, OptimizeObjective):
7552 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
◆ lower_values()
def lower_values |
( |
|
self, |
|
|
|
obj |
|
) |
| |
Definition at line 7560 of file z3py.py.
7560 def lower_values(self, obj):
7561 if not isinstance(obj, OptimizeObjective):
7562 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7563 return obj.lower_values()
◆ maximize()
def maximize |
( |
|
self, |
|
|
|
arg |
|
) |
| |
Add objective function to maximize.
Definition at line 7511 of file z3py.py.
7511 def maximize(self, arg):
7512 """Add objective function to maximize."""
7513 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 7515 of file z3py.py.
7515 def minimize(self, arg):
7516 """Add objective function to minimize."""
7517 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 7540 of file z3py.py.
7541 """Return a model for the last check()."""
7545 raise Z3Exception(
"model is not available")
Referenced by FuncInterp.translate().
◆ objectives()
returns set of objective functions
Definition at line 7582 of file z3py.py.
7582 def objectives(self):
7583 """returns set of objective functions"""
◆ param_descrs()
Return the parameter description set.
Definition at line 7439 of file z3py.py.
7439 def param_descrs(self):
7440 """Return the parameter description set."""
◆ pop()
restore to previously created backtracking point
Definition at line 7523 of file z3py.py.
7524 """restore to previously created backtracking point"""
◆ push()
create a backtracking point for added rules, facts and assertions
Definition at line 7519 of file z3py.py.
7520 """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 7536 of file z3py.py.
7536 def reason_unknown(self):
7537 """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 7429 of file z3py.py.
7429 def set(self, *args, **keys):
7430 """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 7590 of file z3py.py.
7591 """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 7595 of file z3py.py.
7595 def statistics(self):
7596 """Return statistics for the last check`.
◆ unsat_core()
Definition at line 7547 of file z3py.py.
7547 def unsat_core(self):
◆ upper()
Definition at line 7555 of file z3py.py.
7555 def upper(self, obj):
7556 if not isinstance(obj, OptimizeObjective):
7557 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
◆ upper_values()
def upper_values |
( |
|
self, |
|
|
|
obj |
|
) |
| |
Definition at line 7565 of file z3py.py.
7565 def upper_values(self, obj):
7566 if not isinstance(obj, OptimizeObjective):
7567 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7568 return obj.upper_values()
◆ ctx
Definition at line 7418 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(), UserPropagateBase.conflict(), UserPropagateBase.ctx_ref(), 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 7419 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.
def __init__(self, s, ctx=None)
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 pop(self, num_scopes)
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.