From: lianah <lianahady@gmail.com>
Date: Mon, 11 Feb 2013 17:33:28 +0000 (-0500)
Subject: undid the caching that actually hurt performance
X-Git-Tag: cvc5-1.0.0~7361^2~45
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d28123ea624364cbb49c0ce6f17426263affec9a;p=cvc5.git

undid the caching that actually hurt performance
---

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: