From b5969326bc5a771f9739ac6a8087e41fd6eb7b87 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Jan 2016 23:31:36 -0800 Subject: [PATCH] seq API Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 129 ++++++++++++++++++++++++------ src/api/z3_api.h | 2 +- src/ast/rewriter/seq_rewriter.cpp | 3 +- 3 files changed, 107 insertions(+), 27 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 802108163..409d511ef 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8959,11 +8959,8 @@ class SeqRef(ExprRef): def sort(self): return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) - def __add__(self, other): - v = (Ast * 2)() - v[0] = self.as_ast() - v[1] = other.as_ast() - return SeqRef(Z3_mk_seq_concat(self.ctx_ref(), 2, v), self.ctx) + def __add__(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) @@ -8985,23 +8982,36 @@ def _coerce_seq(s, ctx=None): s = String(s, ctx) return s -def _get_ctx2(a, b): +def _get_ctx2(a, b, ctx=None): if is_expr(a): return a.ctx if is_expr(b): return b.ctx - return None + return ctx def is_seq(a): - """Return `True` if `a` is a Z3 sequence expression.""" + """Return `True` if `a` is a Z3 sequence expression. + >>> print (is_seq(Unit(IntVal(0)))) + True + >>> print (is_seq(String("abc"))) + True + """ return isinstance(a, SeqRef) def is_string_sort(a): - """Return `True` if `a` is a Z3 string expression.""" + """Return `True` if `a` is a Z3 string expression. + >>> print (is_string_sort(String("ab"))) + True + """ return isinstance(a, SeqRef) and a.is_string_sort() def is_string_value(a): - """return 'True' if 'a' is a Z3 string constant expression.""" + """return 'True' if 'a' is a Z3 string constant expression. + >>> print (is_string_value(String("a"))) + True + >>> print (is_string_value(String("a") + String("b"))) + False + """ return isinstance(a, SeqRef) and a.is_string_value() def String(s, ctx=None): @@ -9028,21 +9038,42 @@ def Unit(a): return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx) def PrefixOf(a, b): - """Check if 'a' is a prefix of 'b'""" + """Check if 'a' is a prefix of 'b' + >>> s1 = PrefixOf("ab", "abc") + >>> print (simplify(s1)) + True + >>> s2 = PrefixOf("bc", "abc") + >>> print (simplify(s2)) + False + """ ctx = _get_ctx2(a, b) a = _coerce_seq(a, ctx) b = _coerce_seq(b, ctx) return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) def SuffixOf(a, b): - """Check if 'a' is a suffix of 'b'""" + """Check if 'a' is a suffix of 'b' + >>> s1 = SuffixOf("ab", "abc") + >>> print (simplify(s1)) + False + >>> s2 = SuffixOf("bc", "abc") + >>> print (simplify(s2)) + True + """ ctx = _get_ctx2(a, b) a = _coerce_seq(a, ctx) b = _coerce_seq(b, ctx) return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx) def Contains(a, b): - """Check if 'a' contains 'b'""" + """Check if 'a' contains 'b' + >>> s1 = Contains("abc", "ab") + >>> print (simplify(s1)) + True + >>> s2 = SuffixOf("abc", "bc") + >>> print (simplify(s2)) + True + """ ctx = _get_ctx2(a, b) a = _coerce_seq(a, ctx) b = _coerce_seq(b, ctx) @@ -9052,20 +9083,34 @@ def Contains(a, b): # """Extract a sequence at offset with indicated length""" # return SeqRef(Z3_mk_seq_extract(a.ctx_ref(), a.as_ast(), offset.as_ast()), length.ctx) -def Replace(src, dst, s): - """Replace the first occurrence of 'src' by 'dst' in 's'""" - ctx = _get_ctx2(src, _get_ctx2(dst, s)) +def Replace(s, src, dst): + """Replace the first occurrence of 'src' by 'dst' in 's' + >>> r = Replace("aaa", "a", "b") + >>> print (simplify(r)) + "baa" + """ + ctx = _get_ctx2(dst, s) + if ctx is None and is_expr(src): + ctx = src.ctx src = _coerce_seq(src, ctx) dst = _coerce_seq(dst, ctx) s = _coerce_seq(s, ctx) - return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), src.as_ast(), dst.as_ast()), s.ctx) + return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx) def Length(s): - """Obtain the length of a sequence 's'""" - return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast(), s.ctx)) + """Obtain the length of a sequence 's' + >>> l = Length(String("abc")) + >>> print (simplify(l)) + 3 + """ + return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx) def Re(s, ctx=None): - """The regular expression that accepts sequence 's'""" + """The regular expression that accepts sequence 's' + >>> s1 = Re("ab") + >>> s2 = Re(String("ab")) + >>> s3 = Re(Unit(BoolVal(True))) + """ s = _coerce_seq(s, ctx) return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx) @@ -9090,20 +9135,45 @@ def ReSort(s): class ReRef(ExprRef): """Regular expressions.""" - def __add__(self, other): - v = (Ast * 2)() - v[0] = self.as_ast() - v[1] = other.as_ast() - return SeqRef(Z3_mk_re_union(self.ctx_ref(), 2, v), self.ctx) + def __add__(self, other): + return Union(self, other) def is_re(s): return isinstance(s, ReRef) + def InRe(s, re): + """Create regular expression membership test + >>> re = Union(Re("a"),Re("b")) + >>> print (simplify(InRe("a", re))) + True + >>> print (simplify(InRe("b", re))) + True + >>> print (simplify(InRe("c", re))) + False + """ s = _coerce_seq(s, re.ctx) return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx) +def Union(*args): + """Create union of regular expressions. + >>> re = Union(Re("a"), Re("b"), Re("c")) + >>> print (simplify(InRe("d", re))) + False + """ + args = _get_args(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.") + ctx = args[0].ctx + v = (Ast * sz)() + for i in range(sz): + 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. >>> re = Plus(Re("a")) @@ -9117,6 +9187,15 @@ def Plus(re): return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx) def Option(re): + """Create the regular expression that optionally accepts the argument. + >>> re = Option(Re("a")) + >>> print(simplify(InRe("a", re))) + True + >>> print(simplify(InRe("", re))) + True + >>> print(simplify(InRe("aa", re))) + False + """ return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx) def Star(re): diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e00134c06..fab272499 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3251,7 +3251,7 @@ extern "C" { def_API('Z3_mk_seq_replace' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) */ - Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast src, Z3_ast dst, Z3_ast s); + Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst); /** \brief Retrieve from \s the unit sequence positioned at position \c index. diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 2db2391d9..8f6aa6fca 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -822,7 +822,8 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) { br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) { sort* s; VERIFY(m_util.is_re(a, s)); - result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(s)), a); + sort_ref seq(m_util.str.mk_seq(s), m()); + result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(seq)), a); return BR_REWRITE1; }