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

Arrays. More...

+ Inheritance diagram for ArraySortRef:

Public Member Functions

def domain
 
def range
 
- Public Member Functions inherited from SortRef
def as_ast
 
def get_id
 
def kind
 
def subsort
 
def cast
 
def name
 
def __eq__
 
def __ne__
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __str__
 
def __repr__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def hash
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

Additional Inherited Members

- Data Fields inherited from AstRef
 ast
 
 ctx
 

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.

Referenced by ArrayRef.__getitem__().

3826  def domain(self):
3827  """Return the domain of the array sort `self`.
3828 
3829  >>> A = ArraySort(IntSort(), BoolSort())
3830  >>> A.domain()
3831  Int
3832  """
3833  return _to_sort_ref(Z3_get_array_sort_domain(self.ctx_ref(), self.ast), self.ctx)
Z3_sort Z3_API Z3_get_array_sort_domain(__in Z3_context c, __in Z3_sort t)
Return the domain of the given array sort.
def ctx_ref
Definition: z3py.py:305
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.

3835  def range(self):
3836  """Return the range of the array sort `self`.
3837 
3838  >>> A = ArraySort(IntSort(), BoolSort())
3839  >>> A.range()
3840  Bool
3841  """
3842  return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)
Z3_sort Z3_API Z3_get_array_sort_range(__in Z3_context c, __in Z3_sort t)
Return the range of the given array sort.
def ctx_ref
Definition: z3py.py:305