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) | |
![]() | |
use_pp (self) | |
Data Fields | |
ctx = _get_ctx(ctx) | |
goal = goal | |
Additional Inherited Members | |
![]() | |
_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 5601 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 5611 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 5720 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 5694 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 5772 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 5750 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 5872 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 5735 of file z3py.py.
Referenced by Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.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 5783 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 5615 of file z3py.py.
dimacs | ( | self, | |
include_names = True ) |
Return a textual representation of the goal in DIMACS format.
Definition at line 5819 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 5707 of file z3py.py.
Referenced by Goal.__getitem__(), and Goal.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 5633 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 5761 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 5651 of file z3py.py.
Referenced by Goal.precision().
precision | ( | self | ) |
sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the goal.
Definition at line 5815 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 5852 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 5681 of file z3py.py.
Referenced by Goal.__len__(), ParamDescrsRef.__len__(), BitVecNumRef.as_signed_long(), and BitVecSortRef.subsort().
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 5823 of file z3py.py.
Referenced by AstRef.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__copy__(), ModelRef.__copy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), Goal.__deepcopy__(), and ModelRef.__deepcopy__().
ctx = _get_ctx(ctx) |
Definition at line 5605 of file z3py.py.
Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), Goal.__copy__(), ModelRef.__copy__(), AstMap.__deepcopy__(), AstRef.__deepcopy__(), AstVector.__deepcopy__(), Datatype.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), Goal.__deepcopy__(), ModelRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), ParamsRef.__deepcopy__(), Statistics.__deepcopy__(), AstMap.__del__(), AstRef.__del__(), AstVector.__del__(), Context.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), Goal.__del__(), ModelRef.__del__(), ParamDescrsRef.__del__(), ParamsRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), Solver.__del__(), Statistics.__del__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstMap.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstMap.__len__(), AstVector.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), BoolRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), AstMap.__repr__(), ParamDescrsRef.__repr__(), ParamsRef.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstMap.__setitem__(), AstVector.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), AstVector.push(), Solver.push(), QuantifierRef.qid(), ArraySortRef.range(), FuncDeclRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), ParamsRef.set(), Solver.set(), AstVector.sexpr(), Goal.sexpr(), ModelRef.sexpr(), Goal.size(), ParamDescrsRef.size(), QuantifierRef.skolem_id(), AstRef.translate(), AstVector.translate(), Goal.translate(), ModelRef.translate(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
goal = goal |
Definition at line 5606 of file z3py.py.
Referenced by 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().