ExprRef Class Reference

Expressions. More...

Inheritance diagram for ExprRef:

Public Member Functions
def	as_ast
def	get_id
def	sort
def	sort_kind
def	__eq__
def	__ne__
def	decl
def	num_args
def	arg
def	children

---

Detailed Description

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 736 of file z3py.py.

---

Member Function Documentation

def __eq__	(		self,
			other
	)

Return a Z3 expression that represents the constraint `self == other`.

If `other` is `None`, then this method simply returns `False`. 

>>> a = Int('a')
>>> b = Int('b')
>>> a == b
a == b
>>> a == None
False

Definition at line 775 of file z3py.py.

Referenced by Probe.__ne__().

    def __eq__(self, other):
        """Return a Z3 expression that represents the constraint `self == other`.

        If `other` is `None`, then this method simply returns `False`. 

        >>> a = Int('a')
        >>> b = Int('b')
        >>> a == b
        a == b
        >>> a == None
        False
        """
        if other == None:
            return False
        a, b = _coerce_exprs(self, other)
        return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)

def __ne__	(		self,
			other
	)

Return a Z3 expression that represents the constraint `self != other`.

If `other` is `None`, then this method simply returns `True`. 

>>> a = Int('a')
>>> b = Int('b')
>>> a != b
a != b
>>> a != None
True

Reimplemented in FPRef.

Definition at line 792 of file z3py.py.

    def __ne__(self, other):
        """Return a Z3 expression that represents the constraint `self != other`.
        
        If `other` is `None`, then this method simply returns `True`. 

        >>> a = Int('a')
        >>> b = Int('b')
        >>> a != b
        a != b
        >>> a != None
        True
        """
        if other == None:
            return True
        a, b = _coerce_exprs(self, other)
        _args, sz = _to_ast_array((a, b))
        return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)

def arg	(		self,
			idx
	)

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 841 of file z3py.py.

Referenced by ExprRef.children().

    def arg(self, idx):
        """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
        """
        if __debug__:
            _z3_assert(is_app(self), "Z3 application expected")
            _z3_assert(idx < self.num_args(), "Invalid argument index")
        return _to_expr_ref(Z3_get_app_arg(self.ctx_ref(), self.as_ast(), idx), self.ctx)

def as_ast

(

self

)

Return a pointer to the corresponding C Z3_ast object.

Reimplemented from AstRef.

Reimplemented in QuantifierRef, and PatternRef.

Definition at line 746 of file z3py.py.

Referenced by ExprRef.arg(), ExprRef.decl(), ExprRef.get_id(), ExprRef.num_args(), ExprRef.sort(), and BoolRef.sort().

    def as_ast(self):
        return self.ast

def children

(

self

)

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]

Reimplemented in QuantifierRef.

Definition at line 862 of file z3py.py.

    def children(self):
        """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]
        """
        if is_app(self):
            return [self.arg(i) for i in range(self.num_args())]
        else:
            return []

def decl

(

self

)

Return the Z3 function declaration associated with a Z3 application.

>>> f = Function('f', IntSort(), IntSort())
>>> a = Int('a')
>>> t = f(a)
>>> eq(t.decl(), f)
True
>>> (a + 1).decl()
+

Definition at line 810 of file z3py.py.

00810 
00811     def decl(self):
00812         """Return the Z3 function declaration associated with a Z3 application.
00813         
00814         >>> f = Function('f', IntSort(), IntSort())
00815         >>> a = Int('a')
00816         >>> t = f(a)
00817         >>> eq(t.decl(), f)
00818         True
00819         >>> (a + 1).decl()
00820         +
00821         """
00822         if __debug__:
00823             _z3_assert(is_app(self), "Z3 application expected")
00824         return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx)
    

def get_id

(

self

)

Return unique identifier for object. It can be used for hash-tables and maps.

Reimplemented from AstRef.

Reimplemented in QuantifierRef, and PatternRef.

Definition at line 749 of file z3py.py.

    def get_id(self):
        return Z3_get_ast_id(self.ctx_ref(), self.as_ast())

def num_args

(

self

)

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 825 of file z3py.py.

Referenced by ExprRef.arg(), and ExprRef.children().

    def num_args(self):
        """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
        """
        if __debug__:
            _z3_assert(is_app(self), "Z3 application expected")
        return int(Z3_get_app_num_args(self.ctx_ref(), self.as_ast()))

def sort

(

self

)

Return the sort of expression `self`.

>>> x = Int('x')
>>> (x + 1).sort()
Int
>>> y = Real('y')
>>> (x + y).sort()
Real

Reimplemented in FPRef, DatatypeRef, ArrayRef, BitVecRef, ArithRef, QuantifierRef, and BoolRef.

Definition at line 752 of file z3py.py.

Referenced by ArrayRef.domain(), ArrayRef.range(), and ExprRef.sort_kind().

    def sort(self):
        """Return the sort of expression `self`.
        
        >>> x = Int('x')
        >>> (x + 1).sort()
        Int
        >>> y = Real('y')
        >>> (x + y).sort()
        Real
        """
        return _sort(self.ctx, self.as_ast())

def sort_kind

(

self

)

Shorthand for `self.sort().kind()`.

>>> a = Array('a', IntSort(), IntSort())
>>> a.sort_kind() == Z3_ARRAY_SORT
True
>>> a.sort_kind() == Z3_INT_SORT
False

Definition at line 764 of file z3py.py.

    def sort_kind(self):
        """Shorthand for `self.sort().kind()`.
        
        >>> a = Array('a', IntSort(), IntSort())
        >>> a.sort_kind() == Z3_ARRAY_SORT
        True
        >>> a.sort_kind() == Z3_INT_SORT
        False
        """
        return self.sort().kind()