Store the value of the interpretation of a function in a particular point.
Definition at line 5240 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 5270 of file z3py.py.
5270 def arg_value(self, idx):
5271 """Return the value of argument `idx`. 5273 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5275 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5280 >>> f_i.num_entries() 5282 >>> e = f_i.entry(0) 5293 ... except IndexError: 5294 ... print("index error") 5297 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 5323 of file z3py.py.
5324 """Return entry `self` as a Python list. 5325 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5327 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5332 >>> f_i.num_entries() 5334 >>> e = f_i.entry(0) 5338 args = [ self.arg_value(i)
for i
in range(self.num_args())]
5339 args.append(self.value())
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 5252 of file z3py.py.
Referenced by AstRef.__bool__().
5253 """Return the number of arguments in the given entry. 5255 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5257 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5262 >>> f_i.num_entries() 5264 >>> 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 5301 of file z3py.py.
5302 """Return the value of the function at point `self`. 5304 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 5306 >>> s.add(f(0, 1) == 10, f(1, 2) == 20, f(1, 0) == 10) 5311 >>> f_i.num_entries() 5313 >>> 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.