From d28123ea624364cbb49c0ce6f17426263affec9a Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Mon, 11 Feb 2013 12:33:28 -0500
Subject: [PATCH] undid the caching that actually hurt performance

---
 src/theory/bv/bv_subtheory_core.cpp | 8 ++++----
 src/theory/bv/slicer.h              | 1 -
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index e31ab2fdf..d678d7e31 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -99,15 +99,15 @@ void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 }
 
 Node CoreSolver::getBaseDecomposition(TNode a) {
-  if (d_normalFormCache.find(a) != d_normalFormCache.end()) {
-    return d_normalFormCache[a]; 
-  }
+  // if (d_normalFormCache.find(a) != d_normalFormCache.end()) {
+  //   return d_normalFormCache[a]; 
+  // }
 
   // otherwise we must compute the normal form
   std::vector<Node> a_decomp;
   d_slicer->getBaseDecomposition(a, a_decomp);
   Node new_a = utils::mkConcat(a_decomp);
-  d_normalFormCache[a] = new_a;
+  //  d_normalFormCache[a] = new_a;
   return new_a; 
 }
 
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 55cecb117..88254b983 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -230,7 +230,6 @@ class Slicer {
   __gnu_cxx::hash_map<TermId, TNode> d_idToNode;
   __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
   __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
-  __gnu_cxx::hash_map<TNode, std::vector<Node>, TNodeHashFunction> d_decompositionCache; 
   UnionFind d_unionFind;
   ExtractTerm registerTerm(TNode node); 
 public:
-- 
2.30.2