Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
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 732 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 771 of file z3py.py.

Referenced by Probe.__ne__().

00771 
00772     def __eq__(self, other):
00773         """Return a Z3 expression that represents the constraint `self == other`.
00774 
00775         If `other` is `None`, then this method simply returns `False`. 
00776 
00777         >>> a = Int('a')
00778         >>> b = Int('b')
00779         >>> a == b
00780         a == b
00781         >>> a == None
00782         False
00783         """
00784         if other == None:
00785             return False
00786         a, b = _coerce_exprs(self, other)
00787         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

Definition at line 788 of file z3py.py.

00788 
00789     def __ne__(self, other):
00790         """Return a Z3 expression that represents the constraint `self != other`.
00791         
00792         If `other` is `None`, then this method simply returns `True`. 
00793 
00794         >>> a = Int('a')
00795         >>> b = Int('b')
00796         >>> a != b
00797         a != b
00798         >>> a != None
00799         True
00800         """
00801         if other == None:
00802             return True
00803         a, b = _coerce_exprs(self, other)
00804         _args, sz = _to_ast_array((a, b))
00805         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 837 of file z3py.py.

Referenced by ExprRef.children().

00837 
00838     def arg(self, idx):
00839         """Return argument `idx` of the application `self`. 
00840 
00841         This method assumes that `self` is a function application with at least `idx+1` arguments.
00842 
00843         >>> a = Int('a')
00844         >>> b = Int('b')
00845         >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
00846         >>> t = f(a, b, 0)
00847         >>> t.arg(0)
00848         a
00849         >>> t.arg(1)
00850         b
00851         >>> t.arg(2)
00852         0
00853         """
00854         if __debug__:
00855             _z3_assert(is_app(self), "Z3 application expected")
00856             _z3_assert(idx < self.num_args(), "Invalid argument index")
00857         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 742 of file z3py.py.

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

00742 
00743     def as_ast(self):
00744         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 858 of file z3py.py.

00858 
00859     def children(self):
00860         """Return a list containing the children of the given expression
00861 
00862         >>> a = Int('a')
00863         >>> b = Int('b')
00864         >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
00865         >>> t = f(a, b, 0)
00866         >>> t.children()
00867         [a, b, 0]
00868         """
00869         if is_app(self):
00870             return [self.arg(i) for i in range(self.num_args())]
00871         else:
00872             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 806 of file z3py.py.

00806 
00807     def decl(self):
00808         """Return the Z3 function declaration associated with a Z3 application.
00809         
00810         >>> f = Function('f', IntSort(), IntSort())
00811         >>> a = Int('a')
00812         >>> t = f(a)
00813         >>> eq(t.decl(), f)
00814         True
00815         >>> (a + 1).decl()
00816         +
00817         """
00818         if __debug__:
00819             _z3_assert(is_app(self), "Z3 application expected")
00820         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 745 of file z3py.py.

00745 
00746     def get_id(self):
00747         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 821 of file z3py.py.

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

00821 
00822     def num_args(self):
00823         """Return the number of arguments of a Z3 application.
00824 
00825         >>> a = Int('a')
00826         >>> b = Int('b')
00827         >>> (a + b).num_args()
00828         2
00829         >>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
00830         >>> t = f(a, b, 0)
00831         >>> t.num_args()
00832         3
00833         """
00834         if __debug__:
00835             _z3_assert(is_app(self), "Z3 application expected")
00836         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 DatatypeRef, ArrayRef, BitVecRef, ArithRef, QuantifierRef, and BoolRef.

Definition at line 748 of file z3py.py.

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

00748 
00749     def sort(self):
00750         """Return the sort of expression `self`.
00751         
00752         >>> x = Int('x')
00753         >>> (x + 1).sort()
00754         Int
00755         >>> y = Real('y')
00756         >>> (x + y).sort()
00757         Real
00758         """
00759         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 760 of file z3py.py.

00760 
00761     def sort_kind(self):
00762         """Shorthand for `self.sort().kind()`.
00763         
00764         >>> a = Array('a', IntSort(), IntSort())
00765         >>> a.sort_kind() == Z3_ARRAY_SORT
00766         True
00767         >>> a.sort_kind() == Z3_INT_SORT
00768         False
00769         """
00770         return self.sort().kind()

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines