Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions
FuncDeclRef Class Reference

Function Declarations. More...

+ Inheritance diagram for FuncDeclRef:

Public Member Functions

def as_ast
 
def get_id
 
def as_func_decl
 
def name
 
def arity
 
def domain
 
def range
 
def kind
 
def params
 
def __call__
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
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 651 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 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 745 of file z3py.py.

746  def __call__(self, *args):
747  """Create a Z3 application expression using the function `self`, and the given arguments.
748 
749  The arguments must be Z3 expressions. This method assumes that
750  the sorts of the elements in `args` match the sorts of the
751  domain. Limited coercion is supported. For example, if
752  args[0] is a Python integer, and the function expects a Z3
753  integer, then the argument is automatically converted into a
754  Z3 integer.
755 
756  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
757  >>> x = Int('x')
758  >>> y = Real('y')
759  >>> f(x, y)
760  f(x, y)
761  >>> f(x, x)
762  f(x, ToReal(x))
763  """
764  args = _get_args(args)
765  num = len(args)
766  if z3_debug():
767  _z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self)
768  _args = (Ast * num)()
769  saved = []
770  for i in range(num):
771  # self.domain(i).cast(args[i]) may create a new Z3 expression,
772  # then we must save in 'saved' to prevent it from being garbage collected.
773  tmp = self.domain(i).cast(args[i])
774  saved.append(tmp)
775  _args[i] = tmp.as_ast()
776  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.
def __call__
Definition: z3py.py:745
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
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 678 of file z3py.py.

Referenced by FuncDeclRef.__call__(), and FuncDeclRef.domain().

679  def arity(self):
680  """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0.
681 
682  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
683  >>> f.arity()
684  2
685  """
686  return int(Z3_get_arity(self.ctx_ref(), self.ast))
def ctx_ref
Definition: z3py.py:352
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
def as_ast (   self)

Definition at line 658 of file z3py.py.

659  def as_ast(self):
660  return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
Z3_ast Z3_API Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f)
Convert a Z3_func_decl into Z3_ast. This is just type casting.
def ctx_ref
Definition: z3py.py:352
def as_func_decl (   self)

Definition at line 664 of file z3py.py.

665  def as_func_decl(self):
666  return self.ast
def as_func_decl
Definition: z3py.py:664
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 687 of file z3py.py.

Referenced by FuncDeclRef.__call__(), and ArrayRef.__getitem__().

688  def domain(self, i):
689  """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`.
690 
691  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
692  >>> f.domain(0)
693  Int
694  >>> f.domain(1)
695  Real
696  """
697  if z3_debug():
698  _z3_assert(i < self.arity(), "Index out of bounds")
699  return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
Z3_sort Z3_API Z3_get_domain(Z3_context c, Z3_func_decl d, unsigned i)
Return the sort of the i-th parameter of the given function declaration.
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
def get_id (   self)

Definition at line 661 of file z3py.py.

662  def get_id(self):
663  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
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 709 of file z3py.py.

710  def kind(self):
711  """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
712 
713  >>> x = Int('x')
714  >>> d = (x + 1).decl()
715  >>> d.kind() == Z3_OP_ADD
716  True
717  >>> d.kind() == Z3_OP_MUL
718  False
719  """
720  return Z3_get_decl_kind(self.ctx_ref(), self.ast)
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d)
Return declaration kind corresponding to declaration.
def ctx_ref
Definition: z3py.py:352
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 667 of file z3py.py.

668  def name(self):
669  """Return the name of the function declaration `self`.
670 
671  >>> f = Function('f', IntSort(), IntSort())
672  >>> f.name()
673  'f'
674  >>> isinstance(f.name(), str)
675  True
676  """
677  return _symbol2py(self.ctx, Z3_get_decl_name(self.ctx_ref(), self.ast))
Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d)
Return the constant declaration name as a symbol.
def ctx_ref
Definition: z3py.py:352
def params (   self)

Definition at line 721 of file z3py.py.

722  def params(self):
723  ctx = self.ctx
724  n = Z3_get_decl_num_parameters(self.ctx_ref(), self.ast)
725  result = [ None for i in range(n) ]
726  for i in range(n):
727  k = Z3_get_decl_parameter_kind(self.ctx_ref(), self.ast, i)
728  if k == Z3_PARAMETER_INT:
729  result[i] = Z3_get_decl_int_parameter(self.ctx_ref(), self.ast, i)
730  elif k == Z3_PARAMETER_DOUBLE:
731  result[i] = Z3_get_decl_double_parameter(self.ctx_ref(), self.ast, i)
732  elif k == Z3_PARAMETER_RATIONAL:
733  result[i] = Z3_get_decl_rational_parameter(self.ctx_ref(), self.ast, i)
734  elif k == Z3_PARAMETER_SYMBOL:
735  result[i] = Z3_get_decl_symbol_parameter(self.ctx_ref(), self.ast, i)
736  elif k == Z3_PARAMETER_SORT:
737  result[i] = SortRef(Z3_get_decl_sort_parameter(self.ctx_ref(), self.ast, i), ctx)
738  elif k == Z3_PARAMETER_AST:
739  result[i] = ExprRef(Z3_get_decl_ast_parameter(self.ctx_ref(), self.ast, i), ctx)
740  elif k == Z3_PARAMETER_FUNC_DECL:
741  result[i] = FuncDeclRef(Z3_get_decl_func_decl_parameter(self.ctx_ref(), self.ast, i), ctx)
742  else:
743  assert(False)
744  return result
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
Function Declarations.
Definition: z3py.py:651
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
Expressions.
Definition: z3py.py:863
def ctx_ref
Definition: z3py.py:352
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the sort value associated with a sort parameter.
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 700 of file z3py.py.

Referenced by FuncDeclRef.__call__(), and FuncDeclRef.params().

701  def range(self):
702  """Return the sort of the range of a function declaration. For constants, this is the sort of the constant.
703 
704  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
705  >>> f.range()
706  Bool
707  """
708  return _to_sort_ref(Z3_get_range(self.ctx_ref(), self.ast), self.ctx)
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
def ctx_ref
Definition: z3py.py:352