Public Member Functions | |
__init__ (self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None) | |
__del__ (self) | |
depth (self) | |
inconsistent (self) | |
prec (self) | |
precision (self) | |
size (self) | |
__len__ (self) | |
get (self, i) | |
__getitem__ (self, arg) | |
assert_exprs (self, *args) | |
append (self, *args) | |
insert (self, *args) | |
add (self, *args) | |
convert_model (self, model) | |
__repr__ (self) | |
sexpr (self) | |
dimacs (self, include_names=True) | |
translate (self, target) | |
__copy__ (self) | |
__deepcopy__ (self, memo={}) | |
simplify (self, *arguments, **keywords) | |
as_expr (self) | |
Public Member Functions inherited from Z3PPObject | |
use_pp (self) |
Data Fields | |
ctx = _get_ctx(ctx) | |
goal = goal |
Additional Inherited Members | |
Protected Member Functions inherited from Z3PPObject | |
_repr_html_ (self) |
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.
__init__ | ( | self, | |
models = True, | |||
unsat_cores = False, | |||
proofs = False, | |||
ctx = None, | |||
goal = None ) |
Definition at line 5645 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 5655 of file z3py.py.
__copy__ | ( | self | ) |
__deepcopy__ | ( | self, | |
memo = {} ) |
__getitem__ | ( | self, | |
arg ) |
Return a constraint in the goal `self`. >>> g = Goal() >>> x, y = Ints('x y') >>> g.add(x == 0, y > x) >>> g[0] x == 0 >>> g[1] y > x
Definition at line 5764 of file z3py.py.
__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 5738 of file z3py.py.
Referenced by AstVector.__getitem__(), and AstVector.__setitem__().
__repr__ | ( | self | ) |
add | ( | self, | |
* | args ) |
Add constraints. >>> x = Int('x') >>> g = Goal() >>> g.add(x > 0, x < 2) >>> g [x > 0, x < 2]
Definition at line 5816 of file z3py.py.
Referenced by Solver.__iadd__().
append | ( | self, | |
* | args ) |
Add constraints. >>> x = Int('x') >>> g = Goal() >>> g.append(x > 0, x < 2) >>> g [x > 0, x < 2]
Definition at line 5794 of file z3py.py.
as_expr | ( | self | ) |
Return goal `self` as a single Z3 expression. >>> x = Int('x') >>> g = Goal() >>> g.as_expr() True >>> g.add(x > 1) >>> g.as_expr() x > 1 >>> g.add(x < 10) >>> g.as_expr() And(x > 1, x < 10)
Definition at line 5916 of file z3py.py.
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 5779 of file z3py.py.
Referenced by add(), Solver.add(), append(), Solver.append(), insert(), and Solver.insert().
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 5827 of file z3py.py.
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 5659 of file z3py.py.
dimacs | ( | self, | |
include_names = True ) |
Return a textual representation of the goal in DIMACS format.
Definition at line 5863 of file z3py.py.
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 5751 of file z3py.py.
Referenced by __getitem__(), and as_expr().
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 5677 of file z3py.py.
insert | ( | self, | |
* | args ) |
Add constraints. >>> x = Int('x') >>> g = Goal() >>> g.insert(x > 0, x < 2) >>> g [x > 0, x < 2]
Definition at line 5805 of file z3py.py.
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 5695 of file z3py.py.
Referenced by precision().
precision | ( | self | ) |
sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the goal.
Definition at line 5859 of file z3py.py.
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 5896 of file z3py.py.
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 5725 of file z3py.py.
Referenced by __len__().
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 5867 of file z3py.py.
Referenced by AstVector.__copy__(), FuncInterp.__copy__(), __copy__(), ModelRef.__copy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), __deepcopy__(), and ModelRef.__deepcopy__().
ctx = _get_ctx(ctx) |
Definition at line 5649 of file z3py.py.
Referenced by AstMap.__contains__(), AstVector.__copy__(), FuncInterp.__copy__(), __copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), AstVector.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), __deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), AstVector.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), __del__(), ModelRef.__del__(), Solver.__del__(), Statistics.__del__(), AstMap.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__len__(), AstVector.__len__(), ModelRef.__len__(), Statistics.__len__(), AstMap.__repr__(), Statistics.__repr__(), AstMap.__setitem__(), AstVector.__setitem__(), FuncEntry.arg_value(), FuncInterp.arity(), as_expr(), Solver.assert_and_track(), assert_exprs(), Solver.assert_exprs(), Solver.check(), convert_model(), ModelRef.decls(), depth(), dimacs(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), get(), ModelRef.get_interp(), Statistics.get_key_value(), ModelRef.get_sort(), ModelRef.get_universe(), inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), Solver.pop(), prec(), ModelRef.project(), ModelRef.project_with_witness(), AstVector.push(), Solver.push(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), AstVector.sexpr(), sexpr(), ModelRef.sexpr(), size(), AstVector.translate(), translate(), ModelRef.translate(), and FuncEntry.value().
goal = goal |
Definition at line 5650 of file z3py.py.
Referenced by __del__(), assert_exprs(), convert_model(), depth(), dimacs(), get(), inconsistent(), prec(), sexpr(), size(), and translate().