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__
 
def __del__ (self)
 
def __deepcopy__
 
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 718 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 815 of file z3py.py.

815  def __call__(self, *args):
816  """Create a Z3 application expression using the function `self`, and the given arguments.
817 
818  The arguments must be Z3 expressions. This method assumes that
819  the sorts of the elements in `args` match the sorts of the
820  domain. Limited coercion is supported. For example, if
821  args[0] is a Python integer, and the function expects a Z3
822  integer, then the argument is automatically converted into a
823  Z3 integer.
824 
825  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
826  >>> x = Int('x')
827  >>> y = Real('y')
828  >>> f(x, y)
829  f(x, y)
830  >>> f(x, x)
831  f(x, ToReal(x))
832  """
833  args = _get_args(args)
834  num = len(args)
835  _args = (Ast * num)()
836  saved = []
837  for i in range(num):
838  # self.domain(i).cast(args[i]) may create a new Z3 expression,
839  # then we must save in 'saved' to prevent it from being garbage collected.
840  tmp = self.domain(i).cast(args[i])
841  saved.append(tmp)
842  _args[i] = tmp.as_ast()
843  return _to_expr_ref(Z3_mk_app(self.ctx_ref(), self.ast, len(args), _args), self.ctx)
844 
845 
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 domain(self, i)
Definition: z3py.py:756
def range(self)
Definition: z3py.py:768
def ctx_ref(self)
Definition: z3py.py:400
def __call__(self, args)
Definition: z3py.py:815
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 746 of file z3py.py.

746  def arity(self):
747  """Return the number of arguments of a function declaration.
748  If `self` is a constant, then `self.arity()` is 0.
749 
750  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
751  >>> f.arity()
752  2
753  """
754  return int(Z3_get_arity(self.ctx_ref(), self.ast))
755 
def ctx_ref(self)
Definition: z3py.py:400
unsigned Z3_API Z3_get_arity(Z3_context c, Z3_func_decl d)
Alias for Z3_get_domain_size.
def arity(self)
Definition: z3py.py:746
def as_ast (   self)

Definition at line 726 of file z3py.py.

726  def as_ast(self):
727  return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
728 
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(self)
Definition: z3py.py:400
def as_ast(self)
Definition: z3py.py:726
def as_func_decl (   self)

Definition at line 732 of file z3py.py.

732  def as_func_decl(self):
733  return self.ast
734 
def as_func_decl(self)
Definition: z3py.py:732
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 756 of file z3py.py.

Referenced by FuncDeclRef.__call__().

756  def domain(self, i):
757  """Return the sort of the argument `i` of a function declaration.
758  This method assumes that `0 <= i < self.arity()`.
759 
760  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
761  >>> f.domain(0)
762  Int
763  >>> f.domain(1)
764  Real
765  """
766  return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
767 
def domain(self, i)
Definition: z3py.py:756
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 ctx_ref(self)
Definition: z3py.py:400
def get_id (   self)

Definition at line 729 of file z3py.py.

729  def get_id(self):
730  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
731 
def as_ast(self)
Definition: z3py.py:392
def get_id(self)
Definition: z3py.py:729
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 ctx_ref(self)
Definition: z3py.py:400
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 778 of file z3py.py.

778  def kind(self):
779  """Return the internal kind of a function declaration.
780  It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
781 
782  >>> x = Int('x')
783  >>> d = (x + 1).decl()
784  >>> d.kind() == Z3_OP_ADD
785  True
786  >>> d.kind() == Z3_OP_MUL
787  False
788  """
789  return Z3_get_decl_kind(self.ctx_ref(), self.ast)
790 
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(self)
Definition: z3py.py:400
def kind(self)
Definition: z3py.py:778
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 735 of file z3py.py.

735  def name(self):
736  """Return the name of the function declaration `self`.
737 
738  >>> f = Function('f', IntSort(), IntSort())
739  >>> f.name()
740  'f'
741  >>> isinstance(f.name(), str)
742  True
743  """
744  return _symbol2py(self.ctx, Z3_get_decl_name(self.ctx_ref(), self.ast))
745 
def name(self)
Definition: z3py.py:735
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(self)
Definition: z3py.py:400
def params (   self)

Definition at line 791 of file z3py.py.

791  def params(self):
792  ctx = self.ctx
793  n = Z3_get_decl_num_parameters(self.ctx_ref(), self.ast)
794  result = [None for i in range(n)]
795  for i in range(n):
796  k = Z3_get_decl_parameter_kind(self.ctx_ref(), self.ast, i)
797  if k == Z3_PARAMETER_INT:
798  result[i] = Z3_get_decl_int_parameter(self.ctx_ref(), self.ast, i)
799  elif k == Z3_PARAMETER_DOUBLE:
800  result[i] = Z3_get_decl_double_parameter(self.ctx_ref(), self.ast, i)
801  elif k == Z3_PARAMETER_RATIONAL:
802  result[i] = Z3_get_decl_rational_parameter(self.ctx_ref(), self.ast, i)
803  elif k == Z3_PARAMETER_SYMBOL:
804  result[i] = Z3_get_decl_symbol_parameter(self.ctx_ref(), self.ast, i)
805  elif k == Z3_PARAMETER_SORT:
806  result[i] = SortRef(Z3_get_decl_sort_parameter(self.ctx_ref(), self.ast, i), ctx)
807  elif k == Z3_PARAMETER_AST:
808  result[i] = ExprRef(Z3_get_decl_ast_parameter(self.ctx_ref(), self.ast, i), ctx)
809  elif k == Z3_PARAMETER_FUNC_DECL:
810  result[i] = FuncDeclRef(Z3_get_decl_func_decl_parameter(self.ctx_ref(), self.ast, i), ctx)
811  else:
812  assert(False)
813  return result
814 
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:718
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.
def range(self)
Definition: z3py.py:768
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.
def params(self)
Definition: z3py.py:791
def ctx_ref(self)
Definition: z3py.py:400
Expressions.
Definition: z3py.py:957
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 768 of file z3py.py.

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

768  def range(self):
769  """Return the sort of the range of a function declaration.
770  For constants, this is the sort of the constant.
771 
772  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
773  >>> f.range()
774  Bool
775  """
776  return _to_sort_ref(Z3_get_range(self.ctx_ref(), self.ast), self.ctx)
777 
def range(self)
Definition: z3py.py:768
Z3_sort Z3_API Z3_get_range(Z3_context c, Z3_func_decl d)
Return the range of the given declaration.
def ctx_ref(self)
Definition: z3py.py:400