Refactor trigger selection, revisions to --relational-trigger. Properly process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.

10 files changed, 332 insertions, 204 deletions

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 34c7949d6..cfa4190e4 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -139,8 +139,8 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       }else{
         d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
       }
-    }else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
-      Assert( d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT );
+    }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) && 
+              d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){
       //we will be producing candidates via literal matching heuristics
       if( d_pattern.getKind()!=NOT ){
         //candidates will be all equalities
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 491da7116..8c3154c1c 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -60,6 +60,7 @@ struct sortTriggers {
 };
 
 void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
+  Trace("inst-alg-debug") << "reset user triggers" << std::endl;
   //reset triggers
   for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
     for( unsigned i=0; i<it->second.size(); i++ ){
@@ -67,6 +68,7 @@ void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort ef
       it->second[i]->reset( Node::null() );
     }
   }
+  Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
 }
 
 int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
@@ -118,11 +120,13 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
   bool usable = true;
   std::vector< Node > nodes;
   for( unsigned i=0; i<pat.getNumChildren(); i++ ){
-    nodes.push_back( pat[i] );
-    if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], q ) ){
+    Node pat_use = Trigger::getIsUsableTrigger( pat[i], q );
+    if( pat_use.isNull() ){
       Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl;
       usable = false;
       break;
+    }else{
+      nodes.push_back( pat_use );
     }
   }
   if( usable ){
@@ -132,7 +136,12 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
     if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
       d_user_gen_wait[q].push_back( nodes );
     }else{
-      d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW ) );
+      Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW );
+      if( t ){
+        d_user_gen[q].push_back( t );
+      }else{
+        Trace("trigger-warn") << "Failed to construct trigger : " << pat << " due to variable mismatch" << std::endl;
+      }
     }
   }
 }
@@ -154,6 +163,7 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe
 }
 
 void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
+  Trace("inst-alg-debug") << "reset auto-gen triggers" << std::endl;
   //reset triggers
   for( unsigned r=0; r<2; r++ ){
     for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger[r].begin(); it != d_auto_gen_trigger[r].end(); ++it ){
@@ -164,6 +174,7 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort
     }
   }
   d_processed_trigger.clear();
+  Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl;
 }
 
 int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
@@ -235,49 +246,51 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
 }
 
 void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
-  Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << std::endl;
+  Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << ", #var=" << f[0].getNumChildren() << "..." << std::endl;
   if( d_patTerms[0].find( f )==d_patTerms[0].end() ){
     //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
     d_patTerms[0][f].clear();
     d_patTerms[1][f].clear();
     bool ntrivTriggers = options::relationalTriggers();
     std::vector< Node > patTermsF;
-    std::map< Node, int > reqPol;
+    std::map< Node, inst::TriggerTermInfo > tinfo;
     //well-defined function: can assume LHS is only trigger
     if( options::quantFunWellDefined() ){
       Node hd = TermDb::getFunDefHead( f );
       if( !hd.isNull() ){
         hd = d_quantEngine->getTermDatabase()->getInstConstantNode( hd, f );
         patTermsF.push_back( hd );
-        reqPol[hd] = 0;
+        tinfo[hd].init( f, hd );
       }
     }
     //otherwise, use algorithm for collecting pattern terms
     if( patTermsF.empty() ){
       Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
-      Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], reqPol, true );
-      Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
+      Trigger::collectPatTerms( f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], tinfo, true );
       if( ntrivTriggers ){
         sortTriggers st;
         std::sort( patTermsF.begin(), patTermsF.end(), st );
       }
-      for( unsigned i=0; i<patTermsF.size(); i++ ){
-        Assert( reqPol.find( patTermsF[i] )!=reqPol.end() );
-        Trace("auto-gen-trigger-debug") << "   " << patTermsF[i] << " " << reqPol[patTermsF[i]] << std::endl;
+      if( Trace.isOn("auto-gen-trigger-debug") ){
+        Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
+        for( unsigned i=0; i<patTermsF.size(); i++ ){
+          Assert( tinfo.find( patTermsF[i] )!=tinfo.end() );
+          Trace("auto-gen-trigger-debug") << "   " << patTermsF[i];
+          Trace("auto-gen-trigger-debug") << " info[" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl;
+        }
+        Trace("auto-gen-trigger-debug") << std::endl;
       }
-      Trace("auto-gen-trigger-debug") << std::endl;
     }
     //sort into single/multi triggers, calculate which terms should not be considered
-    std::map< Node, std::vector< Node > > varContains;
     std::map< Node, bool > vcMap;
     std::map< Node, bool > rmPatTermsF;
     int last_weight = -1;
     for( unsigned i=0; i<patTermsF.size(); i++ ){
-      d_quantEngine->getTermDatabase()->getVarContainsNode( f, patTermsF[i], varContains[ patTermsF[i] ] );
+      Assert( patTermsF[i].getKind()!=NOT );
       bool newVar = false;
-      for( unsigned j=0; j<varContains[ patTermsF[i] ].size(); j++ ){
-        if( vcMap.find( varContains[ patTermsF[i] ][j] )==vcMap.end() ){
-          vcMap[varContains[ patTermsF[i] ][j]] = true;
+      for( unsigned j=0; j<tinfo[ patTermsF[i] ].d_fv.size(); j++ ){
+        if( vcMap.find( tinfo[ patTermsF[i] ].d_fv[j] )==vcMap.end() ){
+          vcMap[tinfo[ patTermsF[i] ].d_fv[j]] = true;
           newVar = true;
         }
       }
@@ -289,33 +302,46 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         last_weight = curr_w;
       }
     }
-    for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
-      Node pat = it->first;
-      Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl;
+    for( unsigned i=0; i<patTermsF.size(); i++ ){
+      Node pat = patTermsF[i];
       if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){
+        Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl;
         //process the pattern: if it has a required polarity, consider it
-        if( options::instNoEntail() ){
-          Assert( reqPol.find( pat )!=reqPol.end() );
-          int rpol = reqPol[pat];
-          Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << std::endl;
-          if( rpol!=0 ){
-            Assert( pat.getType().isBoolean() );
-            if( pat.getKind()==APPLY_UF ){
+        Assert( tinfo.find( pat )!=tinfo.end() );
+        int rpol = tinfo[pat].d_reqPol;
+        Node rpoleq = tinfo[pat].d_reqPolEq;
+        unsigned num_fv = tinfo[pat].d_fv.size();
+        Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl;
+        if( rpol!=0 ){
+          if( Trigger::isRelationalTrigger( pat ) ){
+            pat = rpol==-1 ? pat.negate() : pat;
+          }else{
+            Assert( Trigger::isAtomicTrigger( pat ) );
+            if( pat.getType().isBoolean() && rpoleq.isNull() ){
               pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+            }else{
+              Assert( !rpoleq.isNull() );
+              if( rpol==-1 ){
+                //all equivalence classes except rpoleq
+                pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
+              }else if( rpol==1 ){
+                //all equivalence classes that are not disequal to rpoleq TODO
+              }
             }
           }
-        }
-        if( it->second.size()==f[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
-          d_patTerms[0][f].push_back( pat );
-          d_is_single_trigger[ pat ] = true;
+          Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
         }else{
-          d_patTerms[1][f].push_back( pat );
-          d_is_single_trigger[ pat ] = false;
+          if( Trigger::isRelationalTrigger( pat ) ){
+            //consider both polarities
+            addPatternToPool( f, pat.negate(), num_fv );
+          }
         }
+        addPatternToPool( f, pat, num_fv );
       }
     }
+    //tinfo not used below this point
     d_made_multi_trigger[f] = false;
-    Trace("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;
+    Trace("auto-gen-trigger") << "Single trigger pool for " << f << " : " << std::endl;
     for( unsigned i=0; i<d_patTerms[0][f].size(); i++ ){
       Trace("auto-gen-trigger") << "   " << d_patTerms[0][f][i] << std::endl;
     }
@@ -427,6 +453,16 @@ 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 ) ) ){
+    d_patTerms[0][q].push_back( pat );
+    d_is_single_trigger[ pat ] = true;
+  }else{
+    d_patTerms[1][q].push_back( pat );
+    d_is_single_trigger[ pat ] = false;
+  }
+}
+
 bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
   if( q.getNumChildren()==3 ){
     std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index d48084514..028f24b27 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -89,6 +89,7 @@ private:
   int process( Node q, Theory::Effort effort, int e );
   /** generate triggers */
   void generateTriggers( Node q );
+  void addPatternToPool( Node q, Node pat, unsigned num_fv );
   //bool addTrigger( inst::Trigger * tr, Node f, unsigned r );
   /** has user patterns */
   bool hasUserPatterns( Node q );
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 90d01ac28..582599680 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -153,7 +153,7 @@ bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
   d_qe->getTermDatabase()->getVarContainsNode( f, icn, var );
   Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
   std::vector< Node > trigger_var;
-  inst::Trigger::getTriggerVariables( d_qe, icn, f, trigger_var );
+  inst::Trigger::getTriggerVariables( icn, f, trigger_var );
   Trace("macros-debug2") << "Done." << std::endl;
   //only if all variables are also trigger variables
   return trigger_var.size()>=var.size();
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 2558dcbee..8db79db9c 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -101,6 +101,8 @@ class EqualityQuery {
 public:
   EqualityQuery(){}
   virtual ~EqualityQuery(){};
+  /** extends engine */
+  virtual bool extendsEngine() { return false; }
   /** contains term */
   virtual bool hasTerm( Node a ) = 0;
   /** get the representative of the equivalence class of a */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 79c300401..5aae4d640 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -244,17 +244,21 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
     ret = ret.negate();
     status = REWRITE_AGAIN_FULL;
   }else if( in.getKind()==FORALL ){
-    //compute attributes
-    QAttributes qa;
-    TermDb::computeQuantAttributes( in, qa );
-    if( !qa.isRewriteRule() ){
-      for( int op=0; op<COMPUTE_LAST; op++ ){
-        if( doOperation( in, op, qa ) ){
-          ret = computeOperation( in, op, qa );
-          if( ret!=in ){
-            rew_op = op;
-            status = REWRITE_AGAIN_FULL;
-            break;
+    if( in[1].isConst() ){
+      return RewriteResponse( status, in[1] );
+    }else{
+      //compute attributes
+      QAttributes qa;
+      TermDb::computeQuantAttributes( in, qa );
+      if( !qa.isRewriteRule() ){
+        for( int op=0; op<COMPUTE_LAST; op++ ){
+          if( doOperation( in, op, qa ) ){
+            ret = computeOperation( in, op, qa );
+            if( ret!=in ){
+              rew_op = op;
+              status = REWRITE_AGAIN_FULL;
+              break;
+            }
           }
         }
       }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5d20a7048..763a80af3 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -208,27 +208,26 @@ void TermDb::computeUfEqcTerms( TNode f ) {
 //returns a term n' equivalent to n
 //  - if hasSubs = true, then n is consider under substitution subs
 //  - if mkNewTerms = true, then n' is either null, or a term in the master equality engine
-Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited ) {
+Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy ) {
   std::map< TNode, Node >::iterator itv = visited.find( n );
   if( itv != visited.end() ){
     return itv->second;
   }
   Node ret;
   Trace("term-db-eval") << "evaluate term : " << n << std::endl;
-  eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
-  if( ee->hasTerm( n ) ){
+  if( qy->hasTerm( n ) ){
     Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
-    ret = ee->getRepresentative( n );
+    ret = qy->getRepresentative( n );
   }else if( n.getKind()==BOUND_VARIABLE ){
     if( hasSubs ){
       Assert( subs.find( n )!=subs.end() );
       Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
       if( subsRep ){
-        Assert( ee->hasTerm( subs[n] ) );
-        Assert( ee->getRepresentative( subs[n] )==subs[n] );
+        Assert( qy->hasTerm( subs[n] ) );
+        Assert( qy->getRepresentative( subs[n] )==subs[n] );
         ret = subs[n];
       }else{
-        ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited );
+        ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited, qy );
       }
     }
   }else if( n.getKind()==FORALL ){
@@ -239,7 +238,7 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe
       std::vector< TNode > args;
       bool ret_set = false;
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, visited );
+        TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, visited, qy );
         if( c.isNull() ){
           ret = TNode::null();
           ret_set = true;
@@ -260,9 +259,9 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe
           Trace("term-db-eval") << "Get term from DB" << std::endl;
           TNode nn = d_func_map_trie[f].existsTerm( args );
           Trace("term-db-eval") << "Got term " << nn << std::endl;
-          if( !nn.isNull() && ee->hasTerm( nn ) ){
+          if( !nn.isNull() && qy->hasTerm( nn ) ){
             Trace("term-db-eval") << "return rep " << std::endl;
-            ret = ee->getRepresentative( nn );
+            ret = qy->getRepresentative( nn );
             ret_set = true;
           }
         }
@@ -283,10 +282,10 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe
 }
 
 
-TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs ) {
+TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
+  Assert( !qy->extendsEngine() );
   Trace("term-db-eval") << "evaluate term : " << n << std::endl;
-  eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
-  if( ee->hasTerm( n ) ){
+  if( qy->getEngine()->hasTerm( n ) ){
     Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
     return n;
   }else if( n.getKind()==BOUND_VARIABLE ){
@@ -294,11 +293,11 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
       Assert( subs.find( n )!=subs.end() );
       Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
       if( subsRep ){
-        Assert( ee->hasTerm( subs[n] ) );
-        Assert( ee->getRepresentative( subs[n] )==subs[n] );
+        Assert( qy->getEngine()->hasTerm( subs[n] ) );
+        Assert( qy->getEngine()->getRepresentative( subs[n] )==subs[n] );
         return subs[n];
       }else{
-        return evaluateTerm2( subs[n], subs, subsRep, hasSubs );
+        return evaluateTerm2( subs[n], subs, subsRep, hasSubs, qy );
       }
     }
   }else{
@@ -307,11 +306,11 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
       if( !f.isNull() ){
         std::vector< TNode > args;
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs );
+          TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, qy );
           if( c.isNull() ){
             return TNode::null();
           }
-          c = ee->getRepresentative( c );
+          c = qy->getEngine()->getRepresentative( c );
           Trace("term-db-eval") << "Got child : " << c << std::endl;
           args.push_back( c );
         }
@@ -325,53 +324,59 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
   return TNode::null();
 }
 
-Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms ) {
+Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms, EqualityQuery * qy ) {
+  if( qy==NULL ){
+    qy = d_quantEngine->getEqualityQuery();
+  }
   if( mkNewTerms ){
     std::map< TNode, Node > visited;
-    return evaluateTerm2( n, subs, subsRep, true, visited );
+    return evaluateTerm2( n, subs, subsRep, true, visited, qy );
   }else{
-    return evaluateTerm2( n, subs, subsRep, true );
+    return evaluateTerm2( n, subs, subsRep, true, qy );
   }
 }
 
-Node TermDb::evaluateTerm( TNode n, bool mkNewTerms ) {
+Node TermDb::evaluateTerm( TNode n, bool mkNewTerms, EqualityQuery * qy ) {
+  if( qy==NULL ){
+    qy = d_quantEngine->getEqualityQuery();
+  }
   std::map< TNode, TNode > subs;
   if( mkNewTerms ){
     std::map< TNode, Node > visited;
-    return evaluateTerm2( n, subs, false, false, visited );
+    return evaluateTerm2( n, subs, false, false, visited, qy );
   }else{
-    return evaluateTerm2( n, subs, false, false );
+    return evaluateTerm2( n, subs, false, false, qy );
   }
 }
 
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol ) {
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
+  Assert( !qy->extendsEngine() );
   Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl;
   Assert( n.getType().isBoolean() );
   if( n.getKind()==EQUAL ){
-    TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs );
+    TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs, qy );
     if( !n1.isNull() ){
-      TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs );
+      TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs, qy );
       if( !n2.isNull() ){
         if( n1==n2 ){
           return pol;
         }else{
-          eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
-          Assert( ee->hasTerm( n1 ) );
-          Assert( ee->hasTerm( n2 ) );
+          Assert( qy->getEngine()->hasTerm( n1 ) );
+          Assert( qy->getEngine()->hasTerm( n2 ) );
           if( pol ){
-            return ee->areEqual( n1, n2 );
+            return qy->getEngine()->areEqual( n1, n2 );
           }else{
-            return ee->areDisequal( n1, n2, false );
+            return qy->getEngine()->areDisequal( n1, n2, false );
           }
         }
       }
     }
   }else if( n.getKind()==NOT ){
-    return isEntailed( n[0], subs, subsRep, hasSubs, !pol );
+    return isEntailed( n[0], subs, subsRep, hasSubs, !pol, qy );
   }else if( n.getKind()==OR || n.getKind()==AND ){
     bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( isEntailed( n[i], subs, subsRep, hasSubs, pol ) ){
+      if( isEntailed( n[i], subs, subsRep, hasSubs, pol, qy ) ){
         if( simPol ){
           return true;
         }
@@ -384,31 +389,34 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
     return !simPol;
   }else if( n.getKind()==IFF || n.getKind()==ITE ){
     for( unsigned i=0; i<2; i++ ){
-      if( isEntailed( n[0], subs, subsRep, hasSubs, i==0 ) ){
+      if( isEntailed( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
         unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2;
         bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
-        return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol );
+        return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol, qy );
       }
     }
   }else if( n.getKind()==APPLY_UF ){
-    TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs );
+    TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs, qy );
     if( !n1.isNull() ){
+      Assert( qy->hasTerm( n1 ) );
       if( n1==d_true ){
         return pol;
       }else if( n1==d_false ){
         return !pol;
       }else{
-        eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
-        return ee->getRepresentative( n1 ) == ( pol ? d_true : d_false );
+        return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false );
       }
     }
   }
   return false;
 }
 
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ) {
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
+  if( qy==NULL ){
+    qy = d_quantEngine->getEqualityQuery();
+  }
   if( d_consistent_ee ){
-    return isEntailed( n, subs, subsRep, true, pol );
+    return isEntailed( n, subs, subsRep, true, pol, qy );
   }else{
     //don't check entailment wrt an inconsistent ee
     return false;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 4cba619a8..9177d3a1a 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -20,6 +20,7 @@
 #include "expr/attribute.h"
 #include "theory/theory.h"
 #include "theory/type_enumerator.h"
+#include "theory/quantifiers/quant_util.h"
 
 #include <map>
 
@@ -182,9 +183,9 @@ private:
   /** set has term */
   void setHasTerm( Node n );
   /** evaluate term */
-  TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs );
-  Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited );
-  bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol );
+  TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
+  Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy );
+  bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
 public:
   TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
   ~TermDb(){}
@@ -237,11 +238,11 @@ public:
   /** evaluate a term under a substitution.  Return representative in EE if possible.
    * subsRep is whether subs contains only representatives
    */
-  Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false );
+  Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false, EqualityQuery * qy = NULL );
   /** same as above, but without substitution */
-  Node evaluateTerm( TNode n, bool mkNewTerms = false );
+  Node evaluateTerm( TNode n, bool mkNewTerms = false, EqualityQuery * qy = NULL );
   /** is entailed (incomplete check) */
-  bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
+  bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL );
   /** has term */
   bool hasTermCurrent( Node n, bool useMode = true );
   /** is term eligble for instantiation? */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index b4e00386a..38635b37b 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -30,6 +30,18 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
+void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
+  if( d_fv.empty() ){
+    quantifiers::TermDb::getVarContainsNode( q, n, d_fv );
+  }
+  if( d_reqPol==0 ){
+    d_reqPol = reqPol;
+    d_reqPolEq = reqPolEq;
+  }else{
+    //determined a ground (dis)equality must hold or else q is a tautology?
+  }
+}
+
 /** trigger class constructor */
 Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption )
     : d_quantEngine( qe ), d_f( f )
@@ -122,7 +134,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
     std::map< Node, std::vector< Node > > patterns;
     size_t varCount = 0;
     std::map< Node, std::vector< Node > > varContains;
-    qe->getTermDatabase()->getVarContains( f, temp, varContains );
+    quantifiers::TermDb::getVarContains( f, temp, varContains );
     for( unsigned i=0; i<temp.size(); i++ ){
       bool foundVar = false;
       for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
@@ -213,7 +225,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOpt
 bool Trigger::isUsable( Node n, Node q ){
   if( quantifiers::TermDb::getInstConstAttr(n)==q ){
     if( isAtomicTrigger( n ) ){
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
         if( !isUsable( n[i], q ) ){
           return false;
         }
@@ -238,68 +250,91 @@ bool Trigger::isUsable( Node n, Node q ){
   }
 }
 
-Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
-  Trace("trigger-debug") << "Is " << n << " a usable trigger? pol/hasPol=" << pol << "/" << hasPol << std::endl;
+Node Trigger::getIsUsableEq( Node q, Node n ) {
+  Assert( isRelationalTrigger( n ) );
+  for( unsigned i=0; i<2; i++) {
+    if( isUsableEqTerms( q, n[i], n[1-i] ) ){
+      if( i==1 && ( n.getKind()==EQUAL || n.getKind()==IFF ) && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){
+        return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );  
+      }else{
+        return n;
+      }
+    }
+  }
+  return Node::null();
+}
+
+bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
+  if( n1.getKind()==INST_CONSTANT ){
+    if( options::relationalTriggers() ){
+      if( !quantifiers::TermDb::hasInstConstAttr(n2) ){
+        return true;
+      }else if( n2.getKind()==INST_CONSTANT ){
+        return true;
+      }
+    }
+  }else if( isAtomicTrigger( n1 ) && isUsable( n1, q ) ){
+    if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermDb::containsTerm( n1, n2 ) ){
+      return true;
+    }else if( !quantifiers::TermDb::hasInstConstAttr(n2) ){
+      return true;
+    }
+  }
+  return false;
+}
+
+Node Trigger::getIsUsableTrigger( Node n, Node q ) {
+  bool pol = true;
+  Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
   if( n.getKind()==NOT ){
     pol = !pol;
     n = n[0];
   }
-  if( options::relationalTriggers() ){
-    if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
-      Node rtr;
-      bool do_negate = hasPol && pol;
-      bool is_arith = n[0].getType().isReal();
-      for( unsigned i=0; i<2; i++) {
-        if( n[1-i].getKind()==INST_CONSTANT ){
-          if( ( ( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ) || !quantifiers::TermDb::hasInstConstAttr(n[i]) ) && 
-              ( !do_negate || is_arith ) ){
-            rtr = n;
-            break;
-          }
-          if( n[i].getKind()==INST_CONSTANT && ( !hasPol || pol ) ){
-            do_negate = true;
-            rtr = n;
-            break;
+  if( n.getKind()==INST_CONSTANT ){
+    return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+  }else if( isRelationalTrigger( n ) ){
+    Node rtr = getIsUsableEq( q, n );
+    if( rtr.isNull() && n[0].getType().isReal() ){
+      //try to solve relation
+      std::map< Node, Node > m;
+      if( QuantArith::getMonomialSumLit(n, m) ){
+        for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
+          bool trySolve = false;
+          if( !it->first.isNull() ){
+            if( it->first.getKind()==INST_CONSTANT ){
+              trySolve = options::relationalTriggers();
+            }else if( isUsableTrigger( it->first, q ) ){
+              trySolve = true;
+            }
           }
-        }
-      }
-      if( is_arith ){
-        //try to rearrange?
-        std::map< Node, Node > m;
-        if( QuantArith::getMonomialSumLit(n, m) ){
-          for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
-            if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){
-              Node veq;
-              if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){
-                int vti = veq[0]==it->first ? 1 : 0;
-                if( ( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ) || !quantifiers::TermDb::hasInstConstAttr(veq[vti]) ){
-                  rtr = veq;
-                }
-              }
+          if( trySolve ){
+            Trace("trigger-debug") << "Try to solve for " << it->first << std::endl;
+            Node veq;
+            if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){
+              rtr = getIsUsableEq( q, veq );
             }
+            //either all solves will succeed or all solves will fail
+            break;
           }
         }
       }
-      if( !rtr.isNull() ){
-        Trace("relational-trigger") << "Relational trigger : " << std::endl;
-        Trace("relational-trigger") << "    " << rtr << " (from " << n << ")" << std::endl;
-        Trace("relational-trigger") << "    in quantifier " << f << std::endl;
-        if( hasPol ){
-          Trace("relational-trigger") << "    polarity : " << pol << std::endl;
-        }
-        Node rtr2 = do_negate ? rtr.negate() : rtr;
-        Trace("relational-trigger") << "    return : " << rtr2 << std::endl;
-        return rtr2;
-      }
     }
-  }
-  bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f );
-  Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl;
-  if( usable ){
-    return n;
+    if( !rtr.isNull() ){
+      Trace("relational-trigger") << "Relational trigger : " << std::endl;
+      Trace("relational-trigger") << "    " << rtr << " (from " << n << ")" << std::endl;
+      Trace("relational-trigger") << "    in quantifier " << q << std::endl;
+      Node rtr2 = pol ? rtr : rtr.negate();
+      Trace("relational-trigger") << "    return : " << rtr2 << std::endl;
+      return rtr2;
+    }
   }else{
-    return Node::null();
+    bool usable = quantifiers::TermDb::getInstConstAttr(n)==q && isAtomicTrigger( n ) && isUsable( n, q );
+    Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==q) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
+    if( usable ){
+      return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+    }
   }
+  return Node::null();
 }
 
 bool Trigger::isUsableTrigger( Node n, Node q ){
@@ -319,6 +354,14 @@ bool Trigger::isAtomicTriggerKind( Kind k ) {
          k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON;
 }
 
+bool Trigger::isRelationalTrigger( Node n ) {
+  return isRelationalTriggerKind( n.getKind() );
+}
+
+bool Trigger::isRelationalTriggerKind( Kind k ) {
+  return k==EQUAL || k==IFF || k==GEQ;
+}
+  
 bool Trigger::isCbqiKind( Kind k ) {
   return quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ||
          k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER;
@@ -347,40 +390,63 @@ 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, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, 
-                                quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
-                                std::map< Node, int >& reqPol, std::vector< Node >& added,
+bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
+                                quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 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 ] = 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( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){
       bool rec = true;
       Node nu;
       bool nu_single = false;
       if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
-        nu = getIsUsableTrigger( n, f, pol, hasPol );
+        nu = getIsUsableTrigger( n, q );
         if( !nu.isNull() ){
-          reqPol[ nu ] = hasEPol ? ( epol ? 1 : -1 ) : 0;
-          visited[ nu ] = nu;
-          quantifiers::TermDb::computeVarContains( nu, visited_fv[ nu ] );
-          nu_single = visited_fv[nu].size()==f[0].getNumChildren();
-          retVal = true;
-          if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
-            rec = false;
+          Assert( nu.getKind()!=NOT );
+          Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
+          Node reqEq;
+          if( nu.getKind()==IFF || nu.getKind()==EQUAL ){
+            if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){
+              if( hasPol ){
+                reqEq = nu[1];
+              }
+              nu = nu[0];
+            }
+          }
+          Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) );
+          Assert( isUsableTrigger( nu, q ) );
+          //do not add if already excluded
+          bool add = true;
+          if( n!=nu ){
+            std::map< Node, Node >::iterator itvu = visited.find( nu );
+            if( itvu!=visited.end() && itvu->second.isNull() ){
+              add = false;
+            }
+          }
+          if( add ){
+            Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
+            visited[ nu ] = nu;
+            tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
+            nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
+            retVal = true;
+            if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
+              rec = false;
+            }
           }
         }
       }
       if( rec ){
+        Node nrec = nu.isNull() ? n : nu;
         std::vector< Node > added2;
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        for( unsigned i=0; i<nrec.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, visited_fv, tstrt, exclude, reqPol, added2, newPol, newHasPol, newEPol, newHasEPol ) ){
+          QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol );
+          QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
+          if( collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol ) ){
             retVal = true;
           }
         }
@@ -388,15 +454,19 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited,
           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;
+            Assert( tinfo.find( added2[i] )!=tinfo.end() );
+            if( added2[i]!=nu ){
+              if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
+                rm_nu = true;
+              }
+              added.push_back( added2[i] );
+            }else{
+              Assert( false );
             }
-            added.push_back( added2[i] );
           }
           if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
             visited[nu] = Node::null();
-            reqPol.erase( nu );
+            tinfo.erase( nu );
           }else{
             added.push_back( nu );
           }
@@ -448,7 +518,7 @@ int Trigger::getTriggerWeight( Node n ) {
     return 0;
   }else{
     if( options::relationalTriggers() ){
-      if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
+      if( isRelationalTrigger( n ) ){
         for( unsigned i=0; i<2; i++ ){
           if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermDb::hasInstConstAttr( n[1-i] ) ){
             return 0;
@@ -492,17 +562,17 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector<
   return true;
 }
 
-void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
-                               std::map< Node, int >& reqPol, bool filterInst ){
+void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
+                               std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){
   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;
-    std::map< Node, int > reqPol2;
-    collectPatTerms( qe, f, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol2, false );
+    std::map< Node, TriggerTermInfo > tinfo2;
+    collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false );
     std::vector< Node > temp;
     temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
-    qe->getTermDatabase()->filterInstances( temp );
+    quantifiers::TermDb::filterInstances( temp );
     if( temp.size()!=patTerms2.size() ){
       Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl;
       Trace("trigger-filter-instance") << "Old: ";
@@ -517,7 +587,10 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
     }
     if( tstrt==quantifiers::TRIGGER_SEL_ALL ){
       for( unsigned i=0; i<temp.size(); i++ ){
-        reqPol[temp[i]] = reqPol2[temp[i]];
+        //copy information
+        tinfo[temp[i]].d_fv.insert( tinfo[temp[i]].d_fv.end(), tinfo2[temp[i]].d_fv.begin(), tinfo2[temp[i]].d_fv.end() );
+        tinfo[temp[i]].d_reqPol = tinfo2[temp[i]].d_reqPol;
+        tinfo[temp[i]].d_reqPolEq = tinfo2[temp[i]].d_reqPolEq;
         patTerms.push_back( temp[i] );
       }
       return;
@@ -530,10 +603,9 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
       }
     }
   }
-  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 ){
+  collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true );
+  for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){
     if( !visited[it->first].isNull() ){
       patTerms.push_back( it->first );
     }
@@ -615,15 +687,15 @@ Node Trigger::getInversion( Node n, Node x ) {
   return Node::null();
 }
 
-void Trigger::getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ) {
+void Trigger::getTriggerVariables( Node icn, Node q, std::vector< Node >& t_vars ) {
   std::vector< Node > patTerms;
-  std::map< Node, int > reqPol;
+  std::map< Node, TriggerTermInfo > tinfo;
   //collect all patterns from icn
   std::vector< Node > exclude;
-  collectPatTerms( qe, f, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, reqPol );
+  collectPatTerms( q, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo );
   //collect all variables from all patterns in patTerms, add to t_vars
   for( unsigned i=0; i<patTerms.size(); i++ ){
-    qe->getTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars );
+    quantifiers::TermDb::getVarContainsNode( q, patTerms[i], t_vars );
   }
 }
 
@@ -655,7 +727,7 @@ InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) {
 
 Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
   if( nodes.empty() ){
-    return d_tr;
+    return d_tr.empty() ? NULL : d_tr[0];
   }else{
     Node n = nodes.back();
     nodes.pop_back();
@@ -669,13 +741,7 @@ Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
 
 void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
   if( nodes.empty() ){
-    if(d_tr != NULL){
-      // TODO: Andy can you look at fmf/QEpres-uf.855035.smt?
-      delete d_tr;
-      d_tr = NULL;
-    }
-    Assert(d_tr == NULL);
-    d_tr = t;
+    d_tr.push_back( t );
   }else{
     Node n = nodes.back();
     nodes.pop_back();
@@ -688,7 +754,6 @@ void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
 
 
 TriggerTrie::TriggerTrie()
-    : d_tr( NULL )
 {}
 
 TriggerTrie::~TriggerTrie() {
@@ -699,7 +764,9 @@ TriggerTrie::~TriggerTrie() {
   }
   d_children.clear();
 
-  if(d_tr != NULL) { delete d_tr; }
+  for( unsigned i=0; i<d_tr.size(); i++ ){
+    delete d_tr[i];
+  }
 }
 
 }/* CVC4::theory::inst namespace */
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 06e9011c7..41f2a1c38 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -42,6 +42,16 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
+class TriggerTermInfo {
+public:
+  TriggerTermInfo() : d_reqPol(0){}
+  ~TriggerTermInfo(){}
+  std::vector< Node > d_fv;
+  int d_reqPol;
+  Node d_reqPolEq;
+  void init( Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null() );
+};
+
 /** A collect of nodes representing a trigger. */
 class Trigger {
  public:
@@ -91,14 +101,16 @@ class Trigger {
   static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n,
                              int matchOption = 0, bool keepAll = true,
                              int trOption = TR_MAKE_NEW );
-  static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n,
-                               std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt,
-                               std::vector< Node >& exclude, std::map< Node, int >& reqPol,
+  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 );
   /** is usable trigger */
   static bool isUsableTrigger( Node n, Node q );
+  static Node getIsUsableTrigger( Node n, Node q );
   static bool isAtomicTrigger( Node n );
   static bool isAtomicTriggerKind( Kind k );
+  static bool isRelationalTrigger( Node n );
+  static bool isRelationalTriggerKind( Kind k );
   static bool isCbqiKind( Kind k );
   static bool isSimpleTrigger( Node n );
   static bool isBooleanTermTrigger( Node n );
@@ -111,8 +123,7 @@ class Trigger {
   static Node getInversionVariable( Node n );
   static Node getInversion( Node n, Node x );
   /** get all variables that E-matching can possibly handle */
-  static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f,
-                                   std::vector< Node >& t_vars );
+  static void getTriggerVariables( Node icn, Node f, std::vector< Node >& t_vars );
 
   void debugPrint( const char * c ) {
     Trace(c) << "TRIGGER( ";
@@ -122,19 +133,17 @@ class Trigger {
     }
     Trace(c) << " )";
   }
-
 private:
   /** trigger constructor */
   Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0 );
 
   /** is subterm of trigger usable */
   static bool isUsable( Node n, Node q );
-  static Node getIsUsableTrigger( Node n, Node f, bool pol = true,
-                                  bool hasPol = false );
+  static Node getIsUsableEq( Node q, Node eq );
+  static bool isUsableEqTerms( Node q, Node n1, Node n2 );
   /** collect all APPLY_UF pattern terms for f in n */
-  static bool collectPatTerms2( Node f, Node n, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& visited_fv, 
-                                quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
-                                std::map< Node, int >& reqPol, std::vector< Node >& added,
+  static bool collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
+                                quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
                                 bool pol, bool hasPol, bool epol, bool hasEPol );
 
   std::vector< Node > d_nodes;
@@ -169,7 +178,7 @@ private:
   inst::Trigger* getTrigger2( std::vector< Node >& nodes );
   void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
 
-  inst::Trigger* d_tr;
+  std::vector< inst::Trigger* > d_tr;
   std::map< TNode, TriggerTrie* > d_children;
 };/* class inst::Trigger::TriggerTrie */