mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 23:53:25 +00:00
Code Activity

Merge pull request #1410 from bannsec/assertion_slices

Browse source 
Allowing slices and negative index in assertions
This commit is contained in:
Nikolaj Bjorner 2017-12-18 17:07:09 -08:00 • committed by GitHub
commit d80c4307a6
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -5140,10 +5140,19 @@ class AstVector(Z3PPObject):
>>> A[1] >>> A[1]
y y
""" """
if isinstance(i, int):
if i < 0:
i += self.__len__()
if i >= self.__len__(): if i >= self.__len__():
raise IndexError raise IndexError
return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx) 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`.