Function Declarations. More...
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) |
![]() | |
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) |
![]() | |
def | use_pp (self) |
Additional Inherited Members | |
![]() | |
ast | |
ctx | |
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.
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.
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().
def as_ast | ( | self | ) |
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__().
def get_id | ( | self | ) |
Definition at line 601 of file z3py.py.
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
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.
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__().