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 __call__ (self, args)
 
- Public Member Functions inherited from AstRef
def __init__ (self, ast, ctx=None)
 
def __del__ (self)
 
def __str__ (self)
 
def __repr__ (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 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 591 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 661 of file z3py.py.

661  def __call__(self, *args):
662  """Create a Z3 application expression using the function `self`, and the given arguments.
663 
664  The arguments must be Z3 expressions. This method assumes that
665  the sorts of the elements in `args` match the sorts of the
666  domain. Limited coersion is supported. For example, if
667  args[0] is a Python integer, and the function expects a Z3
668  integer, then the argument is automatically converted into a
669  Z3 integer.
670 
671  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
672  >>> x = Int('x')
673  >>> y = Real('y')
674  >>> f(x, y)
675  f(x, y)
676  >>> f(x, x)
677  f(x, ToReal(x))
678  """
679  args = _get_args(args)
680  num = len(args)
681  if __debug__:
682  _z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self)
683  _args = (Ast * num)()
684  saved = []
685  for i in range(num):
686  # self.domain(i).cast(args[i]) may create a new Z3 expression,
687  # then we must save in 'saved' to prevent it from being garbage collected.
688  tmp = self.domain(i).cast(args[i])
689  saved.append(tmp)
690  _args[i] = tmp.as_ast()
691  return _to_expr_ref(Z3_mk_app(self.ctx_ref(), self.ast, len(args), _args), self.ctx)
692 
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:627
def range(self)
Definition: z3py.py:640
def ctx_ref(self)
Definition: z3py.py:304
def __call__(self, args)
Definition: z3py.py:661
def arity(self)
Definition: z3py.py:618
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 618 of file z3py.py.

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

618  def arity(self):
619  """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0.
620 
621  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
622  >>> f.arity()
623  2
624  """
625  return int(Z3_get_arity(self.ctx_ref(), self.ast))
626 
def ctx_ref(self)
Definition: z3py.py:304
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:618
def as_ast (   self)

Definition at line 598 of file z3py.py.

598  def as_ast(self):
599  return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
600 
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:304
def as_ast(self)
Definition: z3py.py:598
def as_func_decl (   self)

Definition at line 604 of file z3py.py.

604  def as_func_decl(self):
605  return self.ast
606 
def as_func_decl(self)
Definition: z3py.py:604
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 627 of file z3py.py.

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

627  def domain(self, i):
628  """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`.
629 
630  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
631  >>> f.domain(0)
632  Int
633  >>> f.domain(1)
634  Real
635  """
636  if __debug__:
637  _z3_assert(i < self.arity(), "Index out of bounds")
638  return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
639 
def domain(self, i)
Definition: z3py.py:627
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:304
def arity(self)
Definition: z3py.py:618
def get_id (   self)

Definition at line 601 of file z3py.py.

601  def get_id(self):
602  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
603 
def as_ast(self)
Definition: z3py.py:296
def get_id(self)
Definition: z3py.py:601
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:304
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 649 of file z3py.py.

649  def kind(self):
650  """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
651 
652  >>> x = Int('x')
653  >>> d = (x + 1).decl()
654  >>> d.kind() == Z3_OP_ADD
655  True
656  >>> d.kind() == Z3_OP_MUL
657  False
658  """
659  return Z3_get_decl_kind(self.ctx_ref(), self.ast)
660 
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:304
def kind(self)
Definition: z3py.py:649
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 607 of file z3py.py.

607  def name(self):
608  """Return the name of the function declaration `self`.
609 
610  >>> f = Function('f', IntSort(), IntSort())
611  >>> f.name()
612  'f'
613  >>> isinstance(f.name(), str)
614  True
615  """
616  return _symbol2py(self.ctx, Z3_get_decl_name(self.ctx_ref(), self.ast))
617 
def name(self)
Definition: z3py.py:607
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:304
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 640 of file z3py.py.

Referenced by FuncDeclRef.__call__().

640  def range(self):
641  """Return the sort of the range of a function declaration. For constants, this is the sort of the constant.
642 
643  >>> f = Function('f', IntSort(), RealSort(), BoolSort())
644  >>> f.range()
645  Bool
646  """
647  return _to_sort_ref(Z3_get_range(self.ctx_ref(), self.ast), self.ctx)
648 
def range(self)
Definition: z3py.py:640
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:304