Public Member Functions | |
def | __init__ (self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None) |
def | __del__ (self) |
def | depth (self) |
def | inconsistent (self) |
def | prec (self) |
def | precision (self) |
def | size (self) |
def | __len__ (self) |
def | get (self, i) |
def | __getitem__ (self, arg) |
def | assert_exprs (self, args) |
def | append (self, args) |
def | insert (self, args) |
def | add (self, args) |
def | __repr__ (self) |
def | sexpr (self) |
def | translate (self, target) |
def | simplify (self, arguments, keywords) |
def | as_expr (self) |
![]() | |
def | use_pp (self) |
Data Fields | |
ctx | |
goal | |
Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible). Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals. A goal has a solution if one of its subgoals has a solution. A goal is unsatisfiable if all subgoals are unsatisfiable.
def __init__ | ( | self, | |
models = True , |
|||
unsat_cores = False , |
|||
proofs = False , |
|||
ctx = None , |
|||
goal = None |
|||
) |
Definition at line 4727 of file z3py.py.
def __del__ | ( | self | ) |
def __getitem__ | ( | self, | |
arg | |||
) |
def __len__ | ( | self | ) |
Return the number of constraints in the goal `self`. >>> g = Goal() >>> len(g) 0 >>> x, y = Ints('x y') >>> g.add(x == 0, y > x) >>> len(g) 2
def __repr__ | ( | self | ) |
def add | ( | self, | |
args | |||
) |
Add constraints. >>> x = Int('x') >>> g = Goal() >>> g.add(x > 0, x < 2) >>> g [x > 0, x < 2]
Definition at line 4896 of file z3py.py.
Referenced by Fixedpoint.__iadd__(), and Optimize.__iadd__().
def append | ( | self, | |
args | |||
) |
Add constraints. >>> x = Int('x') >>> g = Goal() >>> g.append(x > 0, x < 2) >>> g [x > 0, x < 2]
def as_expr | ( | self | ) |
def assert_exprs | ( | self, | |
args | |||
) |
Assert constraints into the goal. >>> x = Int('x') >>> g = Goal() >>> g.assert_exprs(x > 0, x < 2) >>> g [x > 0, x < 2]
Definition at line 4859 of file z3py.py.
Referenced by Fixedpoint.add(), Optimize.add(), Fixedpoint.append(), and Fixedpoint.insert().
def depth | ( | self | ) |
Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`. >>> x, y = Ints('x y') >>> g = Goal() >>> g.add(x == 0, y >= x + 1) >>> g.depth() 0 >>> r = Then('simplify', 'solve-eqs')(g) >>> # r has 1 subgoal >>> len(r) 1 >>> r[0].depth() 2
def get | ( | self, | |
i | |||
) |
def inconsistent | ( | self | ) |
Return `True` if `self` contains the `False` constraints. >>> x, y = Ints('x y') >>> g = Goal() >>> g.inconsistent() False >>> g.add(x == 0, x == 1) >>> g [x == 0, x == 1] >>> g.inconsistent() False >>> g2 = Tactic('propagate-values')(g)[0] >>> g2.inconsistent() True
Definition at line 4757 of file z3py.py.
def insert | ( | self, | |
args | |||
) |
Add constraints. >>> x = Int('x') >>> g = Goal() >>> g.insert(x > 0, x < 2) >>> g [x > 0, x < 2]
def prec | ( | self | ) |
Return the precision (under-approximation, over-approximation, or precise) of the goal `self`. >>> g = Goal() >>> g.prec() == Z3_GOAL_PRECISE True >>> x, y = Ints('x y') >>> g.add(x == y + 1) >>> g.prec() == Z3_GOAL_PRECISE True >>> t = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10) >>> g2 = t(g)[0] >>> g2 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0] >>> g2.prec() == Z3_GOAL_PRECISE False >>> g2.prec() == Z3_GOAL_UNDER True
Definition at line 4775 of file z3py.py.
Referenced by Goal.precision().
def precision | ( | self | ) |
def sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the goal.
Definition at line 4910 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
def simplify | ( | self, | |
arguments, | |||
keywords | |||
) |
def size | ( | self | ) |
def translate | ( | self, | |
target | |||
) |
Copy goal `self` to context `target`. >>> x = Int('x') >>> g = Goal() >>> g.add(x > 10) >>> g [x > 10] >>> c2 = Context() >>> g2 = g.translate(c2) >>> g2 [x > 10] >>> g.ctx == main_ctx() True >>> g2.ctx == c2 True >>> g2.ctx == main_ctx() False
Definition at line 4914 of file z3py.py.
ctx |
Definition at line 4730 of file z3py.py.
Referenced by Probe.__call__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), ApplyResult.convert_model(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_num_levels(), Fixedpoint.get_rules(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Optimize.pop(), Fixedpoint.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), and Fixedpoint.update_rule().