Public Member Functions | |
def | sort |
def | domain |
def | range |
def | __getitem__ |
def __getitem__ | ( | self, | |
arg | |||
) |
Return the Z3 expression `self[arg]`. >>> a = Array('a', IntSort(), BoolSort()) >>> i = Int('i') >>> a[i] a[i] >>> a[i].sexpr() '(select a i)'
Definition at line 3873 of file z3py.py.
03873 03874 def __getitem__(self, arg): 03875 """Return the Z3 expression `self[arg]`. 03876 03877 >>> a = Array('a', IntSort(), BoolSort()) 03878 >>> i = Int('i') 03879 >>> a[i] 03880 a[i] 03881 >>> a[i].sexpr() 03882 '(select a i)' 03883 """ 03884 arg = self.domain().cast(arg) 03885 return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
def domain | ( | self | ) |
Shorthand for `self.sort().domain()`. >>> a = Array('a', IntSort(), BoolSort()) >>> a.domain() Int
Definition at line 3855 of file z3py.py.
Referenced by ArrayRef.__getitem__().
def range | ( | self | ) |
Shorthand for `self.sort().range()`. >>> a = Array('a', IntSort(), BoolSort()) >>> a.range() Bool
def sort | ( | self | ) |
Return the array sort of the array expression `self`. >>> a = Array('a', IntSort(), BoolSort()) >>> a.sort() Array(Int, Bool)
Reimplemented from ExprRef.
Definition at line 3846 of file z3py.py.
Referenced by ArrayRef.domain(), and ArrayRef.range().
03846 03847 def sort(self): 03848 """Return the array sort of the array expression `self`. 03849 03850 >>> a = Array('a', IntSort(), BoolSort()) 03851 >>> a.sort() 03852 Array(Int, Bool) 03853 """ 03854 return ArraySortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)