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.
Definition at line 624 of file z3py.py.
def __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 coersion 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 694 of file z3py.py.
694 def __call__(self, *args):
695 """Create a Z3 application expression using the function `self`, and the given arguments. 697 The arguments must be Z3 expressions. This method assumes that 698 the sorts of the elements in `args` match the sorts of the 699 domain. Limited coersion is supported. For example, if 700 args[0] is a Python integer, and the function expects a Z3 701 integer, then the argument is automatically converted into a 704 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 712 args = _get_args(args)
715 _z3_assert(num == self.arity(),
"Incorrect number of arguments to %s" % self)
716 _args = (Ast * num)()
721 tmp = self.domain(i).cast(args[i])
723 _args[i] = tmp.as_ast()
724 return _to_expr_ref(
Z3_mk_app(self.ctx_ref(), self.ast, len(args), _args), self.ctx)
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
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 651 of file z3py.py.
Referenced by FuncDeclRef.__call__(), and FuncDeclRef.domain().
652 """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0. 654 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 658 return int(Z3_get_arity(self.ctx_ref(), self.ast))
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 660 of file z3py.py.
Referenced by FuncDeclRef.__call__().
661 """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`. 663 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 670 _z3_assert(i < self.arity(),
"Index out of bounds")
671 return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
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 673 of file z3py.py.
Referenced by FuncDeclRef.__call__().
674 """Return the sort of the range of a function declaration. For constants, this is the sort of the constant. 676 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 680 return _to_sort_ref(Z3_get_range(self.ctx_ref(), self.ast), self.ctx)