From d695767f61f752ca8aecfe53792dd0fd1b90ec1e Mon Sep 17 00:00:00 2001 From: bannsec Date: Mon, 18 Dec 2017 21:48:54 +0000 Subject: [PATCH] Allowing slices and negative index in assertions --- src/api/python/z3/z3.py | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 3bf48b611..4cc401156 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -5140,9 +5140,18 @@ class AstVector(Z3PPObject): >>> A[1] y """ - if i >= self.__len__(): - raise IndexError - return _to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, i), self.ctx) + + if isinstance(i, int): + 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): """Update AST at position `i`.