mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

Allowing slices and negative index in assertions

Browse source
This commit is contained in:
bannsec 2017-12-18 21:48:54 +00:00
parent 94d1695b01
commit d695767f61
1 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/api/python/z3/z3.py
View file

@ -5140,9 +5140,18 @@ class AstVector(Z3PPObject):
>>> A[1] >>> A[1]
y y
""" """
if i >= self.__len__():
raise IndexError if isinstance(i, int):
return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx) if i < 0:
i += self.__len__()
if i >= self.__len__():
raise IndexError
return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx)
elif isinstance(i, slice):
return [_to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, ii), self.ctx) for ii in range(*i.indices(self.__len__()))]
def __setitem__(self, i, v): def __setitem__(self, i, v):
"""Update AST at position `i`. """Update AST at position `i`.