diff options
| -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; |