aggressive skolem sharing

3 files changed, 51 insertions, 15 deletions

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index ebd15e88c..cd74b9309 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -59,6 +59,10 @@ Node SkolemCache::mkTypedSkolemCached(
   {
     Node sk = mkTypedSkolem(tn, c);
     d_skolemCache[a][b][id] = sk;
+    
+    if (id == SK_FIRST_CTN_PRE) {
+      d_preSkolems[sk] = std::make_pair(a, b);
+    }
 
     /*
     if (id == SK_FIRST_CTN_POST && a.getKind() == STRING_SUBSTR) {
@@ -122,6 +126,26 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
         PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b)));
   }
 
+  if (id == SK_ID_C_SPT) {
+    id = SK_SUFFIX_REM;
+    b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b));
+  }
+
+  if (id == SK_ID_VC_SPT) {
+    id = SK_SUFFIX_REM;
+    b = nm->mkConst(Rational(1));
+  }
+
+  if (id == SK_ID_DEQ_Y) {
+    id = SK_PREFIX;
+    b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b));
+  } else if (id == SK_ID_DEQ_X) {
+    id = SK_PREFIX;
+    Node aOld = a;
+    a = b;
+    b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, aOld));
+  }
+
   // SK_PURIFY(str.substr x 0 (str.indexof x y 0)) ---> SK_FIRST_CTN_PRE(x, y)
   if (id == SK_PURIFY && a.getKind() == kind::STRING_SUBSTR)
   {
@@ -129,18 +153,11 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     Node n = a[1];
     Node m = a[2];
 
-    if (n == d_zero) {
-      if (m.getKind() == kind::STRING_STRIDOF && m[0] == s && m[2] == d_zero)
-      {
-          id = SK_FIRST_CTN_PRE;
-          a = m[0];
-          b = m[1];
-      } else {
-        id = SK_PREFIX;
-        a = s;
-        // b = Rewriter::rewrite(nm->mkNode(MINUS, m, nm->mkConst(Rational(1))));
-        b = m;
-      }
+    if (n == d_zero)
+    {
+      id = SK_PREFIX;
+      a = s;
+      b = m;
     }
     else if (TheoryStringsRewriter::checkEntailArith(
                  nm->mkNode(PLUS, n, m), nm->mkNode(STRING_LENGTH, s)))
@@ -151,6 +168,13 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     }
   }
 
+  if (id == SK_PREFIX && b.getKind() == kind::STRING_STRIDOF && a == b[0]
+      && b[2] == d_zero)
+  {
+    id = SK_FIRST_CTN_PRE;
+    b = b[2];
+  }
+
   if (id == SK_FIRST_CTN_PRE)
   {
     // SK_FIRST_CTN_PRE((str.substr x 0 n), y) ---> SK_FIRST_CTN_PRE(x, y)
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index e227a4263..2cd03bfe6 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -138,6 +138,8 @@ class SkolemCache
   /** Returns true if n is a skolem allocated by this class */
   bool isSkolem(Node n) const;
 
+  std::map<Node, std::pair<Node, Node>> d_preSkolems;
+
  private:
   TheoryStrings* d_ts;
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 77be51ce6..d01579b2e 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3148,10 +3148,20 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
                             isRev ? SkolemCache::SK_ID_C_SPT_REV
                                   : SkolemCache::SK_ID_C_SPT,
                             "c_spt");
-                        Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << ", p=" << p << std::endl;        
+                        Node lem = other_str.eqNode( isRev ? mkConcat( sk, prea ) : mkConcat(prea, sk) );;
+                        if (false && !isRev && d_sk_cache.d_preSkolems.find(Node(other_str)) != d_sk_cache.d_preSkolems.end()) {
+                          Node aa, bb;
+                          std::tie(aa, bb) = d_sk_cache.d_preSkolems.find(other_str)->second;
+                          if (bb == NodeManager::currentNM()->mkConst(strb)) {
+                            lem = other_str.eqNode(prea); // other_str.eqNode(mkConcat(prea, NodeManager::currentNM()->mkConst(String(""))));
+                            sk = Node::null();
+                          }
+                        }
+                        Trace("strings-csp") << "Const Split: " << other_str << " " << prea << " is removed from " << stra << " due to " << strb << ", p=" << p << std::endl;        
                         //set info
-                        info.d_conc = other_str.eqNode( isRev ? mkConcat( sk, prea ) : mkConcat(prea, sk) );
-                        info.d_new_skolem[LENGTH_SPLIT].push_back(sk);
+                        info.d_conc = lem;
+                        if (!sk.isNull())
+                          info.d_new_skolem[LENGTH_SPLIT].push_back(sk);
                         info.d_id = INFER_SSPLIT_CST_PROP;
                         info_valid = true;
                       }