From 40e9e4c7f85ba7e8387228e9180fb837f995eed2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Dec 2015 10:44:19 -0800 Subject: [PATCH] more rewrites Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 95 +++++++++++++++++++++++++++---- src/ast/rewriter/seq_rewriter.h | 1 + src/ast/seq_decl_plugin.cpp | 9 +++ src/ast/seq_decl_plugin.h | 5 ++ 4 files changed, 98 insertions(+), 12 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 2568639c3..d9ed8f6e0 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -115,22 +115,75 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con return BR_FAILED; } +/* + string + string = string + a + (b + c) = (a + b) + c + a + "" = a + "" + a = a + (a + string) + string = a + string +*/ br_status seq_rewriter::mk_str_concat(expr* a, expr* b, expr_ref& result) { - std::string c, d; - if (m_util.str.is_const(a, c) && m_util.str.is_const(b, d)) { - result = m_util.str.mk_string(c + d); + std::string s1, s2; + expr* c, *d; + bool isc1 = m_util.str.is_const(a, s1); + bool isc2 = m_util.str.is_const(b, s2); + if (isc1 && isc2) { + result = m_util.str.mk_string(s1 + s2); + return BR_DONE; + } + if (m_util.str.is_concat(b, c, d)) { + result = m_util.str.mk_concat(m_util.str.mk_concat(a, c), d); + return BR_REWRITE2; + } + if (isc1 && s1.length() == 0) { + result = b; + return BR_DONE; + } + if (isc2 && s2.length() == 0) { + result = a; + return BR_DONE; + } + if (m_util.str.is_concat(a, c, d) && + m_util.str.is_const(d, s1) && isc2) { + result = m_util.str.mk_string(s1 + s2); return BR_DONE; } return BR_FAILED; } + br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) { std::string b; - if (m_util.str.is_const(a, b)) { + m_es.reset(); + m_util.str.get_concat(a, m_es); + unsigned len = 0; + unsigned j = 0; + for (unsigned i = 0; i < m_es.size(); ++i) { + if (m_util.str.is_const(m_es[i], b)) { + len += b.length(); + } + else { + m_es[j] = m_es[i]; + ++j; + } + } + if (j == 0) { result = m_autil.mk_numeral(rational(b.length()), true); return BR_DONE; } + if (j != m_es.size()) { + expr_ref_vector es(m()); + for (unsigned i = 0; i < j; ++i) { + es.push_back(m_util.str.mk_length(m_es[i])); + } + if (len != 0) { + es.push_back(m_autil.mk_numeral(rational(len), true)); + } + result = m_autil.mk_add(es.size(), es.c_ptr()); + return BR_DONE; + } return BR_FAILED; } + br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result) { std::string s; rational pos, len; @@ -151,6 +204,7 @@ br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) { } return BR_FAILED; } + br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) { std::string c; rational r; @@ -166,10 +220,14 @@ br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) { } return BR_FAILED; } + br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result) { std::string s1, s2; rational r; - if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && m_autil.is_numeral(c, r) && r.is_unsigned()) { + bool isc1 = m_util.str.is_const(a, s1); + bool isc2 = m_util.str.is_const(b, s2); + + if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) { for (unsigned i = r.get_unsigned(); i < s1.length(); ++i) { if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) { result = m_autil.mk_numeral(rational(i) - r, true); @@ -179,15 +237,23 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu result = m_autil.mk_numeral(rational(-1), true); return BR_DONE; } - if (m_util.str.is_const(b, s2) && s2.length() == 0) { + if (m_autil.is_numeral(c, r) && r.is_neg()) { + result = m_autil.mk_numeral(rational(-1), true); + return BR_DONE; + } + + if (isc2 && s2.length() == 0) { result = c; return BR_DONE; } + // Enhancement: walk segments of a, determine which segments must overlap, must not overlap, may overlap. return BR_FAILED; } + br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) { std::string s1, s2, s3; - if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && m_util.str.is_const(c, s3)) { + if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && + m_util.str.is_const(c, s3)) { std::ostringstream buffer; for (unsigned i = 0; i < s1.length(); ) { if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) { @@ -206,12 +272,14 @@ br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& resu result = a; return BR_DONE; } - return BR_FAILED; } + br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) { std::string s1, s2; - if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2)) { + bool isc1 = m_util.str.is_const(a, s1); + bool isc2 = m_util.str.is_const(b, s2); + if (isc1 && isc2) { bool prefix = s1.length() <= s2.length(); for (unsigned i = 0; i < s1.length() && prefix; ++i) { prefix = s1[i] == s2[i]; @@ -219,15 +287,17 @@ br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) { result = m().mk_bool_val(prefix); return BR_DONE; } - if (m_util.str.is_const(a, s1) && s1.length() == 0) { + if (isc1 && s1.length() == 0) { result = m().mk_true(); return BR_DONE; } return BR_FAILED; } + br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) { std::string s1, s2; - if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2)) { + bool isc1 = m_util.str.is_const(a, s1); + if (isc1 && m_util.str.is_const(b, s2)) { bool suffix = s1.length() <= s2.length(); for (unsigned i = 0; i < s1.length() && suffix; ++i) { suffix = s1[s1.length() - i - 1] == s2[s2.length() - i - 1]; @@ -235,12 +305,13 @@ br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) { result = m().mk_bool_val(suffix); return BR_DONE; } - if (m_util.str.is_const(a, s1) && s1.length() == 0) { + if (isc1 && s1.length() == 0) { result = m().mk_true(); return BR_DONE; } return BR_FAILED; } + br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) { rational r; if (m_autil.is_numeral(a, r)) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index f2a152640..cefa451fa 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -32,6 +32,7 @@ Notes: class seq_rewriter { seq_util m_util; arith_util m_autil; + ptr_vector m_es; br_status mk_str_concat(expr* a, expr* b, expr_ref& result); br_status mk_str_length(expr* a, expr_ref& result); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 19b5b3321..4cd89285a 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -355,3 +355,12 @@ bool seq_decl_plugin::is_value(app* e) const { app* seq_util::str::mk_string(symbol const& s) { return u.seq.mk_string(s); } + +void seq_util::str::get_concat(expr* e, ptr_vector& es) const { + expr* e1, *e2; + while (is_concat(e, e1, e2)) { + get_concat(e1, es); + e = e2; + } + es.push_back(e); +} diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index b81f87ec0..4443b4bb2 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -181,6 +181,9 @@ public: bool is_const(expr const* n, std::string& s) const { return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol().str(), true); } + bool is_const(expr const* n, symbol& s) const { + return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true); + } bool is_string(sort* s) const { return is_sort_of(s, m_fid, STRING_SORT); } bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_CONCAT); } @@ -209,6 +212,8 @@ public: MATCH_UNARY(is_itos); MATCH_UNARY(is_stoi); MATCH_BINARY(is_in_regexp); + + void get_concat(expr* e, ptr_vector& es) const; }; class re {