Improve regexp rewriter, simplify regexp preprocess, add basic trans closure for string contains, refactoring.

6 files changed, 226 insertions, 261 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f203c7d1e..a4f18e57b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3297,10 +3297,9 @@ void SmtEnginePrivate::processAssertions() {
   if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl;
     dumpAssertions("pre-strings-pp", d_assertions);
-    ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() );
-    //for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-    //  d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
-    //}
+    if( !options::stringLazyPreproc() ){
+      ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() );
+    }
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
     dumpAssertions("post-strings-pp", d_assertions);
   }
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 02a1db47a..618296a95 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -119,7 +119,6 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
   d_false = NodeManager::currentNM()->mkConst( false );
 
   d_card_size = 128;
-  //d_opt_regexp_gcd = true;
 }
 
 TheoryStrings::~TheoryStrings() {
@@ -222,8 +221,7 @@ EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
   return EQUALITY_UNKNOWN;
 }
 
-void TheoryStrings::propagate(Effort e)
-{
+void TheoryStrings::propagate(Effort e) {
   // direct propagation now
 }
 
@@ -243,7 +241,7 @@ bool TheoryStrings::propagate(TNode literal) {
 }
 
 /** explain */
-void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){
+void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions) {
   Debug("strings-explain") << "Explain " << literal << " " << d_conflict << std::endl;
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
@@ -286,7 +284,6 @@ Node TheoryStrings::explain( TNode literal ){
 
 void TheoryStrings::presolve() {
   Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl;
-  d_opt_fmf = options::stringFMF();
 
   if(!options::stdASCII()) {
     d_card_size = 256;
@@ -345,9 +342,6 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
   }
   ////step 2 : assign arbitrary values for unknown lengths?
   // confirmed by calculus invariant, see paper
-  //for( unsigned i=0; i<col.size(); i++ ){
-  //  if(
-  //}
   Trace("strings-model") << "Assign to equivalence classes..." << std::endl;
   //step 3 : assign values to equivalence classes that are pure variables
   for( unsigned i=0; i<col.size(); i++ ){
@@ -623,6 +617,8 @@ bool TheoryStrings::doPreprocess( Node atom ) {
     d_preproc_cache[ atom ] = true;
     std::vector< Node > new_nodes;
     Node res = d_preproc.decompose( atom, new_nodes );
+    Assert( res==atom );
+    /*
     if( atom!=res ){
       //check if reduction/deduction
       std::vector< Node > subs_lhs;
@@ -650,6 +646,7 @@ bool TheoryStrings::doPreprocess( Node atom ) {
     }else{
       Trace("strings-assertion-debug") << "...preprocess ok." << std::endl;
     }
+    */
     if( !new_nodes.empty() ){
       Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
       nnlem = Rewriter::rewrite( nnlem );
@@ -666,23 +663,6 @@ bool TheoryStrings::doPreprocess( Node atom ) {
   return addFact;
 }
 
-bool TheoryStrings::hasProcessed() {
-  return d_conflict || !d_lemma_cache.empty() || !d_pending.empty();
-}
-
-void TheoryStrings::addToExplanation( Node a, Node b, std::vector< Node >& exp ) {
-  if( a!=b ){
-    Debug("strings-explain") << "Add to explanation : " << a << " == " << b << std::endl;
-    Assert( areEqual( a, b ) );
-    exp.push_back( a.eqNode( b ) );
-  }
-}
-void TheoryStrings::addToExplanation( Node lit, std::vector< Node >& exp ) {
-  if( !lit.isNull() ){
-    exp.push_back( lit );
-  }
-}
-
 TheoryStrings::EqcInfo::EqcInfo(  context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) {
 
 }
@@ -867,6 +847,24 @@ void TheoryStrings::doPendingLemmas() {
   d_pending_req_phase.clear();
 }
 
+bool TheoryStrings::hasProcessed() {
+  return d_conflict || !d_lemma_cache.empty() || !d_pending.empty();
+}
+
+void TheoryStrings::addToExplanation( Node a, Node b, std::vector< Node >& exp ) {
+  if( a!=b ){
+    Debug("strings-explain") << "Add to explanation : " << a << " == " << b << std::endl;
+    Assert( areEqual( a, b ) );
+    exp.push_back( a.eqNode( b ) );
+  }
+}
+
+void TheoryStrings::addToExplanation( Node lit, std::vector< Node >& exp ) {
+  if( !lit.isNull() ){
+    exp.push_back( lit );
+  }
+}
+
 bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
   std::vector< std::vector< Node > > &normal_forms,  std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) {
   Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
@@ -2448,64 +2446,6 @@ void TheoryStrings::checkFlatForms() {
   }
 }
 
-void TheoryStrings::checkNormalForms() {
-  Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
-  //calculate normal forms for each equivalence class, possibly adding splitting lemmas
-  d_normal_forms.clear();
-  d_normal_forms_exp.clear();
-  std::map< Node, Node > nf_to_eqc;
-  std::map< Node, Node > eqc_to_exp;
-  for( unsigned i=0; i<d_strings_eqc.size(); i++ ) {
-    Node eqc = d_strings_eqc[i];
-    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;
-    normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
-    Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
-    if( d_conflict ) {
-      return;
-    } else if ( d_pending.empty() && d_lemma_cache.empty() ) {
-      Node nf_term = mkConcat( nf );
-      if( nf_to_eqc.find( nf_term )!=nf_to_eqc.end() ) {
-        //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
-        //two equivalence classes have same normal form, merge
-        nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] );
-        Node eq = eqc.eqNode( nf_to_eqc[nf_term] );
-        sendInfer( mkAnd( nf_exp ), eq, "Normal_Form" );
-      } else {
-        nf_to_eqc[nf_term] = eqc;
-        eqc_to_exp[eqc] = mkAnd( nf_exp );
-      }
-    }
-    Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl;
-  }
-
-  if(Trace.isOn("strings-nf")) {
-    Trace("strings-nf") << "**** Normal forms are : " << std::endl;
-    for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
-      Trace("strings-nf") << "  N[" << it->second << "] = " << it->first << std::endl;
-    }
-    Trace("strings-nf") << std::endl;
-  }
-  if( !hasProcessed() ){
-    checkExtendedFuncsEval( 1 );
-    Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
-    if( !hasProcessed() ){
-      if( !options::stringEagerLen() ){
-        checkLengthsEqc();
-        if( hasProcessed() ){
-          return;
-        }
-      }
-      //process disequalities between equivalence classes
-      checkDeqNF();
-      Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
-    }
-  }
-  Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
-}
-
 Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ){
   if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
     // a loop
@@ -2581,6 +2521,64 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
 }
 
 
+void TheoryStrings::checkNormalForms() {
+  Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
+  //calculate normal forms for each equivalence class, possibly adding splitting lemmas
+  d_normal_forms.clear();
+  d_normal_forms_exp.clear();
+  std::map< Node, Node > nf_to_eqc;
+  std::map< Node, Node > eqc_to_exp;
+  for( unsigned i=0; i<d_strings_eqc.size(); i++ ) {
+    Node eqc = d_strings_eqc[i];
+    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;
+    normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
+    Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
+    if( d_conflict ) {
+      return;
+    } else if ( d_pending.empty() && d_lemma_cache.empty() ) {
+      Node nf_term = mkConcat( nf );
+      if( nf_to_eqc.find( nf_term )!=nf_to_eqc.end() ) {
+        //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
+        //two equivalence classes have same normal form, merge
+        nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] );
+        Node eq = eqc.eqNode( nf_to_eqc[nf_term] );
+        sendInfer( mkAnd( nf_exp ), eq, "Normal_Form" );
+      } else {
+        nf_to_eqc[nf_term] = eqc;
+        eqc_to_exp[eqc] = mkAnd( nf_exp );
+      }
+    }
+    Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl;
+  }
+
+  if(Trace.isOn("strings-nf")) {
+    Trace("strings-nf") << "**** Normal forms are : " << std::endl;
+    for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
+      Trace("strings-nf") << "  N[" << it->second << "] = " << it->first << std::endl;
+    }
+    Trace("strings-nf") << std::endl;
+  }
+  if( !hasProcessed() ){
+    checkExtendedFuncsEval( 1 );
+    Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
+    if( !hasProcessed() ){
+      if( !options::stringEagerLen() ){
+        checkLengthsEqc();
+        if( hasProcessed() ){
+          return;
+        }
+      }
+      //process disequalities between equivalence classes
+      checkDeqNF();
+      Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
+    }
+  }
+  Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
+}
+
 void TheoryStrings::checkDeqNF() {
   if( !d_conflict && d_lemma_cache.empty() ){
     std::vector< std::vector< Node > > cols;
@@ -3775,24 +3773,26 @@ void TheoryStrings::checkConstantEquivalenceClasses( TermIndex* ti, std::vector<
 }
 
 void TheoryStrings::checkExtendedFuncsEval( int effort ) {
+  Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl;
   if( effort==0 ){
     d_extf_vars.clear();
   }
+  d_extf_pol.clear();
   d_extf_exp.clear();
   d_extf_info.clear();
   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 ){
       Node n = (*it).first;
-      int n_pol = 0;
+      d_extf_pol[n] = 0;
       if( n.getType().isBoolean() ){
         if( areEqual( n, d_true ) ){
-          n_pol = 1;
+          d_extf_pol[n] = 1;
         }else if( areEqual( n, d_false ) ){
-          n_pol = -1;
+          d_extf_pol[n] = -1;
         }
       }
-      Trace("strings-extf-debug") << "Check extf " << n << "..." << std::endl;
+      Trace("strings-extf-debug") << "Check extf " << n << ", pol = " << d_extf_pol[n] << "..." << std::endl;
       if( effort==0 ){
         std::map< Node, bool > visited;
         collectVars( n, d_extf_vars[n], visited );
@@ -3888,14 +3888,14 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
               return;
             }
           }
-        }else if( ( nrc.getKind()==kind::OR && n_pol==-1 ) || ( nrc.getKind()==kind::AND && n_pol==1 ) ){
+        }else if( ( nrc.getKind()==kind::OR && d_extf_pol[n]==-1 ) || ( nrc.getKind()==kind::AND && d_extf_pol[n]==1 ) ){
           //infer the consequence of each
           d_ext_func_terms[n] = false;
-          d_extf_exp[n].push_back( n_pol==-1 ? n.negate() : n );
+          d_extf_exp[n].push_back( d_extf_pol[n]==-1 ? n.negate() : n );
           Trace("strings-extf-debug") << "  decomposable..." << std::endl;
-          Trace("strings-extf") << "  resolve extf : " << nr << " -> " << nrc << ", pol = " << n_pol << std::endl;
+          Trace("strings-extf") << "  resolve extf : " << nr << " -> " << nrc << ", pol = " << d_extf_pol[n] << std::endl;
           for( unsigned i=0; i<nrc.getNumChildren(); i++ ){
-            sendInfer( mkAnd( d_extf_exp[n] ), n_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
+            sendInfer( mkAnd( d_extf_exp[n] ), d_extf_pol[n]==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
           }
         }else{
           to_reduce = nrc;
@@ -3904,25 +3904,33 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
         to_reduce = n;
       }
       if( !to_reduce.isNull() ){
-        checkExtfInference( n, to_reduce, n_pol, effort );
+        checkExtfInference( n, to_reduce, effort );
         if( effort==1 ){
           Trace("strings-extf") << "  cannot rewrite extf : " << to_reduce << std::endl;
         }
+        if( Trace.isOn("strings-extf-list") ){
+          Trace("strings-extf-list") << "  * " << to_reduce;
+          if( d_extf_pol[n]!=0 ){
+            Trace("strings-extf-list") << ", pol = " << d_extf_pol[n];
+          }
+          if( n!=to_reduce ){
+            Trace("strings-extf-list") << ", from " << n;
+          }
+          Trace("strings-extf-list") << std::endl;
+        }
       }
     }else{
       Trace("strings-extf-debug")  << "  already reduced " << (*it).first << std::endl;
     }
   }
-  /*
-  for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
-    if( (*it).second ){
-
-    }
-  }
-  */
+  //for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+  //  if( (*it).second ){
+  //  }
+  //}
 }
 
-void TheoryStrings::checkExtfInference( Node n, Node nr, int n_pol, int effort ){
+void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){
+  int n_pol = d_extf_pol[n];
   if( n_pol!=0 ){
     //add original to explanation
     d_extf_exp[n].push_back( n_pol==1 ? n : n.negate() );
@@ -3949,8 +3957,21 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, int n_pol, int effort )
         Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
         bool pol = n_pol==1;
         if( std::find( d_extf_info[nr[0]].d_ctn[pol].begin(), d_extf_info[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info[nr[0]].d_ctn[pol].end() ){
+          Trace("strings-extf-debug") << "  store contains info : " << nr[0] << " " << pol << " " << nr[1] << std::endl;
           d_extf_info[nr[0]].d_ctn[pol].push_back( nr[1] );
           d_extf_info[nr[0]].d_ctn_from[pol].push_back( n );
+          //transitive closure for contains
+          bool opol = !pol;
+          for( unsigned i=0; i<d_extf_info[nr[0]].d_ctn[opol].size(); i++ ){
+            Node onr = d_extf_info[nr[0]].d_ctn[opol][i];
+            Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1] ).negate();
+            std::vector< Node > exp;
+            exp.insert( exp.end(), d_extf_exp[n].begin(), d_extf_exp[n].end() );
+            Node ofrom = d_extf_info[nr[0]].d_ctn_from[opol][i];
+            Assert( d_extf_exp.find( ofrom )!=d_extf_exp.end() );
+            exp.insert( exp.end(), d_extf_exp[ofrom].begin(), d_extf_exp[ofrom].end() );
+            sendInfer( mkAnd( exp ), conc, "CTN_Trans" );
+          }
         }else{
           Trace("strings-extf-debug") << "  redundant." << std::endl;
           d_ext_func_terms[n] = false;
@@ -4394,7 +4415,7 @@ Node TheoryStrings::getNormalSymRegExp(Node r, std::vector<Node> &nf_exp) {
 //// Finite Model Finding
 
 Node TheoryStrings::getNextDecisionRequest() {
-  if(d_opt_fmf && !d_conflict) {
+  if( options::stringFMF() && !d_conflict ){
     Node in_var_lsum = d_input_var_lsum.get();
     //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl;
     //initialize the term we will minimize
@@ -4451,9 +4472,6 @@ Node TheoryStrings::getNextDecisionRequest() {
   return Node::null();
 }
 
-void TheoryStrings::assertNode( Node lit ) {
-}
-
 void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) {
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 84f137ca5..bc53528f8 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -128,9 +128,6 @@ private:
   Node d_one;
   CVC4::Rational RMAXINT;
   unsigned d_card_size;
-  // Options
-  bool d_opt_fmf;
-  bool d_opt_regexp_gcd;
   // Helper functions
   Node getRepresentative( Node t );
   bool hasTerm( Node a );
@@ -175,9 +172,7 @@ private:
   NodeSet d_extf_infer_cache;
 
   bool doPreprocess( Node atom );
-  bool hasProcessed();
-  void addToExplanation( Node a, Node b, std::vector< Node >& exp );
-  void addToExplanation( Node lit, std::vector< Node >& exp );
+
 
 private:
   NodeSet d_congruent;
@@ -240,6 +235,20 @@ private:
   NodeNodeMap d_proxy_var;
   NodeNodeMap d_proxy_var_to_length;
 private:
+
+  //initial check
+  void checkInit();
+  void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
+  //extended functions evaluation check
+  void checkExtendedFuncsEval( int effort = 0 );
+  void checkExtfInference( Node n, Node nr, int effort );
+  void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited );
+  Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
+  //flat forms check
+  void checkFlatForms();
+  Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
+  //normal forms check
+  void checkNormalForms();
   void mergeCstVec(std::vector< Node > &vec_strings);
   bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
         std::vector< std::vector< Node > > &normal_forms,
@@ -265,22 +274,12 @@ private:
   bool processDeq( Node n1, Node n2 );
   int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
   int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
-  //bool unrollStar( Node atom );
-  Node mkRegExpAntec(Node atom, Node ant);
-
-  void checkInit();
-  void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
-  void checkExtendedFuncsEval( int effort = 0 );
-  void checkExtfInference( Node n, Node nr, int n_pol, int effort );
-  void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited );
-  void checkFlatForms();
-  void checkNormalForms();
-  Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
   void checkDeqNF();
-  void checkLengthsEqc();
-  void checkCardinality();
-  bool checkInductiveEquations();
+
+  //check for extended functions
+  void checkExtendedFuncs();
   //check membership constraints
+  Node mkRegExpAntec(Node atom, Node ant);
   Node normalizeRegexp(Node r);
   bool normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps);
   bool applyRConsume( CVC4::String &s, Node &r);
@@ -290,21 +289,25 @@ private:
     std::map< Node, std::vector< Node > > &memb_with_exps,
     std::map< Node, std::vector< Node > > &XinR_with_exps);
   void checkMemberships();
-  //temp
   bool checkMemberships2();
   bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
     std::vector< Node > &processed, std::vector< Node > &cprocessed,
     std::vector< Node > &nf_exp);
-  void checkExtendedFuncs();
+  //check contains
   void checkPosContains( std::vector< Node >& posContains );
   void checkNegContains( std::vector< Node >& negContains );
-  Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
-
+  //lengths normalize check
+  void checkLengthsEqc();
+  //cardinality check
+  void checkCardinality();
+  
 public:
+  /** preregister term */
   void preRegisterTerm(TNode n);
+  /** Expand definition */
   Node expandDefinition(LogicRequest &logicRequest, Node n);
+  /** Check at effort e */
   void check(Effort e);
-
   /** Conflict when merging two constants */
   void conflict(TNode a, TNode b);
   /** called when a new equivalence class is created */
@@ -320,12 +323,15 @@ public:
 protected:
   /** compute care graph */
   void computeCareGraph();
-
+  
   //do pending merges
   void assertPendingFact(Node atom, bool polarity, Node exp);
   void doPendingFacts();
   void doPendingLemmas();
-
+  bool hasProcessed();
+  void addToExplanation( Node a, Node b, std::vector< Node >& exp );
+  void addToExplanation( Node lit, std::vector< Node >& exp );
+  
   //register term
   bool registerTerm( Node n );
   //send lemma
@@ -381,11 +387,13 @@ private:
   //extended string terms and whether they have been reduced
   NodeBoolMap d_ext_func_terms;
   std::map< Node, std::map< Node, std::vector< Node > > > d_extf_vars;
+  // list of terms that something (does not) contain and their explanation
   class ExtfInfo {
   public:
     std::map< bool, std::vector< Node > > d_ctn;
     std::map< bool, std::vector< Node > > d_ctn_from;
   };
+  std::map< Node, int > d_extf_pol;
   std::map< Node, std::vector< Node > > d_extf_exp;
   std::map< Node, ExtfInfo > d_extf_info;
   //collect extended operator terms
@@ -432,7 +440,6 @@ private:
 public:
   //for finite model finding
   Node getNextDecisionRequest();
-  void assertNode( Node lit );
 
 public:
 /** statistics class */
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 8f899cd46..8224d6352 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -2,8 +2,8 @@
 /*! \file theory_strings_preprocess.cpp
  ** \verbatim
  ** Original author: Tianyi Liang
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -30,104 +30,30 @@ StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){
   d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
 }
 
-void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &ret ) {
-  int k = r.getKind();
+void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &new_nodes ) {
+  CVC4::Kind k = r.getKind();
   switch( k ) {
-    case kind::REGEXP_EMPTY: {
-      Node eq = NodeManager::currentNM()->mkConst( false );
-      ret.push_back( eq );
-      break;
-    }
-    case kind::REGEXP_SIGMA: {
-      Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
-      Node eq = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));
-      ret.push_back( eq );
-      break;
-    }
     case kind::REGEXP_RANGE: {
       Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
       Node eq = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));
-      ret.push_back( eq );
-      eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
-      ret.push_back( eq );
-      break;
-    }
-    case kind::STRING_TO_REGEXP: {
-      Node eq = s.eqNode( r[0] );
-      ret.push_back( eq );
-      break;
-    }
-    case kind::REGEXP_CONCAT: {
-      bool flag = true;
-      std::vector< Node > cc;
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        if(r[i].getKind() == kind::STRING_TO_REGEXP) {
-          cc.push_back( r[i][0] );
-        } else {
-          flag = false;
-          break;
-        }
-      }
-      if(flag) {
-        Node eq = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc));
-        ret.push_back(eq);
-      } else {
-        Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
-        ret.push_back( eq );
-      }
-      break;
-    }
-    case kind::REGEXP_UNION: {
-      std::vector< Node > c_or;
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        std::vector< Node > ntmp;
-        processRegExp( s, r[i], ntmp );
-        Node lem = ntmp.size()==1 ? ntmp[0] : NodeManager::currentNM()->mkNode(kind::AND, ntmp);
-        c_or.push_back( lem );
-      }
-      Node eq = NodeManager::currentNM()->mkNode(kind::OR, c_or);
-      ret.push_back( eq );
-      break;
-    }
-    case kind::REGEXP_INTER: {
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        processRegExp( s, r[i], ret );
-      }
-      break;
-    }
-    case kind::REGEXP_STAR: {
-      if(r[0].getKind() == kind::REGEXP_SIGMA) {
-        ret.push_back(NodeManager::currentNM()->mkConst(true));
-      } else {
-        Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
-        ret.push_back( eq );
-      }
+      new_nodes.push_back( eq );
       break;
     }
+    case kind::REGEXP_STAR:
+    case kind::REGEXP_CONCAT:
     case kind::REGEXP_LOOP: {
-      Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
-      ret.push_back( eq );
+      //do nothing
       break;
     }
     default: {
-      Trace("strings-error") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;
+      //all others should be rewritten by now
+      Trace("strings-error") << "Unsupported term: " << r << " in processRegExp." << std::endl;
       Assert( false, "Unsupported Term" );
     }
   }
 }
 
-bool StringsPreprocess::checkStarPlus( Node t ) {
-  if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) {
-    for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
-      if( checkStarPlus(t[i]) ){
-        return true;
-      }
-    }
-    return false;
-  } else {
-    return true;
-  }
-}
+/*
 int StringsPreprocess::checkFixLenVar( Node t ) {
   int ret = 2;
   if(t.getKind() == kind::EQUAL) {
@@ -152,7 +78,8 @@ int StringsPreprocess::checkFixLenVar( Node t ) {
   }
   return ret;
 }
-Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool during_pp ) {
+*/
+Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
   NodeNodeMap::const_iterator i = d_cache.find(t);
   if(i != d_cache.end()) {
     return (*i).second.isNull() ? t : (*i).second;
@@ -160,15 +87,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
 
   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 || 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 ) {
@@ -193,16 +111,29 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
     }
   } else */
   if( t.getKind() == kind::STRING_IN_REGEXP ) {
-    Node t0 = simplify( t[0], new_nodes, during_pp );
-
-    //rewrite it
+    //process any reductions
     std::vector< Node > ret;
-    processRegExp( t0, t[1], ret );
-
-    Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
-    n = Rewriter::rewrite(n);
-    d_cache[t] = (t == n) ? Node::null() : n;
-    retNode = n;
+    processRegExp( t[0], t[1], ret );
+    Node conc;
+    if( !ret.empty() ){
+      conc = ret.size()==1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
+    }
+    if( options::stringLazyPreproc() ){
+      //implication as lemma
+      if( !conc.isNull() ){
+        new_nodes.push_back( NodeManager::currentNM()->mkNode( kind::IMPLIES, t, conc ) );
+      }
+      d_cache[t] = t;
+    }else{
+      //rewrite as conjunction
+      Node n = t;
+      if( !conc.isNull() ){
+        n = NodeManager::currentNM()->mkNode( kind::AND, t, conc );
+        n = Rewriter::rewrite( n );
+      }
+      d_cache[t] = n;
+      retNode = n;
+    }
   } else if( t.getKind() == kind::STRING_SUBSTR ) {
     /*
     Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
@@ -595,7 +526,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
   return retNode;
 }
 
-Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool during_pp) {
+Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
   NodeNodeMap::const_iterator i = d_cache.find(t);
   if(i != d_cache.end()) {
     return (*i).second.isNull() ? t : (*i).second;
@@ -603,7 +534,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool
 
   unsigned num = t.getNumChildren();
   if(num == 0) {
-    return simplify(t, new_nodes, during_pp);
+    return simplify(t, new_nodes);
   } else {
     bool changed = false;
     std::vector< Node > cc;
@@ -611,7 +542,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool
       cc.push_back(t.getOperator());
     }
     for(unsigned i=0; i<t.getNumChildren(); i++) {
-      Node s = decompose(t[i], new_nodes, during_pp);
+      Node s = decompose(t[i], new_nodes);
       cc.push_back( s );
       if(s != t[i]) {
         changed = true;
@@ -619,9 +550,9 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool
     }
     if(changed) {
       Node tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc );
-      return simplify(tmp, new_nodes, during_pp);
+      return simplify(tmp, new_nodes);
     } else {
-      return simplify(t, new_nodes, during_pp);
+      return simplify(t, new_nodes);
     }
   }
 }
@@ -629,7 +560,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool
 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, true );
+    Node curr = decompose( vec_node[i], new_nodes );
     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 08fe478c4..22eb9eb91 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -2,8 +2,8 @@
 /*! \file theory_strings_preprocess.h
  ** \verbatim
  ** Original author: Tianyi Liang
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Major contributors: Morgan Deters, Andrew Reynolds
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -36,14 +36,13 @@ class StringsPreprocess {
   //Constants
   Node d_zero;
 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, bool during_pp );
+  //int checkFixLenVar( Node t );
+  void processRegExp( Node s, Node r, std::vector< Node > &new_nodes );
+  Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
   StringsPreprocess( context::UserContext* u );
 
-  Node decompose( Node t, std::vector< Node > &new_nodes, bool during_pp = false );
+  Node decompose( Node t, std::vector< Node > &new_nodes );
   void simplify(std::vector< Node > &vec_node);
 };
 
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 2d6c1e3af..168606462 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -673,7 +673,6 @@ Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) {
   Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl;
   Node retNode = node;
   std::vector<Node> node_vec;
-  bool emptyflag = false;
   //Node allNode = Node::null();
   for(unsigned i=0; i<node.getNumChildren(); ++i) {
     if(node[i].getKind() == kind::REGEXP_INTER) {
@@ -685,7 +684,6 @@ Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) {
           }
         }
       } else if(tmpNode.getKind() == kind::REGEXP_EMPTY) {
-        emptyflag = true;
         retNode = tmpNode;
         break;
       } else if(tmpNode.getKind() == kind::REGEXP_STAR && tmpNode[0].getKind() == kind::REGEXP_SIGMA) {
@@ -696,7 +694,6 @@ Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) {
         }
       }
     } else if(node[i].getKind() == kind::REGEXP_EMPTY) {
-      emptyflag = true;
       retNode = node[i];
       break;
     } else if(node[i].getKind() == kind::REGEXP_STAR && node[i][0].getKind() == kind::REGEXP_SIGMA) {
@@ -707,7 +704,7 @@ Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) {
       }
     }
   }
-  if(!emptyflag) {
+  if( retNode==node ){
     std::vector< Node > nvec;
     retNode = node_vec.size() == 0 ?
           NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, nvec)) :
@@ -911,18 +908,32 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
       retNode = NodeManager::currentNM()->mkConst( true );
     }
   }else if( r.getKind() == kind::REGEXP_CONCAT ){
-    bool flag = true;
+    bool allSigma = true;
+    bool allString = true;
+    std::vector< Node > cc;
     for(unsigned i=0; i<r.getNumChildren(); i++) {
       Assert( r[i].getKind() != kind::REGEXP_EMPTY );
       if( r[i].getKind() != kind::REGEXP_SIGMA ){
-        flag = false;
-        break;
+        allSigma = false;
+      }
+      if( r[i].getKind() != kind::STRING_TO_REGEXP ){
+        allString = false;
+      }else{
+        cc.push_back( r[i] );
       }
     }
-    if( flag ){
+    if( allSigma ){
       Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational( r.getNumChildren() ) );
       retNode = num.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x));
+    }else if( allString ){
+      retNode = x.eqNode( mkConcat( kind::STRING_CONCAT, cc ) );
+    }
+  }else if( r.getKind()==kind::REGEXP_INTER || r.getKind()==kind::REGEXP_UNION ){
+    std::vector< Node > mvec;
+    for( unsigned i=0; i<r.getNumChildren(); i++ ){
+      mvec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r[i] ) );
     }
+    retNode = NodeManager::currentNM()->mkNode( r.getKind()==kind::REGEXP_INTER ? kind::AND : kind::OR, mvec );
   }else if(r.getKind() == kind::STRING_TO_REGEXP) {
     retNode = x.eqNode(r[0]);
   }else if(x != node[0] || r != node[1]) {