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

add some conveniences for expressing string constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-08 16:19:32 -08:00
parent e1ade258a0
commit 03cef7b03c
1 changed files with 17 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3572,15 +3572,19 @@ def Concat(*args):
if __debug__: if __debug__:
_z3_assert(sz >= 2, "At least two arguments expected.") _z3_assert(sz >= 2, "At least two arguments expected.")
ctx = args[0].ctx ctx = None
for a in args:
if is_seq(args[0]): if is_expr(a):
if __debug__: ctx = a.ctx
_z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") break
v = (Ast * sz)() if is_seq(args[0]) or isinstance(args[0], str):
for i in range(sz): args = [_coerce_seq(s, ctx) for s in args]
if __debug__:
_z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
v = (Ast * sz)()
for i in range(sz):
v[i] = args[i].as_ast() v[i] = args[i].as_ast()
return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
if is_re(args[0]): if is_re(args[0]):
if __debug__: if __debug__:
@ -9066,7 +9070,12 @@ class SeqRef(ExprRef):
def __add__(self, other): def __add__(self, other):
return Concat(self, other) return Concat(self, other)
def __radd__(self, other):
return Concat(other, self)
def __getitem__(self, i): def __getitem__(self, i):
if _is_int(i):
i = IntVal(i, self.ctx)
return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
def is_string(self): def is_string(self):