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 );