Public Member Functions | |
__init__ (self, result, ctx) | |
__deepcopy__ (self, memo={}) | |
__del__ (self) | |
__len__ (self) | |
__getitem__ (self, idx) | |
__repr__ (self) | |
sexpr (self) | |
as_expr (self) | |
Public Member Functions inherited from Z3PPObject | |
use_pp (self) |
Data Fields | |
result = result | |
ctx = ctx |
Additional Inherited Members | |
Protected Member Functions inherited from Z3PPObject | |
_repr_html_ (self) |
An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters.
__init__ | ( | self, | |
result, | |||
ctx ) |
Definition at line 8269 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 8277 of file z3py.py.
__deepcopy__ | ( | self, | |
memo = {} ) |
__getitem__ | ( | self, | |
idx ) |
Return one of the subgoals stored in ApplyResult object `self`. >>> a, b = Ints('a b') >>> g = Goal() >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) >>> t = Tactic('split-clause') >>> r = t(g) >>> r[0] [a == 0, Or(b == 0, b == 1), a > b] >>> r[1] [a == 1, Or(b == 0, b == 1), a > b]
Definition at line 8300 of file z3py.py.
__len__ | ( | self | ) |
Return the number of subgoals in `self`. >>> a, b = Ints('a b') >>> g = Goal() >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) >>> t = Tactic('split-clause') >>> r = t(g) >>> len(r) 2 >>> t = Then(Tactic('split-clause'), Tactic('split-clause')) >>> len(t(g)) 4 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values')) >>> len(t(g)) 1
Definition at line 8281 of file z3py.py.
__repr__ | ( | self | ) |
as_expr | ( | self | ) |
Return a Z3 expression consisting of all subgoals. >>> x = Int('x') >>> g = Goal() >>> g.add(x > 1) >>> g.add(Or(x == 2, x == 3)) >>> r = Tactic('simplify')(g) >>> r [[Not(x <= 1), Or(x == 2, x == 3)]] >>> r.as_expr() And(Not(x <= 1), Or(x == 2, x == 3)) >>> r = Tactic('split-clause')(g) >>> r [[x > 1, x == 2], [x > 1, x == 3]] >>> r.as_expr() Or(And(x > 1, x == 2), And(x > 1, x == 3))
Definition at line 8324 of file z3py.py.
sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the set of subgoals in `self`.
Definition at line 8320 of file z3py.py.