Stores the interpretation of a function in a Z3 model.
Definition at line 5460 of file z3py.py.
Return the function interpretation as a Python list.
>>> f = Function('f', IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[f]
[0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
>>> m[f].as_list()
[[0, 1], [1, 1], [2, 0], 1]
Definition at line 5553 of file z3py.py.
5554 """Return the function interpretation as a Python list. 5555 >>> f = Function('f', IntSort(), IntSort()) 5557 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5562 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5564 [[0, 1], [1, 1], [2, 0], 1] 5566 r = [ self.entry(i).as_list()
for i
in range(self.num_entries())]
5567 r.append(self.else_value())
expr range(expr const &lo, expr const &hi)
Return the `else` value for a function interpretation.
Return None if Z3 did not specify the `else` value for
this object.
>>> f = Function('f', IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[f]
[0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
>>> m[f].else_value()
1
Definition at line 5476 of file z3py.py.
5476 def else_value(self):
5478 Return the `else` value for a function interpretation. 5479 Return None if Z3 did not specify the `else` value for 5482 >>> f = Function('f', IntSort(), IntSort()) 5484 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5489 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5490 >>> m[f].else_value() 5495 return _to_expr_ref(r, self.ctx)
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.
Return an entry at position `idx < self.num_entries()` in the function interpretation `self`.
>>> f = Function('f', IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[f]
[0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
>>> m[f].num_entries()
3
>>> m[f].entry(0)
[0, 1]
>>> m[f].entry(1)
[1, 1]
>>> m[f].entry(2)
[2, 0]
Definition at line 5529 of file z3py.py.
5529 def entry(self, idx):
5530 """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`. 5532 >>> f = Function('f', IntSort(), IntSort()) 5534 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5539 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5540 >>> m[f].num_entries() 5549 if idx >= self.num_entries():
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...
Return the number of entries/points in the function interpretation `self`.
>>> f = Function('f', IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0) == 1, f(1) == 1, f(2) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[f]
[0 -> 1, 1 -> 1, 2 -> 0, else -> 1]
>>> m[f].num_entries()
3
Definition at line 5499 of file z3py.py.
Referenced by FuncInterp.entry().
5499 def num_entries(self):
5500 """Return the number of entries/points in the function interpretation `self`. 5502 >>> f = Function('f', IntSort(), IntSort()) 5504 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5509 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5510 >>> m[f].num_entries() unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.