Theory strings preprocess (#4534)

This makes it so that the main reduce function in TheoryStringsPreprocess is static, so that it can be used both by the solver and the proof checker.

It also updates the functions to make use of IndexVar for constructing canonical universal variables.

2 files changed, 183 insertions, 145 deletions

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 939146a3d..50c6ede62 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -38,48 +38,45 @@ StringsPreprocess::StringsPreprocess(SkolemCache* sc,
                                      SequencesStatistics& stats)
     : d_sc(sc), d_statistics(stats)
 {
-  //Constants
-  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
-  d_one = NodeManager::currentNM()->mkConst(Rational(1));
-  d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
 }
 
 StringsPreprocess::~StringsPreprocess(){
 
 }
 
-Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
-  unsigned prev_new_nodes = new_nodes.size();
-  Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t << std::endl;
+Node StringsPreprocess::reduce(Node t,
+                               std::vector<Node>& asserts,
+                               SkolemCache* sc)
+{
+  Trace("strings-preprocess-debug")
+      << "StringsPreprocess::reduce: " << t << std::endl;
   Node retNode = t;
-  NodeManager *nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
+  Node zero = nm->mkConst(Rational(0));
+  Node one = nm->mkConst(Rational(1));
+  Node negOne = nm->mkConst(Rational(-1));
 
   if( t.getKind() == kind::STRING_SUBSTR ) {
     // processing term:  substr( s, n, m )
     Node s = t[0];
     Node n = t[1];
     Node m = t[2];
-    Node skt = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst");
+    Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst");
     Node t12 = nm->mkNode(PLUS, n, m);
     t12 = Rewriter::rewrite(t12);
     Node lt0 = nm->mkNode(STRING_LENGTH, s);
     //start point is greater than or equal zero
-    Node c1 = nm->mkNode(GEQ, n, d_zero);
+    Node c1 = nm->mkNode(GEQ, n, zero);
     //start point is less than end of string
     Node c2 = nm->mkNode(GT, lt0, n);
     //length is positive
-    Node c3 = nm->mkNode(GT, m, d_zero);
+    Node c3 = nm->mkNode(GT, m, zero);
     Node cond = nm->mkNode(AND, c1, c2, c3);
 
     Node emp = Word::mkEmptyWord(t.getType());
 
-    Node sk1 = n == d_zero ? emp
-                           : d_sc->mkSkolemCached(
-                                 s, n, SkolemCache::SK_PREFIX, "sspre");
-    Node sk2 = ArithEntail::check(t12, lt0)
-                   ? emp
-                   : d_sc->mkSkolemCached(
-                       s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr");
+    Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre");
+    Node sk2 = 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);
@@ -89,7 +86,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node b13 = nm->mkNode(
         OR,
         nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, nm->mkNode(PLUS, n, m))),
-        nm->mkNode(EQUAL, lsk2, d_zero));
+        nm->mkNode(EQUAL, lsk2, zero));
     // Length of the result is at most m
     Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m);
 
@@ -112,7 +109,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     // satisfied. If n + m is less than the length of s, then len(sk2) = 0
     // cannot be satisfied because we have the constraint that len(skt) <= m,
     // so sk2 must be greater than 0.
-    new_nodes.push_back( lemma );
+    asserts.push_back(lemma);
 
     // Thus, substr( s, n, m ) = skt
     retNode = skt;
@@ -123,15 +120,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node x = t[0];
     Node y = t[1];
     Node n = t[2];
-    Node skk = nm->mkSkolem("iok", nm->integerType(), "created for indexof");
+    Node skk = sc->mkTypedSkolemCached(
+        nm->integerType(), t, SkolemCache::SK_PURIFY, "iok");
 
     Node negone = nm->mkConst(Rational(-1));
     Node krange = nm->mkNode(GEQ, skk, negone);
     // assert:   indexof( x, y, n ) >= -1
-    new_nodes.push_back( krange );
+    asserts.push_back(krange);
     krange = nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, x), skk);
     // assert:   len( x ) >= indexof( x, y, z )
-    new_nodes.push_back( krange );
+    asserts.push_back(krange);
 
     // substr( x, n, len( x ) - n )
     Node st = nm->mkNode(STRING_SUBSTR,
@@ -139,16 +137,16 @@ 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");
+        sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre");
     Node io4 =
-        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost");
+        sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost");
 
     // ~contains( substr( x, n, len( x ) - n ), y )
     Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate();
     // n > len( x )
     Node c12 = nm->mkNode(GT, n, nm->mkNode(STRING_LENGTH, x));
     // 0 > n
-    Node c13 = nm->mkNode(GT, d_zero, n);
+    Node c13 = nm->mkNode(GT, zero, n);
     Node cond1 = nm->mkNode(OR, c11, c12, c13);
     // skk = -1
     Node cc1 = skk.eqNode(negone);
@@ -171,8 +169,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                   nm->mkNode(
                       STRING_SUBSTR,
                       y,
-                      d_zero,
-                      nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), d_one))),
+                      zero,
+                      nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), one))),
               y)
             .negate();
     // skk = n + len( io2 )
@@ -189,7 +187,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //       skk = n + len( io2 )
     // for fresh io2, io4.
     Node rr = nm->mkNode(ITE, cond1, cc1, nm->mkNode(ITE, cond2, cc2, cc3));
-    new_nodes.push_back( rr );
+    asserts.push_back(rr);
 
     // Thus, indexof( x, y, n ) = skk.
     retNode = skk;
@@ -198,7 +196,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
   {
     // processing term:  int.to.str( n )
     Node n = t[0];
-    Node itost = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost");
+    Node itost = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost");
     Node leni = nm->mkNode(STRING_LENGTH, itost);
 
     std::vector<Node> conc;
@@ -206,21 +204,20 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     argTypes.push_back(nm->integerType());
     Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
 
-    Node lem = nm->mkNode(GEQ, leni, d_one);
+    Node lem = nm->mkNode(GEQ, leni, one);
     conc.push_back(lem);
 
     lem = n.eqNode(nm->mkNode(APPLY_UF, u, leni));
     conc.push_back(lem);
 
-    lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero));
+    lem = zero.eqNode(nm->mkNode(APPLY_UF, u, zero));
     conc.push_back(lem);
 
-    Node x = nm->mkBoundVar(nm->integerType());
-    Node xPlusOne = nm->mkNode(PLUS, x, d_one);
+    Node x = SkolemCache::mkIndexVar(t);
+    Node xPlusOne = nm->mkNode(PLUS, x, one);
     Node xbv = nm->mkNode(BOUND_VAR_LIST, x);
-    Node g =
-        nm->mkNode(AND, nm->mkNode(GEQ, x, d_zero), nm->mkNode(LT, x, leni));
-    Node sx = nm->mkNode(STRING_SUBSTR, itost, x, d_one);
+    Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, leni));
+    Node sx = nm->mkNode(STRING_SUBSTR, itost, x, one);
     Node ux = nm->mkNode(APPLY_UF, u, x);
     Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne);
     Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
@@ -229,10 +226,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node ten = nm->mkConst(Rational(10));
     Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
     Node leadingZeroPos =
-        nm->mkNode(AND, x.eqNode(d_zero), nm->mkNode(GT, leni, d_one));
+        nm->mkNode(AND, x.eqNode(zero), nm->mkNode(GT, leni, one));
     Node cb = nm->mkNode(
         AND,
-        nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, d_one, d_zero)),
+        nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, one, zero)),
         nm->mkNode(LT, c, ten));
 
     Node ux1lem = nm->mkNode(GEQ, n, ux1);
@@ -241,11 +238,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     lem = nm->mkNode(FORALL, xbv, lem);
     conc.push_back(lem);
 
-    Node nonneg = nm->mkNode(GEQ, n, d_zero);
+    Node nonneg = nm->mkNode(GEQ, n, zero);
 
     Node emp = Word::mkEmptyWord(t.getType());
     lem = nm->mkNode(ITE, nonneg, nm->mkNode(AND, conc), itost.eqNode(emp));
-    new_nodes.push_back(lem);
+    asserts.push_back(lem);
     // assert:
     // IF n>=0
     // THEN:
@@ -274,26 +271,27 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     retNode = itost;
   } else if( t.getKind() == kind::STRING_STOI ) {
     Node s = t[0];
-    Node stoit = nm->mkSkolem("stoit", nm->integerType(), "created for stoi");
+    Node stoit = sc->mkTypedSkolemCached(
+        nm->integerType(), t, SkolemCache::SK_PURIFY, "stoit");
     Node lens = nm->mkNode(STRING_LENGTH, s);
 
     std::vector<Node> conc1;
-    Node lem = stoit.eqNode(d_neg_one);
+    Node lem = stoit.eqNode(negOne);
     conc1.push_back(lem);
 
     Node emp = Word::mkEmptyWord(s.getType());
     Node sEmpty = s.eqNode(emp);
     Node k = nm->mkSkolem("k", nm->integerType());
-    Node kc1 = nm->mkNode(GEQ, k, d_zero);
+    Node kc1 = nm->mkNode(GEQ, k, zero);
     Node kc2 = nm->mkNode(LT, k, lens);
     Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
     Node codeSk = nm->mkNode(
         MINUS,
-        nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, d_one)),
+        nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)),
         c0);
     Node ten = nm->mkConst(Rational(10));
     Node kc3 = nm->mkNode(
-        OR, nm->mkNode(LT, codeSk, d_zero), nm->mkNode(GEQ, codeSk, ten));
+        OR, nm->mkNode(LT, codeSk, zero), nm->mkNode(GEQ, codeSk, ten));
     conc1.push_back(nm->mkNode(OR, sEmpty, nm->mkNode(AND, kc1, kc2, kc3)));
 
     std::vector<Node> conc2;
@@ -304,24 +302,22 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     lem = stoit.eqNode(nm->mkNode(APPLY_UF, u, lens));
     conc2.push_back(lem);
 
-    lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero));
+    lem = zero.eqNode(nm->mkNode(APPLY_UF, u, zero));
     conc2.push_back(lem);
 
-    lem = nm->mkNode(GT, lens, d_zero);
+    lem = nm->mkNode(GT, lens, zero);
     conc2.push_back(lem);
 
-    Node x = nm->mkBoundVar(nm->integerType());
+    Node x = SkolemCache::mkIndexVar(t);
     Node xbv = nm->mkNode(BOUND_VAR_LIST, x);
-    Node g =
-        nm->mkNode(AND, nm->mkNode(GEQ, x, d_zero), nm->mkNode(LT, x, lens));
-    Node sx = nm->mkNode(STRING_SUBSTR, s, x, d_one);
+    Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, lens));
+    Node sx = nm->mkNode(STRING_SUBSTR, s, x, one);
     Node ux = nm->mkNode(APPLY_UF, u, x);
-    Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, d_one));
+    Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, one));
     Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
 
     Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
-    Node cb =
-        nm->mkNode(AND, nm->mkNode(GEQ, c, d_zero), nm->mkNode(LT, c, ten));
+    Node cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten));
 
     Node ux1lem = nm->mkNode(GEQ, stoit, ux1);
 
@@ -329,9 +325,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     lem = nm->mkNode(FORALL, xbv, lem);
     conc2.push_back(lem);
 
-    Node sneg = nm->mkNode(LT, stoit, d_zero);
+    Node sneg = nm->mkNode(LT, stoit, zero);
     lem = nm->mkNode(ITE, sneg, nm->mkNode(AND, conc1), nm->mkNode(AND, conc2));
-    new_nodes.push_back(lem);
+    asserts.push_back(lem);
 
     // assert:
     // IF stoit < 0
@@ -362,10 +358,10 @@ 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");
+        sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre");
     Node rp2 =
-        d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost");
-    Node rpw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw");
+        sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost");
+    Node rpw = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw");
 
     // y = ""
     Node emp = Word::mkEmptyWord(tn);
@@ -387,10 +383,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        rp1,
                        nm->mkNode(kind::STRING_SUBSTR,
                                   y,
-                                  d_zero,
+                                  zero,
                                   nm->mkNode(kind::MINUS,
                                              nm->mkNode(kind::STRING_LENGTH, y),
-                                             d_one))),
+                                             one))),
                    y)
             .negate();
 
@@ -410,7 +406,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                                     cond2,
                                     nm->mkNode(kind::AND, c21, c22, c23),
                                     rpw.eqNode(x)));
-    new_nodes.push_back( rr );
+    asserts.push_back(rr);
 
     // Thus, replace( x, y, z ) = rpw.
     retNode = rpw;
@@ -421,16 +417,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node x = t[0];
     Node y = t[1];
     Node z = t[2];
-    Node rpaw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw");
+    Node rpaw = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw");
 
-    Node numOcc = d_sc->mkTypedSkolemCached(
+    Node numOcc = sc->mkTypedSkolemCached(
         nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc");
     std::vector<TypeNode> argTypes;
     argTypes.push_back(nm->integerType());
     Node us =
         nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
     TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType());
-    Node uf = d_sc->mkTypedSkolemCached(
+    Node uf = sc->mkTypedSkolemCached(
         ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf");
 
     Node ufno = nm->mkNode(APPLY_UF, uf, numOcc);
@@ -438,27 +434,27 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node rem = nm->mkNode(STRING_SUBSTR, x, ufno, nm->mkNode(STRING_LENGTH, x));
 
     std::vector<Node> lem;
-    lem.push_back(nm->mkNode(GEQ, numOcc, d_zero));
-    lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, d_zero)));
+    lem.push_back(nm->mkNode(GEQ, numOcc, zero));
+    lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, zero)));
     lem.push_back(usno.eqNode(rem));
-    lem.push_back(nm->mkNode(APPLY_UF, uf, d_zero).eqNode(d_zero));
-    lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(d_neg_one));
+    lem.push_back(nm->mkNode(APPLY_UF, uf, zero).eqNode(zero));
+    lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(negOne));
 
-    Node i = nm->mkBoundVar(nm->integerType());
+    Node i = SkolemCache::mkIndexVar(t);
     Node bvli = nm->mkNode(BOUND_VAR_LIST, i);
     Node bound =
-        nm->mkNode(AND, nm->mkNode(GEQ, i, d_zero), nm->mkNode(LT, i, numOcc));
+        nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc));
     Node ufi = nm->mkNode(APPLY_UF, uf, i);
-    Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, d_one));
+    Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, one));
     Node ii = nm->mkNode(STRING_STRIDOF, x, y, ufi);
     Node cc = nm->mkNode(
         STRING_CONCAT,
         nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)),
         z,
-        nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, d_one)));
+        nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one)));
 
     std::vector<Node> flem;
-    flem.push_back(ii.eqNode(d_neg_one).negate());
+    flem.push_back(ii.eqNode(negOne).negate());
     flem.push_back(nm->mkNode(APPLY_UF, us, i).eqNode(cc));
     flem.push_back(
         ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y))));
@@ -487,7 +483,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node emp = Word::mkEmptyWord(t.getType());
     Node assert =
         nm->mkNode(ITE, y.eqNode(emp), rpaw.eqNode(x), nm->mkNode(AND, lem));
-    new_nodes.push_back(assert);
+    asserts.push_back(assert);
 
     // Thus, replaceall( x, y, z ) = rpaw
     retNode = rpaw;
@@ -495,19 +491,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
   else if (t.getKind() == STRING_TOLOWER || t.getKind() == STRING_TOUPPER)
   {
     Node x = t[0];
-    Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r");
+    Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r");
 
     Node lenx = nm->mkNode(STRING_LENGTH, x);
     Node lenr = nm->mkNode(STRING_LENGTH, r);
     Node eqLenA = lenx.eqNode(lenr);
 
-    Node i = nm->mkBoundVar(nm->integerType());
+    Node i = SkolemCache::mkIndexVar(t);
     Node bvi = nm->mkNode(BOUND_VAR_LIST, i);
 
-    Node ci =
-        nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, d_one));
-    Node ri =
-        nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, d_one));
+    Node ci = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, one));
+    Node ri = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, one));
 
     Node lb = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65));
     Node ub = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90));
@@ -521,7 +515,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
         ci);
 
     Node bound =
-        nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, lenr));
+        nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
     Node rangeA =
         nm->mkNode(FORALL, bvi, nm->mkNode(OR, bound.negate(), ri.eqNode(res)));
 
@@ -533,7 +527,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //     str.code( str.substr(r,i,1) ) = ite( 97 <= ci <= 122, ci-32, ci)
     // where ci = str.code( str.substr(x,i,1) )
     Node assert = nm->mkNode(AND, eqLenA, rangeA);
-    new_nodes.push_back(assert);
+    asserts.push_back(assert);
 
     // Thus, toLower( x ) = r
     retNode = r;
@@ -541,22 +535,22 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
   else if (t.getKind() == STRING_REV)
   {
     Node x = t[0];
-    Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r");
+    Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r");
 
     Node lenx = nm->mkNode(STRING_LENGTH, x);
     Node lenr = nm->mkNode(STRING_LENGTH, r);
     Node eqLenA = lenx.eqNode(lenr);
 
-    Node i = nm->mkBoundVar(nm->integerType());
+    Node i = SkolemCache::mkIndexVar(t);
     Node bvi = nm->mkNode(BOUND_VAR_LIST, i);
 
     Node revi = nm->mkNode(
-        MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, d_one));
-    Node ssr = nm->mkNode(STRING_SUBSTR, r, i, d_one);
-    Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, d_one);
+        MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one));
+    Node ssr = nm->mkNode(STRING_SUBSTR, r, i, one);
+    Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, one);
 
     Node bound =
-        nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, lenr));
+        nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
     Node rangeA = nm->mkNode(
         FORALL, bvi, nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx)));
     // assert:
@@ -564,7 +558,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //   forall i. 0 <= i < len(r) =>
     //     substr(r,i,1) = substr(x,len(x)-(i+1),1)
     Node assert = nm->mkNode(AND, eqLenA, rangeA);
-    new_nodes.push_back(assert);
+    asserts.push_back(assert);
 
     // Thus, (str.rev x) = r
     retNode = r;
@@ -576,31 +570,38 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //negative contains reduces to existential
     Node lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
     Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
-    Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+    Node b1 = SkolemCache::mkIndexVar(t);
     Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
-    Node body = NodeManager::currentNM()->mkNode( kind::AND, 
-                  NodeManager::currentNM()->mkNode( kind::LEQ, d_zero, b1 ),
-                  NodeManager::currentNM()->mkNode( kind::LEQ, b1, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ) ),
-                  NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens), s )                
-                );
+    Node body = NodeManager::currentNM()->mkNode(
+        kind::AND,
+        NodeManager::currentNM()->mkNode(kind::LEQ, zero, b1),
+        NodeManager::currentNM()->mkNode(
+            kind::LEQ,
+            b1,
+            NodeManager::currentNM()->mkNode(kind::MINUS, lenx, lens)),
+        NodeManager::currentNM()->mkNode(
+            kind::EQUAL,
+            NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens),
+            s));
     retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body );
   }
   else if (t.getKind() == kind::STRING_LEQ)
   {
-    Node ltp = nm->mkSkolem("ltp", nm->booleanType());
+    Node ltp = sc->mkTypedSkolemCached(
+        nm->booleanType(), t, SkolemCache::SK_PURIFY, "ltp");
     Node k = nm->mkSkolem("k", nm->integerType());
 
     std::vector<Node> conj;
-    conj.push_back(nm->mkNode(GEQ, k, d_zero));
+    conj.push_back(nm->mkNode(GEQ, k, zero));
     Node substr[2];
     Node code[2];
     for (unsigned r = 0; r < 2; r++)
     {
       Node ta = t[r];
       Node tb = t[1 - r];
-      substr[r] = nm->mkNode(STRING_SUBSTR, ta, d_zero, k);
+      substr[r] = nm->mkNode(STRING_SUBSTR, ta, zero, k);
       code[r] =
-          nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, d_one));
+          nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, one));
       conj.push_back(nm->mkNode(LEQ, k, nm->mkNode(STRING_LENGTH, ta)));
     }
     conj.push_back(substr[0].eqNode(substr[1]));
@@ -632,18 +633,29 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //        ELSE: str.code(substr( x, k, 1 )) > str.code(substr( y, k, 1 ))
     Node assert =
         nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj));
-    new_nodes.push_back(assert);
+    asserts.push_back(assert);
 
     // Thus, str.<=( x, y ) = ltp
     retNode = ltp;
   }
+  return retNode;
+}
 
+Node StringsPreprocess::simplify(Node t, std::vector<Node>& asserts)
+{
+  size_t prev_asserts = asserts.size();
+  // call the static reduce routine
+  Node retNode = reduce(t, asserts, d_sc);
   if( t!=retNode ){
     Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl;
-    if(!new_nodes.empty()) {
-      Trace("strings-preprocess") << " ... new nodes (" << (new_nodes.size()-prev_new_nodes) << "):" << std::endl;
-      for(unsigned int i=prev_new_nodes; i<new_nodes.size(); ++i) {
-        Trace("strings-preprocess") << "   " << new_nodes[i] << std::endl;
+    if (!asserts.empty())
+    {
+      Trace("strings-preprocess")
+          << " ... new nodes (" << (asserts.size() - prev_asserts)
+          << "):" << std::endl;
+      for (size_t i = prev_asserts; i < asserts.size(); ++i)
+      {
+        Trace("strings-preprocess") << "   " << asserts[i] << std::endl;
       }
     }
     d_statistics.d_reductions << t.getKind();
@@ -656,14 +668,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
   return retNode;
 }
 
-Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, std::map< Node, Node >& visited ){
+Node StringsPreprocess::simplifyRec(Node t,
+                                    std::vector<Node>& asserts,
+                                    std::map<Node, Node>& visited)
+{
   std::map< Node, Node >::iterator it = visited.find(t);
   if( it!=visited.end() ){
     return it->second;
   }else{
     Node retNode = t;
     if( t.getNumChildren()==0 ){
-      retNode = simplify( t, new_nodes );
+      retNode = simplify(t, asserts);
     }else if( t.getKind()!=kind::FORALL ){
       bool changed = false;
       std::vector< Node > cc;
@@ -671,7 +686,7 @@ Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, st
         cc.push_back( t.getOperator() );
       }
       for(unsigned i=0; i<t.getNumChildren(); i++) {
-        Node s = simplifyRec( t[i], new_nodes, visited );
+        Node s = simplifyRec(t[i], asserts, visited);
         cc.push_back( s );
         if( s!=t[i] ) {
           changed = true;
@@ -681,24 +696,27 @@ Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, st
       if( changed ){
         tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc );
       }
-      retNode = simplify( tmp, new_nodes ); 
+      retNode = simplify(tmp, asserts);
     }
     visited[t] = retNode;
     return retNode;
   }
 }
 
-Node StringsPreprocess::processAssertion( Node n, std::vector< Node > &new_nodes ) {
+Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts)
+{
   std::map< Node, Node > visited;
-  std::vector< Node > new_nodes_curr;
-  Node ret = simplifyRec( n, new_nodes_curr, visited );
-  while( !new_nodes_curr.empty() ){
-    Node curr = new_nodes_curr.back();
-    new_nodes_curr.pop_back();
-    std::vector< Node > new_nodes_tmp;
-    curr = simplifyRec( curr, new_nodes_tmp, visited );
-    new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() );
-    new_nodes.push_back( curr );
+  std::vector<Node> asserts_curr;
+  Node ret = simplifyRec(n, asserts_curr, visited);
+  while (!asserts_curr.empty())
+  {
+    Node curr = asserts_curr.back();
+    asserts_curr.pop_back();
+    std::vector<Node> asserts_tmp;
+    curr = simplifyRec(curr, asserts_tmp, visited);
+    asserts_curr.insert(
+        asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end());
+    asserts.push_back(curr);
   }
   return ret;
 }
@@ -708,18 +726,22 @@ void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){
   for( unsigned i=0; i<vec_node.size(); i++ ){
     Trace("strings-preprocess-debug") << "Preprocessing assertion " << vec_node[i] << std::endl;
     //preprocess until fixed point
-    std::vector< Node > new_nodes;
-    std::vector< Node > new_nodes_curr;
-    new_nodes_curr.push_back( vec_node[i] );
-    while( !new_nodes_curr.empty() ){
-      Node curr = new_nodes_curr.back();
-      new_nodes_curr.pop_back();
-      std::vector< Node > new_nodes_tmp;
-      curr = simplifyRec( curr, new_nodes_tmp, visited );
-      new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() );
-      new_nodes.push_back( curr );
+    std::vector<Node> asserts;
+    std::vector<Node> asserts_curr;
+    asserts_curr.push_back(vec_node[i]);
+    while (!asserts_curr.empty())
+    {
+      Node curr = asserts_curr.back();
+      asserts_curr.pop_back();
+      std::vector<Node> asserts_tmp;
+      curr = simplifyRec(curr, asserts_tmp, visited);
+      asserts_curr.insert(
+          asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end());
+      asserts.push_back(curr);
     }
-    Node res = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
+    Node res = asserts.size() == 1
+                   ? asserts[0]
+                   : NodeManager::currentNM()->mkNode(kind::AND, asserts);
     if( res!=vec_node[i] ){
       res = Rewriter::rewrite( res );
       PROOF( ProofManager::currentPM()->addDependence( res, vec_node[i] ); );
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index fb6404aa6..1392b4ea1 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -44,21 +44,41 @@ class StringsPreprocess {
                     context::UserContext* u,
                     SequencesStatistics& stats);
   ~StringsPreprocess();
+  /** The reduce routine
+   *
+   * This is the main routine for constructing the reduction lemma for
+   * an extended function t. It returns the simplified form of t, as well
+   * as assertions for t, interpeted conjunctively.  The reduction lemma
+   * for t is:
+   *   asserts[0] ^ ... ^ asserts[n] ^ t = t'
+   * where t' is the term returned by this method.
+   * The argument sc defines the methods for generating new Skolem variables.
+   * The return value is t itself if it is not reduced by this class.
+   *
+   * The reduction lemma for t is a way of specifying the complete semantics
+   * of t. In other words, any model satisfying the reduction lemma of t
+   * correctly interprets t.
+   *
+   * @param t The node to reduce,
+   * @param asserts The vector for storing the assertions that correspond to
+   * the reduction of t,
+   * @param sc The skolem cache for generating new variables,
+   * @return The reduced form of t.
+   */
+  static Node reduce(Node t, std::vector<Node>& asserts, SkolemCache* sc);
   /**
-   * Returns a node t' such that
-   *   (exists k) new_nodes => t = t'
-   * is valid, where k are the free skolems introduced when constructing
-   * new_nodes.
+   * Calls the above method for the skolem cache owned by this class, and
+   * records statistics.
    */
-  Node simplify(Node t, std::vector<Node>& new_nodes);
+  Node simplify(Node t, std::vector<Node>& asserts);
   /**
    * Applies simplifyRec on t until a fixed point is reached, and returns
    * the resulting term t', which is such that
-   *   (exists k) new_nodes => t = t'
+   *   (exists k) asserts => t = t'
    * is valid, where k are the free skolems introduced when constructing
-   * new_nodes.
+   * asserts.
    */
-  Node processAssertion(Node t, std::vector<Node>& new_nodes);
+  Node processAssertion(Node t, std::vector<Node>& asserts);
   /**
    * Replaces all formulas t in vec_node with an equivalent formula t' that
    * contains no free instances of extended functions (that is, extended
@@ -68,21 +88,17 @@ class StringsPreprocess {
   void processAssertions(std::vector<Node>& vec_node);
 
  private:
-  /** commonly used constants */
-  Node d_zero;
-  Node d_one;
-  Node d_neg_one;
   /** pointer to the skolem cache used by this class */
   SkolemCache* d_sc;
   /** Reference to the statistics for the theory of strings/sequences. */
   SequencesStatistics& d_statistics;
   /**
    * Applies simplify to all top-level extended function subterms of t. New
-   * assertions created in this reduction are added to new_nodes. The argument
+   * assertions created in this reduction are added to asserts. The argument
    * visited stores a cache of previous results.
    */
   Node simplifyRec(Node t,
-                   std::vector<Node>& new_nodes,
+                   std::vector<Node>& asserts,
                    std::map<Node, Node>& visited);
 };