Function Declarations. More...
Public Member Functions | |
def | as_ast |
def | get_id |
def | as_func_decl |
def | name |
def | arity |
def | domain |
def | range |
def | kind |
def | __call__ |
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 657 of file z3py.py.
00657 00658 def __call__(self, *args): 00659 """Create a Z3 application expression using the function `self`, and the given arguments. 00660 00661 The arguments must be Z3 expressions. This method assumes that 00662 the sorts of the elements in `args` match the sorts of the 00663 domain. Limited coersion is supported. For example, if 00664 args[0] is a Python integer, and the function expects a Z3 00665 integer, then the argument is automatically converted into a 00666 Z3 integer. 00667 00668 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 00669 >>> x = Int('x') 00670 >>> y = Real('y') 00671 >>> f(x, y) 00672 f(x, y) 00673 >>> f(x, x) 00674 f(x, ToReal(x)) 00675 """ 00676 args = _get_args(args) 00677 num = len(args) 00678 if __debug__: 00679 _z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self) 00680 _args = (Ast * num)() 00681 saved = [] 00682 for i in range(num): 00683 # self.domain(i).cast(args[i]) may create a new Z3 expression, 00684 # then we must save in 'saved' to prevent it from being garbage collected. 00685 tmp = self.domain(i).cast(args[i]) 00686 saved.append(tmp) 00687 _args[i] = tmp.as_ast() 00688 return _to_expr_ref(Z3_mk_app(self.ctx_ref(), self.ast, len(args), _args), self.ctx)
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 614 of file z3py.py.
Referenced by FuncDeclRef.__call__(), and FuncDeclRef.domain().
00614 00615 def arity(self): 00616 """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0. 00617 00618 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 00619 >>> f.arity() 00620 2 00621 """ 00622 return int(Z3_get_arity(self.ctx_ref(), self.ast))
def as_ast | ( | self | ) |
Return a pointer to the corresponding C Z3_ast object.
Reimplemented from AstRef.
Definition at line 594 of file z3py.py.
Referenced by ExprRef.arg(), ExprRef.decl(), FuncDeclRef.get_id(), ExprRef.get_id(), ExprRef.num_args(), ExprRef.sort(), and BoolRef.sort().
00594 00595 def as_ast(self): 00596 return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
def as_func_decl | ( | self | ) |
Definition at line 600 of file z3py.py.
00600 00601 def as_func_decl(self): 00602 return self.ast
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 623 of file z3py.py.
Referenced by FuncDeclRef.__call__().
00623 00624 def domain(self, i): 00625 """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`. 00626 00627 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 00628 >>> f.domain(0) 00629 Int 00630 >>> f.domain(1) 00631 Real 00632 """ 00633 if __debug__: 00634 _z3_assert(i < self.arity(), "Index out of bounds") 00635 return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
def get_id | ( | self | ) |
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 645 of file z3py.py.
00645 00646 def kind(self): 00647 """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc. 00648 00649 >>> x = Int('x') 00650 >>> d = (x + 1).decl() 00651 >>> d.kind() == Z3_OP_ADD 00652 True 00653 >>> d.kind() == Z3_OP_MUL 00654 False 00655 """ 00656 return Z3_get_decl_kind(self.ctx_ref(), self.ast)
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 603 of file z3py.py.
00603 00604 def name(self): 00605 """Return the name of the function declaration `self`. 00606 00607 >>> f = Function('f', IntSort(), IntSort()) 00608 >>> f.name() 00609 'f' 00610 >>> isinstance(f.name(), str) 00611 True 00612 """ 00613 return _symbol2py(self.ctx, Z3_get_decl_name(self.ctx_ref(), self.ast))
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 636 of file z3py.py.
Referenced by FuncDeclRef.__call__().
00636 00637 def range(self): 00638 """Return the sort of the range of a function declaration. For constants, this is the sort of the constant. 00639 00640 >>> f = Function('f', IntSort(), RealSort(), BoolSort()) 00641 >>> f.range() 00642 Bool 00643 """ 00644 return _to_sort_ref(Z3_get_range(self.ctx_ref(), self.ast), self.ctx)