Unify skolems

9 files changed, 464 insertions, 61 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 41df85455..935d5bdf6 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -65,6 +65,8 @@ libcvc4_add_sources(
   dtype_selector.cpp
   record.cpp
   record.h
+  proof_skolem_cache.cpp
+  proof_skolem_cache.h
   sygus_datatype.cpp
   sygus_datatype.h
   uninterpreted_constant.cpp
diff --git a/src/expr/proof_skolem_cache.cpp b/src/expr/proof_skolem_cache.cpp
new file mode 100644
index 000000000..d982ef35b
--- /dev/null
+++ b/src/expr/proof_skolem_cache.cpp
@@ -0,0 +1,183 @@
+/*********************                                                        */
+/*! \file proof_skolem_cache.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of proof skolem cache
+ **/
+
+#include "expr/proof_skolem_cache.h"
+
+#include "expr/attribute.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+struct WitnessFormAttributeId
+{
+};
+typedef expr::Attribute<WitnessFormAttributeId, Node> WitnessFormAttribute;
+
+struct SkolemFormAttributeId
+{
+};
+typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;
+
+struct PurifySkolemAttributeId
+{
+};
+typedef expr::Attribute<PurifySkolemAttributeId, Node> PurifySkolemAttribute;
+
+Node ProofSkolemCache::mkSkolem(Node v,
+                                Node pred,
+                                const std::string& prefix,
+                                const std::string& comment,
+                                int flags)
+{
+  Assert(v.getKind() == BOUND_VARIABLE);
+  // make the witness term
+  NodeManager* nm = NodeManager::currentNM();
+  Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
+  // translate pred to witness form, since pred itself may contain skolem
+  Node predw = getWitnessForm(pred);
+  // make the witness term, which should not contain any skolem
+  Node w = nm->mkNode(CHOICE, bvl, predw);  // will change to WITNESS
+  // make the skolem
+  Node k = nm->mkSkolem(prefix, v.getType(), comment, flags);
+  // remember its mapping
+  WitnessFormAttribute wfa;
+  k.setAttribute(wfa, w);
+  SkolemFormAttribute sfa;
+  w.setAttribute(sfa, k);
+  Trace("pf-skolem") << "ProofSkolemCache::mkSkolem: " << k << " : " << w
+                     << 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)
+{
+  return convertInternal(n, true);
+}
+
+Node ProofSkolemCache::getSkolemForm(Node n)
+{
+  return convertInternal(n, false);
+}
+
+Node ProofSkolemCache::convertInternal(Node n, bool toWitness)
+{
+  if (n.isNull())
+  {
+    return n;
+  }
+  Trace("pf-skolem") << "ProofSkolemCache::convertInternal: " << toWitness
+                     << " " << n << std::endl;
+  WitnessFormAttribute wfa;
+  SkolemFormAttribute sfa;
+  NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      if (toWitness && cur.hasAttribute(wfa))
+      {
+        visited[cur] = cur.getAttribute(wfa);
+      }
+      else if (!toWitness && cur.hasAttribute(sfa))
+      {
+        visited[cur] = cur.getAttribute(sfa);
+      }
+      else
+      {
+        visited[cur] = Node::null();
+        visit.push_back(cur);
+        for (const Node& cn : cur)
+        {
+          visit.push_back(cn);
+        }
+      }
+    }
+    else if (it->second.isNull())
+    {
+      Node ret = cur;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == metakind::PARAMETERIZED)
+      {
+        children.push_back(cur.getOperator());
+      }
+      for (const Node& cn : cur)
+      {
+        it = visited.find(cn);
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cn != it->second;
+        children.push_back(it->second);
+      }
+      if (childChanged)
+      {
+        ret = nm->mkNode(cur.getKind(), children);
+      }
+      if (toWitness)
+      {
+        cur.setAttribute(wfa, ret);
+      }
+      else
+      {
+        cur.setAttribute(sfa, ret);
+      }
+      visited[cur] = ret;
+    }
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  Assert(!visited.find(n)->second.isNull());
+  return visited[n];
+}
+
+void ProofSkolemCache::convertToWitnessFormVec(std::vector<Node>& vec)
+{
+  for (unsigned i = 0, nvec = vec.size(); i < nvec; i++)
+  {
+    vec[i] = getWitnessForm(vec[i]);
+  }
+}
+void ProofSkolemCache::convertToSkolemFormVec(std::vector<Node>& vec)
+{
+  for (unsigned i = 0, nvec = vec.size(); i < nvec; i++)
+  {
+    vec[i] = getSkolemForm(vec[i]);
+  }
+}
+
+}  // namespace CVC4
diff --git a/src/expr/proof_skolem_cache.h b/src/expr/proof_skolem_cache.h
new file mode 100644
index 000000000..9d9e0fefb
--- /dev/null
+++ b/src/expr/proof_skolem_cache.h
@@ -0,0 +1,123 @@
+/*********************                                                        */
+/*! \file proof_skolem_cache.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Proof skolem cache utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_SKOLEM_CACHE_H
+#define CVC4__EXPR__PROOF_SKOLEM_CACHE_H
+
+#include <string>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+/**
+ * A manager for skolems that can be used in proofs. This is designed to be
+ * trusted interface to NodeManager::mkSkolem, where one
+ * must provide a definition for the skolem they create in terms of a
+ * predicate that the introduced variable is intended to witness.
+ *
+ * It is implemented by mapping terms to an attribute corresponding to their
+ * "witness form" as described below. Hence, this class does not impact the
+ * reference counting of skolem variables which may be deleted if they are not
+ * used.
+ */
+class ProofSkolemCache
+{
+ public:
+  ProofSkolemCache() {}
+  ~ProofSkolemCache() {}
+  /**
+   * This makes a skolem of same type as bound variable v, (say its type is T),
+   * whose definition is (witness ((v T)) pred). This definition is maintained
+   * by this class.
+   *
+   * Notice that (exists ((v T)) pred) should be a valid formula. This fact
+   * captures the reason for why the returned Skolem was introduced.
+   *
+   * Take as an example extensionality in arrays:
+   *
+   * (declare-fun a () (Array Int Int))
+   * (declare-fun b () (Array Int Int))
+   * (assert (not (= a b)))
+   *
+   * To witness the index where the arrays a and b are disequal, it is intended
+   * we call this method on:
+   *   Node k = mkSkolem( x, F )
+   * where F is:
+   *   (=> (not (= a b)) (not (= (select a x) (select b x))))
+   * and x is a fresh bound variable of integer type. Internally, this will map
+   * k to the term:
+   *   (witness ((x Int)) (=> (not (= a b))
+   *                          (not (= (select a x) (select b x)))))
+   * A lemma generated by the array solver for extensionality may safely use
+   * the skolem k in the standard way:
+   *   (=> (not (= a b)) (not (= (select a k) (select b k))))
+   * Furthermore, notice that the following lemma does not involve fresh
+   * skolem variables and is valid according to the theory of arrays extended
+   * with support for witness:
+   *   (let ((w (witness ((x Int)) (=> (not (= a b))
+   *                                   (not (= (select a x) (select b x)))))))
+   *     (=> (not (= a b)) (not (= (select a w) (select b w)))))
+   * This version of the lemma, which requires no explicit tracking of free
+   * Skolem variables, can be obtained by a call to getWitnessForm(...)
+   * below. We call this the "witness form" of the lemma above.
+   *
+   * @param v The bound variable of the same type of the Skolem to create.
+   * @param pred The desired property of the Skolem to create, in terms of bound
+   * variable v.
+   * @param prefix The prefix of the name of the Skolem
+   * @param comment Debug information about the Skolem
+   * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
+   * @return The skolem whose witness form is registered by this class.
+   */
+  static Node mkSkolem(Node v,
+                       Node pred,
+                       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
+   * @return n in witness form.
+   */
+  static Node getWitnessForm(Node n);
+  /** convert to Skolem form
+   *
+   * @param n The term or formula to convert to Skolem form described above
+   * @return n in Skolem form.
+   */
+  static Node getSkolemForm(Node n);
+  /** convert to witness form vector */
+  static void convertToWitnessFormVec(std::vector<Node>& vec);
+  /** convert to Skolem form vector */
+  static void convertToSkolemFormVec(std::vector<Node>& vec);
+
+ private:
+  /** Convert to witness or skolem form */
+  static Node convertInternal(Node n, bool toWitness);
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 9989c89f4..ab528ac03 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1440,11 +1440,11 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       }
     }
     SkolemCache* skc = d_termReg.getSkolemCache();
-    Node sk = skc->mkSkolemCached(
-        x,
-        y,
-        isRev ? SkolemCache::SK_ID_V_SPT_REV : SkolemCache::SK_ID_V_SPT,
-        "v_spt");
+    Node sk = skc->mkSkolemCached(x,
+                                  y,
+                                  isRev ? SkolemCache::SK_ID_V_UNIFIED_SPT_REV
+                                        : SkolemCache::SK_ID_V_UNIFIED_SPT,
+                                  "v_spt");
     iinfo.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk);
     Node eq1 =
         x.eqNode(isRev ? utils::mkNConcat(sk, y) : utils::mkNConcat(y, sk));
@@ -1909,15 +1909,18 @@ void CoreSolver::processDeq(Node ni, Node nj)
         Node sk2 =
             skc->mkSkolemCached(x, y, SkolemCache::SK_ID_DEQ_Y, "y_dsplit");
         Node sk3 =
-            skc->mkSkolemCached(x, y, SkolemCache::SK_ID_DEQ_Z, "z_dsplit");
+            skc->mkSkolemCached(y, x, SkolemCache::SK_ID_V_SPT, "z_dsplit");
+        Node sk4 =
+            skc->mkSkolemCached(x, y, SkolemCache::SK_ID_V_SPT, "w_dsplit");
         d_termReg.registerTermAtomic(sk3, LENGTH_GEQ_ONE);
+        d_termReg.registerTermAtomic(sk4, LENGTH_GEQ_ONE);
         Node sk1Len = utils::mkNLength(sk1);
         conc.push_back(sk1Len.eqNode(xLenTerm));
         Node sk2Len = utils::mkNLength(sk2);
         conc.push_back(sk2Len.eqNode(yLenTerm));
         conc.push_back(nm->mkNode(OR,
                                   y.eqNode(utils::mkNConcat(sk1, sk3)),
-                                  x.eqNode(utils::mkNConcat(sk2, sk3))));
+                                  x.eqNode(utils::mkNConcat(sk2, sk4))));
         d_im.sendInference(antec,
                            antecNewLits,
                            nm->mkNode(AND, conc),
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 4d92c372f..14b12104d 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
+#include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 #include "util/rational.h"
 
 using namespace CVC4::kind;
@@ -24,7 +26,7 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-SkolemCache::SkolemCache()
+SkolemCache::SkolemCache(bool useOpts) : d_useOpts(useOpts)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_strType = nm->stringType();
@@ -44,18 +46,63 @@ Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
 Node SkolemCache::mkTypedSkolemCached(
     TypeNode tn, Node a, Node b, SkolemId id, const char* c)
 {
+  Trace("skolem-cache") << "mkTypedSkolemCached start: (" << id << ", " << a
+                        << ", " << b << ")" << std::endl;
+  SkolemId idOrig = id;
   a = a.isNull() ? a : Rewriter::rewrite(a);
   b = b.isNull() ? b : Rewriter::rewrite(b);
 
-  if (tn == d_strType)
+  std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
+
+  // optimization: if we aren't asking for the purification skolem for constant
+  // a, and the skolem is equivalent to a, then we just return a.
+  if (d_useOpts && idOrig != SK_PURIFY && id == SK_PURIFY && a.isConst())
   {
-    std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
+    Trace("skolem-cache") << "...optimization: return constant " << a
+                          << std::endl;
+    return a;
   }
 
   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
   if (it == d_skolemCache[a][b].end())
   {
-    Node sk = mkTypedSkolem(tn, c);
+    NodeManager* nm = NodeManager::currentNM();
+    Node sk;
+    switch (id)
+    {
+      // exists k. k = a
+      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:
+      case SK_ID_VC_SPT:
+      case SK_ID_VC_SPT_REV:
+      case SK_FIRST_CTN_POST:
+      case SK_ID_C_SPT:
+      case SK_ID_C_SPT_REV:
+      case SK_ID_DC_SPT:
+      case SK_ID_DC_SPT_REM:
+      case SK_ID_DEQ_X:
+      case SK_ID_DEQ_Y:
+      case SK_FIRST_CTN_PRE:
+      case SK_PREFIX:
+      case SK_SUFFIX_REM:
+        Unhandled() << "Expected to eliminate Skolem ID " << id << std::endl;
+        break;
+      case SK_NUM_OCCUR:
+      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;
+    }
+    d_allSkolems.insert(sk);
     d_skolemCache[a][b][id] = sk;
     return sk;
   }
@@ -71,12 +118,8 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
 
 Node SkolemCache::mkSkolem(const char* c)
 {
-  return mkTypedSkolem(d_strType, c);
-}
-
-Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
-{
-  Node n = NodeManager::currentNM()->mkSkolem(c, tn, "string skolem");
+  // TODO: eliminate this
+  Node n = NodeManager::currentNM()->mkSkolem(c, d_strType, "string skolem");
   d_allSkolems.insert(n);
   return n;
 }
@@ -89,26 +132,31 @@ bool SkolemCache::isSkolem(Node n) const
 std::tuple<SkolemCache::SkolemId, Node, Node>
 SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
 {
-  Trace("skolem-cache") << "normalizeStringSkolem start: (" << id << ", " << a
-                        << ", " << b << ")" << std::endl;
 
   NodeManager* nm = NodeManager::currentNM();
 
+  // eliminate in terms of prefix/suffix_rem
   if (id == SK_FIRST_CTN_POST)
   {
     // SK_FIRST_CTN_POST(x, y) --->
     //   SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y)))
     id = SK_SUFFIX_REM;
     Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre");
-    b = Rewriter::rewrite(nm->mkNode(
-        PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b)));
+    b = nm->mkNode(
+        PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b));
   }
-
-  if (id == SK_ID_C_SPT)
+  else if (id == SK_ID_V_SPT || id == SK_ID_C_SPT)
   {
-    // SK_ID_C_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y))
+    // SK_ID_*_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y))
     id = SK_SUFFIX_REM;
-    b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b));
+    b = nm->mkNode(STRING_LENGTH, b);
+  }
+  else if (id == SK_ID_V_SPT_REV || id == SK_ID_C_SPT_REV)
+  {
+    // SK_ID_*_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) (str.len y)))
+    id = SK_PREFIX;
+    b = nm->mkNode(
+        MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(STRING_LENGTH, b));
   }
   else if (id == SK_ID_VC_SPT)
   {
@@ -120,8 +168,8 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
   {
     // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
     id = SK_PREFIX;
-    b = Rewriter::rewrite(nm->mkNode(
-        MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConst(Rational(1))));
+    b = nm->mkNode(
+        MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConst(Rational(1)));
   }
   else if (id == SK_ID_DC_SPT)
   {
@@ -141,47 +189,54 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     id = SK_PREFIX;
     Node aOld = a;
     a = b;
-    b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, aOld));
+    b = nm->mkNode(STRING_LENGTH, aOld);
   }
   else if (id == SK_ID_DEQ_Y)
   {
     // SK_ID_DEQ_Y(x, y) ---> SK_PREFIX(x, (str.len y))
     id = SK_PREFIX;
-    b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b));
+    b = nm->mkNode(STRING_LENGTH, b);
   }
-
-  if (id == SK_PURIFY && a.getKind() == kind::STRING_SUBSTR)
+  else if (id == SK_FIRST_CTN_PRE)
   {
-    Node s = a[0];
-    Node n = a[1];
-    Node m = a[2];
+    // SK_FIRST_CTN_PRE(x,y) ---> SK_PREFIX(x, indexof(x,y,0))
+    id = SK_PREFIX;
+    b = nm->mkNode(STRING_STRIDOF, a, b, d_zero);
+  }
 
-    if (n == d_zero)
-    {
-      // SK_PURIFY((str.substr x 0 m)) ---> SK_PREFIX(x, m)
-      id = SK_PREFIX;
-      a = s;
-      b = m;
-    }
-    else if (ArithEntail::check(nm->mkNode(PLUS, n, m),
-                                nm->mkNode(STRING_LENGTH, s)))
-    {
-      // SK_PURIFY((str.substr x n m)) ---> SK_SUFFIX_REM(x, n)
-      // if n + m >= (str.len x)
-      id = SK_SUFFIX_REM;
-      a = s;
-      b = n;
-    }
+  if (id == SK_ID_V_UNIFIED_SPT || id == SK_ID_V_UNIFIED_SPT_REV)
+  {
+    bool isRev = (id == SK_ID_V_UNIFIED_SPT_REV);
+    Node la = nm->mkNode(STRING_LENGTH, a);
+    Node lb = nm->mkNode(STRING_LENGTH, b);
+    Node ta = isRev ? utils::mkPrefix(a, nm->mkNode(MINUS, la, lb))
+                    : utils::mkSuffix(a, lb);
+    Node tb = isRev ? utils::mkPrefix(b, nm->mkNode(MINUS, lb, la))
+                    : utils::mkSuffix(b, la);
+    id = SK_PURIFY;
+    a = nm->mkNode(ITE, nm->mkNode(GEQ, la, lb), ta, tb);
+    b = Node::null();
   }
 
-  if (id == SK_PREFIX && b.getKind() == kind::STRING_STRIDOF && a == b[0]
-      && b[2] == d_zero)
+  // now, eliminate prefix/suffix_rem in terms of purify
+  if (id == SK_PREFIX)
+  {
+    // SK_PREFIX(x,y) ---> SK_PURIFY(substr(x,0,y))
+    id = SK_PURIFY;
+    a = utils::mkPrefix(a, b);
+    b = Node::null();
+  }
+  else if (id == SK_SUFFIX_REM)
   {
-    // SK_PREFIX(x, (str.indexof x y 0)) ---> SK_FIRST_CTN_PRE(x, y)
-    id = SK_FIRST_CTN_PRE;
-    b = b[1];
+    // SK_SUFFIX_REM(x,y) ---> SK_PURIFY(substr(x,y,str.len(x)-y))
+    id = SK_PURIFY;
+    a = utils::mkSuffix(a, b);
+    b = Node::null();
   }
 
+  a = a.isNull() ? a : Rewriter::rewrite(a);
+  b = b.isNull() ? b : Rewriter::rewrite(b);
+
   Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
                         << ", " << b << ")" << std::endl;
   return std::make_tuple(id, a, b);
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 8fcf46c14..a88b3cfb7 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -22,6 +22,7 @@
 #include <unordered_set>
 
 #include "expr/node.h"
+#include "expr/proof_skolem_cache.h"
 
 namespace CVC4 {
 namespace theory {
@@ -35,7 +36,13 @@ namespace strings {
 class SkolemCache
 {
  public:
-  SkolemCache();
+  /**
+   * Constructor.
+   *
+   * useOpts determines if we aggressively share Skolems or return the constants
+   * they are entailed to be equal to.
+   */
+  SkolemCache(bool useOpts = true);
   /** Identifiers for skolem types
    *
    * The comments below document the properties of each skolem introduced by
@@ -52,7 +59,7 @@ class SkolemCache
     // exists k. k = a
     SK_PURIFY,
     // a != "" ^ b = "ccccd" ^ a ++ "d" ++ a' = b ++ b' =>
-    //    exists k. a = "cccc" + k
+    //    exists k. a = "cccc" ++ k
     SK_ID_C_SPT,
     SK_ID_C_SPT_REV,
     // a != "" ^ b = "c" ^ len(a)!=len(b) ^ a ++ a' = b ++ b' =>
@@ -63,6 +70,8 @@ class SkolemCache
     //    exists k. len( k )>0 ^ ( a ++ k = b OR a = b ++ k )
     SK_ID_V_SPT,
     SK_ID_V_SPT_REV,
+    SK_ID_V_UNIFIED_SPT,
+    SK_ID_V_UNIFIED_SPT_REV,
     // a != ""  ^ b = "c" ^ a ++ a' != b ++ b' =>
     //    exists k, k_rem.
     //         len( k ) = 1 ^
@@ -75,7 +84,6 @@ class SkolemCache
     //           ( a = k_x ++ k_z OR b = k_y ++ k_z ) )
     SK_ID_DEQ_X,
     SK_ID_DEQ_Y,
-    SK_ID_DEQ_Z,
     // contains( a, b ) =>
     //    exists k_pre, k_post. a = k_pre ++ b ++ k_post ^
     //                          ~contains(k_pre ++ substr( b, 0, len(b)-1 ), b)
@@ -126,8 +134,6 @@ class SkolemCache
   Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c);
   /** Returns a (uncached) skolem of type string with name c */
   Node mkSkolem(const char* c);
-  /** Same as above, but for custom type tn */
-  Node mkTypedSkolem(TypeNode tn, const char* c);
   /** Returns true if n is a skolem allocated by this class */
   bool isSkolem(Node n) const;
 
@@ -149,7 +155,8 @@ class SkolemCache
   std::tuple<SkolemId, Node, Node> normalizeStringSkolem(SkolemId id,
                                                          Node a,
                                                          Node b);
-
+  /** whether we are using optimizations */
+  bool d_useOpts;
   /** string type */
   TypeNode d_strType;
   /** Constant node zero */
@@ -158,6 +165,8 @@ class SkolemCache
   std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
   /** the set of all skolems we have generated */
   std::unordered_set<Node, NodeHashFunction> d_allSkolems;
+  /** A proof skolem cache */
+  ProofSkolemCache d_pskc;
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 3d898b40b..631d4b8e4 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -368,6 +368,11 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n,
                                               LengthStatus s,
                                               std::map<Node, bool>& reqPhase)
 {
+  if (n.isConst())
+  {
+    return Node::null();
+  }
+
   Assert(n.getType().isStringLike());
   NodeManager* nm = NodeManager::currentNM();
   Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index b64a0df01..d0f789a79 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -157,6 +157,19 @@ Node mkNLength(Node t)
   return Rewriter::rewrite(NodeManager::currentNM()->mkNode(STRING_LENGTH, t));
 }
 
+Node mkPrefix(Node t, Node n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  return nm->mkNode(STRING_SUBSTR, t, nm->mkConst(Rational(0)), n);
+}
+
+Node mkSuffix(Node t, Node n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  return nm->mkNode(
+      STRING_SUBSTR, t, n, nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, t), n));
+}
+
 Node getConstantComponent(Node t)
 {
   if (t.getKind() == STRING_TO_REGEXP)
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index 9fc23499a..fd6e5122b 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -83,6 +83,16 @@ Node mkNConcat(const std::vector<Node>& c, TypeNode tn);
 Node mkNLength(Node t);
 
 /**
+ * Returns (pre t n), which is (str.substr t 0 n).
+ */
+Node mkPrefix(Node t, Node n);
+
+/**
+ * Returns (suf t n), which is (str.substr t n (- (str.len t) n)).
+ */
+Node mkSuffix(Node t, Node n);
+
+/**
  * Get constant component. Returns the string constant represented by the
  * string or regular expression t. For example:
  *   "ABC" -> "ABC", (str.to.re "ABC") -> "ABC", (str.++ x "ABC") -> null