Stores the interpretation of a function in a Z3 model.
Definition at line 5345 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 5435 of file z3py.py.
5436 """Return the function interpretation as a Python list. 5437 >>> f = Function('f', IntSort(), IntSort()) 5439 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5444 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5446 [[0, 1], [1, 1], [2, 0], 1] 5448 r = [ self.entry(i).as_list()
for i
in range(self.num_entries())]
5449 r.append(self.else_value())
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 5358 of file z3py.py.
5358 def else_value(self):
5360 Return the `else` value for a function interpretation. 5361 Return None if Z3 did not specify the `else` value for 5364 >>> f = Function('f', IntSort(), IntSort()) 5366 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5371 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5372 >>> m[f].else_value() 5377 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 5411 of file z3py.py.
5411 def entry(self, idx):
5412 """Return an entry at position `idx < self.num_entries()` in the function interpretation `self`. 5414 >>> f = Function('f', IntSort(), IntSort()) 5416 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5421 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5422 >>> m[f].num_entries() 5431 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 5381 of file z3py.py.
Referenced by FuncInterp.entry().
5381 def num_entries(self):
5382 """Return the number of entries/points in the function interpretation `self`. 5384 >>> f = Function('f', IntSort(), IntSort()) 5386 >>> s.add(f(0) == 1, f(1) == 1, f(2) == 0) 5391 [0 -> 1, 1 -> 1, 2 -> 0, else -> 1] 5392 >>> 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.