Store the value of the interpretation of a function in a particular point.
Definition at line 5395 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()
3
>>> e = f_i.entry(0)
>>> e
[0, 1, 10]
>>> e.num_args()
2
>>> e.arg_value(0)
0
>>> e.arg_value(1)
1
>>> try:
... e.arg_value(2)
... except IndexError:
... print("index error")
index error
Definition at line 5428 of file z3py.py.
5428 def arg_value(self, idx):
5429 """Return the value of argument `idx`. 5431 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5433 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5438 >>> f_i.num_entries() 5440 >>> e = f_i.entry(0) 5451 ... except IndexError: 5452 ... print("index error") 5455 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()
3
>>> e = f_i.entry(0)
>>> e.as_list()
[0, 1, 10]
Definition at line 5481 of file z3py.py.
5482 """Return entry `self` as a Python list. 5483 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5485 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5490 >>> f_i.num_entries() 5492 >>> e = f_i.entry(0) 5496 args = [ self.arg_value(i)
for i
in range(self.num_args())]
5497 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()
3
>>> e = f_i.entry(0)
>>> e.num_args()
2
Definition at line 5410 of file z3py.py.
Referenced by AstRef.__bool__().
5411 """Return the number of arguments in the given entry. 5413 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5415 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5420 >>> f_i.num_entries() 5422 >>> 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()
3
>>> e = f_i.entry(0)
>>> e
[0, 1, 10]
>>> e.num_args()
2
>>> e.value()
10
Definition at line 5459 of file z3py.py.
5460 """Return the value of the function at point `self`. 5462 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5464 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5469 >>> f_i.num_entries() 5471 >>> 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.