Function Declarations. More...
Public Member Functions | |
as_ast (self) | |
get_id (self) | |
as_func_decl (self) | |
name (self) | |
arity (self) | |
domain (self, i) | |
range (self) | |
kind (self) | |
params (self) | |
__call__ (self, *args) | |
Public Member Functions inherited from AstRef | |
__init__ (self, ast, ctx=None) | |
__del__ (self) | |
__deepcopy__ (self, memo={}) | |
__str__ (self) | |
__repr__ (self) | |
__eq__ (self, other) | |
__hash__ (self) | |
__nonzero__ (self) | |
__bool__ (self) | |
sexpr (self) | |
ctx_ref (self) | |
eq (self, other) | |
translate (self, target) | |
__copy__ (self) | |
hash (self) | |
py_value (self) | |
Public Member Functions inherited from Z3PPObject | |
use_pp (self) |
Additional Inherited Members | |
Data Fields inherited from AstRef | |
ast = ast | |
ctx = _get_ctx(ctx) | |
Protected Member Functions inherited from Z3PPObject | |
_repr_html_ (self) |
Function Declarations.
Function declaration. Every constant and function have an associated declaration. The declaration assigns a name, a sort (i.e., type), and for function the sort (i.e., type) of each of its arguments. Note that, in Z3, a constant is a function with 0 arguments.
__call__ | ( | self, | |
* | args ) |
Create a Z3 application expression using the function `self`, and the given arguments. The arguments must be Z3 expressions. This method assumes that the sorts of the elements in `args` match the sorts of the domain. Limited coercion is supported. For example, if args[0] is a Python integer, and the function expects a Z3 integer, then the argument is automatically converted into a Z3 integer. >>> f = Function('f', IntSort(), RealSort(), BoolSort()) >>> x = Int('x') >>> y = Real('y') >>> f(x, y) f(x, y) >>> f(x, x) f(x, ToReal(x))
Definition at line 855 of file z3py.py.
arity | ( | self | ) |
Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0. >>> f = Function('f', IntSort(), RealSort(), BoolSort()) >>> f.arity() 2
Definition at line 782 of file z3py.py.
as_ast | ( | self | ) |
as_func_decl | ( | self | ) |
domain | ( | self, | |
i ) |
Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`. >>> f = Function('f', IntSort(), RealSort(), BoolSort()) >>> f.domain(0) Int >>> f.domain(1) Real
Definition at line 792 of file z3py.py.
Referenced by __call__().
get_id | ( | self | ) |
Return unique identifier for object. It can be used for hash-tables and maps.
Reimplemented from AstRef.
Definition at line 765 of file z3py.py.
kind | ( | self | ) |
Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc. >>> x = Int('x') >>> d = (x + 1).decl() >>> d.kind() == Z3_OP_ADD True >>> d.kind() == Z3_OP_MUL False
Definition at line 814 of file z3py.py.
name | ( | self | ) |
Return the name of the function declaration `self`. >>> f = Function('f', IntSort(), IntSort()) >>> f.name() 'f' >>> isinstance(f.name(), str) True
Definition at line 771 of file z3py.py.
params | ( | self | ) |
Definition at line 827 of file z3py.py.
range | ( | self | ) |
Return the sort of the range of a function declaration. For constants, this is the sort of the constant. >>> f = Function('f', IntSort(), RealSort(), BoolSort()) >>> f.range() Bool
Definition at line 804 of file z3py.py.
Referenced by __call__(), and params().