From a9f5c2f864efd10ef18fac438b5cd4504ea63866 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Dec 2015 15:01:46 -0800 Subject: [PATCH] seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 101 ++++++++++++++++++++++++++++++ src/ast/seq_decl_plugin.h | 13 +++- 2 files changed, 112 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 96590a40a..a46d4207b 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -20,6 +20,7 @@ Notes: #include"seq_rewriter.h" #include"arith_decl_plugin.h" #include"ast_pp.h" +#include"ast_util.h" br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { @@ -186,6 +187,21 @@ br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) { result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str())); return BR_DONE; } + // check if subsequence of a is in b. + ptr_vector as, bs; + m_util.str.get_concat(a, as); + m_util.str.get_concat(b, bs); + bool found = false; + for (unsigned i = 0; !found && i < bs.size(); ++i) { + if (as.size() > bs.size() - i) break; + unsigned j = 0; + for (; j < as.size() && as[j] == bs[i+j]; ++j) {}; + found = j == as.size(); + } + if (found) { + result = m().mk_true(); + return BR_DONE; + } return BR_FAILED; } @@ -275,6 +291,80 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { result = m().mk_true(); return BR_DONE; } + expr* a1 = m_util.str.get_leftmost_concat(a); + expr* b1 = m_util.str.get_leftmost_concat(b); + isc1 = m_util.str.is_string(a1, s1); + isc2 = m_util.str.is_string(b1, s2); + ptr_vector as, bs; + + if (a1 != b1 && isc1 && isc2) { + if (s1.length() <= s2.length()) { + if (strncmp(s1.c_str(), s2.c_str(), s1.length()) == 0) { + if (a == a1) { + result = m().mk_true(); + return BR_DONE; + } + m_util.str.get_concat(a, as); + m_util.str.get_concat(b, bs); + SASSERT(as.size() > 1); + s2 = std::string(s2.c_str() + s1.length(), s2.length() - s1.length()); + bs[0] = m_util.str.mk_string(s2); + m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1), + m_util.str.mk_concat(bs.size(), bs.c_ptr())); + return BR_REWRITE_FULL; + } + else { + result = m().mk_false(); + return BR_DONE; + } + } + else { + if (strncmp(s1.c_str(), s2.c_str(), s2.length()) == 0) { + if (b == b1) { + result = m().mk_false(); + return BR_DONE; + } + m_util.str.get_concat(a, as); + m_util.str.get_concat(b, bs); + SASSERT(bs.size() > 1); + s1 = std::string(s1.c_str() + s2.length(), s1.length() - s2.length()); + as[0] = m_util.str.mk_string(s1); + m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr()), + m_util.str.mk_concat(bs.size()-1, bs.c_ptr()+1)); + return BR_REWRITE_FULL; + } + else { + result = m().mk_false(); + return BR_DONE; + } + } + } + if (a1 != b1) { + return BR_FAILED; + } + m_util.str.get_concat(a, as); + m_util.str.get_concat(b, bs); + unsigned i = 0; + for (; i < as.size() && i < bs.size() && as[i] == bs[i]; ++i) {}; + if (i == as.size()) { + result = m().mk_true(); + return BR_DONE; + } + if (i == bs.size()) { + expr_ref_vector es(m()); + for (unsigned j = i; j < as.size(); ++i) { + es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j])); + } + result = mk_and(es); + return BR_REWRITE3; + } + if (i > 0) { + a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i); + b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i); + result = m_util.str.mk_prefix(a, b); + return BR_DONE; + } + UNREACHABLE(); return BR_FAILED; } @@ -293,6 +383,17 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { result = m().mk_true(); return BR_DONE; } + if (m_util.str.is_empty(b)) { + result = m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), a); + return BR_REWRITE3; + } + // concatenation is left-associative, so a2, b2 are not concatenations + expr* a1, *a2, *b1, *b2; + if (m_util.str.is_concat(a, a1, a2) && + m_util.str.is_concat(b, b1, b2) && a2 == b2) { + result = m_util.str.mk_suffix(a1, b1); + return BR_REWRITE1; + } return BR_FAILED; } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c61e3cc43..8cef2e391 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -164,13 +164,19 @@ public: public: str(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {} + sort* mk_seq(sort* s) { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, ¶m); } + app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); } app* mk_string(symbol const& s); app* mk_string(char const* s) { return mk_string(symbol(s)); } app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); } app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); } + expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); } app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); } app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); } - app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); } + app* mk_contains(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); } + app* mk_prefix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_PREFIX, 2, es); } + app* mk_suffix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); } + bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); } @@ -181,7 +187,9 @@ public: return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true); } - bool is_empty(expr const* n) const { symbol s; return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && strcmp(s.bare_str(),"") == 0); } + bool is_empty(expr const* n) const { symbol s; + return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); + } bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); } bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); } bool is_extract(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); } @@ -210,6 +218,7 @@ public: MATCH_BINARY(is_in_re); void get_concat(expr* e, ptr_vector& es) const; + expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; } }; class re {