Store the value of the interpretation of a function in a particular point.
Definition at line 5669 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 5702 of file z3py.py.
5702 def arg_value(self, idx):
5703 """Return the value of argument `idx`. 5705 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5707 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5712 >>> f_i.num_entries() 5714 >>> e = f_i.entry(0) 5725 ... except IndexError: 5726 ... print("index error") 5729 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 5755 of file z3py.py.
5756 """Return entry `self` as a Python list. 5757 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5759 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5764 >>> f_i.num_entries() 5766 >>> e = f_i.entry(0) 5770 args = [ self.arg_value(i)
for i
in range(self.num_args())]
5771 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 5684 of file z3py.py.
Referenced by AstRef.__bool__().
5685 """Return the number of arguments in the given entry. 5687 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5689 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5694 >>> f_i.num_entries() 5696 >>> 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 5733 of file z3py.py.
5734 """Return the value of the function at point `self`. 5736 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5738 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5743 >>> f_i.num_entries() 5745 >>> 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.