From a74ef394ec98ee42daf1c69f251e036561f64ef6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 30 Jul 2020 10:19:32 -0700
Subject: [PATCH] some more rewrites

---
 src/ast/rewriter/seq_rewriter.cpp | 24 ++++++++++++++++++++++--
 src/ast/rewriter/seq_rewriter.h   |  1 +
 2 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 528c84502..88e9fde32 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -824,7 +824,6 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
         result = m_autil.mk_add(es.size(), es.c_ptr());
         return BR_REWRITE2;
     }
-#if 0
     expr* s = nullptr, *offset = nullptr, *length = nullptr;
     if (str().is_extract(a, s, offset, length)) {
         expr_ref len_s(str().mk_length(s), m());
@@ -843,7 +842,6 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
                             result);
         return BR_REWRITE_FULL;
     }
-#endif
     return BR_FAILED;
 }
 
@@ -3811,6 +3809,9 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
         return reduce_re_eq(l, r, result);
     }
     bool changed = false;
+    if (reduce_eq_empty(l, r, result)) 
+        return BR_REWRITE3;
+
     if (!reduce_eq(l, r, new_eqs, changed)) {
         result = m().mk_false();
         TRACE("seq_verbose", tout << result << "\n";);
@@ -4207,6 +4208,25 @@ bool seq_rewriter::reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs,
     return true;
 }
 
+bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
+    if (str().is_empty(r))
+        std::swap(l,r);
+    if (!str().is_empty(l))
+        return false;
+    expr* s = nullptr, *offset = nullptr, *len = nullptr;
+    if (str().is_extract(r, s, offset, len)) {
+        expr_ref len_s(str().mk_length(s), m()); 
+        expr_ref_vector fmls(m());
+        fmls.push_back(m_autil.mk_lt(offset, m_autil.mk_int(0)));
+        fmls.push_back(m().mk_eq(s, l));
+        fmls.push_back(m_autil.mk_lt(len, m_autil.mk_int(0)));
+        fmls.push_back(m_autil.mk_ge(offset, len_s));
+        result = m().mk_or(fmls);
+        return true;
+    }
+    return false;
+}
+
 bool seq_rewriter::reduce_by_length(expr_ref_vector& ls, expr_ref_vector& rs,
                                     expr_ref_pair_vector& eqs) {
 
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 16f9c6048..8e23ed0fe 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -268,6 +268,7 @@ class seq_rewriter {
     bool reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
     bool reduce_by_length(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
     bool reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
+    bool reduce_eq_empty(expr* l, expr* r, expr_ref& result);
     bool min_length(expr_ref_vector const& es, unsigned& len);
     expr* concat_non_empty(expr_ref_vector& es);