Public Member Functions | |
__init__ (self, entry, ctx) | |
__deepcopy__ (self, memo={}) | |
__del__ (self) | |
num_args (self) | |
arg_value (self, idx) | |
value (self) | |
as_list (self) | |
__repr__ (self) |
Data Fields | |
entry = entry | |
ctx = ctx |
Store the value of the interpretation of a function in a particular point.
__init__ | ( | self, | |
entry, | |||
ctx ) |
Definition at line 6233 of file z3py.py.
__del__ | ( | self | ) |
Definition at line 6241 of file z3py.py.
__deepcopy__ | ( | self, | |
memo = {} ) |
__repr__ | ( | self | ) |
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 6263 of file z3py.py.
Referenced by as_list().
as_list | ( | self | ) |
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 6316 of file z3py.py.
Referenced by __repr__().
num_args | ( | self | ) |
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 6245 of file z3py.py.
Referenced by AstRef.__bool__(), arg_value(), and as_list().
value | ( | self | ) |
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 6294 of file z3py.py.
Referenced by as_list().
ctx = ctx |
Definition at line 6235 of file z3py.py.
Referenced by FuncInterp.__copy__(), ModelRef.__copy__(), __deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), __del__(), FuncInterp.__del__(), ModelRef.__del__(), Solver.__del__(), Statistics.__del__(), ModelRef.__getitem__(), Statistics.__getitem__(), ModelRef.__len__(), Statistics.__len__(), Statistics.__repr__(), arg_value(), FuncInterp.arity(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.check(), ModelRef.decls(), FuncInterp.else_value(), FuncInterp.entry(), ModelRef.eval(), ModelRef.get_interp(), Statistics.get_key_value(), ModelRef.get_sort(), ModelRef.get_universe(), Statistics.keys(), Solver.model(), num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), Solver.pop(), ModelRef.project(), ModelRef.project_with_witness(), Solver.push(), Solver.reset(), Solver.set(), ModelRef.sexpr(), ModelRef.translate(), and value().
entry = entry |
Definition at line 6234 of file z3py.py.
Referenced by __deepcopy__(), __del__(), arg_value(), FuncInterp.as_list(), num_args(), and value().