diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 9129cb854..1a9ef204b 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -931,9 +931,9 @@ def _to_expr_ref(a, ctx): if sk == Z3_ROUNDING_MODE_SORT: return FPRMRef(a, ctx) if sk == Z3_SEQ_SORT: - return SeqRef(a, ctx) + return SeqRef(a, ctx) if sk == Z3_RE_SORT: - return ReRef(a, ctx) + return ReRef(a, ctx) return ExprRef(a, ctx) def _coerce_expr_merge(s, a): @@ -3573,24 +3573,24 @@ def Concat(*args): ctx = args[0].ctx if is_seq(args[0]): - if __debug__: - _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") - v = (Ast * sz)() + 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() - 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 __debug__: - _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") - v = (Ast * sz)() - for i in range(sz): - v[i] = args[i].as_ast() - return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx) - + if __debug__: + _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") + v = (Ast * sz)() + for i in range(sz): + v[i] = args[i].as_ast() + return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx) + if __debug__: _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") - r = args[0] + r = args[0] for i in range(sz - 1): r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx) return r @@ -3607,14 +3607,14 @@ def Extract(high, low, a): "c" """ if isinstance(high, str): - high = StringVal(high) + high = StringVal(high) if is_seq(high): - s = high - offset = _py2expr(low, high.ctx) - length = _py2expr(a, high.ctx) - - if __debug__: - _z3_assert(is_int(offset) and is_int(length), "Second and third arguments must be integers") + s = high + offset = _py2expr(low, high.ctx) + length = _py2expr(a, high.ctx) + + if __debug__: + _z3_assert(is_int(offset) and is_int(length), "Second and third arguments must be integers") return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) if __debug__: _z3_assert(low <= high, "First argument must be greater than or equal to second argument") @@ -8951,15 +8951,15 @@ class SeqSortRef(SortRef): """Sequence sort.""" def is_string(self): - """Determine if sort is a string - >>> s = StringSort() - >>> s.is_string() - True - >>> s = SeqSort(IntSort()) - >>> s.is_string() - False - """ - return Z3_is_string_sort(self.ctx_ref(), self.ast) + """Determine if sort is a string + >>> s = StringSort() + >>> s.is_string() + True + >>> s = SeqSort(IntSort()) + >>> s.is_string() + False + """ + return Z3_is_string_sort(self.ctx_ref(), self.ast) def StringSort(ctx=None): """Create a string sort @@ -8983,19 +8983,19 @@ class SeqRef(ExprRef): """Sequence expression.""" def sort(self): - return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) + return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) def __add__(self, other): - return Concat(self, other) + return Concat(self, other) def __getitem__(self, i): - 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): - return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast())) + return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast())) def is_string_value(self): - return Z3_is_string(self.ctx_ref(), self.as_ast()) + return Z3_is_string(self.ctx_ref(), self.as_ast()) def as_string(self): """Return a string representation of sequence expression.""" @@ -9004,17 +9004,17 @@ class SeqRef(ExprRef): def _coerce_seq(s, ctx=None): if isinstance(s, str): - ctx = _get_ctx(ctx) - s = StringVal(s, ctx) + ctx = _get_ctx(ctx) + s = StringVal(s, ctx) return s def _get_ctx2(a, b, ctx=None): if is_expr(a): - return a.ctx + return a.ctx if is_expr(b): - return b.ctx + return b.ctx if ctx is None: - ctx = main_ctx() + ctx = main_ctx() return ctx def is_seq(a): @@ -9136,7 +9136,7 @@ def Replace(s, src, dst): """ ctx = _get_ctx2(dst, s) if ctx is None and is_expr(src): - ctx = src.ctx + ctx = src.ctx src = _coerce_seq(src, ctx) dst = _coerce_seq(dst, ctx) s = _coerce_seq(s, ctx) @@ -9154,12 +9154,12 @@ def IndexOf(s, substr, offset): """ ctx = None if is_expr(offset): - ctx = offset.ctx + ctx = offset.ctx ctx = _get_ctx2(s, substr, ctx) s = _coerce_seq(s, ctx) substr = _coerce_seq(substr, ctx) if isinstance(offset, int): - offset = IntVal(offset, ctx) + offset = IntVal(offset, ctx) return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx) def Length(s): @@ -9191,10 +9191,10 @@ class ReSortRef(SortRef): def ReSort(s): if is_ast(s): - return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.as_ast()), ctx) + return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.as_ast()), ctx) if s is None or isinstance(s, Context): - ctx = _get_ctx(s) - return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), ctx) + ctx = _get_ctx(s) + return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), ctx) raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument") @@ -9202,7 +9202,7 @@ class ReRef(ExprRef): """Regular expressions.""" def __add__(self, other): - return Union(self, other) + return Union(self, other) def is_re(s): @@ -9232,13 +9232,12 @@ def Union(*args): sz = len(args) if __debug__: _z3_assert(sz >= 2, "At least two arguments expected.") - _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") + _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") ctx = args[0].ctx v = (Ast * sz)() for i in range(sz): - v[i] = args[i].as_ast() + v[i] = args[i].as_ast() return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx) - def Plus(re): """Create the regular expression accepting one or more repetitions of argument.