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 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 3859 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 3862 of file z3py.py.

3863  def domain(self):
3864  """Return the domain of the array sort `self`.
3865 
3866  >>> A = ArraySort(IntSort(), BoolSort())
3867  >>> A.domain()
3868  Int
3869  """
3870  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.
def ctx_ref
Definition: z3py.py:304
def range (   self)
Return the range of the array sort `self`.

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

Definition at line 3871 of file z3py.py.

3872  def range(self):
3873  """Return the range of the array sort `self`.
3874 
3875  >>> A = ArraySort(IntSort(), BoolSort())
3876  >>> A.range()
3877  Bool
3878  """
3879  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:304