Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator 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__
 
def __hash__
 
- Public Member Functions inherited from AstRef
def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
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 4206 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 4209 of file z3py.py.

Referenced by ArrayRef.__getitem__().

4210  def domain(self):
4211  """Return the domain of the array sort `self`.
4212 
4213  >>> A = ArraySort(IntSort(), BoolSort())
4214  >>> A.domain()
4215  Int
4216  """
4217  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(Z3_context c, Z3_sort t)
Return the domain of the given array sort. In the case of a multi-dimensional array, this function returns the sort of the first dimension.
def ctx_ref
Definition: z3py.py:352
def range (   self)
Return the range of the array sort `self`.

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

Definition at line 4218 of file z3py.py.

4219  def range(self):
4220  """Return the range of the array sort `self`.
4221 
4222  >>> A = ArraySort(IntSort(), BoolSort())
4223  >>> A.range()
4224  Bool
4225  """
4226  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(Z3_context c, Z3_sort t)
Return the range of the given array sort.
def ctx_ref
Definition: z3py.py:352