Fix

4 files changed, 43 insertions, 34 deletions

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 05cb82a7c..81cbd235d 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -33,23 +33,23 @@ SkolemCache::SkolemCache()
   d_zero = nm->mkConst(Rational(0));
 }
 
-Node SkolemCache::mkSkolemCached(Node a, Node b, Node c, SkolemId id, const char* name)
+Node SkolemCache::mkSkolemCached(Node a, Node b, Node c, SkolemId id, const char* name, LengthStatus ls)
 {
-  return mkTypedSkolemCached(d_strType, a, b, c, id, name);
+  return mkTypedSkolemCached(d_strType, a, b, c, id, name, ls);
 }
 
-Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* name)
+Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* name, LengthStatus ls)
 {
-  return mkTypedSkolemCached(d_strType, a, b, Node::null(), id, name);
+  return mkTypedSkolemCached(d_strType, a, b, Node::null(), id, name, ls);
 }
 
-Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* name)
+Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* name, LengthStatus ls)
 {
-  return mkSkolemCached(a, Node::null(), Node::null(), id, name);
+  return mkSkolemCached(a, Node::null(), Node::null(), id, name, ls);
 }
 
 Node SkolemCache::mkTypedSkolemCached(
-    TypeNode tn, Node a, Node b, Node c, SkolemId id, const char* name)
+    TypeNode tn, Node a, Node b, Node c, SkolemId id, const char* name, LengthStatus ls)
 {
   a = a.isNull() ? a : Rewriter::rewrite(a);
   b = b.isNull() ? b : Rewriter::rewrite(b);
@@ -60,7 +60,7 @@ Node SkolemCache::mkTypedSkolemCached(
     std::tie(id, a, b, c) = normalizeStringSkolem(id, a, b, c);
   }
 
-  std::tuple<Node, Node, Node, SkolemId> args = std::make_tuple(a, b, c, id);
+  std::tuple<Node, Node, Node, SkolemId, LengthStatus> args = std::make_tuple(a, b, c, id, ls);
   const auto& it = d_skolemCache.find(args);
   if (it == d_skolemCache.end())
   {
@@ -70,41 +70,42 @@ Node SkolemCache::mkTypedSkolemCached(
     {
       Node da = depurify(a);
       Node db = depurify(b);
+      Node na = Rewriter::rewrite(nm->mkNode(STRING_SUBSTR, da, d_zero, db));
       sk = mkSkolemCached(
-          Rewriter::rewrite(nm->mkNode(STRING_SUBSTR, da, d_zero, db)),
+          na,
           SK_PURIFY,
-          "pur");
+          name, ls);
     }
     else if (id == SK_SUFFIX_REM)
     {
       Node da = depurify(a);
       Node db = depurify(b);
-      sk = mkSkolemCached(
-          Rewriter::rewrite(
-              nm->mkNode(STRING_SUBSTR,
+      Node na = Rewriter::rewrite(nm->mkNode(STRING_SUBSTR,
                          da,
                          db,
-                         nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, da), db))),
+                         nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, da), db)));
+      sk = mkSkolemCached(na,
           SK_PURIFY,
-          "pur");
+          name, ls);
     }
     else
     {
       sk = mkTypedSkolem(tn, name);
+      d_skolemToArgs[sk] = args;
     }
 
     d_skolemCache[args] = sk;
-    d_skolemToArgs[sk] = args;
     return sk;
   }
   return it->second;
 }
+
 Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
                                       Node a,
                                       SkolemId id,
-                                      const char* name)
+                                      const char* name, LengthStatus ls)
 {
-  return mkTypedSkolemCached(tn, a, Node::null(), Node::null(), id, name);
+  return mkTypedSkolemCached(tn, a, Node::null(), Node::null(), id, name, ls);
 }
 
 Node SkolemCache::mkSkolem(const char* name)
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 1085ab43c..4ccd56bee 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 "theory/strings/infer_info.h"
 
 namespace CVC4 {
 namespace theory {
@@ -134,22 +135,22 @@ class SkolemCache
    * Returns a skolem of type string that is cached for (a,b,id) and has
    * name `name`.
    */
-  Node mkSkolemCached(Node a, Node b, Node c, SkolemId id, const char* name);
+  Node mkSkolemCached(Node a, Node b, Node c, SkolemId id, const char* name, LengthStatus ls = LENGTH_SPLIT);
   /**
    * Returns a skolem of type string that is cached for (a,b,id) and has
    * name `name`.
    */
-  Node mkSkolemCached(Node a, Node b, SkolemId id, const char* name);
+  Node mkSkolemCached(Node a, Node b, SkolemId id, const char* name, LengthStatus ls = LENGTH_SPLIT);
   /**
    * Returns a skolem of type string that is cached for (a,[null],id) and has
    * name `name`.
    */
-  Node mkSkolemCached(Node a, SkolemId id, const char* name);
+  Node mkSkolemCached(Node a, SkolemId id, const char* name, LengthStatus ls = LENGTH_SPLIT);
   /** Same as above, but the skolem to construct has a custom type tn */
   Node mkTypedSkolemCached(
-      TypeNode tn, Node a, Node b, Node c, SkolemId id, const char* name);
+      TypeNode tn, Node a, Node b, Node c, SkolemId id, const char* name, LengthStatus ls = LENGTH_SPLIT);
   /** Same as mkTypedSkolemCached above for (a,[null],id) */
-  Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* name);
+  Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* name, LengthStatus ls = LENGTH_SPLIT);
   /** Returns a (uncached) skolem of type string with name `name` */
   Node mkSkolem(const char* name);
   /** Same as above, but for custom type tn */
@@ -184,9 +185,9 @@ class SkolemCache
   /** Constant node zero */
   Node d_zero;
   /** map from node pairs and identifiers to skolems */
-  std::map<std::tuple<Node, Node, Node, SkolemId>, Node> d_skolemCache;
+  std::map<std::tuple<Node, Node, Node, SkolemId, LengthStatus>, Node> d_skolemCache;
 
-  std::map<Node, std::tuple<Node, Node, Node, SkolemId>> d_skolemToArgs;
+  std::map<Node, std::tuple<Node, Node, Node, SkolemId, LengthStatus>> d_skolemToArgs;
   /** 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 5015207f1..73aa752bc 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3299,8 +3299,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
                             prea,
                             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;        
+                            "c_spt", LENGTH_GEQ_ONE);
                         //set info
                         info.d_conc = nm->mkNode(OR, other_str.eqNode(prea), other_str.eqNode(
                             isRev ? utils::mkNConcat(sk, prea)
@@ -3348,7 +3347,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
                           other_str,
                           isRev ? SkolemCache::SK_ID_VC_SPT_REV
                                 : SkolemCache::SK_ID_VC_SPT,
-                          "vc_spt");
+                          "vc_spt", LENGTH_GEQ_ONE);
                       Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (serial) " << std::endl;
                       info.d_conc = nm->mkNode(OR, other_str.eqNode(firstChar), other_str.eqNode(
                           isRev ? utils::mkNConcat(sk, firstChar)
@@ -3402,13 +3401,13 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
                     nfjv[index],
                     isRev ? SkolemCache::SK_ID_V_SPT_REV_X
                           : SkolemCache::SK_ID_V_SPT_X,
-                    "v_spt_x");
+                    "v_spt_x", LENGTH_GEQ_ONE);
                 Node sk2 = d_sk_cache.mkSkolemCached(
                     nfiv[index],
                     nfjv[index],
                     isRev ? SkolemCache::SK_ID_V_SPT_REV_Y
                           : SkolemCache::SK_ID_V_SPT_Y,
-                    "v_spt_y");
+                    "v_spt_y", LENGTH_GEQ_ONE);
                 // must add length requirement
                 info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk1);
                 info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk2);
@@ -3764,12 +3763,12 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
                 else
                 {
                   Node sk = d_sk_cache.mkSkolemCached(
-                      nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt");
+                      nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt", LENGTH_ONE);
                   d_im.registerLength(sk, LENGTH_ONE);
                   Node skr =
                       d_sk_cache.mkSkolemCached(nconst_k,
                                                 SkolemCache::SK_ID_DC_SPT_REM,
-                                                "dc_spt_rem");
+                                                "dc_spt_rem", LENGTH_GEQ_ONE);
                   d_im.registerLength(skr, LENGTH_GEQ_ONE);
                   Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) );
                   eq1 = Rewriter::rewrite( eq1 );
@@ -3810,9 +3809,9 @@ void TheoryStrings::processDeq( Node ni, Node nj ) {
               Node sk2 = d_sk_cache.mkSkolemCached(
                   i, j, SkolemCache::SK_ID_DEQ_Y, "y_dsplit");
               Node sk3 = d_sk_cache.mkSkolemCached(
-                  i, j, SkolemCache::SK_ID_DEQ_Z, "z_dsplit");
+                  i, j, SkolemCache::SK_ID_DEQ_Z, "z_dsplit", LENGTH_GEQ_ONE);
               Node sk4 = d_sk_cache.mkSkolemCached(
-                  i, j, SkolemCache::SK_ID_DEQ_W, "w_dsplit");
+                  i, j, SkolemCache::SK_ID_DEQ_W, "w_dsplit", LENGTH_GEQ_ONE);
               d_im.registerLength(sk3, LENGTH_GEQ_ONE);
               d_im.registerLength(sk4, LENGTH_GEQ_ONE);
               //Node nemp = sk3.eqNode(d_emptyString).negate();
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index f17944027..e14180e8f 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1836,6 +1836,14 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
     return returnRewrite(node, ret, "ss-len-non-pos");
   }
 
+  if (node[1].getKind() == STRING_LENGTH
+      && node[1][0].getKind() == STRING_SUBSTR && node[1][0][0] == node[0]
+      && node[1][0][1] == zero && checkEntailArith(node[1][0][2]))
+  {
+    Node ret = nm->mkNode(STRING_SUBSTR, node[0], node[1][0][2], node[2]);
+    return returnRewrite(node, ret, "ss-len-substr");
+  }
+
   if (node[0].getKind() == STRING_SUBSTR)
   {
     // (str.substr (str.substr x a b) c d) ---> "" if c >= b