more replace rewrites #4084

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 24, 2020 · 03ba268 · 03ba268
1 parent 7597396
commit 03ba268
Show file tree

Hide file tree

Showing 2 changed files with 56 additions and 0 deletions.
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
@@ -1410,6 +1410,61 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
         result = m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr(), sort_a);
         return BR_REWRITE1;
     }
+    m_lhs.reset();
+    m_rhs.reset();
+    m_util.str.get_concat_units(a, m_lhs);
+    m_util.str.get_concat_units(b, m_rhs);
+    if (m_rhs.empty()) {
+        result = m_util.str.mk_concat(c, a);
+        return BR_REWRITE1;
+    }
+
+    // is b a prefix of m_lhs at position i?
+
+    unsigned i = 0;
+    for (; i < m_lhs.size(); ++i) {
+        lbool is_prefix = l_true;
+        for (unsigned j = 0; j < m_rhs.size(); ++j) {
+            if (i + j >= m_lhs.size()) {                
+                expr_ref a1(m_util.str.mk_concat(i, m_lhs.c_ptr(), sort_a), m());
+                expr_ref a2(m_util.str.mk_concat(m_lhs.size()-i, m_lhs.c_ptr()+i, sort_a), m());
+                result = m().mk_ite(m().mk_eq(a2, b), m_util.str.mk_concat(a1, c), a);
+                return BR_REWRITE_FULL;
+            }
+            expr* b0 = m_rhs.get(j);
+            expr* a0 = m_lhs.get(i+j);
+            if (!m_util.str.is_unit(b0) || !m_util.str.is_unit(a0)) {
+                is_prefix = l_undef;
+                break;
+            }
+            if (m().are_equal(a0, b0))
+                continue;
+            if (m().are_distinct(a0, b0)) {
+                is_prefix = l_false;
+                break;
+            }
+            is_prefix = l_undef;
+            break;
+        }
+        if (is_prefix == l_undef)
+            break;
+        if (is_prefix == l_false)
+            continue;
+        expr_ref_vector es(m());
+        //std::cout << i << " " << m_lhs << "\n";
+        //std::cout << "rhs: " << m_rhs << "\n";
+        es.append(i, m_lhs.c_ptr());
+        es.push_back(c);
+        es.append(m_lhs.size()-i-m_rhs.size(), m_lhs.c_ptr()+i+m_rhs.size());
+        result = m_util.str.mk_concat(es, sort_a);
+        return BR_REWRITE_FULL;        
+    }
+    if (i > 0) {
+        expr_ref a1(m_util.str.mk_concat(i, m_lhs.c_ptr(), sort_a), m());
+        expr_ref a2(m_util.str.mk_concat(m_lhs.size()-i, m_lhs.c_ptr()+i, sort_a), m());
+        result = m_util.str.mk_concat(a1, m_util.str.mk_replace(a2, b, c));
+        return BR_REWRITE_FULL;        
+    }
 
     return BR_FAILED;
 }

diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
@@ -281,6 +281,7 @@ class seq_util {
         app* mk_suffix(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); }
         app* mk_index(expr* a, expr* b, expr* i) const { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); }
         app* mk_last_index(expr* a, expr* b) const { expr* es[2] = { a, b}; return m.mk_app(m_fid, OP_SEQ_LAST_INDEX, 2, es); }
+        app* mk_replace(expr* a, expr* b, expr* c) const { expr* es[3] = { a, b, c}; return m.mk_app(m_fid, OP_SEQ_REPLACE, 3, es); }
         app* mk_unit(expr* u) const { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); }
         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); }