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 e31ab2fdf25af9862b9c7a5cd9de10e57f7791dd..d678d7e31c0c68116959aa2045534eebf4e90179 100644 (file)
--- 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 55cecb117f8b1f0b4031cad9be22aa13895d231b..88254b983100fcdcda2279432eacb2f36ef25be0 100644 (file)
--- 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: