From 248feace34b6679f2803d23bc3c3ac949807be7b Mon Sep 17 00:00:00 2001
From: Mikolas Janota <mikolas.janota@gmail.com>
Date: Mon, 4 Apr 2016 17:00:35 +0100
Subject: [PATCH] fixing the behavior in bv_trailing

---
 src/ast/rewriter/bv_rewriter.cpp |  1 +
 src/ast/rewriter/bv_trailing.cpp | 45 +++++++++++++++++++++++---------
 2 files changed, 34 insertions(+), 12 deletions(-)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 19b4bd122..f77bce5c2 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2094,6 +2094,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
 
     if (m_trailing) {
         st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result);
+        //m_rm_trailing.reset_cache();
         if (st != BR_FAILED) {
             TRACE("eq_remove_trailing", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result, m()) << "\n";);
             return st;
diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp
index eccd2e8cb..ef6a1e577 100644
--- a/src/ast/rewriter/bv_trailing.cpp
+++ b/src/ast/rewriter/bv_trailing.cpp
@@ -26,18 +26,46 @@ struct bv_trailing::imp {
     mk_extract_proc&     m_mk_extract;
     bv_util&             m_util;
     ast_manager&         m_m;
-    map                  m_count_cache;
+    map                  m_count_cache[TRAILING_DEPTH + 1];
+
     imp(mk_extract_proc& mk_extract)
         : m_mk_extract(mk_extract)
         , m_util(mk_extract.bvutil())
         , m_m(mk_extract.m())
         { }
 
-    virtual ~imp() { }
+    virtual ~imp() {
+        reset_cache();
+    }
 
     ast_manager & m() const { return m_util.get_manager(); }
 
-    void reset_cache() { m_count_cache.reset(); }
+    void cache(unsigned depth, expr * e, unsigned min, unsigned max) {
+        SASSERT(depth <= TRAILING_DEPTH);
+        m().inc_ref(e);
+        m_count_cache[depth].insert(e, std::make_pair(min, max));
+        TRACE("bv-trailing", tout << "caching@" << depth <<": " << mk_ismt2_pp(e, m()) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
+    }
+
+    bool is_cached(unsigned depth, expr * e, unsigned& min, unsigned& max) {
+        SASSERT(depth <= TRAILING_DEPTH);
+        const map::obj_map_entry * const oe = m_count_cache[depth].find_core(e);
+        if (oe == NULL) return false;
+        min = oe->get_data().m_value.first;
+        max = oe->get_data().m_value.second;
+        TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m()) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
+        return true;
+    }
+
+
+    void reset_cache() {
+        for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) {
+            map::iterator it = m_count_cache[i].begin();
+            map::iterator end = m_count_cache[i].end();
+            for (; it != end; ++it) m().dec_ref(it->m_key);
+            m_count_cache[i].reset();
+        }
+    }
 
     br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) {
         TRACE("bv-trailing", tout << mk_ismt2_pp(e1, m()) << "\n=\n" << mk_ismt2_pp(e2, m()) << "\n";);
@@ -223,21 +251,14 @@ struct bv_trailing::imp {
     }
 
     void count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth) {
-        std::pair<unsigned, unsigned> cached;
-        if (m_count_cache.find(e, cached)) { // check cache first
-            min = cached.first;
-            max = cached.second;
+        if (is_cached(depth, e, min, max))
             return;
-        }
         SASSERT(e && m_util.is_bv(e));
         count_trailing_core(e, min, max, depth);
         TRACE("bv-trailing", tout << mk_ismt2_pp(e, m()) << "\n:" << min << " - " << max << "\n";);
         SASSERT(min <= max);
         SASSERT(max <= m_util.get_bv_size(e));
-        // store into the cache
-        cached.first = min;
-        cached.second = max;
-        m_count_cache.insert(e, cached);
+        cache(depth, e, min, max);  // store result into the cache
     }
 
     void count_trailing_concat(app * a, unsigned& min, unsigned& max, unsigned depth) {