Public Member Functions | |
def | __init__ |
def | __del__ |
def | __repr__ |
def | sexpr |
def | eval |
def | evaluate |
def | __len__ |
def | get_interp |
def | num_sorts |
def | get_sort |
def | sorts |
def | get_universe |
def | __getitem__ |
def | decls |
Data Fields | |
model | |
ctx |
Model/Solution of a satisfiability problem (aka system of constraints).
def __init__ | ( | self, | |
m, | |||
ctx | |||
) |
def __del__ | ( | self | ) |
def __getitem__ | ( | self, | |
idx | |||
) |
If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpreation is returned. The elements can be retrieved using position or the actual declaration. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0, x < 2, f(x) == 0) >>> s.check() sat >>> m = s.model() >>> len(m) 2 >>> m[0] x >>> m[1] f >>> m[x] 1 >>> m[f] [1 -> 0, else -> 0] >>> for d in m: print("%s -> %s" % (d, m[d])) x -> 1 f -> [1 -> 0, else -> 0]
Definition at line 5466 of file z3py.py.
05466 05467 def __getitem__(self, idx): 05468 """If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpreation is returned. 05469 05470 The elements can be retrieved using position or the actual declaration. 05471 05472 >>> f = Function('f', IntSort(), IntSort()) 05473 >>> x = Int('x') 05474 >>> s = Solver() 05475 >>> s.add(x > 0, x < 2, f(x) == 0) 05476 >>> s.check() 05477 sat 05478 >>> m = s.model() 05479 >>> len(m) 05480 2 05481 >>> m[0] 05482 x 05483 >>> m[1] 05484 f 05485 >>> m[x] 05486 1 05487 >>> m[f] 05488 [1 -> 0, else -> 0] 05489 >>> for d in m: print("%s -> %s" % (d, m[d])) 05490 x -> 1 05491 f -> [1 -> 0, else -> 0] 05492 """ 05493 if isinstance(idx, int): 05494 if idx >= len(self): 05495 raise IndexError 05496 num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model) 05497 if (idx < num_consts): 05498 return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx) 05499 else: 05500 return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx) 05501 if isinstance(idx, FuncDeclRef): 05502 return self.get_interp(idx) 05503 if is_const(idx): 05504 return self.get_interp(idx.decl()) 05505 if isinstance(idx, SortRef): 05506 return self.get_universe(idx) 05507 if __debug__: 05508 _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected") 05509 return None
def __len__ | ( | self | ) |
Return the number of constant and function declarations in the model `self`. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0, f(x) != x) >>> s.check() sat >>> m = s.model() >>> len(m) 2
Definition at line 5345 of file z3py.py.
05345 05346 def __len__(self): 05347 """Return the number of constant and function declarations in the model `self`. 05348 05349 >>> f = Function('f', IntSort(), IntSort()) 05350 >>> x = Int('x') 05351 >>> s = Solver() 05352 >>> s.add(x > 0, f(x) != x) 05353 >>> s.check() 05354 sat 05355 >>> m = s.model() 05356 >>> len(m) 05357 2 05358 """ 05359 return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model))
def __repr__ | ( | self | ) |
def decls | ( | self | ) |
Return a list with all symbols that have an interpreation in the model `self`. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0, x < 2, f(x) == 0) >>> s.check() sat >>> m = s.model() >>> m.decls() [x, f]
Definition at line 5510 of file z3py.py.
05510 05511 def decls(self): 05512 """Return a list with all symbols that have an interpreation in the model `self`. 05513 >>> f = Function('f', IntSort(), IntSort()) 05514 >>> x = Int('x') 05515 >>> s = Solver() 05516 >>> s.add(x > 0, x < 2, f(x) == 0) 05517 >>> s.check() 05518 sat 05519 >>> m = s.model() 05520 >>> m.decls() 05521 [x, f] 05522 """ 05523 r = [] 05524 for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)): 05525 r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx)) 05526 for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)): 05527 r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx)) 05528 return r
def eval | ( | self, | |
t, | |||
model_completion = False |
|||
) |
Evaluate the expression `t` in the model `self`. If `model_completion` is enabled, then a default interpretation is automatically added for symbols that do not have an interpretation in the model `self`. >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0, x < 2) >>> s.check() sat >>> m = s.model() >>> m.eval(x + 1) 2 >>> m.eval(x == 1) True >>> y = Int('y') >>> m.eval(y + x) 1 + y >>> m.eval(y) y >>> m.eval(y, model_completion=True) 0 >>> # Now, m contains an interpretation for y >>> m.eval(y + x) 1
Definition at line 5290 of file z3py.py.
05290 05291 def eval(self, t, model_completion=False): 05292 """Evaluate the expression `t` in the model `self`. If `model_completion` is enabled, then a default interpretation is automatically added for symbols that do not have an interpretation in the model `self`. 05293 05294 >>> x = Int('x') 05295 >>> s = Solver() 05296 >>> s.add(x > 0, x < 2) 05297 >>> s.check() 05298 sat 05299 >>> m = s.model() 05300 >>> m.eval(x + 1) 05301 2 05302 >>> m.eval(x == 1) 05303 True 05304 >>> y = Int('y') 05305 >>> m.eval(y + x) 05306 1 + y 05307 >>> m.eval(y) 05308 y 05309 >>> m.eval(y, model_completion=True) 05310 0 05311 >>> # Now, m contains an interpretation for y 05312 >>> m.eval(y + x) 05313 1 05314 """ 05315 r = (Ast * 1)() 05316 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r): 05317 return _to_expr_ref(r[0], self.ctx) 05318 raise Z3Exception("failed to evaluate expression in the model")
def evaluate | ( | self, | |
t, | |||
model_completion = False |
|||
) |
Alias for `eval`. >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0, x < 2) >>> s.check() sat >>> m = s.model() >>> m.evaluate(x + 1) 2 >>> m.evaluate(x == 1) True >>> y = Int('y') >>> m.evaluate(y + x) 1 + y >>> m.evaluate(y) y >>> m.evaluate(y, model_completion=True) 0 >>> # Now, m contains an interpretation for y >>> m.evaluate(y + x) 1
Definition at line 5319 of file z3py.py.
05319 05320 def evaluate(self, t, model_completion=False): 05321 """Alias for `eval`. 05322 05323 >>> x = Int('x') 05324 >>> s = Solver() 05325 >>> s.add(x > 0, x < 2) 05326 >>> s.check() 05327 sat 05328 >>> m = s.model() 05329 >>> m.evaluate(x + 1) 05330 2 05331 >>> m.evaluate(x == 1) 05332 True 05333 >>> y = Int('y') 05334 >>> m.evaluate(y + x) 05335 1 + y 05336 >>> m.evaluate(y) 05337 y 05338 >>> m.evaluate(y, model_completion=True) 05339 0 05340 >>> # Now, m contains an interpretation for y 05341 >>> m.evaluate(y + x) 05342 1 05343 """ 05344 return self.eval(t, model_completion)
def get_interp | ( | self, | |
decl | |||
) |
Return the interpretation for a given declaration or constant. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0, x < 2, f(x) == 0) >>> s.check() sat >>> m = s.model() >>> m[x] 1 >>> m[f] [1 -> 0, else -> 0]
Definition at line 5360 of file z3py.py.
Referenced by ModelRef.__getitem__().
05360 05361 def get_interp(self, decl): 05362 """Return the interpretation for a given declaration or constant. 05363 05364 >>> f = Function('f', IntSort(), IntSort()) 05365 >>> x = Int('x') 05366 >>> s = Solver() 05367 >>> s.add(x > 0, x < 2, f(x) == 0) 05368 >>> s.check() 05369 sat 05370 >>> m = s.model() 05371 >>> m[x] 05372 1 05373 >>> m[f] 05374 [1 -> 0, else -> 0] 05375 """ 05376 if __debug__: 05377 _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected") 05378 if is_const(decl): 05379 decl = decl.decl() 05380 try: 05381 if decl.arity() == 0: 05382 r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) 05383 if is_as_array(r): 05384 return self.get_interp(get_as_array_func(r)) 05385 else: 05386 return r 05387 else: 05388 return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) 05389 except Z3Exception: 05390 return None
def get_sort | ( | self, | |
idx | |||
) |
Return the unintepreted sort at position `idx` < self.num_sorts(). >>> A = DeclareSort('A') >>> B = DeclareSort('B') >>> a1, a2 = Consts('a1 a2', A) >>> b1, b2 = Consts('b1 b2', B) >>> s = Solver() >>> s.add(a1 != a2, b1 != b2) >>> s.check() sat >>> m = s.model() >>> m.num_sorts() 2 >>> m.get_sort(0) A >>> m.get_sort(1) B
Definition at line 5406 of file z3py.py.
05406 05407 def get_sort(self, idx): 05408 """Return the unintepreted sort at position `idx` < self.num_sorts(). 05409 05410 >>> A = DeclareSort('A') 05411 >>> B = DeclareSort('B') 05412 >>> a1, a2 = Consts('a1 a2', A) 05413 >>> b1, b2 = Consts('b1 b2', B) 05414 >>> s = Solver() 05415 >>> s.add(a1 != a2, b1 != b2) 05416 >>> s.check() 05417 sat 05418 >>> m = s.model() 05419 >>> m.num_sorts() 05420 2 05421 >>> m.get_sort(0) 05422 A 05423 >>> m.get_sort(1) 05424 B 05425 """ 05426 if idx >= self.num_sorts(): 05427 raise IndexError 05428 return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx)
def get_universe | ( | self, | |
s | |||
) |
Return the intepretation for the uninterpreted sort `s` in the model `self`. >>> A = DeclareSort('A') >>> a, b = Consts('a b', A) >>> s = Solver() >>> s.add(a != b) >>> s.check() sat >>> m = s.model() >>> m.get_universe(A) [A!val!0, A!val!1]
Definition at line 5446 of file z3py.py.
Referenced by ModelRef.__getitem__().
05446 05447 def get_universe(self, s): 05448 """Return the intepretation for the uninterpreted sort `s` in the model `self`. 05449 05450 >>> A = DeclareSort('A') 05451 >>> a, b = Consts('a b', A) 05452 >>> s = Solver() 05453 >>> s.add(a != b) 05454 >>> s.check() 05455 sat 05456 >>> m = s.model() 05457 >>> m.get_universe(A) 05458 [A!val!0, A!val!1] 05459 """ 05460 if __debug__: 05461 _z3_assert(isinstance(s, SortRef), "Z3 sort expected") 05462 try: 05463 return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx) 05464 except Z3Exception: 05465 return None
def num_sorts | ( | self | ) |
Return the number of unintepreted sorts that contain an interpretation in the model `self`. >>> A = DeclareSort('A') >>> a, b = Consts('a b', A) >>> s = Solver() >>> s.add(a != b) >>> s.check() sat >>> m = s.model() >>> m.num_sorts() 1
Definition at line 5391 of file z3py.py.
Referenced by ModelRef.get_sort().
05391 05392 def num_sorts(self): 05393 """Return the number of unintepreted sorts that contain an interpretation in the model `self`. 05394 05395 >>> A = DeclareSort('A') 05396 >>> a, b = Consts('a b', A) 05397 >>> s = Solver() 05398 >>> s.add(a != b) 05399 >>> s.check() 05400 sat 05401 >>> m = s.model() 05402 >>> m.num_sorts() 05403 1 05404 """ 05405 return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model))
def sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the model.
Definition at line 5286 of file z3py.py.
Referenced by Fixedpoint.__repr__().
05286 05287 def sexpr(self): 05288 """Return a textual representation of the s-expression representing the model.""" 05289 return Z3_model_to_string(self.ctx.ref(), self.model)
def sorts | ( | self | ) |
Return all uninterpreted sorts that have an interpretation in the model `self`. >>> A = DeclareSort('A') >>> B = DeclareSort('B') >>> a1, a2 = Consts('a1 a2', A) >>> b1, b2 = Consts('b1 b2', B) >>> s = Solver() >>> s.add(a1 != a2, b1 != b2) >>> s.check() sat >>> m = s.model() >>> m.sorts() [A, B]
Definition at line 5429 of file z3py.py.
05429 05430 def sorts(self): 05431 """Return all uninterpreted sorts that have an interpretation in the model `self`. 05432 05433 >>> A = DeclareSort('A') 05434 >>> B = DeclareSort('B') 05435 >>> a1, a2 = Consts('a1 a2', A) 05436 >>> b1, b2 = Consts('b1 b2', B) 05437 >>> s = Solver() 05438 >>> s.add(a1 != a2, b1 != b2) 05439 >>> s.check() 05440 sat 05441 >>> m = s.model() 05442 >>> m.sorts() 05443 [A, B] 05444 """ 05445 return [ self.get_sort(i) for i in range(self.num_sorts()) ]
Definition at line 5274 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__(), ModelRef.__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(), Fixedpoint.add_rule(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), QuantifierRef.body(), BoolSortRef.cast(), DatatypeSortRef.constructor(), ApplyResult.convert_model(), ExprRef.decl(), ModelRef.decls(), RatNumRef.denominator(), FuncDeclRef.domain(), ArraySortRef.domain(), ModelRef.eval(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ModelRef.get_interp(), Fixedpoint.get_rules(), ModelRef.get_sort(), ModelRef.get_universe(), SortRef.kind(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), RatNumRef.numerator(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Fixedpoint.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), Fixedpoint.statistics(), Solver.to_smt2(), Fixedpoint.update_rule(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
Definition at line 5274 of file z3py.py.
Referenced by ModelRef::__del__(), ModelRef::__getitem__(), ModelRef::__len__(), ModelRef::decls(), ModelRef::eval(), ModelRef::get_interp(), ModelRef::get_sort(), ModelRef::get_universe(), ModelRef::num_sorts(), and ModelRef::sexpr().