|
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 7357 of file z3py.py.
◆ __init__()
def __init__ |
( |
|
self, |
|
|
|
ctx = None |
|
) |
| |
Definition at line 7360 of file z3py.py.
7360 def __init__(self, ctx=None):
7361 self.ctx = _get_ctx(ctx)
◆ __del__()
Definition at line 7368 of file z3py.py.
7369 if self.optimize
is not None and self.ctx.ref()
is not None:
◆ __deepcopy__()
def __deepcopy__ |
( |
|
self, |
|
|
|
memo = {} |
|
) |
| |
Definition at line 7365 of file z3py.py.
7365 def __deepcopy__(self, memo={}):
7366 return Optimize(self.optimize, self.ctx)
◆ __iadd__()
def __iadd__ |
( |
|
self, |
|
|
|
fml |
|
) |
| |
Definition at line 7402 of file z3py.py.
7402 def __iadd__(self, fml):
◆ __repr__()
Return a formatted string with all added rules and constraints.
Definition at line 7529 of file z3py.py.
7530 """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 7398 of file z3py.py.
7398 def add(self, *args):
7399 """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
7400 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 7435 of file z3py.py.
7435 def add_soft(self, arg, weight = "1", id = None):
7436 """Add soft constraint with optional weight and optional identifier.
7437 If no weight is supplied, then the penalty for violating the soft constraint
7439 Soft constraints are grouped by identifiers. Soft constraints that are
7440 added without identifiers are grouped by default.
7443 weight =
"%d" % weight
7444 elif isinstance(weight, float):
7445 weight =
"%f" % weight
7446 if not isinstance(weight, str):
7447 raise Z3Exception(
"weight should be a string or an integer")
7452 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 7406 of file z3py.py.
7406 def assert_and_track(self, a, p):
7407 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7409 If `p` is a string, it will be automatically converted into a Boolean constant.
7414 >>> s.assert_and_track(x > 0, 'p1')
7415 >>> s.assert_and_track(x != 1, 'p2')
7416 >>> s.assert_and_track(x < 0, p3)
7417 >>> print(s.check())
7419 >>> c = s.unsat_core()
7429 if isinstance(p, str):
7430 p =
Bool(p, self.ctx)
7431 _z3_assert(isinstance(a, BoolRef),
"Boolean expression expected")
7432 _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 7386 of file z3py.py.
7386 def assert_exprs(self, *args):
7387 """Assert constraints as background axioms for the optimize solver."""
7388 args = _get_args(args)
7391 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
Referenced by Optimize.add().
◆ assertions()
Return an AST vector containing all added constraints.
Definition at line 7521 of file z3py.py.
7521 def assertions(self):
7522 """Return an AST vector containing all added constraints."""
◆ check()
def check |
( |
|
self, |
|
|
* |
assumptions |
|
) |
| |
Check satisfiability while optimizing objective functions.
Definition at line 7470 of file z3py.py.
7470 def check(self, *assumptions):
7471 """Check satisfiability while optimizing objective functions."""
7472 assumptions = _get_args(assumptions)
7473 num = len(assumptions)
7474 _assumptions = (Ast * num)()
7475 for i
in range(num):
7476 _assumptions[i] = assumptions[i].as_ast()
7477 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 7513 of file z3py.py.
7513 def from_file(self, filename):
7514 """Parse assertions and objectives from a file"""
◆ from_string()
def from_string |
( |
|
self, |
|
|
|
s |
|
) |
| |
Parse assertions and objectives from a string
Definition at line 7517 of file z3py.py.
7517 def from_string(self, s):
7518 """Parse assertions and objectives from a string"""
◆ help()
Display a string describing all available options.
Definition at line 7378 of file z3py.py.
7379 """Display a string describing all available options."""
◆ lower()
Definition at line 7493 of file z3py.py.
7493 def lower(self, obj):
7494 if not isinstance(obj, OptimizeObjective):
7495 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
◆ lower_values()
def lower_values |
( |
|
self, |
|
|
|
obj |
|
) |
| |
Definition at line 7503 of file z3py.py.
7503 def lower_values(self, obj):
7504 if not isinstance(obj, OptimizeObjective):
7505 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7506 return obj.lower_values()
◆ maximize()
def maximize |
( |
|
self, |
|
|
|
arg |
|
) |
| |
Add objective function to maximize.
Definition at line 7454 of file z3py.py.
7454 def maximize(self, arg):
7455 """Add objective function to maximize."""
7456 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 7458 of file z3py.py.
7458 def minimize(self, arg):
7459 """Add objective function to minimize."""
7460 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 7483 of file z3py.py.
7484 """Return a model for the last check()."""
7488 raise Z3Exception(
"model is not available")
Referenced by FuncInterp.translate().
◆ objectives()
returns set of objective functions
Definition at line 7525 of file z3py.py.
7525 def objectives(self):
7526 """returns set of objective functions"""
◆ param_descrs()
Return the parameter description set.
Definition at line 7382 of file z3py.py.
7382 def param_descrs(self):
7383 """Return the parameter description set."""
◆ pop()
restore to previously created backtracking point
Definition at line 7466 of file z3py.py.
7467 """restore to previously created backtracking point"""
◆ push()
create a backtracking point for added rules, facts and assertions
Definition at line 7462 of file z3py.py.
7463 """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 7479 of file z3py.py.
7479 def reason_unknown(self):
7480 """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 7372 of file z3py.py.
7372 def set(self, *args, **keys):
7373 """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 7533 of file z3py.py.
7534 """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 7538 of file z3py.py.
7538 def statistics(self):
7539 """Return statistics for the last check`.
◆ unsat_core()
Definition at line 7490 of file z3py.py.
7490 def unsat_core(self):
◆ upper()
Definition at line 7498 of file z3py.py.
7498 def upper(self, obj):
7499 if not isinstance(obj, OptimizeObjective):
7500 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
◆ upper_values()
def upper_values |
( |
|
self, |
|
|
|
obj |
|
) |
| |
Definition at line 7508 of file z3py.py.
7508 def upper_values(self, obj):
7509 if not isinstance(obj, OptimizeObjective):
7510 raise Z3Exception(
"Expecting objective handle returned by maximize/minimize")
7511 return obj.upper_values()
◆ ctx
Definition at line 7361 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 7362 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.