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