Public Member Functions | |
def | __init__ |
def | __deepcopy__ |
def | __del__ |
def | depth |
def | inconsistent |
def | prec |
def | precision |
def | size |
def | __len__ |
def | get |
def | __getitem__ |
def | assert_exprs |
def | append |
def | insert |
def | add |
def | convert_model |
def | __repr__ |
def | sexpr |
def | dimacs |
def | translate |
def | __copy__ |
def | __deepcopy__ |
def | simplify |
def | as_expr |
![]() | |
def | use_pp |
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 5136 of file z3py.py.
def __del__ | ( | self | ) |
def __copy__ | ( | self | ) |
def __deepcopy__ | ( | self, | |
memo = {} |
|||
) |
def __deepcopy__ | ( | self, | |
memo = {} |
|||
) |
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
Definition at line 5230 of file z3py.py.
Referenced by AstVector.__getitem__(), and AstVector.__setitem__().
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 5308 of file z3py.py.
Referenced by Fixedpoint.__iadd__(), and Optimize.__iadd__().
def append | ( | self, | |
args | |||
) |
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 5271 of file z3py.py.
Referenced by Goal.add(), Fixedpoint.add(), Optimize.add(), Goal.append(), Fixedpoint.append(), and Fixedpoint.insert().
def convert_model | ( | self, | |
model | |||
) |
Retrieve model from a satisfiable goal >>> a, b = Ints('a b') >>> g = Goal() >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs')) >>> r = t(g) >>> r[0] [Or(b == 0, b == 1), Not(0 <= b)] >>> r[1] [Or(b == 0, b == 1), Not(1 <= b)] >>> # Remark: the subgoal r[0] is unsatisfiable >>> # Creating a solver for solving the second subgoal >>> s = Solver() >>> s.add(r[1]) >>> s.check() sat >>> s.model() [b = 0] >>> # Model s.model() does not assign a value to `a` >>> # It is a model for subgoal `r[1]`, but not for goal `g` >>> # The method convert_model creates a model for `g` from a model for `r[1]`. >>> r[1].convert_model(s.model()) [b = 0, a = 1]
Definition at line 5319 of file z3py.py.
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
Definition at line 5152 of file z3py.py.
def dimacs | ( | self | ) |
def get | ( | self, | |
i | |||
) |
Return a constraint in the goal `self`. >>> g = Goal() >>> x, y = Ints('x y') >>> g.add(x == 0, y > x) >>> g.get(0) x == 0 >>> g.get(1) y > x
Definition at line 5243 of file z3py.py.
Referenced by Goal.__getitem__(), and Goal.as_expr().
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 5169 of file z3py.py.
def insert | ( | self, | |
args | |||
) |
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 5187 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 5351 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
def simplify | ( | self, | |
arguments, | |||
keywords | |||
) |
Return a new simplified goal. This method is essentially invoking the simplify tactic. >>> g = Goal() >>> x = Int('x') >>> g.add(x + 1 >= 2) >>> g [x + 1 >= 2] >>> g2 = g.simplify() >>> g2 [x >= 1] >>> # g was not modified >>> g [x + 1 >= 2]
Definition at line 5388 of file z3py.py.
def size | ( | self | ) |
Return the number of constraints in the goal `self`. >>> g = Goal() >>> g.size() 0 >>> x, y = Ints('x y') >>> g.add(x == 0, y > x) >>> g.size() 2
Definition at line 5217 of file z3py.py.
Referenced by Goal.__len__().
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 5359 of file z3py.py.
Referenced by Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), and FuncInterp.__deepcopy__().
ctx |
Definition at line 5139 of file z3py.py.
Referenced by Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), AstVector.__getitem__(), AstMap.__getitem__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), FuncEntry.arg_value(), Goal.as_expr(), ApplyResult.as_expr(), Optimize.assert_and_track(), Goal.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Goal.convert_model(), FuncInterp.else_value(), FuncInterp.entry(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), AstMap.keys(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Optimize.unsat_core(), Fixedpoint.update_rule(), and FuncEntry.value().
goal |
Definition at line 5140 of file z3py.py.
Referenced by Goal.__deepcopy__(), Goal.__del__(), Goal.assert_exprs(), Goal.convert_model(), Goal.depth(), Goal.dimacs(), Goal.get(), Goal.inconsistent(), Goal.prec(), Goal.sexpr(), Goal.size(), and Goal.translate().