From 59b935c1af18ec51efacf87b0e45d9134d3aaa1e Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2016 09:38:41 -0500
Subject: [PATCH] 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.

---
 .../quantifiers/inst_match_generator.cpp      |   4 +-
 .../quantifiers/inst_strategy_e_matching.cpp  | 104 ++++---
 .../quantifiers/inst_strategy_e_matching.h    |   1 +
 src/theory/quantifiers/macros.cpp             |   2 +-
 src/theory/quantifiers/quant_util.h           |   2 +
 .../quantifiers/quantifiers_rewriter.cpp      |  26 +-
 src/theory/quantifiers/term_database.cpp      |  90 +++---
 src/theory/quantifiers/term_database.h        |  13 +-
 src/theory/quantifiers/trigger.cpp            | 261 +++++++++++-------
 src/theory/quantifiers/trigger.h              |  33 ++-
 src/theory/quantifiers_engine.cpp             | 170 ++++++------
 src/theory/quantifiers_engine.h               |  14 +-
 test/regress/regress0/quantifiers/Makefile.am |   3 +-
 .../regress0/quantifiers/double-pattern.smt2  |   6 +
 14 files changed, 442 insertions(+), 287 deletions(-)
 create mode 100644 test/regress/regress0/quantifiers/double-pattern.smt2

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 */
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1a2762409..d31865f35 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -142,6 +142,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_rel_dom = NULL;
   d_builder = NULL;
 
+  d_curr_effort_level = QEFFORT_NONE;
   d_total_inst_count_debug = 0;
   //allow theory combination to go first, once initially
   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
@@ -463,6 +464,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
     for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){
+      d_curr_effort_level = quant_e;
       bool success = true;
       //build the model if any module requested it
       if( needsModelE==quant_e ){
@@ -522,6 +524,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
         }
       }
     }
+    d_curr_effort_level = QEFFORT_NONE;
     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
     if( d_hasAddedLemma ){
       //debug information
@@ -756,67 +759,6 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No
   }
 }
 
-bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
-  Assert( f.getKind()==FORALL );
-  Assert( vars.size()==terms.size() );
-  Node body = getInstantiation( f, vars, terms, doVts );  //do virtual term substitution
-  body = quantifiers::QuantifiersRewriter::preprocess( body, true );
-  Trace("inst-debug") << "...preprocess to " << body << std::endl;
-  Trace("inst-assert") << "(assert " << body << ")" << std::endl;
-  //make the lemma
-  Node lem = NodeManager::currentNM()->mkNode( kind::OR, f.negate(), body );
-  //check for duplication
-  if( addLemma( lem ) ){
-    d_total_inst_debug[f]++;
-    d_temp_inst_debug[f]++;
-    d_total_inst_count_debug++;
-    Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
-    for( unsigned i=0; i<terms.size(); i++ ){
-      if( Trace.isOn("inst") ){
-        Trace("inst") << "   " << terms[i];
-        if( Trace.isOn("inst-debug") ){
-          Trace("inst-debug") << ", type=" << terms[i].getType() << ", var_type=" << f[0][i].getType();
-        }
-        Trace("inst") << std::endl;
-      }
-      if( options::cbqi() ){
-        Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
-        bool bad_inst = false;
-        if( !icf.isNull() ){
-          if( icf==f ){
-            bad_inst = true;
-          }else{
-            bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[f] );
-          }
-        }
-        if( bad_inst ){
-          Trace("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
-          for( unsigned i=0; i<terms.size(); i++ ){
-            Trace("inst") << "   " << terms[i] << std::endl;
-          }
-          Unreachable("Bad instantiation");
-        }
-      }
-      Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) );
-    }
-    if( options::instMaxLevel()!=-1 ){
-      uint64_t maxInstLevel = 0;
-      for( unsigned i=0; i<terms.size(); i++ ){
-        if( terms[i].hasAttribute(InstLevelAttribute()) ){
-          if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
-            maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
-          }
-        }
-      }
-      setInstantiationLevelAttr( body, f[1], maxInstLevel+1 );
-    }
-    ++(d_statistics.d_instantiations);
-    return true;
-  }else{
-    ++(d_statistics.d_inst_duplicate);
-    return false;
-  }
-}
 
 bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst ) {
   if( options::incrementalSolving() ){
@@ -847,7 +789,7 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t lev
       Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
     }
     Assert( n.getNumChildren()==qn.getNumChildren() );
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
       setInstantiationLevelAttr( n[i], qn[i], level );
     }
   }
@@ -859,7 +801,7 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
     n.setAttribute(ila,level);
     Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
   }
-  for( int i=0; i<(int)n.getNumChildren(); i++ ){
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
     setInstantiationLevelAttr( n[i], level );
   }
 }
@@ -970,9 +912,11 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
 }
 */
 
-bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
+bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
   if( doCache ){
-    lem = Rewriter::rewrite(lem);
+    if( doRewrite ){
+      lem = Rewriter::rewrite(lem);
+    }
     Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
     if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
       //d_curr_out->lemma( lem, false, true );
@@ -985,6 +929,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
       return false;
     }
   }else{
+    //do not need to rewrite, will be rewritten after sending
     d_lemmas_waiting.push_back( lem );
     return true;
   }
@@ -1012,7 +957,6 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
     if( terms[i].isNull() ){
       terms[i] = d_term_db->getModelBasisTerm( q[0][i].getType() );
     }
-    //make it representative, this is helpful for recognizing duplication
     if( mkRep ){
       //pick the best possible representative for instantiation, based on past use and simplicity of term
       terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i );
@@ -1026,7 +970,29 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
       return false;
     }
 #ifdef CVC4_ASSERTIONS
-    Assert( !quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) );
+    bool bad_inst = false;
+    if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){
+      bad_inst = true;
+    }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){
+      bad_inst = true;
+    }else if( options::cbqi() ){
+      Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
+      if( !icf.isNull() ){
+        if( icf==q ){
+          bad_inst = true;
+        }else{
+          bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] );
+        }      
+      }
+    }
+    //this assertion is critical to soundness
+    if( bad_inst ){
+      Trace("inst")<< "***& Bad Instantiate " << q << " with " << std::endl;
+      for( unsigned j=0; j<terms.size(); j++ ){
+        Trace("inst") << "   " << terms[j] << std::endl;
+      }
+      Assert( false );
+    }      
 #endif
   }
 
@@ -1038,7 +1004,8 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
       }
     }
   }
-  //check for entailment
+  
+  //check for positive entailment
   if( options::instNoEntail() ){
     std::map< TNode, TNode > subs;
     for( unsigned i=0; i<terms.size(); i++ ){
@@ -1053,7 +1020,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
     //Trace("ajr-temp") << "   " << eval << std::endl;
   }
 
-  //check for duplication
+  //check for term vector duplication
   bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst );
   if( alreadyExists ){
     Trace("inst-add-debug") << " -> Already exists." << std::endl;
@@ -1061,16 +1028,57 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
     return false;
   }
 
-
-  //add the instantiation
+  //construct the instantiation
   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
-  bool addedInst = addInstantiationInternal( q, d_term_db->d_vars[q], terms, doVts );
-  //report the result
-  if( addedInst ){
+  Assert( d_term_db->d_vars[q].size()==terms.size() );
+  Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts );  //do virtual term substitution
+  body = quantifiers::QuantifiersRewriter::preprocess( body, true );
+  Trace("inst-debug") << "...preprocess to " << body << std::endl;
+
+  //construct the lemma  
+  Trace("inst-assert") << "(assert " << body << ")" << std::endl;
+  body = Rewriter::rewrite(body);
+  Node lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
+  lem = Rewriter::rewrite(lem);
+
+  //check for lemma duplication
+  if( addLemma( lem, true, false ) ){
+    d_total_inst_debug[q]++;
+    d_temp_inst_debug[q]++;
+    d_total_inst_count_debug++;
+    if( Trace.isOn("inst") ){
+      Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
+      for( unsigned i=0; i<terms.size(); i++ ){
+        if( Trace.isOn("inst") ){
+          Trace("inst") << "   " << terms[i];
+          if( Trace.isOn("inst-debug") ){
+            Trace("inst-debug") << ", type=" << terms[i].getType() << ", var_type=" << q[0][i].getType();
+          }
+          Trace("inst") << std::endl;
+        }
+      }
+    }
+    if( options::instMaxLevel()!=-1 ){
+      uint64_t maxInstLevel = 0;
+      for( unsigned i=0; i<terms.size(); i++ ){
+        if( terms[i].hasAttribute(InstLevelAttribute()) ){
+          if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
+            maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
+          }
+        }
+      }
+      setInstantiationLevelAttr( body, q[1], maxInstLevel+1 );
+    }
+    //notify listeners
+    for( unsigned j=0; j<d_inst_notify.size(); j++ ){
+      d_inst_notify[j]->notifyInstantiation( q, lem, terms, body );
+    }
     Trace("inst-add-debug") << " -> Success." << std::endl;
+    ++(d_statistics.d_instantiations);
     return true;
   }else{
     Trace("inst-add-debug") << " -> Lemma already exists." << std::endl;
+    ++(d_statistics.d_inst_duplicate);
     return false;
   }
 }
@@ -1380,13 +1388,17 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
 }
 
 bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
-  eq::EqualityEngine* ee = getEngine();
-  if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-    if( ee->areDisequal( a, b, false ) ){
-      return true;
+  if( a==b ){
+    return false;
+  }else{
+    eq::EqualityEngine* ee = getEngine();
+    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+      if( ee->areDisequal( a, b, false ) ){
+        return true;
+      }
     }
+    return false;
   }
-  return false;
 }
 
 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 641c7624e..cdf7c3b89 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -81,6 +81,12 @@ public:
   quantifiers::TermDb * getTermDatabase();
 };/* class QuantifiersModule */
 
+class InstantiationNotify {
+public:
+  InstantiationNotify(){}
+  virtual void notifyInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+};
+
 namespace quantifiers {
   class FirstOrderModel;
   //modules
@@ -128,6 +134,8 @@ private:
   TheoryEngine* d_te;
   /** vector of modules for quantifiers */
   std::vector< QuantifiersModule* > d_modules;
+  /** instantiation notify */
+  std::vector< InstantiationNotify* > d_inst_notify;
   /** equality query class */
   EqualityQueryQuantifiersEngine* d_eq_query;
   /** for computing relevance of quantifiers */
@@ -176,6 +184,8 @@ public: //effort levels
     QEFFORT_NONE,
   };
 private:
+  /** current effort level */
+  unsigned d_curr_effort_level;
   /** list of all quantifiers seen */
   std::map< Node, bool > d_quants;
   /** quantifiers reduced */
@@ -303,8 +313,6 @@ private:
   bool reduceQuantifier( Node q );
   /** compute term vector */
   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
-  /** instantiate f with arguments terms */
-  bool addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
   /** record instantiation, return true if it was non-duplicate */
   bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false );
   /** set instantiation level attr */
@@ -321,7 +329,7 @@ public:
   /** do substitution */
   Node getSubstitute( Node n, std::vector< Node >& terms );
   /** add lemma lem */
-  bool addLemma( Node lem, bool doCache = true );
+  bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
   /** add require phase */
   void addRequirePhase( Node lit, bool req );
   /** do instantiation specified by m */
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index f0c9b5a33..784eaf677 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -76,7 +76,8 @@ TESTS =	\
 	subtype-param.smt2 \
 	anti-sk-simp.smt2 \
 	pure_dt_cbqi.smt2 \
-	florian-case-ax.smt2
+	florian-case-ax.smt2 \
+	double-pattern.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/double-pattern.smt2 b/test/regress/regress0/quantifiers/double-pattern.smt2
new file mode 100644
index 000000000..4ce21d446
--- /dev/null
+++ b/test/regress/regress0/quantifiers/double-pattern.smt2
@@ -0,0 +1,6 @@
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int)) (! (! (P x) :pattern ((P x))) :pattern ((P x)))))
+(assert (not (P 0)))
+(check-sat)
-- 
2.30.2