Improved handling of extended operators. Do preprocess on memberships eagerly, only...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ae93176b26d26066f29559461bfd3f33d0075205..337c5104ca556f04103ac7ecef0a3993b4ca6a8e 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3294,18 +3294,16 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-bv-to-bool", d_assertions);
     Trace("smt") << "POST bvToBool" << endl;
   }
-  if( !options::stringLazyPreproc() ){
-    if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
-      Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl;
-      dumpAssertions("pre-strings-pp", d_assertions);
-      CVC4::theory::strings::StringsPreprocess sp;
-      sp.simplify( d_assertions.ref() );
-      //for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      //  d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
-      //}
-      Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
-      dumpAssertions("post-strings-pp", d_assertions);
-    }
+  if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl;
+    dumpAssertions("pre-strings-pp", d_assertions);
+    CVC4::theory::strings::StringsPreprocess sp;
+    sp.simplify( d_assertions.ref() );
+    //for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    //  d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
+    //}
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
+    dumpAssertions("post-strings-pp", d_assertions);
   }
   if( d_smt.d_logic.isQuantified() ){
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;

diff --git a/src/theory/strings/options b/src/theory/strings/options
index 8a839a1188e1fedcf18c4a08eddf897f3a599bcf..21e1a7e4dc2435e1e6aaca187740f6dddd20e006 100644 (file)
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -35,4 +35,7 @@ option stringIgnNegMembership strings-inm --strings-inm bool :default false
 option stringLazyPreproc strings-lazy-pp --strings-lazy-pp bool :default true
  perform string preprocessing lazily
 
+option stringLenGeqZ strings-len-geqz --strings-len-geqz bool :default false
+ strings length greater than zero lemmas
+
 endmodule

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 507c74c53a9e1543149af1122fad0cd4753be08d..444115af447095b01c571ffe54e4f3a56e953a9c 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -26,6 +26,8 @@
 #include "theory/strings/type_enumerator.h"
 #include <cmath>
 
+#define LAZY_ADD_MEMBERSHIP
+
 using namespace std;
 using namespace CVC4::context;
 
@@ -44,14 +46,14 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
   d_nf_pairs(c),
   d_loop_antec(u),
   d_length_intro_vars(u),
-  d_registed_terms_cache(u),
-  d_length_inst(u),
-  d_str_pos_ctn(c),
-  d_str_neg_ctn(c),
+  d_registered_terms_cache(u),
+  d_preproc_cache(u),
+  d_proxy_var(u),
   d_neg_ctn_eqlen(u),
   d_neg_ctn_ulen(u),
   d_pos_ctn_cached(u),
   d_neg_ctn_cached(u),
+  d_ext_func_terms(c),
   d_regexp_memberships(c),
   d_regexp_ucached(u),
   d_regexp_ccached(c),
@@ -330,7 +332,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
       Trace("strings-model") << col[i][j] << " ";
       //check if col[i][j] has only variables
       EqcInfo* ei = getOrMakeEqcInfo( col[i][j], false );
-            Node cst = ei ? ei->d_const_term : Node::null();
+      Node cst = ei ? ei->d_const_term : Node::null();
       if( cst.isNull() ){
         Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() );
         if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){
@@ -414,72 +416,20 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
 // MAIN SOLVER
 /////////////////////////////////////////////////////////////////////////////
 
-/*
+
 void TheoryStrings::preRegisterTerm(TNode n) {
-  if(d_registed_terms_cache.find(n) == d_registed_terms_cache.end()) {
-    Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl;
-    //collectTerms( n );
-    switch (n.getKind()) {
-      case kind::EQUAL:
-        d_equalityEngine.addTriggerEquality(n);
-        break;
-      case kind::STRING_IN_REGEXP:
-        //do not add trigger here
-        d_equalityEngine.addTriggerPredicate(n);
-        break;
-      case kind::STRING_SUBSTR_TOTAL: {
-        Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
-                  NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
-                  NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
-        Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
-        Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
-        Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-        Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-        Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
-        d_statistics.d_new_skolems += 2;
-        Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) );
-        Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-        Node lenc = n[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ) );
-        Node lemma = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, cond,
-          NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
-          n.eqNode(d_emptyString)));
-        Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
-        d_out->lemma(lemma);
-        //d_equalityEngine.addTerm(n);
-      }
-      default: {
-        if(n.getType().isString() && n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
-          if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) {
-            Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-            Node n_len_eq_z = n_len.eqNode( d_zero );
-            n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
-            Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
-                        NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
-            Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
-            d_out->lemma(n_len_geq_zero);
-            d_out->requirePhase( n_len_eq_z, true );
-          }
-          // FMF
-          if( n.getKind() == kind::VARIABLE && options::stringFMF() ) {
-            d_input_vars.insert(n);
-          }
-        }
-        if (n.getType().isBoolean()) {
-          // Get triggered for both equal and dis-equal
-          d_equalityEngine.addTriggerPredicate(n);
-        } else {
-          // Function applications/predicates
-          d_equalityEngine.addTerm(n);
-        }
+  if( d_registered_terms_cache.find(n) == d_registered_terms_cache.end() ) {
+    //check for logic exceptions
+    if( !options::stringExp() ){
+      if( n.getKind()==kind::STRING_STRIDOF ||
+          n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_U16TOS || n.getKind() == kind::STRING_U32TOS ||
+          n.getKind() == kind::STRING_STOI || n.getKind() == kind::STRING_STOU16 || n.getKind() == kind::STRING_STOU32 ||
+          n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){
+        std::stringstream ss;
+        ss << "Term of kind " << n.getKind() << " not supported in default mode, try --strings-exp";
+        throw LogicException(ss.str());
       }
     }
-    d_registed_terms_cache.insert(n);
-  }
-}
-*/
-
-void TheoryStrings::preRegisterTerm(TNode n) {
-  if( d_registed_terms_cache.find(n) == d_registed_terms_cache.end() ) {
     switch( n.getKind() ) {
       case kind::EQUAL: {
         d_equalityEngine.addTriggerEquality(n);
@@ -509,7 +459,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
         }
       }
     }
-    d_registed_terms_cache.insert(n);
+    d_registered_terms_cache.insert(n);
   }
 }
 
@@ -600,20 +550,39 @@ void TheoryStrings::check(Effort e) {
     polarity = fact.getKind() != kind::NOT;
     atom = polarity ? fact : fact[0];
 
-    //run preprocess
+    //run preprocess on memberships
+    bool addFact = true;
     if( options::stringLazyPreproc() ){
-      std::map< Node, Node >::iterator itp = d_preproc_cache.find( atom );
-      if( itp==d_preproc_cache.end() ){
+      NodeBoolMap::const_iterator it = d_preproc_cache.find( atom );
+      if( it==d_preproc_cache.end() ){
+        d_preproc_cache[ atom ] = true;
         std::vector< Node > new_nodes;
         Node res = d_preproc.decompose( atom, new_nodes );
-        d_preproc_cache[atom] = res;
         if( atom!=res ){
-          Trace("strings-assertion-debug") << "...preprocessed to : " << res << std::endl;
-          Node plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res );
-          plem = Rewriter::rewrite( plem );
-          d_out->lemma( plem );
-          Trace("strings-pp-lemma") << "Preprocess eq lemma : " << plem << std::endl;
-          Trace("strings-pp-lemma") << "...from " << fact << std::endl;
+          //check if reduction/deduction
+          std::vector< Node > subs_lhs;
+          std::vector< Node > subs_rhs;
+          subs_lhs.push_back( atom );
+          subs_rhs.push_back( d_true );
+          Node sres = res.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+          sres = Rewriter::rewrite( sres );
+          if( sres!=res ){
+            Node plem = NodeManager::currentNM()->mkNode( kind::IMPLIES, atom, sres );
+            plem = Rewriter::rewrite( plem );
+            d_out->lemma( plem );
+            Trace("strings-pp-lemma") << "Preprocess impl lemma : " << plem << std::endl;
+            Trace("strings-pp-lemma") << "...from " << fact << std::endl;
+          }else{
+            Trace("strings-assertion-debug") << "...preprocessed to : " << res << std::endl;
+            Node plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res );
+            plem = Rewriter::rewrite( plem );
+            d_out->lemma( plem );
+            Trace("strings-pp-lemma") << "Preprocess eq lemma : " << plem << std::endl;
+            Trace("strings-pp-lemma") << "...from " << fact << std::endl;
+            //reduced by preprocess
+            addFact = false;
+            d_preproc_cache[ atom ] = false;
+          }
         }else{
           Trace("strings-assertion-debug") << "...preprocess ok." << std::endl;
         }
@@ -625,26 +594,13 @@ void TheoryStrings::check(Effort e) {
           Trace("strings-pp-lemma") << "...from " << fact << std::endl;
           d_out->lemma( nnlem );
         }
+      }else{
+        addFact = (*it).second;
       }
     }
-
-    //must record string in regular expressions
-    if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
-      addMembership(assertion);
-      //if(polarity || !options::stringIgnNegMembership()) {
-        d_equalityEngine.assertPredicate(atom, polarity, fact);
-      //}
-    } else if (atom.getKind() == kind::STRING_STRCTN) {
-      if(polarity) {
-        d_str_pos_ctn.push_back( atom );
-      } else {
-        d_str_neg_ctn.push_back( atom );
-      }
-      d_equalityEngine.assertPredicate(atom, polarity, fact);
-    } else if (atom.getKind() == kind::EQUAL) {
-      d_equalityEngine.assertEquality(atom, polarity, fact);
-    } else {
-      d_equalityEngine.assertPredicate(atom, polarity, fact);
+    //assert pending fact
+    if( addFact ){
+      assertPendingFact( atom, polarity, fact );
     }
   }
   doPendingFacts();
@@ -654,28 +610,28 @@ void TheoryStrings::check(Effort e) {
   bool addedLemma = false;
   if( e == EFFORT_FULL && !d_conflict && !d_valuation.needCheck() ) {
     Trace("strings-check") << "Theory of strings full effort check " << std::endl;
-    //addedLemma = checkSimple();
-    //Trace("strings-process") << "Done simple checking, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-    //if( !addedLemma ) {
+    addedLemma = checkExtendedFuncsEval();
+    Trace("strings-process") << "Done check extended functions eval, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+    if( !d_conflict && !addedLemma ){
       addedLemma = checkNormalForms();
       Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
       if(!d_conflict && !addedLemma) {
         addedLemma = checkLengthsEqc();
         Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
         if(!d_conflict && !addedLemma) {
-          addedLemma = checkContains();
-          Trace("strings-process") << "Done check contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+          addedLemma = checkExtendedFuncs();
+          Trace("strings-process") << "Done check extended functions, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
           if( !d_conflict && !addedLemma ) {
-            addedLemma = checkMemberships();
-            Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-            if( !d_conflict && !addedLemma ) {
-              addedLemma = checkCardinality();
-              Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-            }
+            addedLemma = checkCardinality();
+            Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+            //if( !d_conflict && !addedLemma ) {
+            //  addedLemma = checkExtendedFuncsReduction();
+            //  Trace("strings-process") << "Done check extended functions reductions, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+            //}
           }
         }
       }
-    //}
+    }
     Trace("strings-check") << "Theory of strings done full effort check " << addedLemma << " " << d_conflict << std::endl;
   }
   if(!d_conflict && !d_terms_cache.empty()) {
@@ -801,32 +757,36 @@ void TheoryStrings::computeCareGraph(){
   Theory::computeCareGraph();
 }
 
-void TheoryStrings::assertPendingFact(Node fact, Node exp) {
-  Trace("strings-pending") << "Assert pending fact : " << fact << " from " << exp << std::endl;
-  bool polarity = fact.getKind() != kind::NOT;
-  TNode atom = polarity ? fact : fact[0];
+void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
+  Trace("strings-pending") << "Assert pending fact : " << atom << " " << polarity << " from " << exp << std::endl;
   Assert(atom.getKind() != kind::OR, "Infer error: a split.");
-  if (atom.getKind() == kind::EQUAL) {
+  if( atom.getKind()==kind::EQUAL ){
+    //AJR : is this necessary?
     for( unsigned j=0; j<2; j++ ) {
-      if( !d_equalityEngine.hasTerm( atom[j] ) ) {
+      if( !d_equalityEngine.hasTerm( atom[j] ) && atom[j].getType().isString() ) {
         //TODO: check!!!
-    registerTerm( atom[j] );
-        d_equalityEngine.addTerm( atom[j] );
+        registerTerm( atom[j] );
       }
     }
     d_equalityEngine.assertEquality( atom, polarity, exp );
   } else {
-    if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
-      addMembership(fact);
-    } else if (atom.getKind() == kind::STRING_STRCTN) {
-      if(polarity) {
-        d_str_pos_ctn.push_back( atom );
-      } else {
-        d_str_neg_ctn.push_back( atom );
+    if( atom.getKind()==kind::STRING_IN_REGEXP ) {
+#ifdef LAZY_ADD_MEMBERSHIP
+      if( d_ext_func_terms.find( atom )==d_ext_func_terms.end() ){
+        Trace("strings-extf-debug") << "Found extended function (membership) : " << atom << std::endl;
+        d_ext_func_terms[atom] = true;
       }
+#else
+      addMembership( polarity ? atom : atom.negate() );
+#endif
     }
     d_equalityEngine.assertPredicate( atom, polarity, exp );
   }
+  //collect extended function terms in the atom
+  if( options::stringExp() ){
+    std::map< Node, bool > visited;
+    collectExtendedFuncTerms( atom, visited );
+  }
 }
 
 void TheoryStrings::doPendingFacts() {
@@ -836,10 +796,14 @@ void TheoryStrings::doPendingFacts() {
     Node exp = d_pending_exp[ fact ];
     if(fact.getKind() == kind::AND) {
       for(size_t j=0; j<fact.getNumChildren(); j++) {
-        assertPendingFact(fact[j], exp);
+        bool polarity = fact[j].getKind() != kind::NOT;
+        TNode atom = polarity ? fact[j] : fact[j][0];
+        assertPendingFact(atom, polarity, exp);
       }
     } else {
-      assertPendingFact(fact, exp);
+      bool polarity = fact.getKind() != kind::NOT;
+      TNode atom = polarity ? fact : fact[0];
+      assertPendingFact(atom, polarity, exp);
     }
     i++;
   }
@@ -1582,10 +1546,10 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
 
 //nf_exp is conjunction
 bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) {
-  Trace("strings-process") << "Process equivalence class " << eqc << std::endl;
+  Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl;
   if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){
     getConcatVec( eqc, nf );
-    Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
+    Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : already visited." << std::endl;
     return false;
   } else if( areEqual( eqc, d_emptyString ) ) {
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
@@ -1602,7 +1566,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
       ++eqc_i;
     }
     //do nothing
-    Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl;
+    Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : empty." << std::endl;
     d_normal_forms_base[eqc] = d_emptyString;
     d_normal_forms[eqc].clear();
     d_normal_forms_exp[eqc].clear();
@@ -1646,9 +1610,9 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
       d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
       d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() );
       d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() );
-      Trace("strings-process") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
+      Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
     } else {
-      Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl;
+      Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl;
       nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() );
       nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() );
       result = true;
@@ -1880,7 +1844,7 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
 }
 
 bool TheoryStrings::registerTerm( Node n ) {
-  if(d_registed_terms_cache.find(n) == d_registed_terms_cache.end()) {
+  if(d_registered_terms_cache.find(n) == d_registered_terms_cache.end()) {
     Debug("strings-register") << "TheoryStrings::registerTerm() " << n << endl;
     if(n.getType().isString()) {
       if(n.getKind() == kind::STRING_SUBSTR_TOTAL) {
@@ -1910,6 +1874,7 @@ bool TheoryStrings::registerTerm( Node n ) {
         Node sk = mkSkolemS("lsym", 2);
         Node eq = Rewriter::rewrite( sk.eqNode(n) );
         Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
+        d_proxy_var[n] = sk;
         d_out->lemma(eq);
         Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
         Node lsum;
@@ -1932,7 +1897,7 @@ bool TheoryStrings::registerTerm( Node n ) {
           d_equalityEngine.assertEquality( ceq, true, d_true );
         }
       }
-      d_registed_terms_cache.insert(n);
+      d_registered_terms_cache.insert(n);
       return true;
     } else {
       AlwaysAssert(false, "String Terms only in registerTerm.");
@@ -1948,9 +1913,11 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
     Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict" << std::endl;
     d_conflict = true;
   } else {
-    Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
+    Node lem;
     if( ant == d_true ) {
       lem = conc;
+    }else{
+      lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc );
     }
     Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl;
     Trace("strings-assert") << "(assert " << lem << ") ; lemma " << c << std::endl;
@@ -1997,6 +1964,13 @@ void TheoryStrings::sendLengthLemma( Node n ){
   d_out->lemma(n_len_geq_zero);
   d_out->requirePhase( n_len_eq_z, true );
   d_out->requirePhase( n_len_eq_z_2, true );
+
+  //AJR: probably a good idea
+  if( options::stringLenGeqZ() ){
+    Node n_len_geq = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
+    n_len_geq = Rewriter::rewrite( n_len_geq );
+    d_out->lemma( n_len_geq );
+  }
 }
 
 Node TheoryStrings::mkConcat( Node n1, Node n2 ) {
@@ -2037,16 +2011,15 @@ Node TheoryStrings::mkSkolemS( const char *c, int isLenSplit ) {
 }
 
 void TheoryStrings::collectTerm( Node n ) {
-  if(d_registed_terms_cache.find(n) == d_registed_terms_cache.end()) {
+  if(d_registered_terms_cache.find(n) == d_registered_terms_cache.end()) {
     d_terms_cache.push_back(n);
   }
 }
 
 
 void TheoryStrings::appendTermLemma() {
-  for(std::vector< Node >::const_iterator it=d_terms_cache.begin();
-      it!=d_terms_cache.begin();it++) {
-        registerTerm(*it);
+  for(std::vector< Node >::const_iterator it=d_terms_cache.begin(); it!=d_terms_cache.begin();it++) {
+    registerTerm(*it);
   }
 }
 
@@ -2124,64 +2097,6 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
     c.push_back( n );
   }
 }
-/*
-bool TheoryStrings::checkSimple() {
-  bool addedLemma = false;
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  while( !eqcs_i.isFinished() ) {
-    Node eqc = (*eqcs_i);
-    if (eqc.getType().isString()) {
-      //EqcInfo* ei = getOrMakeEqcInfo( eqc, true );
-      //get the constant for the equivalence class
-      //int c_len = ...;
-      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-      while( !eqc_i.isFinished() ) {
-        Node n = (*eqc_i);
-        //length axiom
-        if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) {
-          if( d_length_nodes.find(n)==d_length_nodes.end() ) {
-            Trace("strings-dassert-debug") << "get n: " << n << endl;
-            Node sk;
-            //if( d_length_inst.find(n)==d_length_inst.end() ) {
-              //Node nr = d_equalityEngine.getRepresentative( n );
-              sk = NodeManager::currentNM()->mkSkolem( "lsym", n.getType(), "created for length" );
-              d_statistics.d_new_skolems += 1;
-              d_length_intro_vars.insert( sk );
-              Node eq = sk.eqNode(n);
-              eq = Rewriter::rewrite(eq);
-              Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
-              d_out->lemma(eq);
-            //} else {
-            //  sk = d_length_inst[n];
-            //}
-            Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-            Node lsum;
-            if( n.getKind() == kind::STRING_CONCAT ) {
-              std::vector<Node> node_vec;
-              for( unsigned i=0; i<n.getNumChildren(); i++ ) {
-                Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
-                node_vec.push_back(lni);
-              }
-              lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
-            } else if( n.getKind() == kind::CONST_STRING ) {
-              lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
-            }
-            Node ceq = Rewriter::rewrite( skl.eqNode( lsum ) );
-            Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
-            d_out->lemma(ceq);
-            addedLemma = true;
-
-            d_length_nodes.insert(n);
-          }
-        }
-        ++eqc_i;
-      }
-    }
-    ++eqcs_i;
-  }
-  return addedLemma;
-}
-  */
 
 bool TheoryStrings::checkNormalForms() {
   Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
@@ -2244,7 +2159,7 @@ bool TheoryStrings::checkNormalForms() {
     getEquivalenceClasses( eqcs );
     for( unsigned i=0; i<eqcs.size(); i++ ) {
       Node eqc = eqcs[i];
-      Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl;
+      Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc << std::endl;
       std::vector< Node > visited;
       std::vector< Node > nf;
       std::vector< Node > nf_exp;
@@ -2279,7 +2194,7 @@ bool TheoryStrings::checkNormalForms() {
           eqc_to_exp[eqc] = nf_term_exp;
         }
       }
-      Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl;
+      Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl;
     }
 
     if(Debug.isOn("strings-nf")) {
@@ -3279,21 +3194,222 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma
   return true;
 }
 
-bool TheoryStrings::checkContains() {
-  bool addedLemma = checkPosContains();
+bool TheoryStrings::checkExtendedFuncsEval() {
+  bool addedLemma = false;
+  Trace("strings-extf-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl;
+  for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+    if( (*it).second ){
+      //check if all children are in eqc with a constant, if so, we can rewrite
+      Node n = (*it).first;
+      Trace("strings-extf-debug") << "Check extf " << n << "..." << std::endl;
+      std::vector< Node > children;
+      std::vector< Node > exp;
+      std::map< Node, Node > visited;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = inferConstantDefinition( n[i], exp, visited );
+        if( !nc.isNull() ){
+          Trace("strings-extf-debug") << "  child " << i << " : " << nc << std::endl;
+          children.push_back( nc );
+          Assert( nc.getType()==n[i].getType() );
+        }else{
+          Trace("strings-extf-debug") << "  unresolved due to " << n[i] << std::endl;
+          break;
+        }
+      }
+      if( children.size()==n.getNumChildren() ){
+        if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+          children.insert(children.begin(),n.getOperator());
+        }
+        Trace("strings-extf-debug") << "  resolvable by evaluation..." << std::endl;
+        //mark as reduced
+        d_ext_func_terms[n] = false;
+        Node nr = NodeManager::currentNM()->mkNode( n.getKind(), children );
+        Node nrc = Rewriter::rewrite( nr );
+        Assert( nrc.isConst() );
+        Node nrs = getSymbolicDefinition( nr );
+        Node conc;
+        if( !nrs.isNull() ){
+          Trace("strings-extf-debug") << "  symbolic def : " << nrs << std::endl;
+          exp.clear();
+          if( !areEqual( nrs, nrc ) ){
+            //infer symbolic unit
+            if( n.getType().isBoolean() ){
+              conc = nrc==d_true ? nrs : nrs.negate();
+            }else{
+              conc = nrs.eqNode( nrc );
+            }
+          }
+        }else{
+          if( !areEqual( n, nrc ) ){
+            if( n.getType().isBoolean() ){
+              exp.push_back( n );
+              conc = d_false;
+            }else{
+              conc = n.eqNode( nrc );
+            }
+          }
+        }
+        if( !conc.isNull() ){
+          Trace("strings-extf") << "  resolve extf : " << nr << " -> " << nrc << std::endl;
+          if( n.getType().isInteger() || exp.empty() ){
+            sendLemma( mkExplain( exp ), conc, "EXTF" );
+            addedLemma = true;
+          }else{
+            sendInfer( mkExplain( exp ), conc, "EXTF" );
+          }
+          if( d_conflict ){
+            return true;
+          }
+        }
+      }else{
+        Trace("strings-extf-debug") << "  unresolved ext function : " << n << std::endl;
+      }
+    }
+  }
+  doPendingFacts();
+  if( addedLemma ){
+    doPendingLemmas();
+    return true;
+  }else{
+    return false;
+  }
+}
+
+Node TheoryStrings::inferConstantDefinition( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited ) {
+  if( n.isConst() ){
+    return n;
+  }else{
+    Node nr = getRepresentative( n );
+    std::map< Node, Node >::iterator it = visited.find( nr );
+    if( it==visited.end() ){
+      visited[nr] = Node::null();
+      if( nr.isConst() ){
+        exp.push_back( n.eqNode( nr ) );
+        visited[nr] = nr;
+        return nr;
+      }else{
+        EqcInfo* ei = n.getType().isString() ? getOrMakeEqcInfo( nr, false ) : NULL;
+        if( ei && !ei->d_const_term.get().isNull() ){
+          exp.push_back( n.eqNode( ei->d_const_term.get() ) );
+          visited[nr] = ei->d_const_term.get();
+          return ei->d_const_term.get();
+        }else{
+          //scan the equivalence class
+          if( d_equalityEngine.hasTerm( nr ) ){
+            eq::EqClassIterator eqc_i = eq::EqClassIterator( nr, &d_equalityEngine );
+            while( !eqc_i.isFinished() ) {
+              if( (*eqc_i).isConst() ){
+                visited[nr] = *eqc_i;
+                return *eqc_i;
+              }
+              ++eqc_i;
+            }
+          }
+          if( n.getNumChildren()>0 ){
+            std::vector< Node > children;
+            for( unsigned i=0; i<n.getNumChildren(); i++ ){
+              Node nic = inferConstantDefinition( n[i], exp, visited );
+              if( nic.isNull() ){
+                break;
+              }else{
+                children.push_back( nic );
+              }
+            }
+            if( children.size()==n.getNumChildren() ){
+              if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+                children.insert(children.begin(),n.getOperator());
+              }
+              Node ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+              visited[nr] = ret;
+              return ret;
+            }
+          }
+        }
+      }
+    }else{
+      return it->second;
+    }
+  }
+  return Node::null();
+}
+
+Node TheoryStrings::getSymbolicDefinition( Node n ) {
+  if( n.getNumChildren()==0 ){
+    NodeNodeMap::const_iterator it = d_proxy_var.find( n );
+    if( it==d_proxy_var.end() ){
+      return Node::null();
+    }else{
+      return (*it).second;
+    }
+  }else{
+    std::vector< Node > children;
+    if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      children.push_back( n.getOperator() );
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( n.getKind()==kind::STRING_IN_REGEXP && i==1 ){
+        children.push_back( n[i] );
+      }else{
+        Node ns = getSymbolicDefinition( n[i] );
+        if( ns.isNull() ){
+          return Node::null();
+        }else{
+          children.push_back( ns );
+        }
+      }
+    }
+    return NodeManager::currentNM()->mkNode( n.getKind(), children );
+  }
+}
+
+bool TheoryStrings::checkExtendedFuncs() {
+  std::map< bool, std::vector< Node > > pnContains;
+  std::map< bool, std::vector< Node > > pnMem;
+  for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+    if( (*it).second ){
+      Node n = (*it).first;
+      if( n.getKind()==kind::STRING_STRCTN ) {
+        bool pol = areEqual( n, d_true );
+        Assert( pol || areEqual( n, d_false ) );
+        pnContains[pol].push_back( n );
+      }
+#ifdef LAZY_ADD_MEMBERSHIP
+      else if( n.getKind()==kind::STRING_IN_REGEXP ) {
+        bool pol = areEqual( n, d_true );
+        Assert( pol || areEqual( n, d_false ) );
+        pnMem[pol].push_back( n );
+      }
+#endif
+    }
+  }
+
+  bool addedLemma = checkPosContains( pnContains[true] );
   Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
   if(!d_conflict && !addedLemma) {
-    addedLemma = checkNegContains();
+    addedLemma = checkNegContains( pnContains[false] );
     Trace("strings-process") << "Done check negative contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+    if(!d_conflict && !addedLemma) {
+      Trace("strings-process") << "Adding memberships..." << std::endl;
+      //add all non-evaluated memberships
+#ifdef LAZY_ADD_MEMBERSHIP
+      for( std::map< bool, std::vector< Node > >::iterator it=pnMem.begin(); it != pnMem.end(); ++it ){
+        for( unsigned i=0; i<it->second.size(); i++ ){
+          addMembership( it->first ? it->second[i] : it->second[i].negate() );
+        }
+      }
+#endif
+      addedLemma = checkMemberships();
+      Trace("strings-process") << "Done check memberships, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+    }
   }
   return addedLemma;
 }
 
-bool TheoryStrings::checkPosContains() {
+bool TheoryStrings::checkPosContains( std::vector< Node >& posContains ) {
   bool addedLemma = false;
-  for( unsigned i=0; i<d_str_pos_ctn.size(); i++ ) {
+  for( unsigned i=0; i<posContains.size(); i++ ) {
     if( !d_conflict ){
-      Node atom = d_str_pos_ctn[i];
+      Node atom = posContains[i];
       Trace("strings-ctn") << "We have positive contain assertion : " << atom << std::endl;
       Assert( atom.getKind()==kind::STRING_STRCTN );
       Node x = atom[0];
@@ -3323,12 +3439,12 @@ bool TheoryStrings::checkPosContains() {
   }
 }
 
-bool TheoryStrings::checkNegContains() {
+bool TheoryStrings::checkNegContains( std::vector< Node >& negContains ) {
   bool addedLemma = false;
   //check for conflicts
-  for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ){
+  for( unsigned i=0; i<negContains.size(); i++ ){
     if( !d_conflict ){
-      Node atom = d_str_neg_ctn[i];
+      Node atom = negContains[i];
       Trace("strings-ctn") << "We have negative contain assertion : (not " << atom << " )" << std::endl;
       if( areEqual( atom[1], d_emptyString ) ) {
         Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( d_emptyString ) );
@@ -3346,8 +3462,8 @@ bool TheoryStrings::checkNegContains() {
   if( !d_conflict ){
     //check for lemmas
     if(options::stringExp()) {
-      for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ){
-        Node atom = d_str_neg_ctn[i];
+      for( unsigned i=0; i<negContains.size(); i++ ){
+        Node atom = negContains[i];
         Node x = atom[0];
         Node s = atom[1];
         Node lenx = getLength(x);
@@ -3410,7 +3526,7 @@ bool TheoryStrings::checkNegContains() {
         doPendingLemmas();
       }
     } else {
-      if( !d_str_neg_ctn.empty() ){
+      if( !negContains.empty() ){
         throw LogicException("Strings Incomplete (due to Negative Contain) by default, try --strings-exp option.");
       }
     }
@@ -3418,6 +3534,38 @@ bool TheoryStrings::checkNegContains() {
   return addedLemma;
 }
 
+bool TheoryStrings::checkExtendedFuncsReduction() {
+  bool addedLemmas = false;
+  //very lazy reduction?
+  /*
+  if( options::stringLazyPreproc() ){
+    for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+      if( (*it).second ){
+        Node n = (*it).first;
+        if( n.getKind()!=kind::STRING_IN_REGEXP ){
+          if( d_preproc_cache.find( n )==d_preproc_cache.end() ){
+            d_preproc_cache[n] = true;
+            std::vector< Node > new_nodes;
+            Node res = d_preproc.decompose( n, new_nodes );
+            Assert( res==n );
+            if( !new_nodes.empty() ){
+              Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
+              nnlem = Rewriter::rewrite( nnlem );
+              Trace("strings-pp-lemma") << "Reduction lemma : " << nnlem << std::endl;
+              Trace("strings-pp-lemma") << "...from term " << n << std::endl;
+              d_out->lemma( nnlem );
+              addedLemmas = true;
+            }
+          }
+        }
+      }
+    }
+  }
+  */
+  return addedLemmas;
+}
+
+
 CVC4::String TheoryStrings::getHeadConst( Node x ) {
   if( x.isConst() ) {
     return x.getConst< String >();
@@ -3730,6 +3878,24 @@ Node TheoryStrings::mkSplitEq( const char * c, const char * info, Node lhs, Node
   return eq;
 }
 
+void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()==kind::STRING_SUBSTR_TOTAL || n.getKind()==kind::STRING_STRIDOF ||
+        n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_U16TOS || n.getKind() == kind::STRING_U32TOS ||
+        n.getKind() == kind::STRING_STOI || n.getKind() == kind::STRING_STOU16 || n.getKind() == kind::STRING_STOU32 ||
+        n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){
+      if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){
+        Trace("strings-extf-debug") << "Found extended function : " << n << std::endl;
+        d_ext_func_terms[n] = true;
+      }
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      collectExtendedFuncTerms( n[i], visited );
+    }
+  }
+}
+
 // Stats
 TheoryStrings::Statistics::Statistics():
   d_splits("TheoryStrings::NumOfSplitOnDemands", 0),

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 7eda63f37b83848b8b8eaefcc1bd11f6f2789218..d36e99f465363930640fcb06de90b7ff5df1a493 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -168,14 +168,14 @@ private:
   NodeSet d_loop_antec;
   NodeSet d_length_intro_vars;
   // preReg cache
-  NodeSet d_registed_terms_cache;
+  NodeSet d_registered_terms_cache;
   // term cache
   std::vector< Node > d_terms_cache;
   void collectTerm( Node n );
   void appendTermLemma();
   // preprocess cache
   StringsPreprocess d_preproc;
-  std::map< Node, Node > d_preproc_cache;
+  NodeBoolMap d_preproc_cache;
 
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION
@@ -213,7 +213,7 @@ private:
   std::map< Node, EqcInfo* > d_eqc_info;
   EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
   //maintain which concat terms have the length lemma instantiated
-  NodeNodeMap d_length_inst;
+  NodeNodeMap d_proxy_var;
 private:
   void mergeCstVec(std::vector< Node > &vec_strings);
   bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
@@ -264,9 +264,13 @@ private:
   bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
     std::vector< Node > &processed, std::vector< Node > &cprocessed,
     std::vector< Node > &nf_exp);
-  bool checkContains();
-  bool checkPosContains();
-  bool checkNegContains();
+  bool checkExtendedFuncs();
+  bool checkPosContains( std::vector< Node >& posContains );
+  bool checkNegContains( std::vector< Node >& negContains );
+  bool checkExtendedFuncsEval();
+  Node inferConstantDefinition( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited );
+  Node getSymbolicDefinition( Node n );
+  bool checkExtendedFuncsReduction();
 
 public:
   void preRegisterTerm(TNode n);
@@ -288,7 +292,7 @@ protected:
   void computeCareGraph();
 
   //do pending merges
-  void assertPendingFact(Node fact, Node exp);
+  void assertPendingFact(Node atom, bool polarity, Node exp);
   void doPendingFacts();
   void doPendingLemmas();
 
@@ -327,12 +331,14 @@ private:
   Node mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero );
 
   // Special String Functions
-  NodeList d_str_pos_ctn;
-  NodeList d_str_neg_ctn;
   NodeSet d_neg_ctn_eqlen;
   NodeSet d_neg_ctn_ulen;
   NodeSet d_pos_ctn_cached;
   NodeSet d_neg_ctn_cached;
+  //extended string terms and whether they have been reduced
+  NodeBoolMap d_ext_func_terms;
+  //collect extended operator terms
+  void collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited );
 
   // Symbolic Regular Expression
 private:

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 581e2be0a53c721551ca9e29ff025823d8b953e5..787979faac20a22161daf95deef0387c5f66eeab 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -150,7 +150,7 @@ int StringsPreprocess::checkFixLenVar( Node t ) {
   }
   return ret;
 }
-Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
+Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool during_pp ) {
   std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
   if(i != d_cache.end()) {
     return (*i).second.isNull() ? t : (*i).second;
@@ -158,6 +158,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 
   Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl;
   Node retNode = t;
+  if( options::stringLazyPreproc() ){
+    //only process extended operators after preprocess
+    if( during_pp && ( t.getKind() == kind::STRING_SUBSTR_TOTAL || t.getKind() == kind::STRING_STRIDOF ||
+                       t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS ||
+                       t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ||
+                       t.getKind() == kind::STRING_STRREPL ) ){
+      return t;
+    }
+  }
+
   /*int c_id = checkFixLenVar(t);
   if( c_id != 2 ) {
     int v_id = 1 - c_id;
@@ -181,7 +191,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     }
   } else */
   if( t.getKind() == kind::STRING_IN_REGEXP ) {
-    Node t0 = simplify( t[0], new_nodes );
+    Node t0 = simplify( t[0], new_nodes, during_pp );
 
     //rewrite it
     std::vector< Node > ret;
@@ -206,347 +216,329 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
             NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ),
             t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) ));
     new_nodes.push_back( lemma );
-    retNode = t;
     d_cache[t] = t;
   } else if( t.getKind() == kind::STRING_STRIDOF ) {
-    if(options::stringExp()) {
-      Node sk1 = NodeManager::currentNM()->mkSkolem( "io1", NodeManager::currentNM()->stringType(), "created for indexof" );
-      Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" );
-      Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" );
-      Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" );
-      Node skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" );
-      Node eq = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3, sk4 ) );
-      new_nodes.push_back( eq );
-      Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
-      Node krange = NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone );
-      new_nodes.push_back( krange );
-      krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT,
-            NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk) );
-      new_nodes.push_back( krange );
-      krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT,
-            NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] ), d_zero) );
-      new_nodes.push_back( krange );
-      krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GEQ,
-            t[2], d_zero) );
-      new_nodes.push_back( krange );
+    Node sk1 = NodeManager::currentNM()->mkSkolem( "io1", NodeManager::currentNM()->stringType(), "created for indexof" );
+    Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" );
+    Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" );
+    Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" );
+    Node skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" );
+    Node eq = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3, sk4 ) );
+    new_nodes.push_back( eq );
+    Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
+    Node krange = NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone );
+    new_nodes.push_back( krange );
+    krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT,
+          NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk) );
+    new_nodes.push_back( krange );
+    krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT,
+          NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] ), d_zero) );
+    new_nodes.push_back( krange );
+    krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GEQ,
+          t[2], d_zero) );
+    new_nodes.push_back( krange );
 
-      //str.len(s1) < y + str.len(s2)
-      Node c1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::GT,
-              NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] )),
-              NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] )));
-      //str.len(t1) = y
-      Node c2 = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-      //~contain(t234, s2)
-      Node c3 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
-            NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4), t[1] ).negate());
-      //left
-      Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, NodeManager::currentNM()->mkNode( kind::AND, c2, c3 ) );
-      //t3 = s2
-      Node c4 = t[1].eqNode( sk3 );
-      //~contain(t2, s2)
-      Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
-                  NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2,
-                    NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[1], d_zero,
-                      NodeManager::currentNM()->mkNode(kind::MINUS,
-                        NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[1]),
-                        NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))),
-                  t[1] ).negate();
-      //k=str.len(s1, s2)
-      Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH,
-                  NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2 )));
-      //right
-      Node right = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::AND, c2, c4, c5, c6 ));
-      Node cond = skk.eqNode( negone );
-      Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right );
-      new_nodes.push_back( rr );
-      if( options::stringLazyPreproc() ){
-        new_nodes.push_back( t.eqNode( skk ) );
-        d_cache[t] = Node::null();
-      }else{
-        d_cache[t] = skk;
-        retNode = skk;
-      }
-    } else {
-      throw LogicException("string indexof not supported in default mode, try --strings-exp");
+    //str.len(s1) < y + str.len(s2)
+    Node c1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::GT,
+            NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] )),
+            NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] )));
+    //str.len(t1) = y
+    Node c2 = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+    //~contain(t234, s2)
+    Node c3 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
+          NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4), t[1] ).negate());
+    //left
+    Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, NodeManager::currentNM()->mkNode( kind::AND, c2, c3 ) );
+    //t3 = s2
+    Node c4 = t[1].eqNode( sk3 );
+    //~contain(t2, s2)
+    Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
+                NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2,
+                  NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[1], d_zero,
+                    NodeManager::currentNM()->mkNode(kind::MINUS,
+                      NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[1]),
+                      NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))),
+                t[1] ).negate();
+    //k=str.len(s1, s2)
+    Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH,
+                NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2 )));
+    //right
+    Node right = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::AND, c2, c4, c5, c6 ));
+    Node cond = skk.eqNode( negone );
+    Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right );
+    new_nodes.push_back( rr );
+    if( options::stringLazyPreproc() ){
+      new_nodes.push_back( t.eqNode( skk ) );
+      d_cache[t] = Node::null();
+    }else{
+      d_cache[t] = skk;
+      retNode = skk;
     }
   } else if( t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS ) {
-    if(options::stringExp()) {
-      //Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE,
-      //        NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
-      //        t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0])));
-      Node num = t[0];
-      Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
-      Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
+    //Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE,
+    //        NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
+    //        t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0])));
+    Node num = t[0];
+    Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
+    Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
 
-      Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero);
-      if(t.getKind()==kind::STRING_U16TOS) {
-        nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT16_MAX) ), t[0]));
-        Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(5) ), lenp);
-        new_nodes.push_back(lencond);
-      } else if(t.getKind()==kind::STRING_U32TOS) {
-        nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT32_MAX) ), t[0]));
-        Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ), lenp);
-        new_nodes.push_back(lencond);
-      }
+    Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero);
+    if(t.getKind()==kind::STRING_U16TOS) {
+      nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT16_MAX) ), t[0]));
+      Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(5) ), lenp);
+      new_nodes.push_back(lencond);
+    } else if(t.getKind()==kind::STRING_U32TOS) {
+      nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT32_MAX) ), t[0]));
+      Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ), lenp);
+      new_nodes.push_back(lencond);
+    }
 
-      Node lem = NodeManager::currentNM()->mkNode(kind::IFF, nonneg.negate(),
-        pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
-        );
-      new_nodes.push_back(lem);
+    Node lem = NodeManager::currentNM()->mkNode(kind::IFF, nonneg.negate(),
+      pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
+      );
+    new_nodes.push_back(lem);
 
-      //non-neg
-      Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-      Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
-      Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
-            NodeManager::currentNM()->mkNode( kind::GT, lenp, b1 ) ) );
-      Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
-      Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
-      Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
+    //non-neg
+    Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+    Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
+    Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
+          NodeManager::currentNM()->mkNode( kind::GT, lenp, b1 ) ) );
+    Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+    Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
+    Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
 
-      std::vector< TypeNode > argTypes;
-      argTypes.push_back(NodeManager::currentNM()->integerType());
-      Node ufP = NodeManager::currentNM()->mkSkolem("ufP",
-                NodeManager::currentNM()->mkFunctionType(
-                  argTypes, NodeManager::currentNM()->integerType()),
-                "uf type conv P");
-      Node ufM = NodeManager::currentNM()->mkSkolem("ufM",
-                NodeManager::currentNM()->mkFunctionType(
-                  argTypes, NodeManager::currentNM()->integerType()),
-                "uf type conv M");
+    std::vector< TypeNode > argTypes;
+    argTypes.push_back(NodeManager::currentNM()->integerType());
+    Node ufP = NodeManager::currentNM()->mkSkolem("ufP",
+              NodeManager::currentNM()->mkFunctionType(
+                argTypes, NodeManager::currentNM()->integerType()),
+              "uf type conv P");
+    Node ufM = NodeManager::currentNM()->mkSkolem("ufM",
+              NodeManager::currentNM()->mkFunctionType(
+                argTypes, NodeManager::currentNM()->integerType()),
+              "uf type conv M");
 
-      lem = num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero));
-      new_nodes.push_back( lem );
+    lem = num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero));
+    new_nodes.push_back( lem );
 
-      Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b1);
-      Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one));
-      Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b1);
-      Node b1gtz = NodeManager::currentNM()->mkNode(kind::GT, b1, d_zero);
-      Node cc1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS,
-              NodeManager::currentNM()->mkNode(kind::MULT, ufx, ten),
-              NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)) ));
-      cc1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b1gtz, cc1);
-      Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one));
-      Node cc2 = ufx.eqNode(ufMx);
-      cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2);
-      // leading zero
-      Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(b1).negate());
-      Node cc21 = NodeManager::currentNM()->mkNode(kind::IMPLIES, cl, NodeManager::currentNM()->mkNode(kind::GT, ufMx, d_zero));
-      //cc3
-      Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
-      Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
+    Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b1);
+    Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one));
+    Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b1);
+    Node b1gtz = NodeManager::currentNM()->mkNode(kind::GT, b1, d_zero);
+    Node cc1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS,
+            NodeManager::currentNM()->mkNode(kind::MULT, ufx, ten),
+            NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)) ));
+    cc1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b1gtz, cc1);
+    Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one));
+    Node cc2 = ufx.eqNode(ufMx);
+    cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2);
+    // leading zero
+    Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(b1).negate());
+    Node cc21 = NodeManager::currentNM()->mkNode(kind::IMPLIES, cl, NodeManager::currentNM()->mkNode(kind::GT, ufMx, d_zero));
+    //cc3
+    Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
+    Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
 
-      Node b21 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
-      Node b22 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
-      Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b21, b22);
+    Node b21 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+    Node b22 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+    Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b21, b22);
 
-      Node c21 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, b21).eqNode(
-            NodeManager::currentNM()->mkNode(kind::MINUS, lenp, NodeManager::currentNM()->mkNode(kind::PLUS, b1, one) ));
-      Node ch =
-        NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
-        NodeManager::currentNM()->mkConst(::CVC4::String("0")),
-        NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
-        NodeManager::currentNM()->mkConst(::CVC4::String("1")),
-        NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))),
-        NodeManager::currentNM()->mkConst(::CVC4::String("2")),
-        NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))),
-        NodeManager::currentNM()->mkConst(::CVC4::String("3")),
-        NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))),
-        NodeManager::currentNM()->mkConst(::CVC4::String("4")),
-        NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))),
-        NodeManager::currentNM()->mkConst(::CVC4::String("5")),
-        NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))),
-        NodeManager::currentNM()->mkConst(::CVC4::String("6")),
-        NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))),
-        NodeManager::currentNM()->mkConst(::CVC4::String("7")),
-        NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))),
-        NodeManager::currentNM()->mkConst(::CVC4::String("8")),
-        NodeManager::currentNM()->mkConst(::CVC4::String("9")))))))))));
-      Node c22 = pret.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, b21, ch, b22) );
-      Node cc5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, NodeManager::currentNM()->mkNode(kind::AND, c21, c22));
-      std::vector< Node > svec;
-      svec.push_back(cc1);svec.push_back(cc2);
-      svec.push_back(cc21);
-      svec.push_back(cc3);svec.push_back(cc4);svec.push_back(cc5);
-      Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, svec) );
-      conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
-      conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
-      conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, nonneg, conc );
-      new_nodes.push_back( conc );
+    Node c21 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, b21).eqNode(
+          NodeManager::currentNM()->mkNode(kind::MINUS, lenp, NodeManager::currentNM()->mkNode(kind::PLUS, b1, one) ));
+    Node ch =
+      NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
+      NodeManager::currentNM()->mkConst(::CVC4::String("0")),
+      NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
+      NodeManager::currentNM()->mkConst(::CVC4::String("1")),
+      NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))),
+      NodeManager::currentNM()->mkConst(::CVC4::String("2")),
+      NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))),
+      NodeManager::currentNM()->mkConst(::CVC4::String("3")),
+      NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))),
+      NodeManager::currentNM()->mkConst(::CVC4::String("4")),
+      NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))),
+      NodeManager::currentNM()->mkConst(::CVC4::String("5")),
+      NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))),
+      NodeManager::currentNM()->mkConst(::CVC4::String("6")),
+      NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))),
+      NodeManager::currentNM()->mkConst(::CVC4::String("7")),
+      NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))),
+      NodeManager::currentNM()->mkConst(::CVC4::String("8")),
+      NodeManager::currentNM()->mkConst(::CVC4::String("9")))))))))));
+    Node c22 = pret.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, b21, ch, b22) );
+    Node cc5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, NodeManager::currentNM()->mkNode(kind::AND, c21, c22));
+    std::vector< Node > svec;
+    svec.push_back(cc1);svec.push_back(cc2);
+    svec.push_back(cc21);
+    svec.push_back(cc3);svec.push_back(cc4);svec.push_back(cc5);
+    Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, svec) );
+    conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
+    conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
+    conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, nonneg, conc );
+    new_nodes.push_back( conc );
 
-      /*conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::IMPLIES,
-              NodeManager::currentNM()->mkNode(kind::LT, t[0], d_zero),
-              t.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,
-                NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret))));
-      new_nodes.push_back( conc );*/
-      if( options::stringLazyPreproc() && t!=pret ){
-        new_nodes.push_back( t.eqNode( pret ) );
-        d_cache[t] = Node::null();
-      }else{
-        d_cache[t] = pret;
-        retNode = pret;
-      }
-      //don't rewrite processed
-      if(t != pret) {
-        d_cache[pret] = pret;
-      }
-    } else {
-      throw LogicException("string int.to.str not supported in default mode, try --strings-exp");
+    /*conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::IMPLIES,
+            NodeManager::currentNM()->mkNode(kind::LT, t[0], d_zero),
+            t.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,
+              NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret))));
+    new_nodes.push_back( conc );*/
+    if( options::stringLazyPreproc() && t!=pret ){
+      new_nodes.push_back( t.eqNode( pret ) );
+      d_cache[t] = Node::null();
+    }else{
+      d_cache[t] = pret;
+      retNode = pret;
+    }
+    //don't rewrite processed
+    if(t != pret) {
+      d_cache[pret] = pret;
     }
   } else if( t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ) {
-    if(options::stringExp()) {
-      Node str = t[0];
-      Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str);
-      Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, str);
+    Node str = t[0];
+    Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str);
+    Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, str);
 
-      Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
-      Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
-      Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
-      Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
-      std::vector< TypeNode > argTypes;
-      argTypes.push_back(NodeManager::currentNM()->integerType());
-      Node ufP = NodeManager::currentNM()->mkSkolem("ufP",
-                NodeManager::currentNM()->mkFunctionType(
-                  argTypes, NodeManager::currentNM()->integerType()),
-                "uf type conv P");
-      Node ufM = NodeManager::currentNM()->mkSkolem("ufM",
-                NodeManager::currentNM()->mkFunctionType(
-                  argTypes, NodeManager::currentNM()->integerType()),
-                "uf type conv M");
+    Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
+    Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+    Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
+    Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
+    std::vector< TypeNode > argTypes;
+    argTypes.push_back(NodeManager::currentNM()->integerType());
+    Node ufP = NodeManager::currentNM()->mkSkolem("ufP",
+              NodeManager::currentNM()->mkFunctionType(
+                argTypes, NodeManager::currentNM()->integerType()),
+              "uf type conv P");
+    Node ufM = NodeManager::currentNM()->mkSkolem("ufM",
+              NodeManager::currentNM()->mkFunctionType(
+                argTypes, NodeManager::currentNM()->integerType()),
+              "uf type conv M");
 
-      //Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
-      //new_nodes.push_back(pret.eqNode(ufP0));
-      //lemma
-      Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
-        str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
-        pret.eqNode(negone));
+    //Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
+    //new_nodes.push_back(pret.eqNode(ufP0));
+    //lemma
+    Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
+      str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
+      pret.eqNode(negone));
+    new_nodes.push_back(lem);
+    /*lem = NodeManager::currentNM()->mkNode(kind::IFF,
+      t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
+      t.eqNode(d_zero));
+    new_nodes.push_back(lem);*/
+    if(t.getKind()==kind::STRING_U16TOS) {
+      lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("5")), lenp);
       new_nodes.push_back(lem);
-      /*lem = NodeManager::currentNM()->mkNode(kind::IFF,
-        t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
-        t.eqNode(d_zero));
-      new_nodes.push_back(lem);*/
-      if(t.getKind()==kind::STRING_U16TOS) {
-        lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("5")), lenp);
-        new_nodes.push_back(lem);
-      } else if(t.getKind()==kind::STRING_U32TOS) {
-        lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("9")), lenp);
-        new_nodes.push_back(lem);
-      }
-      //cc1
-      Node cc1 = str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
-      //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
-      //cc2
-      std::vector< Node > vec_n;
-      Node p = NodeManager::currentNM()->mkSkolem("p", NodeManager::currentNM()->integerType());
-      Node g = NodeManager::currentNM()->mkNode(kind::GEQ, p, d_zero);
-      vec_n.push_back(g);
-      g = NodeManager::currentNM()->mkNode(kind::GT, lenp, p);
+    } else if(t.getKind()==kind::STRING_U32TOS) {
+      lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("9")), lenp);
+      new_nodes.push_back(lem);
+    }
+    //cc1
+    Node cc1 = str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
+    //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
+    //cc2
+    std::vector< Node > vec_n;
+    Node p = NodeManager::currentNM()->mkSkolem("p", NodeManager::currentNM()->integerType());
+    Node g = NodeManager::currentNM()->mkNode(kind::GEQ, p, d_zero);
+    vec_n.push_back(g);
+    g = NodeManager::currentNM()->mkNode(kind::GT, lenp, p);
+    vec_n.push_back(g);
+    Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, p, one);
+    char chtmp[2];
+    chtmp[1] = '\0';
+    for(unsigned i=0; i<=9; i++) {
+      chtmp[0] = i + '0';
+      std::string stmp(chtmp);
+      g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate();
       vec_n.push_back(g);
-      Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, p, one);
-      char chtmp[2];
-      chtmp[1] = '\0';
-      for(unsigned i=0; i<=9; i++) {
-        chtmp[0] = i + '0';
-        std::string stmp(chtmp);
-        g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate();
-        vec_n.push_back(g);
-      }
-      Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n));
-      //cc3
-      Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-      Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);
-      Node g2 = NodeManager::currentNM()->mkNode(kind::AND,
-            NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero),
-            NodeManager::currentNM()->mkNode(kind::GT, lenp, b2));
-      Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2);
-      Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one));
-      Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2);
-      std::vector< Node > vec_c3;
-      std::vector< Node > vec_c3b;
-      //qx between 0 and 9
-      Node c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
-      vec_c3b.push_back(c3cc);
-      c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
-      vec_c3b.push_back(c3cc);
-      Node sx = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, b2, one);
-      for(unsigned i=0; i<=9; i++) {
-        chtmp[0] = i + '0';
-        std::string stmp(chtmp);
-        c3cc = NodeManager::currentNM()->mkNode(kind::IFF,
-          ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i))),
-          sx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp))));
-        vec_c3b.push_back(c3cc);
-      }
-      //c312
-      Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero);
-      c3cc = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz,
-        ufx.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS,
-          NodeManager::currentNM()->mkNode(kind::MULT, ufx1, ten),
-          ufMx)));
+    }
+    Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n));
+    //cc3
+    Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+    Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);
+    Node g2 = NodeManager::currentNM()->mkNode(kind::AND,
+          NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero),
+          NodeManager::currentNM()->mkNode(kind::GT, lenp, b2));
+    Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2);
+    Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one));
+    Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2);
+    std::vector< Node > vec_c3;
+    std::vector< Node > vec_c3b;
+    //qx between 0 and 9
+    Node c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
+    vec_c3b.push_back(c3cc);
+    c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
+    vec_c3b.push_back(c3cc);
+    Node sx = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, b2, one);
+    for(unsigned i=0; i<=9; i++) {
+      chtmp[0] = i + '0';
+      std::string stmp(chtmp);
+      c3cc = NodeManager::currentNM()->mkNode(kind::IFF,
+        ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i))),
+        sx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp))));
       vec_c3b.push_back(c3cc);
-      c3cc = NodeManager::currentNM()->mkNode(kind::AND, vec_c3b);
-      c3cc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, c3cc) );
-      c3cc = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, c3cc);
-      vec_c3.push_back(c3cc);
-      //unbound
-      c3cc = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero).eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, d_zero));
-      vec_c3.push_back(c3cc);
-      Node lstx = NodeManager::currentNM()->mkNode(kind::MINUS, lenp, one);
-      Node upflstx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, lstx);
-      c3cc = upflstx.eqNode(pret);
-      vec_c3.push_back(c3cc);
-      Node cc3 = NodeManager::currentNM()->mkNode(kind::AND, vec_c3);
-      Node conc = NodeManager::currentNM()->mkNode(kind::ITE, pret.eqNode(negone),
-              NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3);
-      new_nodes.push_back( conc );
-      if( options::stringLazyPreproc() && t!=pret ){
-        new_nodes.push_back( t.eqNode( pret ) );
-        d_cache[t] = Node::null();
-      }else{
-        d_cache[t] = pret;
-        retNode = pret;
-      }
-      if(t != pret) {
-        d_cache[pret] = pret;
-      }
-    } else {
-      throw LogicException("string int.to.str not supported in default mode, try --strings-exp");
+    }
+    //c312
+    Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero);
+    c3cc = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz,
+      ufx.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS,
+        NodeManager::currentNM()->mkNode(kind::MULT, ufx1, ten),
+        ufMx)));
+    vec_c3b.push_back(c3cc);
+    c3cc = NodeManager::currentNM()->mkNode(kind::AND, vec_c3b);
+    c3cc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, c3cc) );
+    c3cc = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, c3cc);
+    vec_c3.push_back(c3cc);
+    //unbound
+    c3cc = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero).eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, d_zero));
+    vec_c3.push_back(c3cc);
+    Node lstx = NodeManager::currentNM()->mkNode(kind::MINUS, lenp, one);
+    Node upflstx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, lstx);
+    c3cc = upflstx.eqNode(pret);
+    vec_c3.push_back(c3cc);
+    Node cc3 = NodeManager::currentNM()->mkNode(kind::AND, vec_c3);
+    Node conc = NodeManager::currentNM()->mkNode(kind::ITE, pret.eqNode(negone),
+            NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3);
+    new_nodes.push_back( conc );
+    if( options::stringLazyPreproc() && t!=pret ){
+      new_nodes.push_back( t.eqNode( pret ) );
+      d_cache[t] = Node::null();
+    }else{
+      d_cache[t] = pret;
+      retNode = pret;
+    }
+    if(t != pret) {
+      d_cache[pret] = pret;
     }
   } else if( t.getKind() == kind::STRING_STRREPL ) {
-    if(options::stringExp()) {
-      Node x = t[0];
-      Node y = t[1];
-      Node z = t[2];
-      Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1", t[0].getType(), "created for replace" );
-      Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" );
-      Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" );
-      Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y );
-      Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) );
-      Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) );
-      Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
-                  NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1,
-                     NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, y, d_zero,
-                        NodeManager::currentNM()->mkNode(kind::MINUS,
-                          NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y),
-                          NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate();
-      Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
-              NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3),
-              skw.eqNode(x) ) );
-      new_nodes.push_back( rr );
-      rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) );
-      new_nodes.push_back( rr );
-      if( options::stringLazyPreproc() ){
-        new_nodes.push_back( t.eqNode( skw ) );
-        d_cache[t] = Node::null();
-      }else{
-        d_cache[t] = skw;
-        retNode = skw;
-      }
-    } else {
-      throw LogicException("string replace not supported in default mode, try --strings-exp");
+    Node x = t[0];
+    Node y = t[1];
+    Node z = t[2];
+    Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1", t[0].getType(), "created for replace" );
+    Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" );
+    Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" );
+    Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y );
+    Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) );
+    Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) );
+    Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
+                NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1,
+                   NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, y, d_zero,
+                      NodeManager::currentNM()->mkNode(kind::MINUS,
+                        NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y),
+                        NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate();
+    Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
+            NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3),
+            skw.eqNode(x) ) );
+    new_nodes.push_back( rr );
+    rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) );
+    new_nodes.push_back( rr );
+    if( options::stringLazyPreproc() ){
+      new_nodes.push_back( t.eqNode( skw ) );
+      d_cache[t] = Node::null();
+    }else{
+      d_cache[t] = skw;
+      retNode = skw;
     }
   } else{
     d_cache[t] = Node::null();
-    retNode = t;
   }
 
   /*if( t.getNumChildren()>0 ) {
@@ -581,7 +573,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
   return retNode;
 }
 
-Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
+Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool during_pp) {
   std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
   if(i != d_cache.end()) {
     return (*i).second.isNull() ? t : (*i).second;
@@ -589,7 +581,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
 
   unsigned num = t.getNumChildren();
   if(num == 0) {
-    return simplify(t, new_nodes);
+    return simplify(t, new_nodes, during_pp);
   } else {
     bool changed = false;
     std::vector< Node > cc;
@@ -597,7 +589,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
       cc.push_back(t.getOperator());
     }
     for(unsigned i=0; i<t.getNumChildren(); i++) {
-      Node s = decompose(t[i], new_nodes);
+      Node s = decompose(t[i], new_nodes, during_pp);
       cc.push_back( s );
       if(s != t[i]) {
         changed = true;
@@ -605,9 +597,9 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
     }
     if(changed) {
       Node tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc );
-      return simplify(tmp, new_nodes);
+      return simplify(tmp, new_nodes, during_pp);
     } else {
-      return simplify(t, new_nodes);
+      return simplify(t, new_nodes, during_pp);
     }
   }
 }
@@ -615,7 +607,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
 void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
   for( unsigned i=0; i<vec_node.size(); i++ ){
     std::vector< Node > new_nodes;
-    Node curr = decompose( vec_node[i], new_nodes );
+    Node curr = decompose( vec_node[i], new_nodes, true );
     if( !new_nodes.empty() ){
       new_nodes.insert( new_nodes.begin(), curr );
       curr = NodeManager::currentNM()->mkNode( kind::AND, new_nodes );

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index d96644bee21de5fc045a3f9b7ada338b11fea314..1255d93e0f1aaa005a57c526e101811f4b393263 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -37,11 +37,12 @@ private:
   bool checkStarPlus( Node t );
   int checkFixLenVar( Node t );
   void processRegExp( Node s, Node r, std::vector< Node > &ret );
-  Node simplify( Node t, std::vector< Node > &new_nodes );
+  Node simplify( Node t, std::vector< Node > &new_nodes, bool during_pp );
 public:
-  Node decompose( Node t, std::vector< Node > &new_nodes );
-  void simplify(std::vector< Node > &vec_node);
   StringsPreprocess();
+
+  Node decompose( Node t, std::vector< Node > &new_nodes, bool during_pp = false );
+  void simplify(std::vector< Node > &vec_node);
 };
 
 }/* CVC4::theory::strings namespace */

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index b796fc80bd8b2b15eb0eeb23b8f82273fde697e5..79efee6e05117a3e36265fe332ed647ae426da80 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -52,13 +52,14 @@ TESTS = \
   reloop.smt2 \
   unsound-0908.smt2 \
   ilc-like.smt2 \ 
+  ilc-l-nt.smt2 \ 
+  artemis-0512-nonterm.smt2 \
   indexof-sym-simp.smt2 \
   bug613.smt2
 
 FAILING_TESTS =
 
 EXTRA_DIST = $(TESTS) \
-  artemis-0512-nonterm.smt2 \
   fmf001.smt2 \
   type002.smt2
 

diff --git a/test/regress/regress0/strings/ilc-l-nt.smt2 b/test/regress/regress0/strings/ilc-l-nt.smt2
new file mode 100755 (executable)
index 0000000..32dfc0b
--- /dev/null
+++ b/test/regress/regress0/strings/ilc-l-nt.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL_SUPPORTED)\r
+(set-info :status unsat)\r
+(set-option :strings-exp true)\r
+ \r
+(declare-fun s () String)\r
+(assert (or (= s "Id like cookies.") (= s "Id not like cookies.")))\r
+ \r
+(declare-fun target () String)\r
+(assert (or (= target "l") (= target "m")))\r
+ \r
+(declare-fun location () Int)\r
+(assert (= (* 2 location) (str.indexof s target 0)))\r
+ \r
+(check-sat)
\ No newline at end of file