Public Member Functions | |
def | __init__ |
def | __deepcopy__ |
def | __del__ |
def | __len__ |
def | __getitem__ |
def | __repr__ |
def | sexpr |
def | as_expr |
![]() | |
def | use_pp |
Data Fields | |
result | |
ctx | |
An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters.
def __del__ | ( | self | ) |
def __deepcopy__ | ( | self, | |
memo = {} |
|||
) |
Definition at line 7526 of file z3py.py.
def __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 7552 of file z3py.py.
def __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 7533 of file z3py.py.
def __repr__ | ( | self | ) |
def 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 7577 of file z3py.py.
def sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the set of subgoals in `self`.
Definition at line 7572 of file z3py.py.
ctx |
Definition at line 7523 of file z3py.py.
Referenced by ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Tactic.apply(), ApplyResult.as_expr(), Tactic.param_descrs(), and Tactic.solver().
result |
Definition at line 7522 of file z3py.py.
Referenced by ApplyResult.__deepcopy__(), ApplyResult.__del__(), ApplyResult.__getitem__(), ApplyResult.__len__(), and ApplyResult.sexpr().