Expressions.
Constraints, formulas and terms are expressions in Z3.
Expressions are ASTs. Every expression has a sort.
There are three main kinds of expressions:
function applications, quantifiers and bounded variables.
A constant is a function application with 0 arguments.
For quantifier free problems, all expressions are
function applications.
Definition at line 769 of file z3py.py.
Return argument `idx` of the application `self`.
This method assumes that `self` is a function application with at least `idx+1` arguments.
>>> a = Int('a')
>>> b = Int('b')
>>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
>>> t = f(a, b, 0)
>>> t.arg(0)
a
>>> t.arg(1)
b
>>> t.arg(2)
0
Definition at line 878 of file z3py.py.
Referenced by AstRef.__bool__(), and ExprRef.children().
879 """Return argument `idx` of the application `self`. 881 This method assumes that `self` is a function application with at least `idx+1` arguments. 885 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 895 _z3_assert(
is_app(self),
"Z3 application expected")
896 _z3_assert(idx < self.num_args(),
"Invalid argument index")
897 return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)
Return a list containing the children of the given expression
>>> a = Int('a')
>>> b = Int('b')
>>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
>>> t = f(a, b, 0)
>>> t.children()
[a, b, 0]
Definition at line 899 of file z3py.py.
900 """Return a list containing the children of the given expression 904 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 910 return [self.arg(i)
for i
in range(self.num_args())]
Return the number of arguments of a Z3 application.
>>> a = Int('a')
>>> b = Int('b')
>>> (a + b).num_args()
2
>>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
>>> t = f(a, b, 0)
>>> t.num_args()
3
Definition at line 862 of file z3py.py.
Referenced by AstRef.__bool__(), ExprRef.arg(), and ExprRef.children().
863 """Return the number of arguments of a Z3 application. 867 >>> (a + b).num_args() 869 >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort()) 875 _z3_assert(
is_app(self),
"Z3 application expected")
876 return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))