FuncDeclRef Class Reference

Function Declarations. More...

Inheritance diagram for FuncDeclRef:

Public Member Functions
def	as_ast
def	name
def	arity
def	domain
def	range
def	kind
def	__call__
Public Member Functions inherited from AstRef
def	__init__
def	__del__
def	__str__
def	__repr__
def	sexpr
def	as_ast
def	ctx_ref
def	eq
def	translate
def	hash
Public Member Functions inherited from Z3PPObject
def	use_pp

Additional Inherited Members
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

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 553 of file z3py.py.

Member Function Documentation

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 617 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))
        """
        args = _get_args(args)
        num = len(args)
        if __debug__:
            _z3_assert(num == self.arity(), "Incorrect number of arguments")
        _args = (Ast * num)()
        saved = []
        for i in range(num):
            # self.domain(i).cast(args[i]) may create a new Z3 expression,
            # then we must save in 'saved' to prevent it from being garbage collected.
            tmp      = self.domain(i).cast(args[i])
            saved.append(tmp)
            _args[i] = tmp.as_ast()
        return _to_expr_ref(Z3_mk_app(self.ctx_ref(), self.ast, len(args), _args), self.ctx)