prepare for base run

4 files changed, 25 insertions, 8 deletions

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 8b9ec5856..4c5e41171 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -48,13 +48,13 @@ Node SkolemCache::mkTypedSkolemCached(
   a = a.isNull() ? a : Rewriter::rewrite(a);
   b = b.isNull() ? b : Rewriter::rewrite(b);
 
-  if (tn == d_strType)
+  if (options::skolemSharing() || tn == d_strType)
   {
     std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
   }
 
   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
-  if (!options::skolemSharing() || it == d_skolemCache[a][b].end())
+  if (it == d_skolemCache[a][b].end())
   {
     Node sk = mkTypedSkolem(tn, c);
     d_skolemCache[a][b][id] = sk;
@@ -95,6 +95,15 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
 
   NodeManager* nm = NodeManager::currentNM();
 
+  if (id == SK_FIRST_CTN_IOPRE || id == SK_FIRST_CTN_RFCPRE)
+  {
+    id = SK_FIRST_CTN_PRE;
+  }
+  else if (id == SK_FIRST_CTN_IOPOST || id == SK_FIRST_CTN_RFCPOST)
+  {
+    id = SK_FIRST_CTN_POST;
+  }
+
   if (id == SK_FIRST_CTN_POST)
   {
     // SK_FIRST_CTN_POST(x, y) --->
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 6f296255b..8cc5146b3 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -97,6 +97,13 @@ class SkolemCache
     // of b in a as the witness for contains( a, b ).
     SK_FIRST_CTN_PRE,
     SK_FIRST_CTN_POST,
+
+    SK_FIRST_CTN_IOPRE,
+    SK_FIRST_CTN_IOPOST,
+
+    SK_FIRST_CTN_RFCPRE,
+    SK_FIRST_CTN_RFCPOST,
+
     // For integer b,
     // len( a ) > b =>
     //    exists k. a = k ++ a' ^ len( k ) = b
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6d3a0b6c0..4eaa9c3aa 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3177,7 +3177,8 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
           Node length_term_j = d_state.getLength(nfjv[index], lexp);
           //split on equality between string lengths (note that splitting on equality between strings is worse since it is harder to process)
           if (!d_state.areDisequal(length_term_i, length_term_j)
-              && !d_state.areEqual(length_term_i, length_term_j))
+              && !d_state.areEqual(length_term_i, length_term_j)
+              && !nfiv[index].isConst() && !nfjv[index].isConst())
           {  // AJR: remove the latter 2 conditions?
             Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl;
             //try to make the lengths equal via splitting on demand
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 6272ad129..e59bc95e8 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -134,9 +134,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                          n,
                          nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n));
     Node io2 =
-        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre");
+        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_IOPRE, "iopre");
     Node io4 =
-        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost");
+        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_IOPOST, "iopost");
 
     // ~contains( substr( x, n, len( x ) - n ), y )
     Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate();
@@ -355,9 +355,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node z = t[2];
     TypeNode tn = t[0].getType();
     Node rp1 =
-        d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre");
-    Node rp2 =
-        d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost");
+        d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_RFCPRE, "rfcpre");
+    Node rp2 = d_sc->mkSkolemCached(
+        x, y, SkolemCache::SK_FIRST_CTN_RFCPOST, "rfcpost");
     Node rpw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw");
 
     // y = ""