From 202ce1edf066be63631bdf0c1ff5cf53e2869bcc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Jun 2022 12:45:29 -0700
Subject: [PATCH] #6100 - two perf fixes

remaining perf bug is dealing with very large bit-widths. mod 2^n should be computed natively based on n instead of 2^n because we pre-populate an array with all values up to n. Suppose n is 10000, the array has size 10000.
---
 src/ast/bv_decl_plugin.cpp          |  7 +++++--
 src/ast/rewriter/array_rewriter.cpp | 13 +++++++++++--
 2 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 74002bb1bee..e6a1f3b796a 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -423,7 +423,8 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
     // This cannot be enforced now, since some Z3 modules try to generate these invalid numerals.
     // After SMT-COMP, I should find all offending modules.
     // For now, I will just simplify the numeral here.
-    parameter p0(mod(parameters[0].get_rational(), rational::power_of_two(bv_size)));
+    rational v = parameters[0].get_rational();
+    parameter p0(mod(v, rational::power_of_two(bv_size)));
     parameter ps[2] = { std::move(p0), parameters[1] };
     sort * bv = get_bv_sort(bv_size);
     return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
@@ -645,11 +646,13 @@ void bv_decl_plugin::get_offset_term(app * a, expr * & t, rational & offset) con
     }
     else {
         t      = a;
-        offset = rational(0);
+        offset.reset();
     }
 }
 
 bool bv_decl_plugin::are_distinct(app * a, app * b) const {
+    if (is_value(a) && is_value(b))
+        return a != b;
 #if 1
     // Check for a + k1 != a + k2   when k1 != k2
     rational a_offset;
diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index b8b30a20690..c432ddd22fb 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -23,6 +23,7 @@ Module Name:
 #include "ast/ast_ll_pp.h"
 #include "ast/rewriter/var_subst.h"
 #include "params/array_rewriter_params.hpp"
+#include "util/util.h"
 
 void array_rewriter::updt_params(params_ref const & _p) {
     array_rewriter_params p(_p);
@@ -161,7 +162,8 @@ br_status array_rewriter::mk_store_core(unsigned num_args, expr * const * args,
 
     return BR_FAILED;
 }
-        
+
+
 br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, expr_ref & result) {
     SASSERT(num_args >= 2);
     if (m_util.is_store(args[0])) {
@@ -172,9 +174,16 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
             result = to_app(args[0])->get_arg(num_args);
             return BR_DONE;
         case l_false: {
+            expr* arg0 = args[0];
+            expr* arg1 = to_app(arg0)->get_arg(0);
+            while (m_util.is_store(arg1) && compare_args<true>(num_args-1, args + 1, to_app(arg0)->get_args() + 1) == l_false) {
+                arg0 = arg1;
+                arg1 = to_app(arg0)->get_arg(0);
+            }
+            
             // select(store(a, I, v), J) --> select(a, J) if I != J
             ptr_buffer<expr> new_args;
-            new_args.push_back(to_app(args[0])->get_arg(0));
+            new_args.push_back(arg1);
             new_args.append(num_args-1, args+1);
             result = m().mk_app(get_fid(), OP_SELECT, num_args, new_args.data());
             return BR_REWRITE1;