Public Member Functions | |
def | __init__ |
def | __del__ |
def | __len__ |
def | __getitem__ |
def | __repr__ |
def | sexpr |
def | convert_model |
def | as_expr |
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 __init__ | ( | self, | |
result, | |||
ctx | |||
) |
def __del__ | ( | self | ) |
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 6348 of file z3py.py.
06348 06349 def __getitem__(self, idx): 06350 """Return one of the subgoals stored in ApplyResult object `self`. 06351 06352 >>> a, b = Ints('a b') 06353 >>> g = Goal() 06354 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 06355 >>> t = Tactic('split-clause') 06356 >>> r = t(g) 06357 >>> r[0] 06358 [a == 0, Or(b == 0, b == 1), a > b] 06359 >>> r[1] 06360 [a == 1, Or(b == 0, b == 1), a > b] 06361 """ 06362 if idx >= len(self): 06363 raise IndexError 06364 return Goal(goal=Z3_apply_result_get_subgoal(self.ctx.ref(), self.result, idx), ctx=self.ctx)
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 6329 of file z3py.py.
06329 06330 def __len__(self): 06331 """Return the number of subgoals in `self`. 06332 06333 >>> a, b = Ints('a b') 06334 >>> g = Goal() 06335 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 06336 >>> t = Tactic('split-clause') 06337 >>> r = t(g) 06338 >>> len(r) 06339 2 06340 >>> t = Then(Tactic('split-clause'), Tactic('split-clause')) 06341 >>> len(t(g)) 06342 4 06343 >>> t = Then(Tactic('split-clause'), Tactic('split-clause'), Tactic('propagate-values')) 06344 >>> len(t(g)) 06345 1 06346 """ 06347 return int(Z3_apply_result_get_num_subgoals(self.ctx.ref(), self.result))
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 6403 of file z3py.py.
06403 06404 def as_expr(self): 06405 """Return a Z3 expression consisting of all subgoals. 06406 06407 >>> x = Int('x') 06408 >>> g = Goal() 06409 >>> g.add(x > 1) 06410 >>> g.add(Or(x == 2, x == 3)) 06411 >>> r = Tactic('simplify')(g) 06412 >>> r 06413 [[Not(x <= 1), Or(x == 2, x == 3)]] 06414 >>> r.as_expr() 06415 And(Not(x <= 1), Or(x == 2, x == 3)) 06416 >>> r = Tactic('split-clause')(g) 06417 >>> r 06418 [[x > 1, x == 2], [x > 1, x == 3]] 06419 >>> r.as_expr() 06420 Or(And(x > 1, x == 2), And(x > 1, x == 3)) 06421 """ 06422 sz = len(self) 06423 if sz == 0: 06424 return BoolVal(False, self.ctx) 06425 elif sz == 1: 06426 return self[0].as_expr() 06427 else: 06428 return Or([ self[i].as_expr() for i in range(len(self)) ])
def convert_model | ( | self, | |
model, | |||
idx = 0 |
|||
) |
Convert a model for a subgoal into a model for the original 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.convert_model(s.model(), 1) [b = 0, a = 1]
Definition at line 6372 of file z3py.py.
06372 06373 def convert_model(self, model, idx=0): 06374 """Convert a model for a subgoal into a model for the original goal. 06375 06376 >>> a, b = Ints('a b') 06377 >>> g = Goal() 06378 >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) 06379 >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs')) 06380 >>> r = t(g) 06381 >>> r[0] 06382 [Or(b == 0, b == 1), Not(0 <= b)] 06383 >>> r[1] 06384 [Or(b == 0, b == 1), Not(1 <= b)] 06385 >>> # Remark: the subgoal r[0] is unsatisfiable 06386 >>> # Creating a solver for solving the second subgoal 06387 >>> s = Solver() 06388 >>> s.add(r[1]) 06389 >>> s.check() 06390 sat 06391 >>> s.model() 06392 [b = 0] 06393 >>> # Model s.model() does not assign a value to `a` 06394 >>> # It is a model for subgoal `r[1]`, but not for goal `g` 06395 >>> # The method convert_model creates a model for `g` from a model for `r[1]`. 06396 >>> r.convert_model(s.model(), 1) 06397 [b = 0, a = 1] 06398 """ 06399 if __debug__: 06400 _z3_assert(idx < len(self), "index out of bounds") 06401 _z3_assert(isinstance(model, ModelRef), "Z3 Model expected") 06402 return ModelRef(Z3_apply_result_convert_model(self.ctx.ref(), self.result, idx, model.model), self.ctx)
def sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the set of subgoals in `self`.
Definition at line 6368 of file z3py.py.
06368 06369 def sexpr(self): 06370 """Return a textual representation of the s-expression representing the set of subgoals in `self`.""" 06371 return Z3_apply_result_to_string(self.ctx.ref(), self.result)
Definition at line 6321 of file z3py.py.
Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), ArrayRef.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), ApplyResult.as_expr(), QuantifierRef.body(), BoolSortRef.cast(), DatatypeSortRef.constructor(), ApplyResult.convert_model(), ExprRef.decl(), RatNumRef.denominator(), FuncDeclRef.domain(), ArraySortRef.domain(), SortRef.kind(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), RatNumRef.numerator(), Tactic.param_descrs(), QuantifierRef.pattern(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
Definition at line 6321 of file z3py.py.
Referenced by ApplyResult::__del__(), ApplyResult::__getitem__(), ApplyResult::__len__(), ApplyResult::convert_model(), and ApplyResult::sexpr().