Public Member Functions | |
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 | 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) |
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 = {} |
|||
) |
def __iadd__ | ( | self, | |
fml | |||
) |
def __repr__ | ( | self | ) |
def add | ( | self, | |
args | |||
) |
Assert constraints as background axioms for the optimize solver. Alias for assert_expr.
Definition at line 7319 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 7327 of file z3py.py.
def assert_exprs | ( | self, | |
args | |||
) |
Assert constraints as background axioms for the optimize solver.
Definition at line 7307 of file z3py.py.
Referenced by Optimize.add().
def assertions | ( | self | ) |
def check | ( | self, | |
assumptions | |||
) |
def from_file | ( | self, | |
filename | |||
) |
Parse assertions and objectives from a file
Definition at line 7405 of file z3py.py.
def from_string | ( | self, | |
s | |||
) |
Parse assertions and objectives from a string
Definition at line 7412 of file z3py.py.
def help | ( | self | ) |
def lower | ( | self, | |
obj | |||
) |
def lower_values | ( | self, | |
obj | |||
) |
def maximize | ( | self, | |
arg | |||
) |
Add objective function to maximize.
Definition at line 7346 of file z3py.py.
def minimize | ( | self, | |
arg | |||
) |
Add objective function to minimize.
Definition at line 7350 of file z3py.py.
def model | ( | self | ) |
def objectives | ( | self | ) |
def param_descrs | ( | self | ) |
def pop | ( | self | ) |
def push | ( | self | ) |
def reason_unknown | ( | self | ) |
def set | ( | self, | |
args, | |||
keys | |||
) |
Set a configuration option. The method `help()` return a string containing all available options.
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 7431 of file z3py.py.
Referenced by Optimize.__repr__().
def statistics | ( | self | ) |
def unsat_core | ( | self | ) |
def upper | ( | self, | |
obj | |||
) |
def upper_values | ( | self, | |
obj | |||
) |
ctx |
Definition at line 7282 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_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 7283 of file z3py.py.
Referenced by Optimize.__deepcopy__(), Optimize.__del__(), Optimize.add_soft(), 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().