diff options
| author | lianah <lianahady@gmail.com> | 2013-02-11 12:33:28 -0500 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-02-11 12:33:28 -0500 |
| commit | d28123ea624364cbb49c0ce6f17426263affec9a (patch) | |
| tree | 5935dda48be4eeeee01a8945f4aba094ee65dd27 | |
| parent | 76805f8b4690093888bbb3d68e4d5c2c6ff221de (diff) | |
undid the caching that actually hurt performance
| -rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 8 | ||||
| -rw-r--r-- | 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: |