Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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 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 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 3714 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 3717 of file z3py.py.

3718  def domain(self):
3719  """Return the domain of the array sort `self`.
3720 
3721  >>> A = ArraySort(IntSort(), BoolSort())
3722  >>> A.domain()
3723  Int
3724  """
3725  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 3726 of file z3py.py.

3727  def range(self):
3728  """Return the range of the array sort `self`.
3729 
3730  >>> A = ArraySort(IntSort(), BoolSort())
3731  >>> A.range()
3732  Bool
3733  """
3734  return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)