More aggressive caching of string skolems. (#2491)

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 2d5bef519a7de2fd2665acdc794798c16254dbab..ba6caaf79a4ae9acb84e78cfc73e76b80fdf29ba 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -22,6 +22,7 @@
 #include "options/strings_options.h"
 #include "proof/proof_manager.h"
 #include "smt/logic_exception.h"
+#include "theory/strings/theory_strings_rewriter.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -66,9 +67,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node c3 = nm->mkNode(GT, m, d_zero);
     Node cond = nm->mkNode(AND, c1, c2, c3);
 
-    Node sk1 = d_sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre");
-    Node sk2 =
-        d_sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr");
+    Node sk1 = n == d_zero ? d_empty_str
+                           : d_sc->mkSkolemCached(
+                                 s, n, SkolemCache::SK_PREFIX, "sspre");
+    Node sk2 = TheoryStringsRewriter::checkEntailArith(t12, lt0)
+                   ? d_empty_str
+                   : d_sc->mkSkolemCached(
+                         s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr");
     Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, skt, sk2));
     //length of first skolem is second argument
     Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
@@ -97,62 +102,63 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
   else if (t.getKind() == kind::STRING_STRIDOF)
   {
     // processing term:  indexof( x, y, n )
+    Node x = t[0];
+    Node y = t[1];
+    Node n = t[2];
     Node skk = nm->mkSkolem("iok", nm->integerType(), "created for indexof");
 
-    Node negone = nm->mkConst(::CVC4::Rational(-1));
-    Node krange = nm->mkNode(kind::GEQ, skk, negone);
+    Node negone = nm->mkConst(Rational(-1));
+    Node krange = nm->mkNode(GEQ, skk, negone);
     // assert:   indexof( x, y, n ) >= -1
     new_nodes.push_back( krange );
-    krange = nm->mkNode(kind::GEQ, nm->mkNode(kind::STRING_LENGTH, t[0]), skk);
+    krange = nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, x), skk);
     // assert:   len( x ) >= indexof( x, y, z )
     new_nodes.push_back( krange );
 
     // substr( x, n, len( x ) - n )
-    Node st = nm->mkNode(
-        kind::STRING_SUBSTR,
-        t[0],
-        t[2],
-        nm->mkNode(kind::MINUS, nm->mkNode(kind::STRING_LENGTH, t[0]), t[2]));
-    Node io2 = nm->mkSkolem("io2", nm->stringType(), "created for indexof");
-    Node io4 = nm->mkSkolem("io4", nm->stringType(), "created for indexof");
+    Node st = nm->mkNode(STRING_SUBSTR,
+                         x,
+                         n,
+                         nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n));
+    Node io2 =
+        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre");
+    Node io4 =
+        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost");
 
     // ~contains( substr( x, n, len( x ) - n ), y )
-    Node c11 = nm->mkNode(kind::STRING_STRCTN, st, t[1]).negate();
+    Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate();
     // n > len( x )
-    Node c12 =
-        nm->mkNode(kind::GT, t[2], nm->mkNode(kind::STRING_LENGTH, t[0]));
+    Node c12 = nm->mkNode(GT, n, nm->mkNode(STRING_LENGTH, x));
     // 0 > n
-    Node c13 = nm->mkNode(kind::GT, d_zero, t[2]);
-    Node cond1 = nm->mkNode(kind::OR, c11, c12, c13);
+    Node c13 = nm->mkNode(GT, d_zero, n);
+    Node cond1 = nm->mkNode(OR, c11, c12, c13);
     // skk = -1
     Node cc1 = skk.eqNode(negone);
 
     // y = ""
-    Node cond2 = t[1].eqNode(nm->mkConst(CVC4::String("")));
+    Node cond2 = y.eqNode(d_empty_str);
     // skk = n
     Node cc2 = skk.eqNode(t[2]);
 
     // substr( x, n, len( x ) - n ) = str.++( io2, y, io4 )
-    Node c31 = st.eqNode(nm->mkNode(kind::STRING_CONCAT, io2, t[1], io4));
+    Node c31 = st.eqNode(nm->mkNode(STRING_CONCAT, io2, y, io4));
     // ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y )
     Node c32 =
         nm->mkNode(
-              kind::STRING_STRCTN,
+              STRING_STRCTN,
               nm->mkNode(
-                  kind::STRING_CONCAT,
+                  STRING_CONCAT,
                   io2,
-                  nm->mkNode(kind::STRING_SUBSTR,
-                             t[1],
-                             d_zero,
-                             nm->mkNode(kind::MINUS,
-                                        nm->mkNode(kind::STRING_LENGTH, t[1]),
-                                        d_one))),
-              t[1])
+                  nm->mkNode(
+                      STRING_SUBSTR,
+                      y,
+                      d_zero,
+                      nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), d_one))),
+              y)
             .negate();
     // skk = n + len( io2 )
-    Node c33 = skk.eqNode(
-        nm->mkNode(kind::PLUS, t[2], nm->mkNode(kind::STRING_LENGTH, io2)));
-    Node cc3 = nm->mkNode(kind::AND, c31, c32, c33);
+    Node c33 = skk.eqNode(nm->mkNode(PLUS, n, nm->mkNode(STRING_LENGTH, io2)));
+    Node cc3 = nm->mkNode(AND, c31, c32, c33);
 
     // assert:
     // IF:   ~contains( substr( x, n, len( x ) - n ), y ) OR n > len(x) OR 0 > n
@@ -163,8 +169,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //       ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y ) ^
     //       skk = n + len( io2 )
     // for fresh io2, io4.
-    Node rr = nm->mkNode(
-        kind::ITE, cond1, cc1, nm->mkNode(kind::ITE, cond2, cc2, cc3));
+    Node rr = nm->mkNode(ITE, cond1, cc1, nm->mkNode(ITE, cond2, cc2, cc3));
     new_nodes.push_back( rr );
 
     // Thus, indexof( x, y, n ) = skk.
@@ -174,7 +179,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //        NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
     //        t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0])));
     Node num = t[0];
-    Node pret = nm->mkSkolem("itost", nm->stringType(), "created for itos");
+    Node pret = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost");
     Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
 
     Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero);