Stores the interpretation of a function in a Z3 model.
Definition at line 5777 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]
[2 -> 0, else -> 1]
>>> m[f].as_list()
[[2, 0], 1]
Definition at line 5877 of file z3py.py.
5878 """Return the function interpretation as a Python list. 5879 >>> f = Function('f', IntSort(), IntSort()) 5881 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5890 r = [ self.entry(i).as_list()
for i
in range(self.num_entries())]
5891 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]
[2 -> 0, else -> 1]
>>> m[f].else_value()
1
Definition at line 5793 of file z3py.py.
5793 def else_value(self):
5795 Return the `else` value for a function interpretation. 5796 Return None if Z3 did not specify the `else` value for 5799 >>> f = Function('f', IntSort(), IntSort()) 5801 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5807 >>> m[f].else_value() 5812 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]
[2 -> 0, else -> 1]
>>> m[f].num_entries()
1
>>> m[f].entry(0)
[2, 0]
Definition at line 5846 of file z3py.py.
5846 def entry(self, idx):
5847 """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`. 5849 >>> f = Function('f', IntSort(), IntSort()) 5851 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5857 >>> m[f].num_entries() 5862 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 interpretation. It represents the value of f in a particular p...
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]
[2 -> 0, else -> 1]
>>> m[f].num_entries()
1
Definition at line 5816 of file z3py.py.
Referenced by FuncInterp.entry().
5816 def num_entries(self):
5817 """Return the number of entries/points in the function interpretation `self`. 5819 >>> f = Function('f', IntSort(), IntSort()) 5821 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5827 >>> 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.