Merge branch 'master' of https://github.com/CVC4/CVC4

23 files changed, 912 insertions, 191 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index cfaa6d1ad..9e3fed20a 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -197,16 +197,17 @@ void CandidateGeneratorQEAll::reset( Node eqc ) {
 
 Node CandidateGeneratorQEAll::getNextCandidate() {
   while( !d_eq.isFinished() ){
-    Node n = (*d_eq);
+    TNode n = (*d_eq);
     ++d_eq;
     if( n.getType().isSubtypeOf( d_match_pattern_type ) ){
-      if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
+      TNode nh = d_qe->getTermDatabase()->getHasTermEqc( n );
+      if( !nh.isNull() ){
         if( options::instMaxLevel()!=-1 ){
-          n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index );
+          nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index );
         }
         d_firstTime = false;
         //an equivalence class with the same type as the pattern, return it
-        return n;
+        return nh;
       }
     }
   }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index ffe64beba..bf9409f06 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -248,7 +248,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
         Node t = getModelTerm( conj->d_candidates[i] );
         model_terms.push_back( t );
-        Trace("cegqi-engine") << t << " ";
+        Trace("cegqi-engine") << conj->d_candidates[i] << " -> " << t << " ";
       }
       Trace("cegqi-engine") << std::endl;
       d_quantEngine->addInstantiation( q, model_terms, false );
@@ -279,7 +279,7 @@ bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node
   for( unsigned i=0; i<n.size(); i++ ){
     Node nv = getModelValue( n[i] );
     v.push_back( nv );
-    Trace("cegqi-engine") << nv << " ";
+    Trace("cegqi-engine") << n[i] << " -> " << nv << " ";
     if( nv.isNull() ){
       success = false;
     }
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 06552196d..2f8822b53 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -352,7 +352,8 @@ bool ConjectureGenerator::isGroundTerm( TNode n ) {
 }

 

 bool ConjectureGenerator::needsCheck( Theory::Effort e ) {

-  return e==Theory::EFFORT_FULL;

+  // synchonized with instantiation engine

+  return d_quantEngine->getInstWhenNeedsCheck( e );

 }

 

 bool ConjectureGenerator::hasEnumeratedUf( Node n ) {

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 8918a6dac..b9e8aef09 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -530,12 +530,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
                   //skip inst constant nodes
                   while( nv<maxs[index] && nv<=max_i &&
                          r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
-                    childIndex[index]++;
-                    nv = childIndex[index]+1;
+                    nv++;
                   }
                 }
                 if( nv<maxs[index] && nv<=max_i ){
-                  childIndex[index]++;
+                  childIndex[index] = nv;
                   index++;
                 }else{
                   childIndex.pop_back();
@@ -545,8 +544,11 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
             }
             success = index>=0;
             if( success ){
-              Trace("inst-alg-rd") << "Try instantiation..." << std::endl;
-              index--;
+              Trace("inst-alg-rd") << "Try instantiation { ";
+              for( unsigned j=0; j<childIndex.size(); j++ ){
+                Trace("inst-alg-rd") << childIndex[j] << " ";
+              }
+              Trace("inst-alg-rd") << "}" << std::endl;
               //try instantiation
               std::vector< Node > terms;
               for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
@@ -560,6 +562,8 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
                 Trace("inst-alg-rd") << "Success!" << std::endl;
                 ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
                 return STATUS_UNKNOWN;
+              }else{
+                index--;
               }
             }
           }while( success );
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index ade6d4313..b53919aaf 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -31,7 +31,7 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ){
 
 }
 
@@ -178,37 +178,11 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
 }
 
 bool InstantiationEngine::needsCheck( Theory::Effort e ){
-  if( e==Theory::EFFORT_FULL ){
-    d_ierCounter++;
-  }
-  //determine if we should perform check, based on instWhenMode
-  bool performCheck = false;
-  if( options::instWhenMode()==INST_WHEN_FULL ){
-    performCheck = ( e >= Theory::EFFORT_FULL );
-  }else if( options::instWhenMode()==INST_WHEN_FULL_DELAY ){
-    performCheck = ( e >= Theory::EFFORT_FULL ) && !d_quantEngine->getTheoryEngine()->needCheck();
-  }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){
-    performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
-  }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){
-    performCheck = ( e >= Theory::EFFORT_LAST_CALL );
-  }else{
-    performCheck = true;
-  }
-  static int ierCounter2 = 0;
-  if( e==Theory::EFFORT_LAST_CALL ){
-    ierCounter2++;
-    //with bounded integers, skip every other last call,
-    // since matching loops may occur with infinite quantification
-    if( ierCounter2%2==0 && options::fmfBoundInt() ){
-      performCheck = false;
-    }
-  }
-  return performCheck;
+  return d_quantEngine->getInstWhenNeedsCheck( e );
 }
 
 void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
-    Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl;
     double clSet = 0;
     if( Trace.isOn("inst-engine") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 2fa37ac35..2d427ae0a 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -84,8 +84,6 @@ private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   /** whether the instantiation engine should set incomplete if it cannot answer SAT */
   bool d_setIncomplete;
-  /** inst round counter */
-  int d_ierCounter;
   /** whether each quantifier is active */
   std::map< Node, bool > d_quant_active;
   /** whether we have added cbqi lemma */
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index a8774440e..793e4a611 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -44,6 +44,8 @@ sort INST_PATTERN_LIST_TYPE \
 # a list of instantiation patterns
 operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
 
+operator INST_CLOSURE 1 "predicate for specifying term in instantiation closure."
+
 typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule 
 typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule 
 typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule 
@@ -51,6 +53,7 @@ typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule
 typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule 
 typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule 
 typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule 
+typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule 
 
 # for rewrite rules
 # types...
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index dad173ff5..cac78af46 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -41,7 +41,7 @@ option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
 option cnfQuant --cnf-quant bool :default false
  apply CNF conversion to quantified formulas
 # Whether to NNF quantifier bodies
-option nnfQuant --nnf-quant bool :default false
+option nnfQuant --nnf-quant bool :default true
  apply NNF conversion to quantified formulas
 
 option clauseSplit --clause-split bool :default false
@@ -88,7 +88,7 @@ option fmfFunWellDefined --fmf-fun bool :default false
 option registerQuantBodyTerms --register-quant-body-terms bool :default false
  consider ground terms within bodies of quantified formulas for matching
 
-option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
+option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
  when to apply instantiation
 option instMaxLevel --inst-max-level=N int :read-write :default -1
  maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
@@ -127,7 +127,7 @@ option finiteModelFind finite-model-find --finite-model-find bool :default false
 
 option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose mode for model-based quantifier instantiation
-option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
+option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false
  only add one instantiation per quantifier per round for mbqi
 option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
  only add instantiations for one quantifier per round for mbqi
@@ -196,5 +196,7 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo
 
 option localTheoryExt --local-t-ext bool :default false
   do instantiation based on local theory extensions
+option termDbInstClosure --term-db-inst-closure bool :default false
+  only consider inst closure terms for E-matching
  
 endmodule
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 08fcf319d..e9f85d454 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -29,17 +29,17 @@ namespace quantifiers {
 static const std::string instWhenHelp = "\
 Modes currently supported by the --inst-when option:\n\
 \n\
-full (default)\n\
+full-last-call (default)\n\
++ Alternate running instantiation rounds at full effort and last\n\
+  call.  In other words, interleave instantiation and theory combination.\n\
+\n\
+full\n\
 + Run instantiation round at full effort, before theory combination.\n\
 \n\
 full-delay \n\
 + Run instantiation round at full effort, before theory combination, after\n\
   all other theories have finished.\n\
 \n\
-full-last-call\n\
-+ Alternate running instantiation rounds at full effort and last\n\
-  call.  In other words, interleave instantiation and theory combination.\n\
-\n\
 last-call\n\
 + Run instantiation at last call effort, after theory combination and\n\
   and theories report sat.\n\
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0ed175393..1e6ec3a02 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -309,11 +309,19 @@ Node QuantifiersRewriter::computeNNF( Node body ){
     }else{
       std::vector< Node > children;
       Kind k = body[0].getKind();
+      
       if( body[0].getKind()==OR || body[0].getKind()==AND ){
+        k = body[0].getKind()==AND ? OR : AND;
         for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
-          children.push_back( computeNNF( body[0][i].notNode() ) );
+          Node nc = computeNNF( body[0][i].notNode() );
+          if( nc.getKind()==k ){
+            for( unsigned j=0; j<nc.getNumChildren(); j++ ){
+              children.push_back( nc[j] );
+            }
+          }else{
+            children.push_back( nc );
+          }
         }
-        k = body[0].getKind()==AND ? OR : AND;
       }else if( body[0].getKind()==IFF ){
         for( int i=0; i<2; i++ ){
           Node nn = i==0 ? body[0][i] : body[0][i].notNode();
@@ -335,10 +343,18 @@ Node QuantifiersRewriter::computeNNF( Node body ){
   }else{
     std::vector< Node > children;
     bool childrenChanged = false;
+    bool isAssoc = body.getKind()==AND || body.getKind()==OR;
     for( int i=0; i<(int)body.getNumChildren(); i++ ){
       Node nc = computeNNF( body[i] );
-      children.push_back( nc );
-      childrenChanged = childrenChanged || nc!=body[i];
+      if( isAssoc && nc.getKind()==body.getKind() ){
+        for( unsigned j=0; j<nc.getNumChildren(); j++ ){
+          children.push_back( nc[j] );
+        }
+        childrenChanged = true;
+      }else{
+        children.push_back( nc );
+        childrenChanged = childrenChanged || nc!=body[i];
+      }
     }
     if( childrenChanged ){
       return NodeManager::currentNM()->mkNode( body.getKind(), children );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a95de086a..34c40c8c4 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -111,13 +111,17 @@ Node TermDb::getOperator( Node n ) {
   }
 }
 
-void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
+void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){
   //don't add terms in quantifier bodies
   if( withinQuant && !options::registerQuantBodyTerms() ){
     return;
   }
+  bool rec = false;
   if( d_processed.find( n )==d_processed.end() ){
     d_processed.insert(n);
+    if( withinInstClosure ){
+      d_iclosure_processed.insert( n );
+    }
     d_type_map[ n.getType() ].push_back( n );
     //if this is an atomic trigger, consider adding it
     //Call the children?
@@ -137,9 +141,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
         d_op_map[op].push_back( n );
         added.insert( n );
 
-        for( size_t i=0; i<n.getNumChildren(); i++ ){
-          addTerm( n[i], added, withinQuant );
-          if( options::eagerInstQuant() ){
+        if( options::eagerInstQuant() ){
+          for( size_t i=0; i<n.getNumChildren(); i++ ){
             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
               int addedLemmas = 0;
               for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
@@ -149,10 +152,15 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
           }
         }
       }
-    }else{
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        addTerm( n[i], added, withinQuant );
-      }
+    }
+    rec = true;
+  }else if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
+    d_iclosure_processed.insert( n );
+    rec = true;
+  }
+  if( rec ){
+    for( size_t i=0; i<n.getNumChildren(); i++ ){
+      addTerm( n[i], added, withinQuant, withinInstClosure );
     }
   }
 }
@@ -317,30 +325,65 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
 }
 
 bool TermDb::hasTermCurrent( Node n ) {
-  //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n );
-  if( options::termDbMode()==TERM_DB_ALL ){
-    return true;
-  }else if( options::termDbMode()==TERM_DB_RELEVANT ){
-    return d_has_map.find( n )!=d_has_map.end();
-  }else{
-    Assert( false );
+  if( options::termDbInstClosure() && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
     return false;
+  }else{
+    //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
+    if( options::termDbMode()==TERM_DB_ALL ){
+      return true;
+    }else if( options::termDbMode()==TERM_DB_RELEVANT ){
+      return d_has_map.find( n )!=d_has_map.end();
+    }else{
+      Assert( false );
+      return false;
+    }
   }
 }
 
-void TermDb::setHasTerm( Node n ) {
-  if( inst::Trigger::isAtomicTrigger( n ) ){
-    if( d_has_map.find( n )==d_has_map.end() ){
-      d_has_map[n] = true;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        setHasTerm( n[i] );
+Node TermDb::getHasTermEqc( Node r ) {
+  if( hasTermCurrent( r ) ){
+    return r;
+  }else{
+    if( options::termDbInstClosure()  ){
+      std::map< Node, Node >::iterator it = d_has_eqc.find( r );
+      if( it==d_has_eqc.end() ){
+        Node h;
+        eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+        while( h.isNull() && !eqc_i.isFinished() ){
+          TNode n = (*eqc_i);
+          ++eqc_i;
+          if( hasTermCurrent( n ) ){
+            h = n;
+          }
+        }
+        d_has_eqc[r] = h;
+        return h;
+      }else{
+        return it->second;
       }
+    }else{
+      //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc
+      return Node::null();
+    }
+  }
+}
+
+void TermDb::setHasTerm( Node n ) {
+  //if( inst::Trigger::isAtomicTrigger( n ) ){
+  if( d_has_map.find( n )==d_has_map.end() ){
+    d_has_map[n] = true;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      setHasTerm( n[i] );
     }
+  }
+    /*
   }else{
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       setHasTerm( n[i] );
     }
   }
+  */
 }
 
 void TermDb::reset( Theory::Effort effort ){
@@ -356,6 +399,7 @@ void TermDb::reset( Theory::Effort effort ){
   //compute has map
   if( options::termDbMode()==TERM_DB_RELEVANT ){
     d_has_map.clear();
+    d_has_eqc.clear();
     eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
     while( !eqcs_i.isFinished() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 2b151bb04..cb9f5eeef 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -123,6 +123,8 @@ private:
   QuantifiersEngine* d_quantEngine;
   /** terms processed */
   std::hash_set< Node, NodeHashFunction > d_processed;
+  /** terms processed */
+  std::hash_set< Node, NodeHashFunction > d_iclosure_processed;
 private:
   /** select op map */
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
@@ -144,6 +146,8 @@ public:
   std::map< Node, std::vector< Node > > d_op_map;
   /** has map */
   std::map< Node, bool > d_has_map;
+  /** map from reps to a term in eqc in d_has_map */
+  std::map< Node, Node > d_has_eqc;
   /** map from APPLY_UF functions to trie */
   std::map< Node, TermArgTrie > d_func_map_trie;
   std::map< Node, TermArgTrie > d_func_map_eqc_trie;
@@ -152,7 +156,7 @@ public:
   /** map from type nodes to terms of that type */
   std::map< TypeNode, std::vector< Node > > d_type_map;
   /** add a term to the database */
-  void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
+  void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false );
   /** reset (calculate which terms are active) */
   void reset( Theory::Effort effort );
   /** get operator*/
@@ -176,6 +180,8 @@ public:
   bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
   /** has term */
   bool hasTermCurrent( Node n );
+  /** get has term eqc */
+  Node getHasTermEqc( Node r );
   
 //for model basis
 private:
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5c68e52a7..de0f98af6 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -35,7 +35,6 @@ using namespace CVC4::theory::quantifiers;
 
 TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
   Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
-  d_numRestarts(0),
   d_masterEqualityEngine(0)
 {
   d_numInstantiations = 0;
@@ -97,6 +96,10 @@ Node TheoryQuantifiers::getValue(TNode n) {
   }
 }
 
+void TheoryQuantifiers::computeCareGraph() {
+  //do nothing
+}
+
 void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) {
   if(fullModel) {
     for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
@@ -126,12 +129,22 @@ void TheoryQuantifiers::check(Effort e) {
     case kind::FORALL:
       assertUniversal( assertion );
       break;
+    case kind::INST_CLOSURE:
+      getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
+      break;
+    case kind::EQUAL:
+      //do nothing
+      break;
     case kind::NOT:
       {
         switch( assertion[0].getKind()) {
         case kind::FORALL:
           assertExistential( assertion );
           break;
+        case kind::EQUAL:
+          //do nothing
+          break;
+        case kind::INST_CLOSURE: //cannot negate inst closure
         default:
           Unhandled(assertion[0].getKind());
           break;
@@ -182,23 +195,7 @@ bool TheoryQuantifiers::flipDecision(){
   //}else{
   //  return false;
   //}
-
-  if( !d_out->flipDecision() ){
-    return restart();
-  }
-  return true;
-}
-
-bool TheoryQuantifiers::restart(){
-  static const int restartLimit = 0;
-  if( d_numRestarts==restartLimit ){
-    Debug("quantifiers-flip") << "No more restarts." << std::endl;
-    return false;
-  }else{
-    d_numRestarts++;
-    Debug("quantifiers-flip") << "Do restart." << std::endl;
-    return true;
-  }
+  return false;
 }
 
 void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index aace13b24..6d3fa4d46 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -44,17 +44,15 @@ private:
   /** number of instantiations */
   int d_numInstantiations;
   int d_baseDecLevel;
-  /** number of restarts */
-  int d_numRestarts;
 
   eq::EqualityEngine* d_masterEqualityEngine;
-
+private:
+  void computeCareGraph();  
 public:
   TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
   ~TheoryQuantifiers();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
-
   void addSharedTerm(TNode t);
   void notifyEq(TNode lhs, TNode rhs);
   void preRegisterTerm(TNode n);
@@ -73,7 +71,6 @@ public:
 private:
   void assertUniversal( Node n );
   void assertExistential( Node n );
-  bool restart();
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 5d86c29c0..341e656c7 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -84,6 +84,12 @@ struct QuantifierInstPatternTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw(TypeCheckingExceptionPrivate) {
     Assert(n.getKind() == kind::INST_PATTERN );
+    if( check ){
+      TypeNode tn = n[0].getType(check);
+      if( tn.isFunction() ){
+        throw TypeCheckingExceptionPrivate(n[0], "Pattern must be a list of fully-applied terms.");
+      }
+    }
     return nodeManager->instPatternType();
   }
 };/* struct QuantifierInstPatternTypeRule */
@@ -120,6 +126,20 @@ struct QuantifierInstPatternListTypeRule {
 };/* struct QuantifierInstPatternListTypeRule */
 
 
+struct QuantifierInstClosureTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw(TypeCheckingExceptionPrivate) {
+    Assert(n.getKind() == kind::INST_CLOSURE );
+    if( check ){
+      TypeNode tn = n[0].getType(check);
+      if( tn.isBoolean() ){
+        throw TypeCheckingExceptionPrivate(n, "argument of inst-closure must be non-boolean");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* struct QuantifierInstClosureTypeRule */
+
 class RewriteRuleTypeRule {
 public:
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 04b6c5d16..d6c6f4667 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -171,8 +171,9 @@ d_lemmas_produced_c(u){
     d_builder = NULL;
   }
 
-  //options
   d_total_inst_count_debug = 0;
+  d_ierCounter = 0;
+  d_ierCounter_lc = 0;
 }
 
 QuantifiersEngine::~QuantifiersEngine(){
@@ -251,6 +252,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
     return;
   }
+  if( e==Theory::EFFORT_FULL ){
+    d_ierCounter++;
+  }else if( e==Theory::EFFORT_LAST_CALL ){
+    d_ierCounter_lc++;
+  }
   bool needsCheck = false;
   bool needsModel = false;
   bool needsFullModel = false;
@@ -472,9 +478,9 @@ Node QuantifiersEngine::getNextDecisionRequest(){
   return Node::null();
 }
 
-void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
+void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
   std::set< Node > added;
-  getTermDatabase()->addTerm( n, added, withinQuant );
+  getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
   //maybe have triggered instantiations if we are doing eager instantiation
   if( options::eagerInstQuant() ){
     flushLemmas();
@@ -825,6 +831,30 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool
   return addSplit( fm );
 }
 
+bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
+  //determine if we should perform check, based on instWhenMode
+  bool performCheck = false;
+  if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){
+    performCheck = ( e >= Theory::EFFORT_FULL );
+  }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
+    performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
+  }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
+    performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+  }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
+    performCheck = ( e >= Theory::EFFORT_LAST_CALL );
+  }else{
+    performCheck = true;
+  }
+  if( e==Theory::EFFORT_LAST_CALL ){
+    //with bounded integers, skip every other last call,
+    // since matching loops may occur with infinite quantification
+    if( d_ierCounter_lc%2==0 && options::fmfBoundInt() ){
+      performCheck = false;
+    }
+  }
+  return performCheck;
+}
+
 void QuantifiersEngine::flushLemmas(){
   if( !d_lemmas_waiting.empty() ){
     //take default output channel if none is provided
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 199fe79b9..ac782a536 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -169,6 +169,9 @@ private:
   std::map< Node, int > d_total_inst_debug;
   std::map< Node, int > d_temp_inst_debug;
   int d_total_inst_count_debug;
+  /** inst round counters */
+  int d_ierCounter;
+  int d_ierCounter_lc;
 private:
   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
 public:
@@ -273,6 +276,8 @@ public:
   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
   /** get number of waiting lemmas */
   int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
+  /** get needs check */
+  bool getInstWhenNeedsCheck( Theory::Effort e );
   /** set instantiation level attr */
   static void setInstantiationLevelAttr( Node n, uint64_t level );
   /** is term eligble for instantiation? */
@@ -290,7 +295,7 @@ public:
   /** get trigger database */
   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
   /** add term to database */
-  void addTermToDatabase( Node n, bool withinQuant = false );
+  void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
   /** get the master equality engine */
   eq::EqualityEngine* getMasterEqualityEngine() ;
   /** debug print equality engine */
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 69b089c84..016983059 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1157,9 +1157,10 @@ void RegExpOpr::getCharSet( Node r, std::set<unsigned> &pcset, SetNodes &pvset )
       }
       case kind::REGEXP_INTER: {
         //TODO: Overapproximation for now
-        for(unsigned i=0; i<r.getNumChildren(); i++) {
-          getCharSet(r[i], cset, vset);
-        }
+        //for(unsigned i=0; i<r.getNumChildren(); i++) {
+          //getCharSet(r[i], cset, vset);
+        //}
+        getCharSet(r[0], cset, vset);
         break;
       }
       case kind::REGEXP_STAR: {
@@ -1382,7 +1383,8 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) {
   }
 }
 Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node > cache, bool &spflag, unsigned cnt ) {
-  Trace("regexp-intersect") << "Starting INTERSECT:\n  "<< mkString(r1) << ",\n  " << mkString(r2) << std::endl;
+  //(checkConstRegExp(r1) && checkConstRegExp(r2))
+  Trace("regexp-intersect") << "Starting INTERSECT(" << cnt << "):\n  "<< mkString(r1) << ",\n  " << mkString(r2) << std::endl;
   //if(Trace.isOn("regexp-debug")) {
   //  Trace("regexp-debug") << "... with cache:\n";
   //  for(std::map< PairNodes, Node >::const_iterator itr=cache.begin();
@@ -1397,9 +1399,9 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node
   std::pair < Node, Node > p(r1, r2);
   std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_inter_cache.find(p);
   Node rNode;
-  if(itr != d_inter_cache.end()) {
-    rNode = itr->second;
-  } else {
+//  if(itr != d_inter_cache.end()) {
+//    rNode = itr->second;
+//  } else {
     if(r1 == d_emptyRegexp || r2 == d_emptyRegexp) {
       rNode = d_emptyRegexp;
     } else if(r1 == d_emptySingleton || r2 == d_emptySingleton) {
@@ -1414,79 +1416,138 @@ Node RegExpOpr::intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node
         rNode = d_emptyRegexp;
       }
     } else if(r1 == r2) {
-      rNode = convert1(cnt, r1);
+      rNode = r1; //convert1(cnt, r1);
     } else {
       PairNodes p(r1, r2);
       std::map< PairNodes, Node >::const_iterator itrcache = cache.find(p);
       if(itrcache != cache.end()) {
         rNode = itrcache->second;
       } else {
-        if(checkConstRegExp(r1) && checkConstRegExp(r2)) {
-          std::vector< unsigned > cset;
-          std::set< unsigned > cset1, cset2;
-          std::set< Node > vset1, vset2;
-          firstChars(r1, cset1, vset1);
-          firstChars(r2, cset2, vset2);
-          std::set_intersection(cset1.begin(), cset1.end(), cset2.begin(), cset1.end(),
-               std::inserter(cset, cset.begin()));
-          std::vector< Node > vec_nodes;
-          Node delta_exp;
-          int flag = delta(r1, delta_exp);
-          int flag2 = delta(r2, delta_exp);
-          if(flag != 2 && flag2 != 2) {
-            if(flag == 1 && flag2 == 1) {
-              vec_nodes.push_back(d_emptySingleton);
-            } else {
-              //TODO
-              spflag = true;
-            }
-          }
-          if(Trace.isOn("regexp-debug")) {
-            Trace("regexp-debug") << "Try CSET( " << cset.size() << " ) = ";
-            for(std::vector<unsigned>::const_iterator itr = cset.begin();
-              itr != cset.end(); itr++) {
-              CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
-              Trace("regexp-debug") << c << ", ";
-            }
-            Trace("regexp-debug") << std::endl;
+        std::vector< unsigned > cset;
+        std::set< unsigned > cset1, cset2;
+        std::set< Node > vset1, vset2;
+        firstChars(r1, cset1, vset1);
+        firstChars(r2, cset2, vset2);
+        std::set_intersection(cset1.begin(), cset1.end(), cset2.begin(), cset1.end(),
+             std::inserter(cset, cset.begin()));
+        std::vector< Node > vec_nodes;
+        Node delta_exp;
+        int flag = delta(r1, delta_exp);
+        int flag2 = delta(r2, delta_exp);
+        if(flag != 2 && flag2 != 2) {
+          if(flag == 1 && flag2 == 1) {
+            vec_nodes.push_back(d_emptySingleton);
+          } else {
+            //TODO
+            spflag = true;
           }
+        }
+        if(Trace.isOn("regexp-debug")) {
+          Trace("regexp-debug") << "Try CSET( " << cset.size() << " ) = ";
           for(std::vector<unsigned>::const_iterator itr = cset.begin();
             itr != cset.end(); itr++) {
             CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
-            Node r1l = derivativeSingle(r1, c);
-            Node r2l = derivativeSingle(r2, c);
-            std::map< PairNodes, Node > cache2(cache);
-            PairNodes p(r1, r2);
-            cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt)));
-            Node rt = intersectInternal2(r1l, r2l, cache2, spflag, cnt+1);
-            rt = convert1(cnt, rt);
-            if(spflag) {
-              //TODO:
-              return Node::null();
-            }
-            rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
-              NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );
-            vec_nodes.push_back(rt);
+            Trace("regexp-debug") << c << ", ";
           }
-          rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] :
-              NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);
-          rNode = Rewriter::rewrite( rNode );
-        } else {
-          //TODO: non-empty var set
-          spflag = true;
+          Trace("regexp-debug") << std::endl;
+        }
+        for(std::vector<unsigned>::const_iterator itr = cset.begin();
+          itr != cset.end(); itr++) {
+          CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );
+          Node r1l = derivativeSingle(r1, c);
+          Node r2l = derivativeSingle(r2, c);
+          std::map< PairNodes, Node > cache2(cache);
+          PairNodes p(r1, r2);
+          cache2[ p ] = NodeManager::currentNM()->mkNode(kind::REGEXP_RV, NodeManager::currentNM()->mkConst(CVC4::Rational(cnt)));
+          Node rt = intersectInternal2(r1l, r2l, cache2, spflag, cnt+1);
+          //if(spflag) {
+            //return Node::null();
+          //}
+          rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
+            NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );
+          vec_nodes.push_back(rt);
         }
+        rNode = vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] :
+            NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes);
+        rNode = Rewriter::rewrite( rNode );
+        rNode = convert1(cnt, rNode);
+        rNode = Rewriter::rewrite( rNode );
       }
     }
-    d_inter_cache[p] = rNode;
-  }
-  Trace("regexp-intersect") << "End of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl;
+//    d_inter_cache[p] = rNode;
+//  }
+  Trace("regexp-intersect") << "End(" << cnt << ") of INTERSECT( " << mkString(r1) << ", " << mkString(r2) << " ) = " << mkString(rNode) << std::endl;
   return rNode;
 }
+
+Node RegExpOpr::removeIntersection(Node r) {
+  Assert( checkConstRegExp(r) );
+  std::map < Node, Node >::const_iterator itr = d_rm_inter_cache.find(r);
+  Node retNode;
+  if(itr != d_rm_inter_cache.end()) {
+    retNode = itr->second;
+  } else {
+    switch(r.getKind()) {
+      case kind::REGEXP_EMPTY: {
+        retNode = r;
+        break;
+      }
+      case kind::REGEXP_SIGMA: {
+        retNode = r;
+        break;
+      }
+      case kind::STRING_TO_REGEXP: {
+        retNode = r;
+        break;
+      }
+      case kind::REGEXP_CONCAT: {
+        std::vector< Node > vec_nodes;
+        for(unsigned i=0; i<r.getNumChildren(); i++) {
+          Node tmpNode = removeIntersection( r[i] );
+          vec_nodes.push_back( tmpNode );
+        }
+        retNode = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes) );
+        break;
+      }
+      case kind::REGEXP_UNION: {
+        std::vector< Node > vec_nodes;
+        for(unsigned i=0; i<r.getNumChildren(); i++) {
+          Node tmpNode = removeIntersection( r[i] );
+          vec_nodes.push_back( tmpNode );
+        }
+        retNode = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes) );
+        break;
+      }
+      case kind::REGEXP_INTER: {
+        retNode = removeIntersection( r[0] );
+        for(unsigned i=1; i<r.getNumChildren(); i++) {
+          bool spflag = false;
+          Node tmpNode = removeIntersection( r[i] );
+          retNode = intersect( retNode, tmpNode, spflag );
+        }
+        break;
+      }
+      case kind::REGEXP_STAR: {
+        retNode = removeIntersection( r[0] );
+        retNode = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, retNode) );
+        break;
+      }
+      default: {
+        Unreachable();
+      }
+    }
+    d_rm_inter_cache[r] = retNode;
+  }
+  Trace("regexp-intersect") << "Remove INTERSECTION( " << mkString(r) << " ) = " << mkString(retNode) << std::endl;
+  return retNode;
+}
+
 Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) {
-  //std::map< unsigned, std::set< PairNodes > > cache;
-  std::map< PairNodes, Node > cache;
   if(checkConstRegExp(r1) && checkConstRegExp(r2)) {
-    return intersectInternal2(r1, r2, cache, spflag, 1);
+    Node rr1 = removeIntersection(r1);
+    Node rr2 = removeIntersection(r2);
+    std::map< PairNodes, Node > cache;
+    return intersectInternal2(rr1, rr2, cache, spflag, 1);
   } else {
     spflag = true;
     return Node::null();
@@ -1653,8 +1714,115 @@ void RegExpOpr::splitRegExp(Node r, std::vector< PairNodes > &pset) {
   }
 }
 
+void RegExpOpr::flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec) {
+  Assert(false);
+  Assert(checkConstRegExp(r));
+  switch( r.getKind() ) {
+      case kind::REGEXP_EMPTY: {
+        //TODO
+        break;
+      }
+      case kind::REGEXP_SIGMA: {
+        CVC4::String s("a");
+        std::pair< CVC4::String, unsigned > tmp(s, 0);
+        //TODO
+        break;
+      }
+      case kind::STRING_TO_REGEXP: {
+        Assert(r[0].isConst());
+        CVC4::String s = r[0].getConst< CVC4::String >();
+        std::pair< CVC4::String, unsigned > tmp(s, 0);
+        //TODO
+        break;
+      }
+      case kind::REGEXP_CONCAT: {
+        for(unsigned i=0; i<r.getNumChildren(); i++) {
+          //TODO
+        }
+        break;
+      }
+      case kind::REGEXP_UNION: {
+        for(unsigned i=0; i<r.getNumChildren(); ++i) {
+          //TODO
+        }
+        break;
+      }
+      case kind::REGEXP_INTER: {
+        //TODO
+        break;
+      }
+      case kind::REGEXP_STAR: {
+        //TODO
+        break;
+      }
+      default: {
+        Unreachable();
+      }
+  }
+}
+
+void RegExpOpr::disjunctRegExp(Node r, std::vector<Node> &vec_or) {
+  switch(r.getKind()) {
+      case kind::REGEXP_EMPTY: {
+        vec_or.push_back(r);
+        break;
+      }
+      case kind::REGEXP_SIGMA: {
+        vec_or.push_back(r);
+        break;
+      }
+      case kind::STRING_TO_REGEXP: {
+        vec_or.push_back(r);
+        break;
+      }
+      case kind::REGEXP_CONCAT: {
+        disjunctRegExp(r[0], vec_or);
+        for(unsigned i=1; i<r.getNumChildren(); i++) {
+          std::vector<Node> vec_con;
+          disjunctRegExp(r[i], vec_con);
+          std::vector<Node> vec_or2;
+          for(unsigned k1=0; k1<vec_or.size(); k1++) {
+            for(unsigned k2=0; k2<vec_con.size(); k2++) {
+              Node tmp = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_or[k1], vec_con[k2]) );
+              if(std::find(vec_or2.begin(), vec_or2.end(), tmp) == vec_or2.end()) {
+                vec_or2.push_back( tmp );
+              }
+            }
+          }
+          vec_or = vec_or2;
+        }
+        break;
+      }
+      case kind::REGEXP_UNION: {
+        for(unsigned i=0; i<r.getNumChildren(); ++i) {
+          std::vector<Node> vec_or2;
+          disjunctRegExp(r[i], vec_or2);
+          vec_or.insert(vec_or.end(), vec_or2.begin(), vec_or2.end());
+        }
+        break;
+      }
+      case kind::REGEXP_INTER: {
+        Assert(checkConstRegExp(r));
+        Node rtmp = r[0];
+        bool spflag = false;
+        for(unsigned i=1; i<r.getNumChildren(); ++i) {
+          rtmp = intersect(rtmp, r[i], spflag);
+        }
+        disjunctRegExp(rtmp, vec_or);
+        break;
+      }
+      case kind::REGEXP_STAR: {
+        vec_or.push_back(r);
+        break;
+      }
+      default: {
+        Unreachable();
+      }
+  }
+}
+
 //printing
-std::string RegExpOpr::niceChar( Node r ) {
+std::string RegExpOpr::niceChar(Node r) {
   if(r.isConst()) {
     std::string s = r.getConst<CVC4::String>().toString() ;
     return s == "" ? "{E}" : ( s == " " ? "{ }" : s.size()>1? "("+s+")" : s );
@@ -1666,12 +1834,12 @@ std::string RegExpOpr::niceChar( Node r ) {
 std::string RegExpOpr::mkString( Node r ) {
   std::string retStr;
   if(r.isNull()) {
-    retStr = "Empty";
+    retStr = "Phi";
   } else {
     int k = r.getKind();
     switch( k ) {
       case kind::REGEXP_EMPTY: {
-        retStr += "Empty";
+        retStr += "Phi";
         break;
       }
       case kind::REGEXP_SIGMA: {
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index ce3093528..3b898e5f5 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -64,6 +64,7 @@ private:
   std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_cset_cache;
   std::map< Node, std::pair< std::set<unsigned>, std::set<Node> > > d_fset_cache;
   std::map< PairNodes, Node > d_inter_cache;
+  std::map< Node, Node > d_rm_inter_cache;
   std::map< Node, std::vector< PairNodes > > d_split_cache;
   //bool checkStarPlus( Node t );
   void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes );
@@ -79,6 +80,7 @@ private:
   Node convert1(unsigned cnt, Node n);
   void convert2(unsigned cnt, Node n, Node &r1, Node &r2);
   Node intersectInternal2( Node r1, Node r2, std::map< PairNodes, Node > cache, bool &spflag, unsigned cnt );
+  Node removeIntersection(Node r);
   void firstChars( Node r, std::set<unsigned> &pcset, SetNodes &pvset );
 
   //TODO: for intersection
@@ -96,6 +98,8 @@ public:
   Node intersect(Node r1, Node r2, bool &spflag);
   Node complement(Node r, int &ret);
   void splitRegExp(Node r, std::vector< PairNodes > &pset);
+  void flattenRegExp(Node r, std::vector< std::pair< CVC4::String, unsigned > > &fvec);
+  void disjunctRegExp(Node r, std::vector<Node> &vec_or);
 
   std::string mkString( Node r );
 };
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ead8a44f8..0df551847 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -55,9 +55,11 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
   d_regexp_memberships(c),
   d_regexp_ucached(u),
   d_regexp_ccached(c),
-  d_str_re_map(c),
+  d_pos_memberships(c),
+  d_neg_memberships(c),
   d_inter_cache(c),
   d_inter_index(c),
+  d_processed_memberships(c),
   d_regexp_ant(c),
   d_input_vars(u),
   d_input_var_lsum(u),
@@ -484,8 +486,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
           if( n.getKind() == kind::VARIABLE && options::stringFMF() ) {
             d_input_vars.insert(n);
           }
-        }
-        if (n.getType().isBoolean()) {
+        } else if (n.getType().isBoolean()) {
           // Get triggered for both equal and dis-equal
           d_equalityEngine.addTriggerPredicate(n);
         } else {
@@ -2514,6 +2515,318 @@ Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) {
   }
 }
 
+Node TheoryStrings::normalizeRegexp(Node r) {
+  Node nf_r = r;
+  if(d_nf_regexps.find(r) != d_nf_regexps.end()) {
+    nf_r = d_nf_regexps[r];
+  } else {
+    std::vector< Node > nf_exp;
+    if(!d_regexp_opr.checkConstRegExp(r)) {
+      switch( r.getKind() ) {
+        case kind::REGEXP_EMPTY:
+        case kind::REGEXP_SIGMA: {
+          break;
+        }
+        case kind::STRING_TO_REGEXP: {
+          if(r[0].isConst()) {
+            break;
+          } else {
+            if(d_normal_forms.find( r[0] ) != d_normal_forms.end()) {
+              nf_r = mkConcat( d_normal_forms[r[0]] );
+              Debug("regexp-nf") << "Term: " << r[0] << " has a normal form " << nf_r << std::endl;
+              nf_exp.insert(nf_exp.end(), d_normal_forms_exp[r[0]].begin(), d_normal_forms_exp[r[0]].end());
+              nf_r = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, nf_r) );
+            }
+          }
+        }
+        case kind::REGEXP_CONCAT:
+        case kind::REGEXP_UNION: 
+        case kind::REGEXP_INTER: {
+          bool flag = false;
+          std::vector< Node > vec_nodes;
+          for(unsigned i=0; i<r.getNumChildren(); ++i) {
+            Node rtmp = normalizeRegexp(r[i]);
+            vec_nodes.push_back(rtmp);
+            if(rtmp != r[i]) {
+              flag = true;
+            }
+          }
+          if(flag) {
+            Node rtmp = vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode(r.getKind(), vec_nodes);
+            nf_r = Rewriter::rewrite( rtmp );
+          }
+        }
+        case kind::REGEXP_STAR: {
+          Node rtmp = normalizeRegexp(r[0]);
+          if(rtmp != r[0]) {
+            rtmp = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, rtmp);
+            nf_r = Rewriter::rewrite( rtmp );
+          }
+        }
+        default: {
+          Unreachable();
+        }
+      }
+    }
+    d_nf_regexps[r] = nf_r;
+    d_nf_regexps_exp[r] = nf_exp;
+  }
+  return nf_r;
+}
+
+bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps) {
+  std::map< Node, std::vector< Node > > unprocessed_x_exps;
+  std::map< Node, std::vector< Node > > unprocessed_memberships;
+  std::map< Node, std::vector< Node > > unprocessed_memberships_bases;
+  bool addLemma = false;
+
+  Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl;
+
+  for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin();
+    itr_xr != d_pos_memberships.end(); ++itr_xr ) {
+    Node x = (*itr_xr).first;
+    NodeList* lst = (*itr_xr).second;
+    Node nf_x = x;
+    std::vector< Node > nf_x_exp;
+    if(d_normal_forms.find( x ) != d_normal_forms.end()) {
+      //nf_x = mkConcat( d_normal_forms[x] );
+      nf_x_exp.insert(nf_x_exp.end(), d_normal_forms_exp[x].begin(), d_normal_forms_exp[x].end());
+      //Debug("regexp-nf") << "Term: " << x << " has a normal form " << ret << std::endl;
+    } else {
+      Assert(false);
+    }
+    Trace("regexp-nf") << "Checking Memberships for N(" << x << ") = " << nf_x << " :" << std::endl;
+
+    std::vector< Node > vec_x;
+    std::vector< Node > vec_r;
+    for(NodeList::const_iterator itr_lst = lst->begin();
+        itr_lst != lst->end(); ++itr_lst) {
+      Node r = *itr_lst;
+      Node nf_r = normalizeRegexp((*lst)[0]);
+      Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, nf_r);
+      if(d_processed_memberships.find(memb) == d_processed_memberships.end()) {
+        if(d_regexp_opr.checkConstRegExp(nf_r)) {
+          vec_x.push_back(x);
+          vec_r.push_back(r);
+        } else {
+          Trace("regexp-nf") << "Handling Symbolic Regexp for N(" << r << ") = " << nf_r << std::endl;
+          //TODO: handle symbolic ones
+          addLemma = true;
+        }
+        d_processed_memberships.insert(memb);
+      }
+    }
+    if(!vec_x.empty()) {
+      if(unprocessed_x_exps.find(nf_x) == unprocessed_x_exps.end()) {
+        unprocessed_x_exps[nf_x] = nf_x_exp;
+        unprocessed_memberships[nf_x] = vec_r;
+        unprocessed_memberships_bases[nf_x] = vec_x;
+      } else {
+        unprocessed_x_exps[nf_x].insert(unprocessed_x_exps[nf_x].end(), nf_x_exp.begin(), nf_x_exp.end());
+        unprocessed_memberships[nf_x].insert(unprocessed_memberships[nf_x].end(), vec_r.begin(), vec_r.end());
+        unprocessed_memberships_bases[nf_x].insert(unprocessed_memberships_bases[nf_x].end(), vec_x.begin(), vec_x.end());
+      }
+    }
+  }
+  //Intersection
+  for(std::map< Node, std::vector< Node > >::const_iterator itr = unprocessed_memberships.begin();
+      itr != unprocessed_memberships.end(); ++itr) {
+    Node nf_x = itr->first;
+    std::vector< Node > exp( unprocessed_x_exps[nf_x] );
+    Node r = itr->second[0];
+    //get nf_r
+    Node inter_r = d_nf_regexps[r];
+    exp.insert(exp.end(), d_nf_regexps_exp[r].begin(), d_nf_regexps_exp[r].end());
+    Node x = unprocessed_memberships_bases[itr->first][0];
+    Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r);
+    exp.push_back(memb);
+    for(std::size_t i=1; i < itr->second.size(); i++) {
+      //exps
+      Node r2 = itr->second[i];
+      Node inter_r2 = d_nf_regexps[r2];
+      exp.insert(exp.end(), d_nf_regexps_exp[r2].begin(), d_nf_regexps_exp[r2].end());
+      Node x2 = unprocessed_memberships_bases[itr->first][i];
+      memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x2, r2);
+      exp.push_back(memb);
+      //intersection
+      bool spflag = false;
+      inter_r = d_regexp_opr.intersect(inter_r, inter_r2, spflag);
+      if(inter_r == d_emptyRegexp) {
+        //conflict
+        Node antec = exp.size() == 1? exp[0] : NodeManager::currentNM()->mkNode(kind::AND, exp);
+        Node conc;
+        sendLemma(antec, conc, "INTERSEC CONFLICT");
+        addLemma = true;
+        break;
+      }
+    }
+    //infer
+    if(!d_conflict) {
+      memb = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, inter_r) );
+      memb_with_exps[memb] = exp;
+    } else {
+      break;
+    }
+  }
+
+  return addLemma;
+}
+
+bool TheoryStrings::applyRConsume( CVC4::String &s, Node &r) {
+  Trace("regexp-derivative") << "TheoryStrings::derivative: s=" << s << ", r= " << r << std::endl;
+  Assert( d_regexp_opr.checkConstRegExp(r) );
+
+  if( !s.isEmptyString() ) {
+    Node dc = r;
+
+    for(unsigned i=0; i<s.size(); ++i) {
+      CVC4::String c = s.substr(i, 1);
+      Node dc2;
+      int rt = d_regexp_opr.derivativeS(dc, c, dc2);
+      dc = dc2;
+      if(rt == 0) {
+        Unreachable();
+      } else if(rt == 2) {
+        return false;
+      }
+    }
+    r = dc;
+  }
+
+  return true;
+}
+
+Node TheoryStrings::applyRSplit(Node s1, Node s2, Node r) {
+  Assert(d_regexp_opr.checkConstRegExp(r));
+
+  std::vector< std::pair< Node, Node > > vec_can;
+  d_regexp_opr.splitRegExp(r, vec_can);
+  //TODO: lazy cache or eager?
+  std::vector< Node > vec_or;
+
+  for(unsigned int i=0; i<vec_can.size(); i++) {
+    Node m1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, vec_can[i].first);
+    Node m2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, vec_can[i].second);
+    Node c = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, m1, m2) );
+    vec_or.push_back( c );
+  }
+  Node conc = vec_or.size()==0? Node::null() : vec_or.size()==1 ? vec_or[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::OR, vec_or) );
+  return conc;
+}
+
+bool TheoryStrings::applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps) {
+  if(XinR_with_exps.size() > 0) {
+    //TODO: get vector, var, store.
+    return true;
+  } else  {
+    return false;
+  }
+}
+
+bool TheoryStrings::checkMembershipsWithoutLength(
+  std::map< Node, std::vector< Node > > &memb_with_exps,
+  std::map< Node, std::vector< Node > > &XinR_with_exps) {
+  for(std::map< Node, std::vector< Node > >::const_iterator itr = memb_with_exps.begin();
+      itr != memb_with_exps.end(); ++itr) {
+    Node memb = itr->first;
+    Node s = memb[0];
+    Node r = memb[1];
+    if(s.isConst()) {
+      memb = Rewriter::rewrite( memb );
+      if(memb == d_false) {
+        Node antec = itr->second.size() == 1? itr->second[0] : NodeManager::currentNM()->mkNode(kind::AND, itr->second);
+        Node conc;
+        sendLemma(antec, conc, "MEMBERSHIP CONFLICT");
+        //addLemma = true;
+        return true;
+      } else {
+        Assert(memb == d_true);
+      }
+    } else if(s.getKind() == kind::VARIABLE) {
+      //add to XinR
+      XinR_with_exps[itr->first] = itr->second;
+    } else {
+      Assert(s.getKind() == kind::STRING_CONCAT);
+      Node antec = itr->second.size() == 1? itr->second[0] : NodeManager::currentNM()->mkNode(kind::AND, itr->second);
+      Node conc;
+      for( unsigned i=0; i<s.getNumChildren(); i++ ) {
+        if(s[i].isConst()) {
+          CVC4::String str( s[0].getConst< String >() );
+          //R-Consume, see Tianyi's thesis
+          if(!applyRConsume(str, r)) {
+            sendLemma(antec, conc, "R-Consume CONFLICT");
+            //addLemma = true;
+            return true;
+          }
+        } else {
+          //R-Split, see Tianyi's thesis
+          if(i == s.getNumChildren() - 1) {
+            //add to XinR
+            Node memb2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s[i], r);
+            XinR_with_exps[itr->first] = itr->second;
+          } else {
+            Node s1 = s[i];
+            std::vector< Node > vec_s2;
+            for( unsigned j=i+1; j<s.getNumChildren(); j++ ) {
+              vec_s2.push_back(s[j]);
+            }
+            Node s2 = mkConcat(vec_s2);
+            conc = applyRSplit(s1, s2, r);
+            if(conc == d_true) {
+              break;
+            } else if(conc.isNull() || conc == d_false) {
+              conc = Node::null();
+              sendLemma(antec, conc, "R-Split Conflict");
+              //addLemma = true;
+              return true;
+            } else {
+              sendLemma(antec, conc, "R-Split");
+              //addLemma = true;
+              return true;
+            }
+          }
+        }
+      }
+    }
+  }
+  return false;
+}
+
+bool TheoryStrings::checkMemberships2() {
+  bool addedLemma = false;
+  d_nf_regexps.clear();
+  d_nf_regexps_exp.clear();
+  std::map< Node, std::vector< Node > > memb_with_exps;
+  std::map< Node, std::vector< Node > > XinR_with_exps;
+
+  addedLemma = normalizePosMemberships( memb_with_exps );
+  if(!d_conflict) {
+    // main procedure
+    addedLemma |= checkMembershipsWithoutLength( memb_with_exps, XinR_with_exps );
+    //TODO: check addlemma
+    if (!addedLemma && !d_conflict) {
+      for(std::map< Node, std::vector< Node > >::const_iterator itr = XinR_with_exps.begin();
+          itr != XinR_with_exps.end(); ++itr) {
+        std::vector<Node> vec_or;
+        d_regexp_opr.disjunctRegExp( itr->first, vec_or );
+        Node tmp = NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_or);
+        Trace("regexp-process") << "Got r: " << itr->first << " to " << tmp << std::endl;
+        /*
+        if(r.getKind() == kind::REGEXP_STAR) {
+          //TODO: apply R-Len
+          addedLemma = applyRLen(XinR_with_exps);
+        } else {
+          //TODO: split
+        }
+        */
+      }
+      Assert(false); //TODO:tmp
+    }
+  }
+
+  return addedLemma;
+}
+
 bool TheoryStrings::checkMemberships() {
   bool addedLemma = false;
   bool changed = false;
@@ -2523,8 +2836,8 @@ bool TheoryStrings::checkMemberships() {
   Trace("regexp-debug") << "Checking Memberships ... " << std::endl;
   //if(options::stringEIT()) {
     //TODO: Opt for normal forms
-    for(NodeListMap::const_iterator itr_xr = d_str_re_map.begin();
-      itr_xr != d_str_re_map.end(); ++itr_xr ) {
+    for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin();
+      itr_xr != d_pos_memberships.end(); ++itr_xr ) {
       bool spflag = false;
       Node x = (*itr_xr).first;
       NodeList* lst = (*itr_xr).second;
@@ -3132,11 +3445,11 @@ void TheoryStrings::addMembership(Node assertion) {
   Node r = atom[1];
   if(polarity) {
     NodeList* lst;
-    NodeListMap::iterator itr_xr = d_str_re_map.find( x );
-    if( itr_xr == d_str_re_map.end() ){
+    NodeListMap::iterator itr_xr = d_pos_memberships.find( x );
+    if( itr_xr == d_pos_memberships.end() ){
       lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
                                 ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
-      d_str_re_map.insertDataFromContextMemory( x, lst );
+      d_pos_memberships.insertDataFromContextMemory( x, lst );
     } else {
       lst = (*itr_xr).second;
     }
@@ -3147,16 +3460,29 @@ void TheoryStrings::addMembership(Node assertion) {
       }
     }
     lst->push_back( r );
-  }/* else {
-    if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) {
+  } else {
+    /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) {
       int rt;
       Node r2 = d_regexp_opr.complement(r, rt);
       Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2);
-      d_regexp_memberships.push_back( a );
+    }*/
+    NodeList* lst;
+    NodeListMap::iterator itr_xr = d_neg_memberships.find( x );
+    if( itr_xr == d_neg_memberships.end() ){
+      lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
+                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
+      d_neg_memberships.insertDataFromContextMemory( x, lst );
     } else {
-      d_regexp_memberships.push_back( assertion );
+      lst = (*itr_xr).second;
     }
-  }*/
+    //check
+    for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) {
+      if( r == *itr ) {
+        return;
+      }
+    }
+    lst->push_back( r );
+  }
   d_regexp_memberships.push_back( assertion );
 }
 
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index d9326c316..623647942 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -245,7 +245,18 @@ private:
   bool checkLengthsEqc();
   bool checkCardinality();
   bool checkInductiveEquations();
+  //check membership constraints
+  Node normalizeRegexp(Node r);
+  bool normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps);
+  bool applyRConsume( CVC4::String &s, Node &r);
+  Node applyRSplit(Node s1, Node s2, Node r);
+  bool applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps);
+  bool checkMembershipsWithoutLength(
+    std::map< Node, std::vector< Node > > &memb_with_exps,
+    std::map< Node, std::vector< Node > > &XinR_with_exps);
   bool 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);
@@ -325,10 +336,17 @@ private:
   NodeList d_regexp_memberships;
   NodeSet d_regexp_ucached;
   NodeSet d_regexp_ccached;
+  // stored assertions
+  NodeListMap d_pos_memberships;
+  NodeListMap d_neg_memberships;
+  // semi normal forms for symbolic expression
+  std::map< Node, Node > d_nf_regexps;
+  std::map< Node, std::vector< Node > > d_nf_regexps_exp;
   // intersection
-  NodeListMap d_str_re_map;
   NodeNodeMap d_inter_cache;
   NodeIntMap d_inter_index;
+  // processed memberships
+  NodeSet d_processed_memberships;
   // antecedant for why regexp membership must be true
   NodeNodeMap d_regexp_ant;
   // membership length
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index c952a7b3c..dfec0a795 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -100,7 +100,7 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
         if(!preNode.isNull()) {
           if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) {
             preNode = rewriteConcatString(
-            NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) );
+              NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) );
             node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
             preNode = Node::null();
           } else {
@@ -143,7 +143,10 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) {
     retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
   } else {
     if(!preNode.isNull()) {
-      node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+      bool bflag = (preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() );
+      if(node_vec.empty() || !bflag ) {
+        node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
+      }
     }
     if(node_vec.size() > 1) {
       retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, node_vec);
@@ -160,25 +163,42 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
   Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl;
   Node retNode = node;
   std::vector<Node> node_vec;
-  bool flag = false;
+  bool allflag = false;
   for(unsigned i=0; i<node.getNumChildren(); ++i) {
     if(node[i].getKind() == kind::REGEXP_UNION) {
       Node tmpNode = prerewriteOrRegExp( node[i] );
       if(tmpNode.getKind() == kind::REGEXP_UNION) {
         for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) {
-          node_vec.push_back( tmpNode[j] );
+          if(std::find(node_vec.begin(), node_vec.end(), tmpNode[j]) == node_vec.end()) {
+            if(std::find(node_vec.begin(), node_vec.end(), tmpNode[j]) == node_vec.end()) {
+              node_vec.push_back( tmpNode[j] );
+            }
+          }
         }
+      } else if(tmpNode.getKind() == kind::REGEXP_EMPTY) {
+        //nothing
+      } else if(tmpNode.getKind() == kind::REGEXP_STAR && tmpNode[0].getKind() == kind::REGEXP_SIGMA) {
+        allflag = true;
+        retNode = tmpNode;
+        break;
       } else {
-        node_vec.push_back( tmpNode );
+        if(std::find(node_vec.begin(), node_vec.end(), tmpNode) == node_vec.end()) {
+          node_vec.push_back( tmpNode );
+        }
       }
-      flag = true;
     } else if(node[i].getKind() == kind::REGEXP_EMPTY) {
-      flag = true;
+      //nothing
+    } else if(node[i].getKind() == kind::REGEXP_STAR && node[i][0].getKind() == kind::REGEXP_SIGMA) {
+      allflag = true;
+      retNode = node[i];
+      break;
     } else {
-      node_vec.push_back( node[i] );
+      if(std::find(node_vec.begin(), node_vec.end(), node[i]) == node_vec.end()) {
+        node_vec.push_back( node[i] );
+      }
     }
   }
-  if(flag) {
+  if(!allflag) {
     std::vector< Node > nvec;
     retNode = node_vec.size() == 0 ? NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ) :
           node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec);
@@ -187,6 +207,55 @@ Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
   return retNode;
 }
 
+Node TheoryStringsRewriter::prerewriteAndRegExp(TNode node) {
+  Assert( node.getKind() == kind::REGEXP_INTER );
+  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) {
+      Node tmpNode = prerewriteAndRegExp( node[i] );
+      if(tmpNode.getKind() == kind::REGEXP_INTER) {
+        for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) {
+          if(std::find(node_vec.begin(), node_vec.end(), tmpNode[j]) == node_vec.end()) {
+            node_vec.push_back( tmpNode[j] );
+          }
+        }
+      } 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) {
+        //allNode = tmpNode;
+      } else {
+        if(std::find(node_vec.begin(), node_vec.end(), tmpNode) == node_vec.end()) {
+          node_vec.push_back( tmpNode );
+        }
+      }
+    } 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) {
+      //allNode = node[i];
+    } else {
+      if(std::find(node_vec.begin(), node_vec.end(), node[i]) == node_vec.end()) {
+        node_vec.push_back( node[i] );
+      }
+    }
+  }
+  if(!emptyflag) {
+    std::vector< Node > nvec;
+    retNode = node_vec.size() == 0 ? 
+          NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, nvec)) :
+          node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_INTER, node_vec);
+  }
+  Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl;
+  return retNode;
+}
+
 bool TheoryStringsRewriter::checkConstRegExp( TNode t ) {
   if( t.getKind() != kind::STRING_TO_REGEXP ) {
     for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
@@ -603,6 +672,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
   return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
 
+bool TheoryStringsRewriter::hasEpsilonNode(TNode node) {
+  for(unsigned int i=0; i<node.getNumChildren(); i++) {
+    if(node[i].getKind() == kind::STRING_TO_REGEXP && node[i][0].getKind() == kind::CONST_STRING && node[i][0].getConst<String>().isEmptyString()) {
+      return true;
+    }
+  }
+  return false;
+}
+
 RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
   Node retNode = node;
   Node orig = retNode;
@@ -614,9 +692,36 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
     retNode = prerewriteConcatRegExp(node);
   } else if(node.getKind() == kind::REGEXP_UNION) {
     retNode = prerewriteOrRegExp(node);
+  }else if(node.getKind() == kind::REGEXP_INTER) {
+    retNode = prerewriteAndRegExp(node);
   } else if(node.getKind() == kind::REGEXP_STAR) {
     if(node[0].getKind() == kind::REGEXP_STAR) {
       retNode = node[0];
+    } else if(node[0].getKind() == kind::STRING_TO_REGEXP && node[0][0].getKind() == kind::CONST_STRING && node[0][0].getConst<String>().isEmptyString()) {
+      retNode = node[0];
+    } else if(node[0].getKind() == kind::REGEXP_EMPTY) {
+      retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP,
+        NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
+    } else if(node[0].getKind() == kind::REGEXP_UNION) {
+      Node tmpNode = prerewriteOrRegExp(node[0]);
+      if(tmpNode.getKind() == kind::REGEXP_UNION) {
+        if(hasEpsilonNode(node[0])) {
+          std::vector< Node > node_vec;
+          for(unsigned int i=0; i<node[0].getNumChildren(); i++) {
+            if(node[0][i].getKind() == kind::STRING_TO_REGEXP && node[0][i][0].getKind() == kind::CONST_STRING && node[0][i][0].getConst<String>().isEmptyString()) {
+              //return true;
+            } else {
+              node_vec.push_back(node[0][i]);
+            }
+          }
+          retNode = node_vec.size()==1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec);
+          retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, retNode);
+        }
+      } else if(tmpNode.getKind() == kind::STRING_TO_REGEXP && tmpNode[0].getKind() == kind::CONST_STRING && tmpNode[0].getConst<String>().isEmptyString()) {
+        retNode = tmpNode;
+      } else {
+        retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, tmpNode);
+      }
     }
   } else if(node.getKind() == kind::REGEXP_PLUS) {
     retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0],
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 9d04f107f..a1098f631 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -37,10 +37,12 @@ public:
   static Node rewriteConcatString(TNode node);
   static Node prerewriteConcatRegExp(TNode node);
   static Node prerewriteOrRegExp(TNode node);
+  static Node prerewriteAndRegExp(TNode node);
   static Node rewriteMembership(TNode node);
 
   static RewriteResponse postRewrite(TNode node);
 
+  static bool hasEpsilonNode(TNode node);
   static RewriteResponse preRewrite(TNode node);
 
   static inline void init() {}