Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
ArrayRef Class Reference
+ Inheritance diagram for ArrayRef:

Public Member Functions

def sort
def domain
def range
def __getitem__

Detailed Description

Array expressions. 

Definition at line 3843 of file z3py.py.


Member Function Documentation

def __getitem__ (   self,
  arg 
)
Return the Z3 expression `self[arg]`.

>>> a = Array('a', IntSort(), BoolSort())
>>> i = Int('i')
>>> a[i]
a[i]
>>> a[i].sexpr()
'(select a i)'

Definition at line 3873 of file z3py.py.

03873 
03874     def __getitem__(self, arg):
03875         """Return the Z3 expression `self[arg]`.
03876 
03877         >>> a = Array('a', IntSort(), BoolSort())
03878         >>> i = Int('i')
03879         >>> a[i]
03880         a[i]
03881         >>> a[i].sexpr()
03882         '(select a i)'
03883         """
03884         arg = self.domain().cast(arg)
03885         return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)

def domain (   self)
Shorthand for `self.sort().domain()`.

>>> a = Array('a', IntSort(), BoolSort())
>>> a.domain()
Int

Definition at line 3855 of file z3py.py.

Referenced by ArrayRef.__getitem__().

03855 
03856     def domain(self):
03857         """Shorthand for `self.sort().domain()`.
03858 
03859         >>> a = Array('a', IntSort(), BoolSort())
03860         >>> a.domain()
03861         Int
03862         """
03863         return self.sort().domain()
        
def range (   self)
Shorthand for `self.sort().range()`.

>>> a = Array('a', IntSort(), BoolSort())
>>> a.range()
Bool

Definition at line 3864 of file z3py.py.

03864 
03865     def range(self):
03866         """Shorthand for `self.sort().range()`.
03867 
03868         >>> a = Array('a', IntSort(), BoolSort())
03869         >>> a.range()
03870         Bool
03871         """
03872         return self.sort().range()

def sort (   self)
Return the array sort of the array expression `self`.

>>> a = Array('a', IntSort(), BoolSort())
>>> a.sort()
Array(Int, Bool)

Reimplemented from ExprRef.

Definition at line 3846 of file z3py.py.

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

03846 
03847     def sort(self):
03848         """Return the array sort of the array expression `self`.
03849 
03850         >>> a = Array('a', IntSort(), BoolSort())
03851         >>> a.sort()
03852         Array(Int, Bool)
03853         """
03854         return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
    
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines