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

Detailed Description


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()

Definition at line 3717 of file z3py.py.

3718  def domain(self):
3719  """Return the domain of the array sort `self`.
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()

Definition at line 3726 of file z3py.py.

3727  def range(self):
3728  """Return the range of the array sort `self`.
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)