Z3
Public Member Functions
FuncDeclRef Class Reference

Function Declarations. More...

+ Inheritance diagram for FuncDeclRef:

Public Member Functions

def as_ast (self)
 
def get_id (self)
 
def as_func_decl (self)
 
def name (self)
 
def arity (self)
 
def domain (self, i)
 
def range (self)
 
def kind (self)
 
def params (self)
 
def __call__ (self, args)
 
- Public Member Functions inherited from AstRef
def __init__ (self, ast, ctx=None)
 
def __del__ (self)
 
def __deepcopy__ (self, memo={})
 
def __str__ (self)
 
def __repr__ (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __nonzero__ (self)
 
def __bool__ (self)
 
def sexpr (self)
 
def as_ast (self)
 
def get_id (self)
 
def ctx_ref (self)
 
def eq (self, other)
 
def translate (self, target)
 
def __copy__ (self)
 
def hash (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

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

◆ __call__()

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.

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

◆ arity()

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().

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

◆ as_ast()

def as_ast (   self)

Definition at line 658 of file z3py.py.

658  def as_ast(self):
659  return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
660 
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.

◆ as_func_decl()

def as_func_decl (   self)

Definition at line 664 of file z3py.py.

664  def as_func_decl(self):
665  return self.ast
666 

◆ domain()

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__().

687  def domain(self, i):
688  """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`.
689 
690  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
691  >>> f.domain(0)
692  Int
693  >>> f.domain(1)
694  Real
695  """
696  if z3_debug():
697  _z3_assert(i < self.arity(), "Index out of bounds")
698  return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
699 
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

◆ get_id()

def get_id (   self)

Definition at line 661 of file z3py.py.

661  def get_id(self):
662  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
663 
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.

◆ kind()

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.

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

◆ name()

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.

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

◆ params()

def params (   self)

Definition at line 721 of file z3py.py.

721  def params(self):
722  ctx = self.ctx
723  n = Z3_get_decl_num_parameters(self.ctx_ref(), self.ast)
724  result = [ None for i in range(n) ]
725  for i in range(n):
726  k = Z3_get_decl_parameter_kind(self.ctx_ref(), self.ast, i)
727  if k == Z3_PARAMETER_INT:
728  result[i] = Z3_get_decl_int_parameter(self.ctx_ref(), self.ast, i)
729  elif k == Z3_PARAMETER_DOUBLE:
730  result[i] = Z3_get_decl_double_parameter(self.ctx_ref(), self.ast, i)
731  elif k == Z3_PARAMETER_RATIONAL:
732  result[i] = Z3_get_decl_rational_parameter(self.ctx_ref(), self.ast, i)
733  elif k == Z3_PARAMETER_SYMBOL:
734  result[i] = Z3_get_decl_symbol_parameter(self.ctx_ref(), self.ast, i)
735  elif k == Z3_PARAMETER_SORT:
736  result[i] = SortRef(Z3_get_decl_sort_parameter(self.ctx_ref(), self.ast, i), ctx)
737  elif k == Z3_PARAMETER_AST:
738  result[i] = ExprRef(Z3_get_decl_ast_parameter(self.ctx_ref(), self.ast, i), ctx)
739  elif k == Z3_PARAMETER_FUNC_DECL:
740  result[i] = FuncDeclRef(Z3_get_decl_func_decl_parameter(self.ctx_ref(), self.ast, i), ctx)
741  else:
742  assert(False)
743  return result
744 
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.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3358
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.
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.

◆ range()

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().

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