From aeb4d1864dc3583585c6bb87eeb3431c3a17cefb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Nov 2018 11:39:34 -0800 Subject: [PATCH] clean up suffix/prefix rewriting Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 108 ++++++++++++++++-------------- src/ast/seq_decl_plugin.cpp | 5 ++ src/ast/seq_decl_plugin.h | 1 + 3 files changed, 65 insertions(+), 49 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 6503bdcb9..04ab51538 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -694,7 +694,7 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { } if (as.empty()) { - result = m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b))); + result = m_util.str.mk_is_empty(b); return BR_REWRITE2; } @@ -729,7 +729,7 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { for (; offs < as.size() && cannot_contain_prefix(as[offs].get(), b0); ++offs) {} for (; sz > offs && cannot_contain_suffix(as.get(sz-1), bL); --sz) {} if (offs == sz) { - result = m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b))); + result = m_util.str.mk_is_empty(b); return BR_REWRITE2; } if (offs > 0 || sz < as.size()) { @@ -914,25 +914,23 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { } } } - m_util.str.get_concat(a, as); - m_util.str.get_concat(b, bs); + m_util.str.get_concat_units(a, as); + m_util.str.get_concat_units(b, bs); unsigned i = 0; expr_ref_vector eqs(m()); for (; i < as.size() && i < bs.size(); ++i) { - expr* a = as[i].get(), *b = bs[i].get(); - if (a == b) { + expr* ai = as.get(i), *bi = bs.get(i); + if (m().are_equal(ai, bi)) { continue; } - if (m_util.str.is_unit(a) && m_util.str.is_unit(b)) { - eqs.push_back(m().mk_eq(a, b)); - continue; - } - if (m().is_value(a) && m().is_value(b) && m_util.str.is_string(a) && m_util.str.is_string(b)) { - TRACE("seq", tout << mk_pp(a, m()) << " != " << mk_pp(b, m()) << "\n";); + if (m().are_distinct(ai, bi)) { result = m().mk_false(); return BR_DONE; } - + if (m_util.str.is_unit(ai) && m_util.str.is_unit(bi)) { + eqs.push_back(m().mk_eq(ai, bi)); + continue; + } break; } if (i == as.size()) { @@ -943,7 +941,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { SASSERT(i < as.size()); if (i == bs.size()) { for (unsigned j = i; j < as.size(); ++j) { - eqs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get())); + eqs.push_back(m_util.str.mk_is_empty(as.get(j))); } result = mk_and(eqs); TRACE("seq", tout << result << "\n";); @@ -953,13 +951,13 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { SASSERT(i < as.size() && i < bs.size()); 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); + eqs.push_back(m_util.str.mk_prefix(a, b)); + result = mk_and(eqs); TRACE("seq", tout << result << "\n";); - return BR_DONE; - } - else { - return BR_FAILED; + return BR_REWRITE3; } + + return BR_FAILED; } br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { @@ -973,7 +971,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { return BR_DONE; } if (m_util.str.is_empty(b)) { - result = m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), a); + result = m_util.str.mk_is_empty(a); return BR_REWRITE3; } @@ -1039,36 +1037,48 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { } } } - expr_ref_vector as(m()), bs(m()); - m_util.str.get_concat(a, as); - m_util.str.get_concat(b, bs); - bool change = false; - while (as.size() > 0 && bs.size() > 0 && as.back() == bs.back()) { - as.pop_back(); - bs.pop_back(); - change = true; - } - if (as.size() > 0 && bs.size() > 0 && m().is_value(as.back()) && m().is_value(bs.back())) { - result = m().mk_false(); - return BR_DONE; - } - if (change) { - // suffix("", bs) <- true - if (as.empty()) { - result = m().mk_true(); + expr_ref_vector as(m()), bs(m()), eqs(m()); + m_util.str.get_concat_units(a, as); + m_util.str.get_concat_units(b, bs); + unsigned i = 1, sza = as.size(), szb = bs.size(); + for (; i <= sza && i <= szb; ++i) { + expr* ai = as.get(sza-i), *bi = bs.get(szb-i); + if (m().are_equal(ai, bi)) { + continue; + } + if (m().are_distinct(ai, bi)) { + result = m().mk_false(); return BR_DONE; } - // suffix(as, "") iff as = "" - if (bs.empty()) { - for (unsigned j = 0; j < as.size(); ++j) { - bs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get())); - } - result = mk_and(bs); - return BR_REWRITE3; + if (m_util.str.is_unit(ai) && m_util.str.is_unit(bi)) { + eqs.push_back(m().mk_eq(ai, bi)); + continue; } - result = m_util.str.mk_suffix(m_util.str.mk_concat(as.size(), as.c_ptr()), - m_util.str.mk_concat(bs.size(), bs.c_ptr())); - return BR_DONE; + break; + } + if (i > sza) { + result = mk_and(eqs); + TRACE("seq", tout << result << "\n";); + return BR_REWRITE3; + } + if (i > szb) { + for (unsigned j = i; j <= sza; ++j) { + expr* aj = as.get(sza-j); + eqs.push_back(m_util.str.mk_is_empty(aj)); + } + result = mk_and(eqs); + TRACE("seq", tout << result << "\n";); + return BR_REWRITE3; + } + + if (i > 1) { + SASSERT(i <= sza && i <= szb); + a = m_util.str.mk_concat(sza - i + 1, as.c_ptr()); + b = m_util.str.mk_concat(szb - i + 1, bs.c_ptr()); + eqs.push_back(m_util.str.mk_suffix(a, b)); + result = mk_and(eqs); + TRACE("seq", tout << result << "\n";); + return BR_REWRITE3; } return BR_FAILED; @@ -1226,7 +1236,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { TRACE("seq", tout << seq << "\n";); if (seq.empty()) { - result = m().mk_eq(a, m_util.str.mk_empty(m().get_sort(a))); + result = m_util.str.mk_is_empty(a); } else { result = m().mk_eq(a, m_util.str.mk_concat(seq)); @@ -1888,7 +1898,7 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) { disj.push_back(m_util.str.mk_contains(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i), b)); return true; } - disj.push_back(m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b)))); + disj.push_back(m_util.str.mk_is_empty(b)); return true; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 5a01b63bb..4bcc664a4 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -987,6 +987,11 @@ void seq_util::str::get_concat_units(expr* e, expr_ref_vector& es) const { } } +app* seq_util::str::mk_is_empty(expr* s) const { + return m.mk_eq(mk_empty(get_sort(s)), s); +} + + app* seq_util::re::mk_loop(expr* r, unsigned lo) { parameter param(lo); return m.mk_app(m_fid, OP_RE_LOOP, 1, ¶m, 1, &r); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 80b432f3e..52a764dde 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -252,6 +252,7 @@ public: app* mk_char(zstring const& s, unsigned idx) const; app* mk_itos(expr* i) const { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); } app* mk_stoi(expr* s) const { return m.mk_app(m_fid, OP_STRING_STOI, 1, &s); } + app* mk_is_empty(expr* s) const; bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }