Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions
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.

618  def __call__(self, *args):
619  """Create a Z3 application expression using the function `self`, and the given arguments.
620 
621  The arguments must be Z3 expressions. This method assumes that
622  the sorts of the elements in `args` match the sorts of the
623  domain. Limited coersion is supported. For example, if
624  args[0] is a Python integer, and the function expects a Z3
625  integer, then the argument is automatically converted into a
626  Z3 integer.
627 
628  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
629  >>> x = Int('x')
630  >>> y = Real('y')
631  >>> f(x, y)
632  f(x, y)
633  >>> f(x, x)
634  f(x, ToReal(x))
635  """
636  args = _get_args(args)
637  num = len(args)
638  if __debug__:
639  _z3_assert(num == self.arity(), "Incorrect number of arguments")
640  _args = (Ast * num)()
641  saved = []
642  for i in range(num):
643  # self.domain(i).cast(args[i]) may create a new Z3 expression,
644  # then we must save in 'saved' to prevent it from being garbage collected.
645  tmp = self.domain(i).cast(args[i])
646  saved.append(tmp)
647  _args[i] = tmp.as_ast()
648  return _to_expr_ref(Z3_mk_app(self.ctx_ref(), self.ast, len(args), _args), self.ctx)
def 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 574 of file z3py.py.

Referenced by FuncDeclRef.domain().

575  def arity(self):
576  """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0.
577 
578  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
579  >>> f.arity()
580  2
581  """
582  return int(Z3_get_arity(self.ctx_ref(), self.ast))
def as_ast (   self)

Definition at line 560 of file z3py.py.

561  def as_ast(self):
562  return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
def 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 583 of file z3py.py.

584  def domain(self, i):
585  """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`.
586 
587  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
588  >>> f.domain(0)
589  Int
590  >>> f.domain(1)
591  Real
592  """
593  if __debug__:
594  _z3_assert(i < self.arity(), "Index out of bounds")
595  return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
def 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 605 of file z3py.py.

606  def kind(self):
607  """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
608 
609  >>> x = Int('x')
610  >>> d = (x + 1).decl()
611  >>> d.kind() == Z3_OP_ADD
612  True
613  >>> d.kind() == Z3_OP_MUL
614  False
615  """
616  return Z3_get_decl_kind(self.ctx_ref(), self.ast)
def 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 563 of file z3py.py.

564  def name(self):
565  """Return the name of the function declaration `self`.
566 
567  >>> f = Function('f', IntSort(), IntSort())
568  >>> f.name()
569  'f'
570  >>> isinstance(f.name(), str)
571  True
572  """
573  return _symbol2py(self.ctx, Z3_get_decl_name(self.ctx_ref(), self.ast))
def 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 596 of file z3py.py.

597  def range(self):
598  """Return the sort of the range of a function declaration. For constants, this is the sort of the constant.
599 
600  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
601  >>> f.range()
602  Bool
603  """
604  return _to_sort_ref(Z3_get_range(self.ctx_ref(), self.ast), self.ctx)