Store the value of the interpretation of a function in a particular point.
Definition at line 5712 of file z3py.py.
def arg_value |
( |
|
self, |
|
|
|
idx |
|
) |
| |
Return the value of argument `idx`.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
>>> s.check()
sat
>>> m = s.model()
>>> f_i = m[f]
>>> f_i.num_entries()
1
>>> e = f_i.entry(0)
>>> e
[1, 2, 20]
>>> e.num_args()
2
>>> e.arg_value(0)
1
>>> e.arg_value(1)
2
>>> try:
... e.arg_value(2)
... except IndexError:
... print("index error")
index error
Definition at line 5745 of file z3py.py.
5745 def arg_value(self, idx):
5746 """Return the value of argument `idx`. 5748 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5750 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5755 >>> f_i.num_entries() 5757 >>> e = f_i.entry(0) 5768 ... except IndexError: 5769 ... print("index error") 5772 if idx >= self.num_args():
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
Return entry `self` as a Python list.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
>>> s.check()
sat
>>> m = s.model()
>>> f_i = m[f]
>>> f_i.num_entries()
1
>>> e = f_i.entry(0)
>>> e.as_list()
[1, 2, 20]
Definition at line 5798 of file z3py.py.
5799 """Return entry `self` as a Python list. 5800 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5802 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5807 >>> f_i.num_entries() 5809 >>> e = f_i.entry(0) 5813 args = [ self.arg_value(i)
for i
in range(self.num_args())]
5814 args.append(self.value())
expr range(expr const &lo, expr const &hi)
Return the number of arguments in the given entry.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
>>> s.check()
sat
>>> m = s.model()
>>> f_i = m[f]
>>> f_i.num_entries()
1
>>> e = f_i.entry(0)
>>> e.num_args()
2
Definition at line 5727 of file z3py.py.
Referenced by AstRef.__bool__().
5728 """Return the number of arguments in the given entry. 5730 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5732 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5737 >>> f_i.num_entries() 5739 >>> e = f_i.entry(0) unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
Return the value of the function at point `self`.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> s = Solver()
>>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10)
>>> s.check()
sat
>>> m = s.model()
>>> f_i = m[f]
>>> f_i.num_entries()
1
>>> e = f_i.entry(0)
>>> e
[1, 2, 20]
>>> e.num_args()
2
>>> e.value()
20
Definition at line 5776 of file z3py.py.
5777 """Return the value of the function at point `self`. 5779 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5781 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5786 >>> f_i.num_entries() 5788 >>> e = f_i.entry(0) Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.