|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
|
Z3
|
|
Inheritance diagram for AstVector:Public Member Functions | |
| def | __init__ |
| def | __del__ |
| def | __len__ |
| def | __getitem__ |
| def | __setitem__ |
| def | push |
| def | resize |
| def | __contains__ |
| def | translate |
| def | __repr__ |
| def | sexpr |
Data Fields | |
| vector | |
| ctx | |
| def __init__ | ( | self, | |
v = None, |
|||
ctx = None |
|||
| ) |
Definition at line 4804 of file z3py.py.
04804 04805 def __init__(self, v=None, ctx=None): 04806 self.vector = None 04807 if v == None: 04808 self.ctx = _get_ctx(ctx) 04809 self.vector = Z3_mk_ast_vector(self.ctx.ref()) 04810 else: 04811 self.vector = v 04812 assert ctx != None 04813 self.ctx = ctx 04814 Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
| def __del__ | ( | self | ) |
| def __contains__ | ( | self, | |
| item | |||
| ) |
Return `True` if the vector contains `item`.
>>> x = Int('x')
>>> A = AstVector()
>>> x in A
False
>>> A.push(x)
>>> x in A
True
>>> (x+1) in A
False
>>> A.push(x+1)
>>> (x+1) in A
True
>>> A
[x, x + 1]
Definition at line 4888 of file z3py.py.
04888 04889 def __contains__(self, item): 04890 """Return `True` if the vector contains `item`. 04891 04892 >>> x = Int('x') 04893 >>> A = AstVector() 04894 >>> x in A 04895 False 04896 >>> A.push(x) 04897 >>> x in A 04898 True 04899 >>> (x+1) in A 04900 False 04901 >>> A.push(x+1) 04902 >>> (x+1) in A 04903 True 04904 >>> A 04905 [x, x + 1] 04906 """ 04907 for elem in self: 04908 if elem.eq(item): 04909 return True 04910 return False
| def __getitem__ | ( | self, | |
| i | |||
| ) |
Return the AST at position `i`.
>>> A = AstVector()
>>> A.push(Int('x') + 1)
>>> A.push(Int('y'))
>>> A[0]
x + 1
>>> A[1]
y
Definition at line 4832 of file z3py.py.
04832 04833 def __getitem__(self, i): 04834 """Return the AST at position `i`. 04835 04836 >>> A = AstVector() 04837 >>> A.push(Int('x') + 1) 04838 >>> A.push(Int('y')) 04839 >>> A[0] 04840 x + 1 04841 >>> A[1] 04842 y 04843 """ 04844 if i >= self.__len__(): 04845 raise IndexError 04846 return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
| def __len__ | ( | self | ) |
Return the size of the vector `self`.
>>> A = AstVector()
>>> len(A)
0
>>> A.push(Int('x'))
>>> A.push(Int('x'))
>>> len(A)
2
Definition at line 4819 of file z3py.py.
Referenced by AstVector.__getitem__().
04819 04820 def __len__(self): 04821 """Return the size of the vector `self`. 04822 04823 >>> A = AstVector() 04824 >>> len(A) 04825 0 04826 >>> A.push(Int('x')) 04827 >>> A.push(Int('x')) 04828 >>> len(A) 04829 2 04830 """ 04831 return int(Z3_ast_vector_size(self.ctx.ref(), self.vector))
| def __repr__ | ( | self | ) |
| def __setitem__ | ( | self, | |
| i, | |||
| v | |||
| ) |
Update AST at position `i`.
>>> A = AstVector()
>>> A.push(Int('x') + 1)
>>> A.push(Int('y'))
>>> A[0]
x + 1
>>> A[0] = Int('x')
>>> A[0]
x
Definition at line 4847 of file z3py.py.
04847 04848 def __setitem__(self, i, v): 04849 """Update AST at position `i`. 04850 04851 >>> A = AstVector() 04852 >>> A.push(Int('x') + 1) 04853 >>> A.push(Int('y')) 04854 >>> A[0] 04855 x + 1 04856 >>> A[0] = Int('x') 04857 >>> A[0] 04858 x 04859 """ 04860 if i >= self.__len__(): 04861 raise IndexError 04862 Z3_ast_vector_set(self.ctx.ref(), self.vector, i, v.as_ast())
| def push | ( | self, | |
| v | |||
| ) |
Add `v` in the end of the vector.
>>> A = AstVector()
>>> len(A)
0
>>> A.push(Int('x'))
>>> len(A)
1
Definition at line 4863 of file z3py.py.
04863 04864 def push(self, v): 04865 """Add `v` in the end of the vector. 04866 04867 >>> A = AstVector() 04868 >>> len(A) 04869 0 04870 >>> A.push(Int('x')) 04871 >>> len(A) 04872 1 04873 """ 04874 Z3_ast_vector_push(self.ctx.ref(), self.vector, v.as_ast())
| def resize | ( | self, | |
| sz | |||
| ) |
Resize the vector to `sz` elements.
>>> A = AstVector()
>>> A.resize(10)
>>> len(A)
10
>>> for i in range(10): A[i] = Int('x')
>>> A[5]
x
Definition at line 4875 of file z3py.py.
04875 04876 def resize(self, sz): 04877 """Resize the vector to `sz` elements. 04878 04879 >>> A = AstVector() 04880 >>> A.resize(10) 04881 >>> len(A) 04882 10 04883 >>> for i in range(10): A[i] = Int('x') 04884 >>> A[5] 04885 x 04886 """ 04887 Z3_ast_vector_resize(self.ctx.ref(), self.vector, sz)
| def sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the vector.
Definition at line 4927 of file z3py.py.
Referenced by Fixedpoint.__repr__().
04927 04928 def sexpr(self): 04929 """Return a textual representation of the s-expression representing the vector.""" 04930 return Z3_ast_vector_to_string(self.ctx.ref(), self.vector)
| def translate | ( | self, | |
| other_ctx | |||
| ) |
Copy vector `self` to context `other_ctx`.
>>> x = Int('x')
>>> A = AstVector()
>>> A.push(x)
>>> c2 = Context()
>>> B = A.translate(c2)
>>> B
[x]
Definition at line 4911 of file z3py.py.
04911 04912 def translate(self, other_ctx): 04913 """Copy vector `self` to context `other_ctx`. 04914 04915 >>> x = Int('x') 04916 >>> A = AstVector() 04917 >>> A.push(x) 04918 >>> c2 = Context() 04919 >>> B = A.translate(c2) 04920 >>> B 04921 [x] 04922 """ 04923 return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx)
Definition at line 4804 of file z3py.py.
Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), ArrayRef.__getitem__(), AstVector.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Fixedpoint.add_rule(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), QuantifierRef.body(), BoolSortRef.cast(), DatatypeSortRef.constructor(), ApplyResult.convert_model(), ExprRef.decl(), RatNumRef.denominator(), FuncDeclRef.domain(), ArraySortRef.domain(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), SortRef.kind(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), RatNumRef.numerator(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Fixedpoint.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), Fixedpoint.statistics(), Solver.to_smt2(), Fixedpoint.update_rule(), QuantifierRef.var_name(), and QuantifierRef.var_sort().
Definition at line 4804 of file z3py.py.
Referenced by AstVector::__del__(), AstVector::__getitem__(), AstVector::__len__(), AstVector::__setitem__(), AstVector::push(), AstVector::resize(), AstVector::sexpr(), and AstVector::translate().
1.7.6.1