diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-27 14:08:05 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-27 14:08:05 -0800 |
commit | ce4b09af02662b0433344a4331d5046a3b5ca9b4 (patch) | |
tree | 67636ff5e54653056125fd4cb4e85b3717105513 | |
parent | 9f3b16927f39d64c09b1a6c1206a4f384d8c99a0 (diff) |
Fix stats
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 6 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.h | 3 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index c11833420..d63bd252b 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -49,10 +49,14 @@ Node SkolemCache::mkTypedSkolemCached( a = a.isNull() ? a : Rewriter::rewrite(a); b = b.isNull() ? b : Rewriter::rewrite(b); - if (d_skolemCache[a][b].find(id) != d_skolemCache[a][b].end()) + if (d_skolemCachePreOnly[a][b].find(id) != d_skolemCachePreOnly[a][b].end()) { d_statistics.d_numCachedSkolemsPre += 1; } + else + { + d_skolemCachePreOnly[a][b][id] = Node::null(); + } if (options::skolemSharing() && tn == d_strType) { diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 3946d7622..a6d2390c2 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -168,6 +168,9 @@ class SkolemCache Node d_zero; /** map from node pairs and identifiers to skolems */ std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache; + + std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCachePreOnly; + /** the set of all skolems we have generated */ std::unordered_set<Node, NodeHashFunction> d_allSkolems; |