diff options
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 50 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.h | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
3 files changed, 44 insertions, 12 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index e4b623e93..9f44429a0 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -24,18 +24,48 @@ SkolemCache::SkolemCache() {} Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c) { - if (!a.isNull()) - a = Rewriter::rewrite(a); - if (!b.isNull()) - b = Rewriter::rewrite(b); - std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id); - if (it == d_skolemCache[a][b].end()) + NodeManager* nm = NodeManager::currentNM(); + if (id == SK_FIRST_CTN_PRE || id == SK_FIRST_CTN_POST) + { + Node sk; + std::map<SkolemId, Node>::iterator it = d_skolemFnCache.find(id); + if (it == d_skolemFnCache.end()) + { + std::vector<TypeNode> argTypes; + argTypes.push_back(a.getType()); + if (!b.isNull()) argTypes.push_back(b.getType()); + sk = nm->mkSkolem(c, nm->mkFunctionType(argTypes, nm->stringType())); + d_allSkolems.insert(sk); + d_skolemFnCache[id] = sk; + } + else + { + sk = it->second; + } + Node ret; + if (b.isNull()) + { + ret = nm->mkNode(kind::APPLY_UF, sk, a); + } + else + { + ret = nm->mkNode(kind::APPLY_UF, sk, a, b); + } + return ret; + } + else { - Node sk = mkSkolem(c); - d_skolemCache[a][b][id] = sk; - return sk; + if (!a.isNull()) a = Rewriter::rewrite(a); + if (!b.isNull()) b = Rewriter::rewrite(b); + std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id); + if (it == d_skolemCache[a][b].end()) + { + Node sk = mkSkolem(c); + d_skolemCache[a][b][id] = sk; + return sk; + } + return it->second; } - return it->second; } Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c) diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index c9b9fbe5a..db17ef1e6 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -114,6 +114,8 @@ class SkolemCache private: /** map from node pairs and identifiers to skolems */ std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache; + /** map from node pairs and identifiers to skolems */ + std::map<SkolemId, Node> d_skolemFnCache; /** the set of all skolems we have generated */ std::unordered_set<Node, NodeHashFunction> d_allSkolems; }; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index fb25e1348..a8242084f 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -453,9 +453,9 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) { Node s = n[1]; //positive contains reduces to a equality Node sk1 = d_sk_cache.mkSkolemCached( - x, s, SkolemCache::SK_ID_CTN_PRE, "sc1"); + x, s, SkolemCache::SK_FIRST_CTN_PRE, "sc1"); Node sk2 = d_sk_cache.mkSkolemCached( - x, s, SkolemCache::SK_ID_CTN_POST, "sc2"); + x, s, SkolemCache::SK_FIRST_CTN_POST, "sc2"); Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) ); std::vector< Node > exp_vec; exp_vec.push_back( n ); |