Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.

18 files changed, 225 insertions, 208 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 5192da7de..97116dee4 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -787,7 +787,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
       Trace("ambqi-model-debug") << "Initial terms: " << std::endl;
       for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
         Node n = fm->d_uf_terms[f][i];
-        if( !n.getAttribute(NoMatchAttribute()) ){
+        if( d_qe->getTermDatabase()->isTermActive( n ) ){
           Trace("ambqi-model-debug") << "  " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
           fapps.push_back( n );
         }
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 43f5ee2fd..a0d9bda0f 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -28,7 +28,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
 bool CandidateGenerator::isLegalCandidate( Node n ){
-  return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) ) );
+  return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) );
 }
 
 void CandidateGeneratorQueue::addCandidate( Node n ) {
@@ -59,7 +59,7 @@ Node CandidateGeneratorQueue::getNextCandidate(){
 }
 
 CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) :
-  d_qe( qe ), d_term_iter( -1 ){
+CandidateGenerator( qe ), d_term_iter( -1 ){
   d_op = qe->getTermDatabase()->getMatchOperator( pat );
   Assert( !d_op.isNull() );
   d_op_arity = pat.getNumChildren();
@@ -186,7 +186,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
 }
 
 CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
-  d_match_pattern( mpat ), d_qe( qe ){
+  CandidateGenerator( qe ), d_match_pattern( mpat ){
   Assert( mpat.getKind()==EQUAL );
   for( unsigned i=0; i<2; i++ ){
     if( !quantifiers::TermDb::hasInstConstAttr(mpat[i]) ){
@@ -225,7 +225,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){
 
 
 CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
-  d_match_pattern( mpat ), d_qe( qe ){
+CandidateGenerator( qe ), d_match_pattern( mpat ){
 
   Assert( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF );
   d_match_pattern_type = d_match_pattern[0].getType();
@@ -259,7 +259,7 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){
 
 
 CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) :
-  d_match_pattern( mpat ), d_qe( qe ){
+  CandidateGenerator( qe ), d_match_pattern( mpat ){
   d_match_pattern_type = mpat.getType();
   Assert( mpat.getKind()==INST_CONSTANT );
   d_f = quantifiers::TermDb::getInstConstAttr( mpat );
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 18ef6a086..4fc6969fc 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -33,8 +33,10 @@ namespace inst {
 
 /** base class for generating candidates for matching */
 class CandidateGenerator {
+protected:
+  QuantifiersEngine* d_qe;
 public:
-  CandidateGenerator(){}
+  CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){}
   virtual ~CandidateGenerator(){}
 
   /** Get candidates functions.  These set up a context to get all match candidates.
@@ -54,7 +56,7 @@ public:
   virtual void resetInstantiationRound() = 0;
 public:
   /** legal candidate */
-  static bool isLegalCandidate( Node n );
+  bool isLegalCandidate( Node n );
 };/* class CandidateGenerator */
 
 /** candidate generator queue (for manual candidate generation) */
@@ -63,7 +65,7 @@ private:
   std::vector< Node > d_candidates;
   int d_candidate_index;
 public:
-  CandidateGeneratorQueue() : d_candidate_index( 0 ){}
+  CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){}
   ~CandidateGeneratorQueue() throw() {}
 
   void addCandidate( Node n );
@@ -80,8 +82,6 @@ class CandidateGeneratorQE : public CandidateGenerator
 private:
   //operator you are looking for
   Node d_op;
-  //instantiator pointer
-  QuantifiersEngine* d_qe;
   //the equality class iterator
   unsigned d_op_arity;
   std::vector< quantifiers::TermArgTrie* > d_tindex;
@@ -122,8 +122,6 @@ private:
   Node d_match_pattern;
   Node d_match_gterm;
   bool d_do_mgt;
-  //einstantiator pointer
-  QuantifiersEngine* d_qe;
 public:
   CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
   ~CandidateGeneratorQELitEq() throw() {}
@@ -142,8 +140,6 @@ private:
   Node d_match_pattern;
   //type of disequality
   TypeNode d_match_pattern_type;
-  //einstantiator pointer
-  QuantifiersEngine* d_qe;
 public:
   CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
   ~CandidateGeneratorQELitDeq() throw() {}
@@ -161,8 +157,6 @@ private:
   //equality you are trying to match equalities for
   Node d_match_pattern;
   TypeNode d_match_pattern_type;
-  //einstantiator pointer
-  QuantifiersEngine* d_qe;
   // quantifier/index for the variable we are matching
   Node d_f;
   unsigned d_index;
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 2cc49ef5a..fa71f0132 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -285,7 +285,7 @@ Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
 }
 
 bool ConjectureGenerator::isHandledTerm( TNode n ){
-  return !n.getAttribute(NoMatchAttribute()) && inst::Trigger::isAtomicTrigger( n ) && ( n.getKind()!=APPLY_UF || n.getOperator().getKind()!=SKOLEM );
+  return d_quantEngine->getTermDatabase()->isTermActive( n ) && inst::Trigger::isAtomicTrigger( n ) && ( n.getKind()!=APPLY_UF || n.getOperator().getKind()!=SKOLEM );
 }
 
 Node ConjectureGenerator::getGroundEqc( TNode r ) {
@@ -425,7 +425,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
           while( !eqc_i.isFinished() ){
             TNode n = (*eqc_i);
-            if( getTermDatabase()->hasTermCurrent( n ) && !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){
+            if( getTermDatabase()->hasTermCurrent( n ) && getTermDatabase()->isTermActive( n ) && ( n.getKind()!=EQUAL || isFalse ) ){
               if( firstTime ){
                 Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;
                 firstTime = false;
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 33c853328..8835d00bc 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -405,7 +405,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       bool needsDefault = true;
       for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
         Node n = fm->d_uf_terms[op][i];
-        if( !n.getAttribute(NoMatchAttribute()) ){
+        if( d_qe->getTermDatabase()->isTermActive( n ) ){
           add_conds.push_back( n );
           add_values.push_back( n );
           Node r = fm->getUsedRepresentative(n);
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index bf05de3bb..bd5100a2e 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -150,7 +150,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
         d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
       }
     }else{
-      d_cg = new CandidateGeneratorQueue;
+      d_cg = new CandidateGeneratorQueue( qe );
       Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
       d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
     }
@@ -697,7 +697,7 @@ int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){
   return addedLemmas;
 }
 
-InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) {
+InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ) : d_f( q ), d_match_pattern( pat ) {
   if( d_match_pattern.getKind()==NOT ){
     d_match_pattern = d_match_pattern[0];
     d_pol = false;
@@ -720,10 +720,11 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q
     }
     d_match_pattern_arg_types.push_back( d_match_pattern[i].getType() );
   }
+  d_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
 }
 
 void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) {
-  d_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
+  
 }
 
 int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
@@ -751,6 +752,7 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q
       tat = NULL;
     }
   }
+  Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
   if( tat ){
     InstMatch m( q );
     m.add( baseMatch );
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index a1d907001..49e3c1ec5 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -224,7 +224,7 @@ private:
   void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
 public:
   /** constructors */
-  InstMatchGeneratorSimple( Node q, Node pat );
+  InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe );
   /** destructor */
   ~InstMatchGeneratorSimple() throw() {}
   /** reset instantiation round (call this whenever equivalence classes have changed) */
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 630880690..d58bbcf3a 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -83,9 +83,8 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
 
       Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl;
       if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT  ){
-        int matchOption = 0;
         for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){
-          Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], matchOption, true, Trigger::TR_RETURN_NULL );
+          Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], true, Trigger::TR_RETURN_NULL );
           if( t ){
             d_user_gen[f].push_back( t );
           }
@@ -134,11 +133,10 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
   if( usable ){
     Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
     //check match option
-    int matchOption = 0;
     if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
       d_user_gen_wait[q].push_back( nodes );
     }else{
-      Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW );
+      Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW );
       if( t ){
         d_user_gen[q].push_back( t );
       }else{
@@ -306,6 +304,23 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         last_weight = curr_w;
       }
     }
+    d_num_trigger_vars[f] = vcMap.size();
+    if( d_num_trigger_vars[f]>0 && d_num_trigger_vars[f]<f[0].getNumChildren() ){
+      Trace("auto-gen-trigger-partial") << "Quantified formula : " << f << std::endl;
+      Trace("auto-gen-trigger-partial") << "...does not contain all variables in triggers!!!" << std::endl;
+      if( options::partialTriggers() ){
+        std::vector< Node > vcs[2];
+        for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+          Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+          vcs[ vcMap.find( ic )==vcMap.end() ? 0 : 1 ].push_back( f[0][i] );
+        }
+        for( unsigned i=0; i<2; i++ ){
+          d_vc_partition[i][f] = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, vcs[i] );
+        }
+      }else{
+        return;
+      }
+    }
     for( unsigned i=0; i<patTermsF.size(); i++ ){
       Node pat = patTermsF[i];
       if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){
@@ -381,10 +396,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         }
       }
       //now, generate the trigger...
-      int matchOption = 0;
       Trigger* tr = NULL;
       if( d_is_single_trigger[ patTerms[0] ] ){
-        tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL );
+        tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] );
         d_single_trigger_gen[ patTerms[0] ] = true;
       }else{
         //only generate multi trigger if option set, or if no single triggers exist
@@ -402,29 +416,14 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
           d_made_multi_trigger[f] = true;
         }
         //will possibly want to get an old trigger
-        tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD );
+        tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, false, Trigger::TR_GET_OLD, d_num_trigger_vars[f] );
       }
       if( tr ){
-        unsigned tindex;
-        if( tr->isMultiTrigger() ){
-          //disable all other multi triggers
-          for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][f].begin(); it != d_auto_gen_trigger[1][f].end(); ++it ){
-            d_auto_gen_trigger[1][f][ it->first ] = false;
-          }
-          tindex = 1;
-        }else{
-          tindex = 0;
-        }
-        //making it during an instantiation round, so must reset
-        if( d_auto_gen_trigger[tindex][f].find( tr )==d_auto_gen_trigger[tindex][f].end() ){
-          tr->resetInstantiationRound();
-          tr->reset( Node::null() );
-        }
-        d_auto_gen_trigger[tindex][f][tr] = true;
+        addTrigger( tr, f );
         //if we are generating additional triggers...
-        if( tindex==0 ){
-          int index = 0;
-          if( index<(int)patTerms.size() ){
+        if( !tr->isMultiTrigger() ){
+          unsigned index = 0;
+          if( index<patTerms.size() ){
             //Notice() << "check add additional" << std::endl;
             //check if similar patterns exist, and if so, add them additionally
             int nqfs_curr = 0;
@@ -433,18 +432,13 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
             }
             index++;
             bool success = true;
-            while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
+            while( success && index<patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
               success = false;
               if( !options::relevantTriggers() ||
                   d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
                 d_single_trigger_gen[ patTerms[index] ] = true;
-                Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL );
-                if( tr2 ){
-                  //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
-                  tr2->resetInstantiationRound();
-                  tr2->reset( Node::null() );
-                  d_auto_gen_trigger[0][f][tr2] = true;
-                }
+                Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] );
+                addTrigger( tr2, f );
                 success = true;
               }
               index++;
@@ -458,7 +452,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
 }
 
 void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv ) {
-  if( num_fv==q[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
+  unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren();
+  if( num_fv==num_vars && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
     d_patTerms[0][q].push_back( pat );
     d_is_single_trigger[ pat ] = true;
   }else{
@@ -467,6 +462,38 @@ void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned n
   }
 }
 
+
+void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
+  if( tr ){
+    if( d_num_trigger_vars[q]<q[0].getNumChildren() ){
+      //partial trigger : generate implication to mark user pattern
+      Node ipl = NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, d_quantEngine->getTermDatabase()->getVariableNode( tr->getInstPattern(), q ) );
+      Node qq = NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[1][q], NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[0][q], q[1] ), ipl );
+      Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl;
+      Trace("auto-gen-trigger-partial") << "  " << qq << std::endl;
+      Node lem = NodeManager::currentNM()->mkNode( OR, q.negate(), qq );
+      d_quantEngine->addLemma( lem );
+    }else{
+      unsigned tindex;
+      if( tr->isMultiTrigger() ){
+        //disable all other multi triggers
+        for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][q].begin(); it != d_auto_gen_trigger[1][q].end(); ++it ){
+          d_auto_gen_trigger[1][q][ it->first ] = false;
+        }
+        tindex = 1;
+      }else{
+        tindex = 0;
+      }
+      //making it during an instantiation round, so must reset
+      if( d_auto_gen_trigger[tindex][q].find( tr )==d_auto_gen_trigger[tindex][q].end() ){
+        tr->resetInstantiationRound();
+        tr->reset( Node::null() );
+      }
+      d_auto_gen_trigger[tindex][q][tr] = true;
+    }
+  }
+}
+
 bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
   if( q.getNumChildren()==3 ){
     std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q );
@@ -519,8 +546,7 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
         Trace("local-t-ext") << "  " << patTerms[i] << std::endl;
       }
       Trace("local-t-ext") << std::endl;
-      int matchOption = 0;
-      Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD );
+      Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, true, Trigger::TR_GET_OLD );
       d_lte_trigger[f] = tr;
     }else{
       Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 028f24b27..97d97b10a 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -83,6 +83,9 @@ private:
   std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger;
   //instantiation no patterns
   std::map< Node, std::vector< Node > > d_user_no_gen;
+  // number of trigger variables per quantifier
+  std::map< Node, unsigned > d_num_trigger_vars;
+  std::map< Node, Node > d_vc_partition[2];
 private:
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
@@ -90,7 +93,7 @@ private:
   /** generate triggers */
   void generateTriggers( Node q );
   void addPatternToPool( Node q, Node pat, unsigned num_fv );
-  //bool addTrigger( inst::Trigger * tr, Node f, unsigned r );
+  void addTrigger( inst::Trigger * tr, Node f );
   /** has user patterns */
   bool hasUserPatterns( Node q );
   /** has user patterns */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 3ae36b1d4..42fd7c354 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -114,7 +114,7 @@ bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
 
 
 QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) :
-QModelBuilder( c, qe ) {
+QModelBuilder( c, qe ), d_basisNoMatch( c ) {
 
 }
 
@@ -302,7 +302,7 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
     for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
       Node n = fmig->d_uf_terms[op][i];
       //for calculating if op is constant
-      if( !n.getAttribute(NoMatchAttribute()) ){
+      if( d_qe->getTermDatabase()->isTermActive( n ) ){
         Node v = fmig->getRepresentative( n );
         if( i==0 ){
           d_uf_prefs[op].d_const_val = v;
@@ -312,12 +312,11 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
         }
       }
       //for calculating terms that we don't need to consider
-      if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
-        if( !n.getAttribute(BasisNoMatchAttribute()) ){
+      if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
+        if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
           //need to consider if it is not congruent modulo model basis
           if( !tabt.addTerm( fmig, n ) ){
-             BasisNoMatchAttribute bnma;
-             n.setAttribute(bnma,true);
+            d_basisNoMatch[n] = true;
           }
         }
       }
@@ -382,8 +381,8 @@ bool QModelBuilderIG::isQuantifierActive( Node f ){
 }
 
 bool QModelBuilderIG::isTermActive( Node n ){
-  return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term
-         ( n.getAttribute(ModelBasisArgAttribute())!=0 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
+  return d_qe->getTermDatabase()->isTermActive( n ) || //it is not congruent to another active term
+         ( n.getAttribute(ModelBasisArgAttribute())!=0 && d_basisNoMatch.find( n )==d_basisNoMatch.end() ); //or it has model basis arguments
                                                                                                       //and is not congruent modulo model basis
                                                                                                       //to another active term
 }
@@ -667,7 +666,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
       //if applicable, try to add exceptions here
       if( !tr_terms.empty() ){
         //make a trigger for these terms, add instantiations
-        inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, 0, true, inst::Trigger::TR_MAKE_NEW );
+        inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, true, inst::Trigger::TR_MAKE_NEW );
         //Notice() << "Trigger = " << (*tr) << std::endl;
         tr->resetInstantiationRound();
         tr->reset( Node::null() );
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 906673903..e4f9529a8 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -57,15 +57,6 @@ public:
 
 
 
-/** Attribute true for nodes that should not be used when considered for inst-gen basis */
-struct BasisNoMatchAttributeId {};
-/** use the special for boolean flag */
-typedef expr::Attribute< BasisNoMatchAttributeId,
-                         bool,
-                         expr::attr::NullCleanupStrategy,
-                         true // context dependent
-                       > BasisNoMatchAttribute;
-
 class TermArgBasisTrie {
 private:
   bool addTerm2( FirstOrderModel* fm, Node n, int argIndex );
@@ -85,7 +76,9 @@ public:
   */
 class QModelBuilderIG : public QModelBuilder
 {
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
 protected:
+  BoolMap d_basisNoMatch;
   //map from operators to model preference data
   std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
   //built model uf
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 5aae4d640..2f7864831 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -185,19 +185,11 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
   if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
     Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << std::endl;
     std::vector< Node > args;
-    for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
-      args.push_back( in[0][i] );
-    }
-    Node body = in[1];
+    Node body = in;
     bool doRewrite = false;
-    std::vector< Node > ipl;
-    while( body.getNumChildren()>=2 && body.getKind()==in.getKind() ){
-      if( body.getNumChildren()==3 ){
-        for( unsigned i=0; i<body[2].getNumChildren(); i++ ){
-          ipl.push_back( body[2][i] );
-        }
-      }
-      for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
+    bool firstTime = true;
+    while( body.getNumChildren()==2 && body.getKind()==body[1].getKind() ){
+      for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
         args.push_back( body[0][i] );
       }
       body = body[1];
@@ -207,14 +199,6 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
       std::vector< Node > children;
       children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) );
       children.push_back( body );
-      if( in.getNumChildren()==3 ){
-        for( unsigned i=0; i<in[2].getNumChildren(); i++ ){
-          ipl.push_back( in[2][i] );
-        }
-      }
-      if( !ipl.empty() ){
-        children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, ipl ) );
-      }
       Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
       if( in!=n ){
         Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index b353fce2f..b4b51fd84 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -110,7 +110,7 @@ void RelevantDomain::compute(){
       for( unsigned i=0; i<sz; i++ ){
         Node n = it->second[i];
         //if it is a non-redundant term
-        if( !n.getAttribute(NoMatchAttribute()) ){
+        if( db->isTermActive( n ) ){
           for( unsigned j=0; j<n.getNumChildren(); j++ ){
             RDomain * rf = getRDomain( op, j );
             rf->addTerm( n[j] );
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 5365dbcfa..2c58b8f77 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -175,7 +175,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
                   for( unsigned j=0; j<to_remove.size(); j++ ){
                     Node ns = d_quantEngine->getSubstitute( to_remove[j], inst );
                     Trace("rewrite-engine-inst-debug") << "Will remove : " << ns << std::endl;
-                    ns.setAttribute(NoMatchAttribute(),true);
+                    d_quantEngine->getTermDatabase()->setTermInactive( ns );
                   }
                   */
                 }else{
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 4dcf0e248..b143286cc 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -84,7 +84,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
   }
 }
 
-TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
+TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_inactive_map( c ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
@@ -178,6 +178,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
             }
           }
         }
+      }else{
+        setTermInactive( n );
       }
       rec = true;
     }
@@ -210,7 +212,7 @@ void TermDb::computeUfEqcTerms( TNode f ) {
     for( unsigned i=0; i<d_op_map[f].size(); i++ ){
       TNode n = d_op_map[f][i];
       if( hasTermCurrent( n ) ){
-        if( !n.getAttribute(NoMatchAttribute()) ){
+        if( isTermActive( n ) ){
           computeArgReps( n );
           TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n;
           d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] );
@@ -471,6 +473,18 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
   return isEntailed2( n, subs, subsRep, true, pol, qy );
 }
 
+bool TermDb::isTermActive( Node n ) {
+  return d_inactive_map.find( n )==d_inactive_map.end(); 
+  //return !n.getAttribute(NoMatchAttribute());
+}
+
+void TermDb::setTermInactive( Node n ) {
+  d_inactive_map[n] = true;
+  //Trace("term-db-debug2") << "set no match attribute" << std::endl;
+  //NoMatchAttribute nma;
+  //n.setAttribute(nma,true);
+}
+
 bool TermDb::hasTermCurrent( Node n, bool useMode ) {
   if( !useMode ){
     return d_has_map.find( n )!=d_has_map.end();
@@ -636,7 +650,7 @@ bool TermDb::reset( Theory::Effort effort ){
       Node n = it->second[i];
       //to be added to term index, term must be relevant, and exist in EE
       if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
-        if( !n.getAttribute(NoMatchAttribute()) ){
+        if( isTermActive( n ) ){
           if( options::finiteModelFind() ){
             computeModelBasisArgAttribute( n );
           }
@@ -651,13 +665,11 @@ bool TermDb::reset( Theory::Effort effort ){
             }
           }
           Trace("term-db-debug") << std::endl;
-          if( ee->hasTerm( n ) ){
-            Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
-          }
+          Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
           Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] );
+          Trace("term-db-debug2") << "...add term returned " << at << std::endl;
           if( at!=n && ee->areEqual( at, n ) ){
-            NoMatchAttribute nma;
-            n.setAttribute(nma,true);
+            setTermInactive( n );
             Trace("term-db-debug") << n << " is redundant." << std::endl;
             congruentCount++;
           }else{
@@ -846,9 +858,8 @@ void TermDb::makeInstantiationConstantsFor( Node q ){
       ic.setAttribute( ivna, i );
       InstConstantAttribute ica;
       ic.setAttribute( ica, q );
-      //also set the no-match attribute
-      NoMatchAttribute nma;
-      ic.setAttribute(nma,true);
+      //also set the term inactive
+      setTermInactive( ic );
     }
   }
 }
@@ -906,11 +917,6 @@ Node TermDb::getInstConstAttr( Node n ) {
     }
     InstConstantAttribute ica;
     n.setAttribute(ica, q);
-    if( !q.isNull() ){
-      //also set the no-match attribute
-      NoMatchAttribute nma;
-      n.setAttribute(nma,true);
-    }
   }
   return n.getAttribute(InstConstantAttribute());
 }
@@ -1019,9 +1025,12 @@ Node TermDb::getCounterexampleLiteral( Node q ){
 
 Node TermDb::getInstConstantNode( Node n, Node q ){
   makeInstantiationConstantsFor( q );
-  Node n2 = n.substitute( d_vars[q].begin(), d_vars[q].end(),
-                          d_inst_constants[q].begin(), d_inst_constants[q].end() );
-  return n2;
+  return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() );
+}
+
+Node TermDb::getVariableNode( Node n, Node q ) {
+  makeInstantiationConstantsFor( q );
+  return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() );
 }
 
 Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 266d9b8fa..004292622 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -47,15 +47,6 @@ typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
 struct SynthesisAttributeId {};
 typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
 
-/** Attribute true for nodes that should not be used for matching */
-struct NoMatchAttributeId {};
-/** use the special for boolean flag */
-typedef expr::Attribute< NoMatchAttributeId,
-                         bool,
-                         expr::attr::NullCleanupStrategy,
-                         true // context dependent
-                       > NoMatchAttribute;
-
 // attribute for "contains instantiation constants from"
 struct InstConstantAttributeId {};
 typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
@@ -179,6 +170,7 @@ class TermDb : public QuantifiersUtil {
   friend class ::CVC4::theory::quantifiers::ConjectureGenerator;
   friend class ::CVC4::theory::quantifiers::TermGenEnv;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
@@ -211,6 +203,8 @@ private:
   std::map< Node, std::vector< Node > > d_op_map;
   /** map from type nodes to terms of that type */
   std::map< TypeNode, std::vector< Node > > d_type_map;
+  /** inactive map */
+  NodeBoolMap d_inactive_map;
 
   /** count number of non-redundant ground terms per operator */
   std::map< Node, int > d_op_nonred_count;
@@ -266,6 +260,9 @@ public:
   /** is entailed (incomplete check) */
   bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL );
   bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL );
+  /** is active */
+  bool isTermActive( Node n );
+  void setTermInactive( Node n );
   /** has term */
   bool hasTermCurrent( Node n, bool useMode = true );
   /** is term eligble for instantiation? */
@@ -327,6 +324,7 @@ public:
       instantiation.
    */
   Node getInstConstantNode( Node n, Node q );
+  Node getVariableNode( Node n, Node q );
   /** get substituted node */
   Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms );
 
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 38635b37b..c91194239 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -43,9 +43,8 @@ void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
 }
 
 /** trigger class constructor */
-Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption )
-    : d_quantEngine( qe ), d_f( f )
-{
+Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
+    : d_quantEngine( qe ), d_f( f ) {
   d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
   Trace("trigger") << "Trigger for " << f << ": " << std::endl;
   for( unsigned i=0; i<d_nodes.size(); i++ ){
@@ -53,7 +52,7 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int
   }
   if( d_nodes.size()==1 ){
     if( isSimpleTrigger( d_nodes[0] ) ){
-      d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] );
+      d_mg = new InstMatchGeneratorSimple( f, d_nodes[0], qe );
     }else{
       d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe );
       d_mg->setActiveAdd(true);
@@ -112,6 +111,10 @@ int Trigger::addTerm( Node t ){
   return d_mg->addTerm( d_f, t, d_quantEngine );
 }
 
+Node Trigger::getInstPattern(){
+  return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
+}
+
 int Trigger::addInstantiations( InstMatch& baseMatch ){
   int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine );
   if( addedLemmas>0 ){
@@ -124,77 +127,85 @@ int Trigger::addInstantiations( InstMatch& baseMatch ){
   return addedLemmas;
 }
 
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption ){
-  std::vector< Node > trNodes;
-  if( !keepAll ){
-    //only take nodes that contribute variables to the trigger when added
-    std::vector< Node > temp;
-    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
-    std::map< Node, bool > vars;
-    std::map< Node, std::vector< Node > > patterns;
-    size_t varCount = 0;
-    std::map< Node, std::vector< Node > > varContains;
-    quantifiers::TermDb::getVarContains( f, temp, varContains );
-    for( unsigned i=0; i<temp.size(); i++ ){
-      bool foundVar = false;
+bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
+  //only take nodes that contribute variables to the trigger when added
+  std::vector< Node > temp;
+  temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+  std::map< Node, bool > vars;
+  std::map< Node, std::vector< Node > > patterns;
+  size_t varCount = 0;
+  std::map< Node, std::vector< Node > > varContains;
+  quantifiers::TermDb::getVarContains( q, temp, varContains );
+  for( unsigned i=0; i<temp.size(); i++ ){
+    bool foundVar = false;
+    for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
+      Node v = varContains[ temp[i] ][j];
+      Assert( quantifiers::TermDb::getInstConstAttr(v)==q );
+      if( vars.find( v )==vars.end() ){
+        varCount++;
+        vars[ v ] = true;
+        foundVar = true;
+      }
+    }
+    if( foundVar ){
+      trNodes.push_back( temp[i] );
       for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
         Node v = varContains[ temp[i] ][j];
-        Assert( quantifiers::TermDb::getInstConstAttr(v)==f );
-        if( vars.find( v )==vars.end() ){
-          varCount++;
-          vars[ v ] = true;
-          foundVar = true;
-        }
-      }
-      if( foundVar ){
-        trNodes.push_back( temp[i] );
-        for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
-          Node v = varContains[ temp[i] ][j];
-          patterns[ v ].push_back( temp[i] );
-        }
-      }
-      if( varCount==f[0].getNumChildren() ){
-        break;
+        patterns[ v ].push_back( temp[i] );
       }
     }
-    if( varCount<f[0].getNumChildren() && !options::partialTriggers() ){
-      Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl;
-      for( unsigned i=0; i<nodes.size(); i++) {
-        Trace("trigger-debug") << nodes[i] << " ";
-      }
-      Trace("trigger-debug") << std::endl;
+    if( varCount==n_vars ){
+      break;
+    }
+  }
+  if( varCount<n_vars ){
+    Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl;
+    for( unsigned i=0; i<nodes.size(); i++) {
+      Trace("trigger-debug") << nodes[i] << " ";
+    }
+    Trace("trigger-debug") << std::endl;
 
-      //do not generate multi-trigger if it does not contain all variables
-      return NULL;
-    }else{
-      //now, minimize the trigger
-      for( unsigned i=0; i<trNodes.size(); i++ ){
-        bool keepPattern = false;
-        Node n = trNodes[i];
+    //do not generate multi-trigger if it does not contain all variables
+    return false;
+  }else{
+    //now, minimize the trigger
+    for( unsigned i=0; i<trNodes.size(); i++ ){
+      bool keepPattern = false;
+      Node n = trNodes[i];
+      for( unsigned j=0; j<varContains[ n ].size(); j++ ){
+        Node v = varContains[ n ][j];
+        if( patterns[v].size()==1 ){
+          keepPattern = true;
+          break;
+        }
+      }
+      if( !keepPattern ){
+        //remove from pattern vector
         for( unsigned j=0; j<varContains[ n ].size(); j++ ){
           Node v = varContains[ n ][j];
-          if( patterns[v].size()==1 ){
-            keepPattern = true;
-            break;
-          }
-        }
-        if( !keepPattern ){
-          //remove from pattern vector
-          for( unsigned j=0; j<varContains[ n ].size(); j++ ){
-            Node v = varContains[ n ][j];
-            for( unsigned k=0; k<patterns[v].size(); k++ ){
-              if( patterns[v][k]==n ){
-                patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
-                break;
-              }
+          for( unsigned k=0; k<patterns[v].size(); k++ ){
+            if( patterns[v][k]==n ){
+              patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
+              break;
             }
           }
-          //remove from trigger nodes
-          trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
-          i--;
         }
+        //remove from trigger nodes
+        trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
+        i--;
       }
     }
+  }
+  return true;
+}
+
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, bool keepAll, int trOption, unsigned use_n_vars ){
+  std::vector< Node > trNodes;
+  if( !keepAll ){
+    unsigned n_vars = use_n_vars==0 ? f[0].getNumChildren() : use_n_vars;
+    if( !mkTriggerTerms( f, nodes, n_vars, trNodes ) ){
+      return NULL;
+    }
   }else{
     trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
   }
@@ -211,15 +222,15 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
       }
     }
   }
-  Trigger* t = new Trigger( qe, f, trNodes, matchOption );
+  Trigger* t = new Trigger( qe, f, trNodes );
   qe->getTriggerDatabase()->addTrigger( trNodes, t );
   return t;
 }
 
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption ){
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll, int trOption, unsigned use_n_vars ){
   std::vector< Node > nodes;
   nodes.push_back( n );
-  return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption );
+  return mkTrigger( qe, f, nodes, keepAll, trOption, use_n_vars );
 }
 
 bool Trigger::isUsable( Node n, Node q ){
@@ -343,9 +354,7 @@ bool Trigger::isUsableTrigger( Node n, Node q ){
 }
 
 bool Trigger::isAtomicTrigger( Node n ){
-  Kind k = n.getKind();
-  return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) ||
-         ( k!=APPLY_UF && isAtomicTriggerKind( k ) );
+  return isAtomicTriggerKind( n.getKind() );
 }
 
 bool Trigger::isAtomicTriggerKind( Kind k ) {
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 41f2a1c38..902f73e75 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -76,6 +76,8 @@ class Trigger {
   int addTerm( Node t );
   /** return whether this is a multi-trigger */
   bool isMultiTrigger() { return d_nodes.size()>1; }
+  /** get inst pattern list */
+  Node getInstPattern();
 
   /** add all available instantiations exhaustively, in any equivalence class
       if limitInst>0, limitInst is the max # of instantiations to try */
@@ -84,8 +86,6 @@ class Trigger {
      ie     : quantifier engine;
      f      : forall something ....
      nodes  : (multi-)trigger
-     matchOption : which policy to use for creating matches
-                   (one of InstMatchGenerator::MATCH_GEN_* )
      keepAll: don't remove unneeded patterns;
      trOption : policy for dealing with triggers that already existed
                 (see below)
@@ -95,12 +95,12 @@ class Trigger {
     TR_GET_OLD,     //return a previous trigger if it had already been created
     TR_RETURN_NULL  //return null if a duplicate is found
   };
-  static Trigger* mkTrigger( QuantifiersEngine* qe, Node f,
-                             std::vector< Node >& nodes, int matchOption = 0,
-                             bool keepAll = true, int trOption = TR_MAKE_NEW );
-  static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n,
-                             int matchOption = 0, bool keepAll = true,
-                             int trOption = TR_MAKE_NEW );
+  //nodes input, trNodes output
+  static bool mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes );
+  static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
+                             bool keepAll = true, int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 );
+  static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll = true,
+                             int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 );
   static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt,
                                std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo,
                                bool filterInst = false );
@@ -135,7 +135,7 @@ class Trigger {
   }
 private:
   /** trigger constructor */
-  Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0 );
+  Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes );
 
   /** is subterm of trigger usable */
   static bool isUsable( Node n, Node q );