From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 31 Mar 2016 19:36:25 +0000 (-0500)
Subject: Improvements to trigger selection, min triggers by default. Optimizations for E-match... 
X-Git-Tag: cvc5-1.0.0~6049^2~81
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ccc9cd5aad5248b4a2c86b617d76bc98063a7ea2;p=cvc5.git

Improvements to trigger selection, min triggers by default. Optimizations for E-matching. Minor work to equality infer.
---

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 152e22f14..8a5bacf91 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -602,12 +602,14 @@ theory::quantifiers::UserPatMode OptionsHandler::stringToUserPatMode(std::string
 }
 
 theory::quantifiers::TriggerSelMode OptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) {
-  if(optarg ==  "default" || optarg == "all" ) {
+  if(optarg ==  "default") {
     return theory::quantifiers::TRIGGER_SEL_DEFAULT;
   } else if(optarg == "min") {
     return theory::quantifiers::TRIGGER_SEL_MIN;
   } else if(optarg == "max") {
     return theory::quantifiers::TRIGGER_SEL_MAX;
+  } else if(optarg == "all") {
+    return theory::quantifiers::TRIGGER_SEL_ALL;
   } else if(optarg ==  "help") {
     puts(s_triggerSelModeHelp.c_str());
     exit(1);
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 8aa3756cc..86a783008 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -107,6 +107,8 @@ enum TriggerSelMode {
   TRIGGER_SEL_MIN,
   /** only consider maximal terms for triggers */
   TRIGGER_SEL_MAX,
+  /** consider all terms for triggers */
+  TRIGGER_SEL_ALL,
 };
 
 enum CVC4_PUBLIC PrenexQuantMode {
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index e5cc34f7e..9b2342c4c 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -58,9 +58,11 @@ Node CandidateGeneratorQueue::getNextCandidate(){
   }
 }
 
-CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
-  d_op( op ), d_qe( qe ), d_term_iter( -1 ){
+CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) :
+  d_qe( qe ), d_term_iter( -1 ){
+  d_op = qe->getTermDatabase()->getMatchOperator( pat );
   Assert( !d_op.isNull() );
+  d_op_arity = pat.getNumChildren();
 }
 
 void CandidateGeneratorQE::resetInstantiationRound(){
@@ -77,11 +79,23 @@ void CandidateGeneratorQE::reset( Node eqc ){
     }else{
       eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
       if( ee->hasTerm( eqc ) ){
-        //create an equivalence class iterator in eq class eqc
-        Node rep = ee->getRepresentative( eqc );
-        d_eqc_iter = eq::EqClassIterator( rep, ee );
-        d_mode = cand_term_eqc;
+        quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op );
+        if( tat ){
+#if 1
+          //create an equivalence class iterator in eq class eqc
+          Node rep = ee->getRepresentative( eqc );
+          d_eqc_iter = eq::EqClassIterator( rep, ee );
+          d_mode = cand_term_eqc;
+#else
+          d_tindex.push_back( tat );
+          d_tindex_iter.push_back( tat->d_data.begin() );
+          d_mode = cand_term_tindex;
+#endif     
+        }else{
+          d_mode = cand_term_none;
+        }   
       }else{
+        //the only match is this term itself
         d_n = eqc;
         d_mode = cand_term_ident;
       }
@@ -111,6 +125,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
           }else{
             Node r = d_qe->getEqualityQuery()->getRepresentative( n );
             if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
+              Debug("cand-gen-qe") << "...returning " << n << std::endl;
               return n;
             }
           }
@@ -123,9 +138,40 @@ Node CandidateGeneratorQE::getNextCandidate(){
       Node n = *d_eqc_iter;
       ++d_eqc_iter;
       if( isLegalOpCandidate( n ) ){
+        Debug("cand-gen-qe") << "...returning " << n << std::endl;
         return n;
       }
     }
+  }else if( d_mode==cand_term_tindex ){
+    Debug("cand-gen-qe") << "...get next candidate in tindex " << d_op << " " << d_op_arity << std::endl;
+    //increment the term index iterator
+    if( !d_tindex.empty() ){
+      //populate the vector
+      while( d_tindex_iter.size()<=d_op_arity ){
+        Assert( !d_tindex_iter.empty() );
+        Assert( !d_tindex_iter.back()->second.d_data.empty() );
+        d_tindex.push_back( &(d_tindex_iter.back()->second) );
+        d_tindex_iter.push_back( d_tindex_iter.back()->second.d_data.begin() );
+      }
+      //get the current node
+      Assert( d_tindex_iter.back()->second.hasNodeData() );
+      Node n = d_tindex_iter.back()->second.getNodeData();
+      Debug("cand-gen-qe") << "...returning " << n << std::endl;
+      Assert( !n.isNull() );
+      Assert( isLegalOpCandidate( n ) );
+      //increment
+      bool success = false;
+      do{
+        ++d_tindex_iter.back();
+        if( d_tindex_iter.back()==d_tindex.back()->d_data.end() ){
+          d_tindex.pop_back();
+          d_tindex_iter.pop_back();
+        }else{
+          success = true;
+        }
+      }while( !success && !d_tindex.empty() );
+      return n;   
+    } 
   }else if( d_mode==cand_term_ident ){
     Debug("cand-gen-qe") << "...get next candidate identity" << std::endl;
     if( !d_n.isNull() ){
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 9d8e318aa..f40114897 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -23,6 +23,10 @@
 namespace CVC4 {
 namespace theory {
 
+namespace quantifiers {
+  class TermArgTrie;
+}
+
 class QuantifiersEngine;
 
 namespace inst {
@@ -79,6 +83,9 @@ private:
   //instantiator pointer
   QuantifiersEngine* d_qe;
   //the equality class iterator
+  unsigned d_op_arity;
+  std::vector< quantifiers::TermArgTrie* > d_tindex;
+  std::vector< std::map< TNode, quantifiers::TermArgTrie >::iterator > d_tindex_iter;
   eq::EqClassIterator d_eqc_iter;
   //std::vector< Node > d_eqc;
   int d_term_iter;
@@ -88,6 +95,7 @@ private:
     cand_term_db,
     cand_term_ident,
     cand_term_eqc,
+    cand_term_tindex,
     cand_term_none,
   };
   short d_mode;
@@ -95,7 +103,7 @@ private:
   Node d_n;
   std::map< Node, bool > d_exclude_eqc;
 public:
-  CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
+  CandidateGeneratorQE( QuantifiersEngine* qe, Node pat );
   ~CandidateGeneratorQE() throw() {}
 
   void resetInstantiationRound();
diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp
index fc3a274ac..f1dbb32fa 100644
--- a/src/theory/quantifiers/equality_infer.cpp
+++ b/src/theory/quantifiers/equality_infer.cpp
@@ -26,11 +26,12 @@ using namespace std;
 
 namespace CVC4 {
 
-EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ) {
+EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ), d_rep_exp(c) {
 
 }
 
-EqualityInference::EqualityInference( context::Context* c ) : d_c( c ), d_elim_vars( c ), d_rep_to_eqc( c ), d_uselist( c ), d_pending_merges( c ){
+EqualityInference::EqualityInference( context::Context* c, bool trackExp ) : 
+d_c( c ), d_trackExplain( trackExp ), d_elim_vars( c ), d_rep_to_eqc( c ), d_uselist( c ), d_pending_merges( c ), d_pending_merge_exp( c ){
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
 }
 
@@ -127,6 +128,10 @@ void EqualityInference::setEqcRep( Node t, Node r, EqcInfo * eqci ) {
       Trace("eq-infer") << "Infer two equivalence classes are equal : " << t << " " << t2 << std::endl;
       Trace("eq-infer") << "  since they both normalize to : " << r << std::endl;
       d_pending_merges.push_back( t.eqNode( t2 ) );
+      if( d_trackExplain ){
+        //TODO
+        d_pending_merge_exp.push_back( t.eqNode( t2 ) );
+      }
     }
   }
 }
@@ -232,4 +237,9 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
   }
 }
 
+Node EqualityInference::getPendingMergeExplanation( unsigned i ) { 
+  Assert( d_trackExplain );
+  return d_pending_merge_exp[i]; 
+}  
+
 }
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 70b05c351..2c01c9a80 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.h
@@ -49,8 +49,12 @@ private:
     ~EqcInfo(){}
     context::CDO< Node > d_rep;
     context::CDO< bool > d_valid;
+    //explanation for why d_rep is how it is
+    NodeList d_rep_exp;
   };
 
+  /** track explanations */
+  bool d_trackExplain;
   /** information necessary for equivalence classes */
   NodeMap d_elim_vars;
   std::map< Node, EqcInfo * > d_eqci;
@@ -62,8 +66,10 @@ private:
   void addToUseList( Node used, Node eqc );
   /** pending merges */
   NodeList d_pending_merges;
+  NodeList d_pending_merge_exp;
 public:
-  EqualityInference(context::Context* c);
+  //second argument is whether explanations should be tracked
+  EqualityInference(context::Context* c, bool trackExp = false);
   virtual ~EqualityInference();
   /** input : notification when equality engine is updated */
   void eqNotifyNewClass(TNode t);
@@ -71,6 +77,7 @@ public:
   /** output : inferred equalities */
   unsigned getNumPendingMerges() { return d_pending_merges.size(); }
   Node getPendingMerge( unsigned i ) { return d_pending_merges[i]; }  
+  Node getPendingMergeExplanation( unsigned i );
 };
 
 }
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 7d732ab8a..96f67f042 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -121,7 +121,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
     //create candidate generator
     if( Trigger::isAtomicTrigger( d_match_pattern ) ){
       //we will be scanning lists trying to find d_match_pattern.getOperator()
-      d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op );
+      d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern );
       //if matching on disequality, inform the candidate generator not to match on eqc
       if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){
         ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
@@ -679,6 +679,12 @@ int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){
 }
 
 InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) {
+  if( d_match_pattern.getKind()==NOT ){
+    d_match_pattern = d_match_pattern[0];
+    d_pol = false;
+  }else{
+    d_pol = true;
+  }
   if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
     d_eqc = d_match_pattern[1];
     d_match_pattern = d_match_pattern[0];
@@ -702,16 +708,30 @@ void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe )
 }
 
 int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
-  InstMatch m( q );
-  m.add( baseMatch );
   int addedLemmas = 0;
   quantifiers::TermArgTrie* tat;
   if( d_eqc.isNull() ){
     tat = qe->getTermDatabase()->getTermArgTrie( d_op );
   }else{
-    tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
+    if( d_pol ){
+      tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
+    }else{
+      Node r = qe->getEqualityQuery()->getRepresentative( d_eqc );
+      //iterate over all classes except r
+      tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op );
+      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
+        if( it->first!=r ){
+          InstMatch m( q );
+          m.add( baseMatch );
+          addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
+        }
+      }
+      tat = NULL;
+    }
   }
   if( tat ){
+    InstMatch m( q );
+    m.add( baseMatch );
     addInstantiations( m, qe, addedLemmas, 0, tat );
     return addedLemmas;
   }else{
@@ -723,7 +743,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
   Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
   if( argIndex==(int)d_match_pattern.getNumChildren() ){
     Assert( !tat->d_data.empty() );
-    Node t = tat->d_data.begin()->first;
+    TNode t = tat->getNodeData();
     Debug("simple-trigger") << "Actual term is " << t << std::endl;
     //convert to actual used terms
     for( std::map< int, int >::iterator it = d_var_num.begin(); it != d_var_num.end(); ++it ){
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 58531f3e6..adaae8058 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -212,6 +212,7 @@ private:
   /** match term */
   Node d_match_pattern;
   /** equivalence class */
+  bool d_pol;
   Node d_eqc;
   /** match pattern arg types */
   std::vector< TypeNode > d_match_pattern_arg_types;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index fac83ec5c..7d0fab2ff 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -141,7 +141,7 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
 
 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){
   //how to select trigger terms
-  if( options::triggerSelMode()==TRIGGER_SEL_MIN ){
+  if( options::triggerSelMode()==TRIGGER_SEL_MIN || options::triggerSelMode()==TRIGGER_SEL_DEFAULT ){
     d_tr_strategy = Trigger::TS_MIN_TRIGGER;
   }else if( options::triggerSelMode()==TRIGGER_SEL_MAX ){
     d_tr_strategy = Trigger::TS_MAX_TRIGGER;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 62da8c347..dc1f9990b 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -126,6 +126,8 @@ public:
   /** the data */
   std::map< TNode, TermArgTrie > d_data;
 public:
+  bool hasNodeData() { return !d_data.empty(); }
+  TNode getNodeData() { return d_data.begin()->first; }
   TNode existsTerm( std::vector< TNode >& reps, int argIndex = 0 );
   TNode addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
   bool addTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
@@ -358,26 +360,26 @@ public:
 //for triggers
 private:
   /** helper function for compute var contains */
-  void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited );
+  static void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited );
   /** triggers for each operator */
   std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
   /** helper for is instance of */
-  bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
+  static bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
   /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
-  int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
+  static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 );
 public:
   /** compute var contains */
-  void computeVarContains( Node n, std::vector< Node >& varContains );
+  static void computeVarContains( Node n, std::vector< Node >& varContains );
   /** get var contains for each of the patterns in pats */
-  void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
+  static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
   /** get var contains for node n */
-  void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
-  /** register trigger (for eager quantifier instantiation) */
-  void registerTrigger( inst::Trigger* tr, Node op );
+  static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
   /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
-  int isInstanceOf( Node n1, Node n2 );
+  static int isInstanceOf( Node n1, Node n2 );
   /** filter all nodes that have instances */
-  void filterInstances( std::vector< Node >& nodes );
+  static void filterInstances( std::vector< Node >& nodes );
+  /** register trigger (for eager quantifier instantiation) */
+  void registerTrigger( inst::Trigger* tr, Node op );
 
 //for term ordering
 private:
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 79c677f1c..2a9bf26a6 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -337,7 +337,7 @@ bool Trigger::isCbqiKind( Kind k ) {
 }
 
 bool Trigger::isSimpleTrigger( Node n ){
-  Node t = n;
+  Node t = n.getKind()==NOT ? n[0] : n;
   if( n.getKind()==IFF || n.getKind()==EQUAL ){
     if( !quantifiers::TermDb::hasInstConstAttr( n[1] ) ){
       t = n[0];
@@ -359,70 +359,71 @@ bool Trigger::isSimpleTrigger( Node n ){
 }
 
 //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
-bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& visited, int tstrt, std::vector< Node >& exclude, 
-                                std::map< Node, int >& reqPol, bool pol, bool hasPol, bool epol, bool hasEPol ){
-  std::map< Node, bool >::iterator itv = visited.find( n );
+bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, 
+                                int tstrt, std::vector< Node >& exclude, 
+                                std::map< Node, int >& reqPol, std::vector< Node >& added,
+                                bool pol, bool hasPol, bool epol, bool hasEPol ){
+  std::map< Node, Node >::iterator itv = visited.find( n );
   if( itv==visited.end() ){
-    visited[ n ] = false;
+    visited[ n ] = Node::null();
     Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
     bool retVal = false;
     if( n.getKind()!=FORALL ){
-      if( tstrt==TS_MIN_TRIGGER ){
+      bool rec = true;
+      Node nu;
+      if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
+        nu = getIsUsableTrigger( n, f, pol, hasPol );
+        if( !nu.isNull() ){
+          reqPol[ nu ] = hasEPol ? ( epol ? 1 : -1 ) : 0;
+          visited[ nu ] = nu;
+          quantifiers::TermDb::computeVarContains( nu, visited_fv[ nu ] );
+          retVal = true;
+          if( tstrt==TS_MAX_TRIGGER ){
+            rec = false;
+          }
+        }
+      }
+      if( rec ){
+        std::vector< Node > added2;
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           bool newHasPol, newPol;
           bool newHasEPol, newEPol;
           QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
           QuantPhaseReq::getEntailPolarity( n, i, hasEPol, epol, newHasEPol, newEPol );
-          if( collectPatTerms2( f, n[i], visited, tstrt, exclude, reqPol, newPol, newHasPol, newEPol, newHasEPol ) ){
+          if( collectPatTerms2( f, n[i], visited, visited_fv, tstrt, exclude, reqPol, added2, newPol, newHasPol, newEPol, newHasEPol ) ){
             retVal = true;
           }
         }
-        if( !retVal ){
-          Node nu;
-          if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
-            nu = getIsUsableTrigger( n, f, pol, hasPol );
-          }
-          if( !nu.isNull() ){
-            reqPol[ nu ] = hasEPol ? ( epol==(n.getKind()!=NOT) ? 1 : -1 ) : 0;
-            visited[ nu ] = true;
-            retVal = true;
-          }
-        }
-      }else{
-        Node nu;
-        if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
-          nu = getIsUsableTrigger( n, f, pol, hasPol );
-        }
-        bool rec = true;
         if( !nu.isNull() ){
-          reqPol[ nu ] = hasEPol ? ( epol==(n.getKind()!=NOT) ? 1 : -1 ) : 0;
-          visited[ nu ] = true;
-          retVal = true;
-          if( tstrt==TS_MAX_TRIGGER ){
-            rec = false;
-          }
-        }
-        if( rec ){
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            bool newHasPol, newPol;
-            bool newHasEPol, newEPol;
-            QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
-            QuantPhaseReq::getEntailPolarity( n, i, hasEPol, epol, newHasEPol, newEPol );
-            if( collectPatTerms2( f, n[i], visited, tstrt, exclude, reqPol, newPol, newHasPol, newEPol, newHasEPol ) ){
-              retVal = true;
+          bool rm_nu = false;
+          //discard if we added a subterm as a trigger with all variables that nu has
+          for( unsigned i=0; i<added2.size(); i++ ){
+            Assert( visited_fv.find( added2[i] )!=visited_fv.end() );
+            if( visited_fv[ nu ].size()==visited_fv[added2[i]].size() ){
+              rm_nu = true;
             }
+            added.push_back( added2[i] );
+          }
+          if( rm_nu && tstrt==TS_MIN_TRIGGER ){
+            visited[nu] = Node::null();
+            reqPol.erase( nu );
+          }else{
+            added.push_back( nu );
           }
         }
       }
     }
     return retVal;
   }else{
-    return itv->second;
+    if( itv->second.isNull() ){
+      return false;
+    }else{
+      added.push_back( itv->second );
+      return true;
+    }
   }
 }
 
-
-
 bool Trigger::isBooleanTermTrigger( Node n ) {
   if( n.getKind()==ITE ){
     //check for boolean term converted to ITE
@@ -503,7 +504,7 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector<
 
 void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, 
                                std::map< Node, int >& reqPol, bool filterInst ){
-  std::map< Node, bool > visited;
+  std::map< Node, Node > visited;
   if( filterInst ){
     //immediately do not consider any term t for which another term is an instance of t
     std::vector< Node > patTerms2;
@@ -534,14 +535,16 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
       //do not consider terms that have instances
       for( unsigned i=0; i<patTerms2.size(); i++ ){
         if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
-          visited[ patTerms2[i] ] = false;
+          visited[ patTerms2[i] ] = Node::null();
         }
       }
     }
   }
-  collectPatTerms2( f, n, visited, tstrt, exclude, reqPol, true, true, false, true );
+  std::map< Node, std::vector< Node > > visited_fv;
+  std::vector< Node > added;
+  collectPatTerms2( f, n, visited, visited_fv, tstrt, exclude, reqPol, added, true, true, false, true );
   for( std::map< Node, int >::iterator it = reqPol.begin(); it != reqPol.end(); ++it ){
-    if( visited[it->first] ){
+    if( !visited[it->first].isNull() ){
       patTerms.push_back( it->first );
     }
   }
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 22c4e5905..dfb5a094f 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -140,8 +140,9 @@ private:
   static Node getIsUsableTrigger( Node n, Node f, bool pol = true,
                                   bool hasPol = false );
   /** collect all APPLY_UF pattern terms for f in n */
-  static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& visited, 
-                                int tstrt, std::vector< Node >& exclude, std::map< Node, int >& reqPol,
+  static bool collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, 
+                                int tstrt, std::vector< Node >& exclude, 
+                                std::map< Node, int >& reqPol, std::vector< Node >& added,
                                 bool pol, bool hasPol, bool epol, bool hasEPol );
 
   std::vector< Node > d_nodes;