From bc2020a39b9809b2573686ae813318623d3e318e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 17 Oct 2021 20:24:12 -0700
Subject: [PATCH] #5604

retain array interpretation when available
---
 src/ast/rewriter/array_rewriter.cpp | 99 +++++++++++++++--------------
 src/model/func_interp.cpp           | 16 +++--
 2 files changed, 62 insertions(+), 53 deletions(-)

diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index c25ae1156..88a0ee28e 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -703,8 +703,60 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
         result = m().update_quantifier(lam, quantifier_kind::forall_k, e);
         return BR_REWRITE2; 
     }
-    expr_ref lh1(m()), rh1(m());
+
+    expr_ref_vector fmls(m());
+
+
+    auto has_large_domain = [&](sort* s, unsigned num_stores) {
+        unsigned sz = get_array_arity(s);
+        uint64_t dsz = 1;
+        for (unsigned i = 0; i < sz; ++i) {
+            sort* d = get_array_domain(s, i);
+            if (d->is_infinite() || d->is_very_big())
+                return true;
+            auto const& n = d->get_num_elements();
+            if (n.size() > num_stores)
+                return true;
+            dsz *= n.size();
+            if (dsz > num_stores)
+                return true;
+        }
+        return false;        
+    };
+
+
+    if (m_expand_store_eq) {
+        expr* lhs1 = lhs;
+        expr* rhs1 = rhs;
+        unsigned num_lhs = 0, num_rhs = 0;
+        while (m_util.is_store(lhs1)) {
+            lhs1 = to_app(lhs1)->get_arg(0);
+            ++num_lhs;
+        }
+        while (m_util.is_store(rhs1)) {
+            rhs1 = to_app(rhs1)->get_arg(0);
+            ++num_rhs;
+        }
+        if (lhs1 == rhs1) {
+            mk_eq(lhs, lhs, rhs, fmls);
+            mk_eq(rhs, lhs, rhs, fmls);
+            result = m().mk_and(fmls);
+            return BR_REWRITE_FULL;
+        }
+
+        if (m_util.is_const(lhs1, v) && m_util.is_const(rhs1, w) &&
+            has_large_domain(lhs->get_sort(), std::max(num_lhs, num_rhs))) {
+            mk_eq(lhs, lhs, rhs, fmls);
+            mk_eq(rhs, lhs, rhs, fmls);
+            fmls.push_back(m().mk_eq(v, w));
+            result = m().mk_and(fmls);
+            return BR_REWRITE_FULL;
+        }
+    }
+
+
     if (m_expand_nested_stores) {
+        expr_ref lh1(m()), rh1(m());
         if (is_expandable_store(lhs)) {
             lh1 = expand_store(lhs);        
         }
@@ -719,10 +771,6 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
         }
     }
 
-    if (!m_expand_store_eq) {
-        return BR_FAILED;
-    }
-    expr_ref_vector fmls(m());
 
 #if 0
     // lambda friendly version of array equality rewriting.
@@ -744,46 +792,5 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
     }
 #endif
 
-    expr* lhs1 = lhs;
-    unsigned num_lhs = 0, num_rhs = 0;
-    while (m_util.is_store(lhs1)) {
-        lhs1 = to_app(lhs1)->get_arg(0);
-        ++num_lhs;
-    }
-    expr* rhs1 = rhs;
-    while (m_util.is_store(rhs1)) {
-        rhs1 = to_app(rhs1)->get_arg(0);
-        ++num_rhs;
-    }
-    if (lhs1 == rhs1) {
-        mk_eq(lhs, lhs, rhs, fmls);
-        mk_eq(rhs, lhs, rhs, fmls);
-        result = m().mk_and(fmls);
-        return BR_REWRITE_FULL;
-    }
-    auto has_large_domain = [&](sort* s, unsigned num_stores) {
-        unsigned sz = get_array_arity(s);
-        uint64_t dsz = 1;
-        for (unsigned i = 0; i < sz; ++i) {
-            sort* d = get_array_domain(s, i);
-            if (d->is_infinite() || d->is_very_big())
-                return true;
-            auto const& n = d->get_num_elements();
-            if (n.size() > num_stores)
-                return true;
-            dsz *= n.size();
-            if (dsz > num_stores)
-                return true;
-        }
-        return false;        
-    };
-    if (m_util.is_const(lhs1, v) && m_util.is_const(rhs1, w) &&
-        has_large_domain(lhs->get_sort(), std::max(num_lhs, num_rhs))) {
-        mk_eq(lhs, lhs, rhs, fmls);
-        mk_eq(rhs, lhs, rhs, fmls);
-        fmls.push_back(m().mk_eq(v, w));
-        result = m().mk_and(fmls);
-        return BR_REWRITE_FULL;
-    }
     return BR_FAILED;    
 }
diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index 22443ee1f..1c59b6107 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -280,6 +280,9 @@ void func_interp::compress() {
     }
     // other compression, if else is a default branch.
     // or function encode identity.
+#if 0
+    // breaks array interpretations
+    // #5604
     if (m().is_false(m_else)) {
         expr_ref new_else(get_interp(), m());
         for (func_entry * curr : m_entries) {
@@ -291,7 +294,9 @@ void func_interp::compress() {
         m().dec_ref(m_else);
         m_else = new_else;
     }
-    else if (!m_entries.empty() && is_identity()) {
+    else
+#endif
+        if (!m_entries.empty() && is_identity()) {
         for (func_entry * curr : m_entries) {
             curr->deallocate(m(), m_arity);
         }
@@ -335,14 +340,11 @@ expr * func_interp::get_interp_core() const {
     expr * r = m_else;
     ptr_buffer<expr> vars;
     for (func_entry * curr : m_entries) {
-        if (m_else == curr->get_result()) {
+        if (m_else == curr->get_result()) 
             continue;
-        }
-        if (vars.empty()) {
-            for (unsigned i = 0; i < m_arity; i++) {
+        if (vars.empty()) 
+            for (unsigned i = 0; i < m_arity; i++)                 
                 vars.push_back(m().mk_var(i, curr->get_arg(i)->get_sort()));
-            }
-        }
         ptr_buffer<expr> eqs;
         for (unsigned i = 0; i < m_arity; i++) {
             eqs.push_back(m().mk_eq(vars[i], curr->get_arg(i)));