Automatic global skolem cache

3 files changed, 37 insertions, 5 deletions

diff --git a/src/expr/proof_skolem_cache.cpp b/src/expr/proof_skolem_cache.cpp
index 3ed798d07..640b23b5a 100644
--- a/src/expr/proof_skolem_cache.cpp
+++ b/src/expr/proof_skolem_cache.cpp
@@ -25,6 +25,11 @@ struct WitnessFormAttributeId
 };
 typedef expr::Attribute<WitnessFormAttributeId, Node> WitnessFormAttribute;
 
+struct PurifySkolemAttributeId
+{
+};
+typedef expr::Attribute<PurifySkolemAttributeId, Node> PurifySkolemAttribute;
+
 Node ProofSkolemCache::mkSkolem(Node v,
                                 Node pred,
                                 const std::string& prefix,
@@ -48,6 +53,21 @@ Node ProofSkolemCache::mkSkolem(Node v,
                      << std::endl;
   return k;
 }
+Node ProofSkolemCache::mkPurifySkolem(Node t,
+                      const std::string& prefix,
+                      const std::string& comment,
+                      int flags)
+{
+  PurifySkolemAttribute psa;
+  if (t.hasAttribute(psa))
+  {
+    return t.getAttribute(psa);
+  }
+  Node v = NodeManager::currentNM()->mkBoundVar(t.getType());
+  Node k = mkSkolem(v, v.eqNode(t), prefix, comment, flags);
+  t.setAttribute(psa,k);
+  return k;
+}
 
 Node ProofSkolemCache::getWitnessForm(Node n)
 {
diff --git a/src/expr/proof_skolem_cache.h b/src/expr/proof_skolem_cache.h
index 188413be5..078bd7972 100644
--- a/src/expr/proof_skolem_cache.h
+++ b/src/expr/proof_skolem_cache.h
@@ -88,6 +88,14 @@ class ProofSkolemCache
                        const std::string& prefix,
                        const std::string& comment = "",
                        int flags = NodeManager::SKOLEM_DEFAULT);
+  /**
+   * Same as above, but for special case for (witness ((x T)) (= x t))
+   * where T is the type of t. This skolem is unique for each t.
+   */
+  static Node mkPurifySkolem(Node t,
+                       const std::string& prefix,
+                       const std::string& comment = "",
+                       int flags = NodeManager::SKOLEM_DEFAULT);
   /** convert to witness form
    *
    * @param n The term or formula to convert to witness form described above
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index dec4283d6..3e498929b 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -55,12 +55,13 @@ Node SkolemCache::mkTypedSkolemCached(
   {
     NodeManager* nm = NodeManager::currentNM();
     // the condition
-    Node v = nm->mkBoundVar(tn);
-    Node cond = nm->mkConst(true);
+    Node sk;
     switch (id)
     {
       // exists k. k = a
-      case SK_PURIFY: cond = v.eqNode(a); break;
+      case SK_PURIFY: 
+        sk = d_pskc.mkPurifySkolem(a, c, "string purify skolem");
+        break;
       // these are eliminated by normalizeStringSkolem
       case SK_ID_V_SPT:
       case SK_ID_V_SPT_REV:
@@ -90,11 +91,14 @@ Node SkolemCache::mkTypedSkolemCached(
       //   where n is the number of occurrences of b in a, and k(0)=0.
       case SK_OCCUR_INDEX:
       default:
+      {
         Notice() << "Don't know how to handle Skolem ID " << id << std::endl;
+        Node v = nm->mkBoundVar(tn);
+        Node cond = nm->mkConst(true);
+        sk = d_pskc.mkSkolem(v, cond, c, "string skolem");
+      }
         break;
     }
-    // use the proper way to make skolems while recording witness terms
-    Node sk = d_pskc.mkSkolem(v, cond, c, "string skolem");
     d_allSkolems.insert(sk);
     d_skolemCache[a][b][id] = sk;
     return sk;