ArrayRef Class Reference

Inheritance diagram for ArrayRef:

Public Member Functions
def	sort
def	domain
def	range
def	__getitem__
def	mk_default

---

Detailed Description

Array expressions. 

Definition at line 3880 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 3910 of file z3py.py.

    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)'
        """
        arg = self.domain().cast(arg)
        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 3892 of file z3py.py.

Referenced by ArrayRef.__getitem__().

03892 
03893     def domain(self):
03894         """Shorthand for `self.sort().domain()`.
03895 
03896         >>> a = Array('a', IntSort(), BoolSort())
03897         >>> a.domain()
03898         Int
03899         """
03900         return self.sort().domain()
        

def mk_default

(

self

)

Definition at line 3923 of file z3py.py.

    def mk_default(self):  
        return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx)  

def range

(

self

)

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

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

Definition at line 3901 of file z3py.py.

    def range(self):
        """Shorthand for `self.sort().range()`.

        >>> a = Array('a', IntSort(), BoolSort())
        >>> a.range()
        Bool
        """
        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 3883 of file z3py.py.

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

03883 
03884     def sort(self):
03885         """Return the array sort of the array expression `self`.
03886 
03887         >>> a = Array('a', IntSort(), BoolSort())
03888         >>> a.sort()
03889         Array(Int, Bool)
03890         """
03891         return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)