Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
ArraySortRef Class Reference

Arrays. More...

+ Inheritance diagram for ArraySortRef:

Public Member Functions

def domain
def range

Detailed Description

Arrays.

Array sorts.

Definition at line 3822 of file z3py.py.


Member Function Documentation

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

>>> A = ArraySort(IntSort(), BoolSort())
>>> A.domain()
Int

Definition at line 3825 of file z3py.py.

03825 
03826     def domain(self):
03827         """Return the domain of the array sort `self`.
03828         
03829         >>> A = ArraySort(IntSort(), BoolSort())
03830         >>> A.domain()
03831         Int
03832         """
03833         return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx)
    
def range (   self)
Return the range of the array sort `self`.

>>> A = ArraySort(IntSort(), BoolSort())
>>> A.range()
Bool

Definition at line 3834 of file z3py.py.

03834 
03835     def range(self):
03836         """Return the range of the array sort `self`.
03837         
03838         >>> A = ArraySort(IntSort(), BoolSort())
03839         >>> A.range()
03840         Bool
03841         """
03842         return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)

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