From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 24 Jan 2021 19:55:50 +0000 (-0600)
Subject:  Initial cleaning of e-matching instantiation strategy (#5796)
X-Git-Tag: cvc5-1.0.0~2362
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ae541bb35e7b627f28b13eede29f5870f42b078e;p=cvc5.git

 Initial cleaning of e-matching instantiation strategy (#5796)

In preparation for splitting this into multiple files.

No behavior changes in this PR.
---

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 7dcb9b797..8947370cd 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -22,8 +22,6 @@
 #include "theory/theory_engine.h"
 #include "util/random.h"
 
-using namespace std;
-
 namespace CVC4 {
 
 using namespace kind;
@@ -45,15 +43,14 @@ struct sortQuantifiersForSymbol {
   QuantRelevance* d_quant_rel;
   std::map< Node, Node > d_op_map;
   bool operator() (Node i, Node j) {
-    int nqfsi = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[i]);
-    int nqfsj = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[j]);
+    size_t nqfsi = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[i]);
+    size_t nqfsj = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[j]);
     if( nqfsi<nqfsj ){
       return true;
     }else if( nqfsi>nqfsj ){
       return false;
-    }else{
-      return false;
     }
+    return false;
   }
 };
 
@@ -63,19 +60,20 @@ struct sortTriggers {
     int wj = Trigger::getTriggerWeight( j );
     if( wi==wj ){
       return i<j;
-    }else{
-      return wi<wj;
     }
+    return wi < wj;
   }
 };
 
 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++ ){
-      it->second[i]->resetInstantiationRound();
-      it->second[i]->reset( Node::null() );
+  for (std::pair<const Node, std::vector<Trigger*> >& u : d_user_gen)
+  {
+    for (Trigger* t : u.second)
+    {
+      t->resetInstantiationRound();
+      t->reset(Node::null());
     }
   }
   Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
@@ -84,44 +82,57 @@ void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort ef
 int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
   if( e==0 ){
     return STATUS_UNFINISHED;
-  }else{
-    int peffort =
-        d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT ? 2
-                                                                            : 1;
-    if( e<peffort ){
-      return STATUS_UNFINISHED;
-    }else if( e==peffort ){
-      d_counter[f]++;
+  }
+  options::UserPatMode upm = d_quantEngine->getInstUserPatMode();
+  int peffort = upm == options::UserPatMode::RESORT ? 2 : 1;
+  if (e < peffort)
+  {
+    return STATUS_UNFINISHED;
+  }
+  if (e != peffort)
+  {
+    return STATUS_UNKNOWN;
+  }
+  d_counter[f]++;
 
-      Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl;
-      if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+  Trace("inst-alg") << "-> User-provided instantiate " << f << "..."
+                    << std::endl;
+  if (upm == options::UserPatMode::RESORT)
+  {
+    std::vector<std::vector<Node> >& ugw = d_user_gen_wait[f];
+    for (size_t i = 0, usize = ugw.size(); i < usize; i++)
+    {
+      Trigger* t = Trigger::mkTrigger(
+          d_quantEngine, f, ugw[i], true, Trigger::TR_RETURN_NULL);
+      if (t)
       {
-        for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){
-          Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], true, Trigger::TR_RETURN_NULL );
-          if( t ){
-            d_user_gen[f].push_back( t );
-          }
-        }
-        d_user_gen_wait[f].clear();
+        d_user_gen[f].push_back(t);
       }
+    }
+    ugw.clear();
+  }
 
-      for( unsigned i=0; i<d_user_gen[f].size(); i++ ){
-        bool processTrigger = true;
-        if( processTrigger ){
-          Trace("process-trigger") << "  Process (user) ";
-          d_user_gen[f][i]->debugPrint("process-trigger");
-          Trace("process-trigger") << "..." << std::endl;
-          int numInst = d_user_gen[f][i]->addInstantiations();
-          Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
-          d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
-          if( d_user_gen[f][i]->isMultiTrigger() ){
-            d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
-          }
-          if( d_quantEngine->inConflict() ){
-            break;
-          }
-        }
-      }
+  std::vector<inst::Trigger*>& ug = d_user_gen[f];
+  for (Trigger* t : ug)
+  {
+    if (Trace.isOn("process-trigger"))
+    {
+      Trace("process-trigger") << "  Process (user) ";
+      t->debugPrint("process-trigger");
+      Trace("process-trigger") << "..." << std::endl;
+    }
+    unsigned numInst = t->addInstantiations();
+    Trace("process-trigger")
+        << "  Done, numInst = " << numInst << "." << std::endl;
+    d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
+    if (t->isMultiTrigger())
+    {
+      d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+    }
+    if (d_quantEngine->inConflict())
+    {
+      // we are already in conflict
+      break;
     }
   }
   return STATUS_UNKNOWN;
@@ -130,33 +141,36 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
 void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
   Assert(pat.getKind() == INST_PATTERN);
   //add to generators
-  bool usable = true;
   std::vector< Node > nodes;
-  for( unsigned i=0; i<pat.getNumChildren(); i++ ){
-    Node pat_use = Trigger::getIsUsableTrigger( pat[i], q );
+  for (const Node& p : pat)
+  {
+    Node pat_use = Trigger::getIsUsableTrigger(p, q);
     if( pat_use.isNull() ){
-      Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl;
-      usable = false;
-      break;
+      Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
+                            << " because of " << p << std::endl;
+      return;
     }else{
       nodes.push_back( pat_use );
     }
   }
-  if( usable ){
-    Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
-    //check match option
-    if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+  Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
+  // check match option
+  if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+  {
+    d_user_gen_wait[q].push_back(nodes);
+  }
+  else
+  {
+    Trigger* t =
+        Trigger::mkTrigger(d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW);
+    if (t)
     {
-      d_user_gen_wait[q].push_back( nodes );
+      d_user_gen[q].push_back(t);
     }
     else
     {
-      Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, 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;
-      }
+      Trace("trigger-warn") << "Failed to construct trigger : " << pat
+                            << " due to variable mismatch" << std::endl;
     }
   }
 }
@@ -181,10 +195,16 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::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 ){
-      for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
-        itt->first->resetInstantiationRound();
-        itt->first->reset( Node::null() );
+    std::map<Node, std::map<inst::Trigger*, bool> >& agts =
+        d_auto_gen_trigger[r];
+    for (std::pair<const Node, std::map<inst::Trigger*, bool> >& agt : agts)
+    {
+      for (std::map<inst::Trigger*, bool>::iterator it = agt.second.begin();
+           it != agt.second.end();
+           ++it)
+      {
+        it->first->resetInstantiationRound();
+        it->first->reset(Node::null());
       }
     }
   }
@@ -198,364 +218,492 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
   {
     return STATUS_UNKNOWN;
   }
-  else
+  int peffort = (hasUserPatterns(f) && upMode != options::UserPatMode::IGNORE
+                 && upMode != options::UserPatMode::RESORT)
+                    ? 2
+                    : 1;
+  if (e < peffort)
   {
-    int peffort = (hasUserPatterns(f) && upMode != options::UserPatMode::IGNORE
-                   && upMode != options::UserPatMode::RESORT)
-                      ? 2
-                      : 1;
-    if( e<peffort ){
-      return STATUS_UNFINISHED;
+    return STATUS_UNFINISHED;
+  }
+  Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
+  bool gen = false;
+  if (e == peffort)
+  {
+    if (d_counter.find(f) == d_counter.end())
+    {
+      d_counter[f] = 0;
+      gen = true;
     }else{
-      Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
-      bool gen = false;
-      if( e==peffort ){
-        if( d_counter.find( f )==d_counter.end() ){
-          d_counter[f] = 0;
-          gen = true;
-        }else{
-          d_counter[f]++;
-          gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;
+      d_counter[f]++;
+      gen = d_regenerate && d_counter[f] % d_regenerate_frequency == 0;
+    }
+  }
+  else
+  {
+    gen = true;
+  }
+  if (gen)
+  {
+    generateTriggers(f);
+    if (d_counter[f] == 0 && d_auto_gen_trigger[0][f].empty()
+        && d_auto_gen_trigger[1][f].empty() && f.getNumChildren() == 2)
+    {
+      Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
+    }
+  }
+  if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL)
+  {
+    int max_score = -1;
+    Trigger* max_trigger = nullptr;
+    std::map<Trigger*, bool>& agt = d_auto_gen_trigger[0][f];
+    for (std::map<Trigger*, bool>::iterator it = agt.begin(); it != agt.end();
+         ++it)
+    {
+      Trigger* t = it->first;
+      int score = t->getActiveScore();
+      if (options::triggerActiveSelMode() == options::TriggerActiveSelMode::MIN)
+      {
+        if (score >= 0 && (score < max_score || max_score < 0))
+        {
+          max_score = score;
+          max_trigger = t;
         }
-      }else{
-        gen = true;
       }
-      if( gen ){
-        generateTriggers( f );
-        if( d_counter[f]==0 && d_auto_gen_trigger[0][f].empty() && d_auto_gen_trigger[1][f].empty() && f.getNumChildren()==2 ){
-          Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
+      else
+      {
+        if (score > max_score)
+        {
+          max_score = score;
+          max_trigger = t;
         }
       }
+      agt[t] = false;
+    }
+    if (max_trigger != nullptr)
+    {
+      agt[max_trigger] = true;
+    }
+  }
 
-      //if( e==4 ){
-      //  d_processed_trigger.clear();
-      //  d_quantEngine->getEqualityQuery()->setLiberal( true );
-      //}
-      if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL)
+  bool hasInst = false;
+  for (unsigned r = 0; r < 2; r++)
+  {
+    std::map<Trigger*, bool>& agt = d_auto_gen_trigger[r][f];
+    for (std::map<Trigger*, bool>::iterator it = agt.begin(); it != agt.end();
+         ++it)
+    {
+      Trigger* tr = it->first;
+      if (tr == nullptr || !it->second)
       {
-        int max_score = -1;
-        Trigger * max_trigger = NULL;
-        for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[0][f].begin(); itt != d_auto_gen_trigger[0][f].end(); ++itt ){
-          int score = itt->first->getActiveScore();
-          if (options::triggerActiveSelMode()
-              == options::TriggerActiveSelMode::MIN)
-          {
-            if( score>=0 && ( score<max_score || max_score<0 ) ){
-              max_score = score;
-              max_trigger = itt->first;
-            }
-          }
-          else
-          {
-            if( score>max_score ){
-              max_score = score;
-              max_trigger = itt->first;
-            }
-          }
-          d_auto_gen_trigger[0][f][itt->first] = false;
-        }
-        if( max_trigger!=NULL ){
-          d_auto_gen_trigger[0][f][max_trigger] = true;
-        }
+        // trigger is null or currently disabled
+        continue;
       }
-
-      bool hasInst = false;
-      for( unsigned r=0; r<2; r++ ){
-        for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[r][f].begin(); itt != d_auto_gen_trigger[r][f].end(); ++itt ){
-          Trigger* tr = itt->first;
-          if( tr ){
-            bool processTrigger = itt->second;
-            if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){
-              d_processed_trigger[f][tr] = true;
-              Trace("process-trigger") << "  Process ";
-              tr->debugPrint("process-trigger");
-              Trace("process-trigger") << "..." << std::endl;
-              int numInst = tr->addInstantiations();
-              hasInst = numInst>0 || hasInst;
-              Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
-              d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst;
-              if( r==1 ){
-                d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
-              }
-              if( d_quantEngine->inConflict() ){
-                break;
-              }
-            }
-          }
-        }
-        if( d_quantEngine->inConflict() || ( hasInst && options::multiTriggerPriority() ) ){
-          break;
-        }
+      if (d_processed_trigger[f].find(tr) != d_processed_trigger[f].end())
+      {
+        // trigger is already processed this round
+        continue;
+      }
+      d_processed_trigger[f][tr] = true;
+      Trace("process-trigger") << "  Process ";
+      tr->debugPrint("process-trigger");
+      Trace("process-trigger") << "..." << std::endl;
+      unsigned numInst = tr->addInstantiations();
+      hasInst = numInst > 0 || hasInst;
+      Trace("process-trigger")
+          << "  Done, numInst = " << numInst << "." << std::endl;
+      d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst;
+      if (r == 1)
+      {
+        d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+      }
+      if (d_quantEngine->inConflict())
+      {
+        break;
       }
-      //if( e==4 ){
-      //  d_quantEngine->getEqualityQuery()->setLiberal( false );
-      //}
-      return STATUS_UNKNOWN;
+    }
+    if (d_quantEngine->inConflict()
+        || (hasInst && options::multiTriggerPriority()))
+    {
+      break;
     }
   }
+  return STATUS_UNKNOWN;
 }
 
 void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
   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, inst::TriggerTermInfo > tinfo;
-    //well-defined function: can assume LHS is only trigger
-    if( options::quantFunWellDefined() ){
-      Node hd = QuantAttributes::getFunDefHead( f );
-      if( !hd.isNull() ){
-        hd = d_quantEngine->getTermUtil()
-                 ->substituteBoundVariablesToInstConstants(hd, f);
-        patTermsF.push_back( hd );
-        tinfo[hd].init( f, hd );
+
+  // first, generate the set of pattern terms
+  if (!generatePatternTerms(f))
+  {
+    Trace("auto-gen-trigger-debug")
+        << "...failed to generate pattern terms" << std::endl;
+    return;
+  }
+
+  // then, group them to make triggers
+  unsigned rmin = d_patTerms[0][f].empty() ? 1 : 0;
+  unsigned rmax = options::multiTriggerWhenSingle() ? 1 : rmin;
+  for (unsigned r = rmin; r <= rmax; r++)
+  {
+    std::vector<Node> patTerms;
+    std::vector<Node>& ptc = d_patTerms[r][f];
+    for (const Node& p : ptc)
+    {
+      if (r == 1 || d_single_trigger_gen.find(p) == d_single_trigger_gen.end())
+      {
+        patTerms.push_back(p);
       }
     }
-    //otherwise, use algorithm for collecting pattern terms
-    if( patTermsF.empty() ){
-      Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f );
-      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 );
+    if (patTerms.empty())
+    {
+      continue;
+    }
+    Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
+    // sort terms based on relevance
+    if (options::relevantTriggers())
+    {
+      Assert(d_quant_rel);
+      sortQuantifiersForSymbol sqfs;
+      sqfs.d_quant_rel = d_quant_rel;
+      for (const Node& p : patTerms)
+      {
+        Assert(d_pat_to_mpat.find(p) != d_pat_to_mpat.end());
+        Assert(d_pat_to_mpat[p].hasOperator());
+        sqfs.d_op_map[p] = d_pat_to_mpat[p].getOperator();
       }
-      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] << std::endl;
-          Trace("auto-gen-trigger-debug2") << "     info = [" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl;
+      // sort based on # occurrences (this will cause Trigger to select rarer
+      // symbols)
+      std::sort(patTerms.begin(), patTerms.end(), sqfs);
+      if (Debug.isOn("relevant-trigger"))
+      {
+        Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
+        for (const Node& p : patTerms)
+        {
+          Debug("relevant-trigger")
+              << "   " << p << " from " << d_pat_to_mpat[p] << " (";
+          Debug("relevant-trigger") << d_quant_rel->getNumQuantifiersForSymbol(
+                                           d_pat_to_mpat[p].getOperator())
+                                    << ")" << std::endl;
         }
-        Trace("auto-gen-trigger-debug") << std::endl;
       }
     }
-    //sort into single/multi triggers, calculate which terms should not be considered
-    std::map< Node, bool > vcMap;
-    std::map< Node, bool > rmPatTermsF;
-    int last_weight = -1;
-    for( unsigned i=0; i<patTermsF.size(); i++ ){
-      Assert(patTermsF[i].getKind() != NOT);
-      bool newVar = false;
-      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;
+    // now, generate the trigger...
+    Trigger* tr = NULL;
+    if (d_is_single_trigger[patTerms[0]])
+    {
+      tr = Trigger::mkTrigger(d_quantEngine,
+                              f,
+                              patTerms[0],
+                              false,
+                              Trigger::TR_RETURN_NULL,
+                              d_num_trigger_vars[f]);
+      d_single_trigger_gen[patTerms[0]] = true;
+    }
+    else
+    {
+      // only generate multi trigger if option set, or if no single triggers
+      // exist
+      if (!d_patTerms[0][f].empty())
+      {
+        if (options::multiTriggerWhenSingle())
+        {
+          Trace("multi-trigger-debug")
+              << "Resort to choosing multi-triggers..." << std::endl;
+        }
+        else
+        {
+          return;
         }
       }
-      int curr_w = Trigger::getTriggerWeight( patTermsF[i] );
-      // triggers whose value is maximum (2) are considered expendable.
-      if (ntrivTriggers && !newVar && last_weight != -1 && curr_w > last_weight
-          && curr_w >= 2)
+      // if we are re-generating triggers, shuffle based on some method
+      if (d_made_multi_trigger[f])
       {
-        Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
-        rmPatTermsF[patTermsF[i]] = true;
-      }else{
-        last_weight = curr_w;
+        std::shuffle(patTerms.begin(),
+                     patTerms.end(),
+                     Random::getRandom());  // shuffle randomly
       }
-    }
-    d_num_trigger_vars[f] = vcMap.size();
-    if( d_num_trigger_vars[f]>0 && d_num_trigger_vars[f]<f[0].getNumChildren() ){
-      Trace("auto-gen-trigger-partial") << "Quantified formula : " << f << std::endl;
-      Trace("auto-gen-trigger-partial") << "...does not contain all variables in triggers!!!" << std::endl;
-      // Invoke partial trigger strategy: partition variables of quantified
-      // formula into (X,Y) where X are contained in a trigger and Y are not.
-      // We then force a split of the quantified formula so that it becomes:
-      //   forall X. forall Y. P( X, Y )
-      // and hence is treatable by E-matching. We only do this for "standard"
-      // quantified formulas (those with only two children), since this
-      // technique should not be used for e.g. quantifiers marked for
-      // quantifier elimination.
-      QAttributes qa;
-      QuantAttributes::computeQuantAttributes(f, qa);
-      if (options::partialTriggers() && qa.isStandard())
+      else
       {
-        std::vector< Node > vcs[2];
-        for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-          Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i );
-          vcs[ vcMap.find( ic )==vcMap.end() ? 0 : 1 ].push_back( f[0][i] );
-        }
-        for( unsigned i=0; i<2; i++ ){
-          d_vc_partition[i][f] = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, vcs[i] );
-        }
-      }else{
-        return;
+        d_made_multi_trigger[f] = true;
       }
+      // will possibly want to get an old trigger
+      tr = Trigger::mkTrigger(d_quantEngine,
+                              f,
+                              patTerms,
+                              false,
+                              Trigger::TR_GET_OLD,
+                              d_num_trigger_vars[f]);
     }
-    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;
-        Node mpat = pat;
-        //process the pattern: if it has a required polarity, consider it
-        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 ){
-          Assert(rpol == 1 || rpol == -1);
-          if( Trigger::isRelationalTrigger( pat ) ){
-            pat = rpol==-1 ? pat.negate() : pat;
-          }else{
-            Assert(Trigger::isAtomicTrigger(pat));
-            if( pat.getType().isBoolean() && rpoleq.isNull() ){
-              if (options::literalMatchMode() == options::LiteralMatchMode::USE)
-              {
-                pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
-              }
-              else if (options::literalMatchMode()
-                       != options::LiteralMatchMode::NONE)
-              {
-                pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
-              }
-            }else{
-              Assert(!rpoleq.isNull());
-              if( rpol==-1 ){
-                if (options::literalMatchMode()
-                    != options::LiteralMatchMode::NONE)
-                {
-                  //all equivalence classes except rpoleq
-                  pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
-                }
-              }else if( rpol==1 ){
-                if (options::literalMatchMode()
-                    == options::LiteralMatchMode::AGG)
-                {
-                  //only equivalence class rpoleq
-                  pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq );
-                }
-                //all equivalence classes that are not disequal to rpoleq TODO?
-              }
-            }
-          }
-          Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
-        }else{
-          if( Trigger::isRelationalTrigger( pat ) ){
-            //consider both polarities
-            addPatternToPool( f, pat.negate(), num_fv, mpat );
-          }
+    if (tr == nullptr)
+    {
+      // did not generate a trigger
+      continue;
+    }
+    addTrigger(tr, f);
+    if (tr->isMultiTrigger())
+    {
+      // only add a single multi-trigger
+      continue;
+    }
+    // if we are generating additional triggers...
+    size_t index = 0;
+    if (index < patTerms.size())
+    {
+      // check if similar patterns exist, and if so, add them additionally
+      unsigned nqfs_curr = 0;
+      if (options::relevantTriggers())
+      {
+        nqfs_curr =
+            d_quant_rel->getNumQuantifiersForSymbol(patTerms[0].getOperator());
+      }
+      index++;
+      bool success = true;
+      while (success && index < patTerms.size()
+             && d_is_single_trigger[patTerms[index]])
+      {
+        success = false;
+        if (!options::relevantTriggers()
+            || d_quant_rel->getNumQuantifiersForSymbol(
+                   patTerms[index].getOperator())
+                   <= nqfs_curr)
+        {
+          d_single_trigger_gen[patTerms[index]] = true;
+          Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
+                                            f,
+                                            patTerms[index],
+                                            false,
+                                            Trigger::TR_RETURN_NULL,
+                                            d_num_trigger_vars[f]);
+          addTrigger(tr2, f);
+          success = true;
         }
-        addPatternToPool( f, pat, num_fv, mpat );
+        index++;
       }
     }
-    //tinfo not used below this point
-    d_made_multi_trigger[f] = false;
-    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;
+  }
+}
+
+bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
+{
+  if (d_patTerms[0].find(f) != d_patTerms[0].end())
+  {
+    // already generated
+    return true;
+  }
+  // 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, inst::TriggerTermInfo> tinfo;
+  TermUtil* tu = d_quantEngine->getTermUtil();
+  NodeManager* nm = NodeManager::currentNM();
+  // well-defined function: can assume LHS is only pattern
+  if (options::quantFunWellDefined())
+  {
+    Node hd = QuantAttributes::getFunDefHead(f);
+    if (!hd.isNull())
+    {
+      hd = tu->substituteBoundVariablesToInstConstants(hd, f);
+      patTermsF.push_back(hd);
+      tinfo[hd].init(f, hd);
+    }
+  }
+  // otherwise, use algorithm for collecting pattern terms
+  if (patTermsF.empty())
+  {
+    Node bd = tu->getInstConstantBody(f);
+    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);
     }
-    if( !d_patTerms[1][f].empty() ){
-      Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
-      for( unsigned i=0; i<d_patTerms[1][f].size(); i++ ){
-        Trace("auto-gen-trigger") << "   " << d_patTerms[1][f][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 (const Node& p : patTermsF)
+      {
+        Assert(tinfo.find(p) != tinfo.end());
+        Trace("auto-gen-trigger-debug") << "   " << p << std::endl;
+        Trace("auto-gen-trigger-debug2")
+            << "     info = [" << tinfo[p].d_reqPol << ", "
+            << tinfo[p].d_reqPolEq << ", " << tinfo[p].d_fv.size() << "]"
+            << std::endl;
       }
+      Trace("auto-gen-trigger-debug") << std::endl;
     }
   }
-
-  unsigned rmin = d_patTerms[0][f].empty() ? 1 : 0;
-  unsigned rmax = options::multiTriggerWhenSingle() ? 1 : rmin;
-  for( unsigned r=rmin; r<=rmax; r++ ){
-    std::vector< Node > patTerms;
-    for( int i=0; i<(int)d_patTerms[r][f].size(); i++ ){
-      if( r==1 || d_single_trigger_gen.find( d_patTerms[r][f][i] )==d_single_trigger_gen.end() ){
-        patTerms.push_back( d_patTerms[r][f][i] );
+  // sort into single/multi triggers, calculate which terms should not be
+  // considered
+  std::map<Node, bool> vcMap;
+  std::map<Node, bool> rmPatTermsF;
+  int last_weight = -1;
+  for (const Node& p : patTermsF)
+  {
+    Assert(p.getKind() != NOT);
+    bool newVar = false;
+    inst::TriggerTermInfo& tip = tinfo[p];
+    for (const Node& v : tip.d_fv)
+    {
+      if (vcMap.find(v) == vcMap.end())
+      {
+        vcMap[v] = true;
+        newVar = true;
+      }
+    }
+    int curr_w = Trigger::getTriggerWeight(p);
+    // triggers whose value is maximum (2) are considered expendable.
+    if (ntrivTriggers && !newVar && last_weight != -1 && curr_w > last_weight
+        && curr_w >= 2)
+    {
+      Trace("auto-gen-trigger-debug")
+          << "...exclude expendible non-trivial trigger : " << p << std::endl;
+      rmPatTermsF[p] = true;
+    }
+    else
+    {
+      last_weight = curr_w;
+    }
+  }
+  d_num_trigger_vars[f] = vcMap.size();
+  if (d_num_trigger_vars[f] > 0
+      && d_num_trigger_vars[f] < f[0].getNumChildren())
+  {
+    Trace("auto-gen-trigger-partial")
+        << "Quantified formula : " << f << std::endl;
+    Trace("auto-gen-trigger-partial")
+        << "...does not contain all variables in triggers!!!" << std::endl;
+    // Invoke partial trigger strategy: partition variables of quantified
+    // formula into (X,Y) where X are contained in a trigger and Y are not.
+    // We then force a split of the quantified formula so that it becomes:
+    //   forall X. forall Y. P( X, Y )
+    // and hence is treatable by E-matching. We only do this for "standard"
+    // quantified formulas (those with only two children), since this
+    // technique should not be used for e.g. quantifiers marked for
+    // quantifier elimination.
+    QAttributes qa;
+    QuantAttributes::computeQuantAttributes(f, qa);
+    if (options::partialTriggers() && qa.isStandard())
+    {
+      std::vector<Node> vcs[2];
+      for (size_t i = 0, nchild = f[0].getNumChildren(); i < nchild; i++)
+      {
+        Node ic = tu->getInstantiationConstant(f, i);
+        vcs[vcMap.find(ic) == vcMap.end() ? 0 : 1].push_back(f[0][i]);
       }
+      for (size_t i = 0; i < 2; i++)
+      {
+        d_vc_partition[i][f] = nm->mkNode(BOUND_VAR_LIST, vcs[i]);
+      }
+    }
+    else
+    {
+      return false;
+    }
+  }
+  for (const Node& patf : patTermsF)
+  {
+    Node pat = patf;
+    if (rmPatTermsF.find(pat) != rmPatTermsF.end())
+    {
+      continue;
     }
-    if( !patTerms.empty() ){
-      Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
-      //sort terms based on relevance
-      if( options::relevantTriggers() ){
-        Assert(d_quant_rel);
-        sortQuantifiersForSymbol sqfs;
-        sqfs.d_quant_rel = d_quant_rel;
-        for( unsigned i=0; i<patTerms.size(); i++ ){
-          Assert(d_pat_to_mpat.find(patTerms[i]) != d_pat_to_mpat.end());
-          Assert(d_pat_to_mpat[patTerms[i]].hasOperator());
-          sqfs.d_op_map[ patTerms[i] ] = d_pat_to_mpat[patTerms[i]].getOperator();
-        }        
-        //sort based on # occurrences (this will cause Trigger to select rarer symbols)
-        std::sort( patTerms.begin(), patTerms.end(), sqfs );
-        if (Debug.isOn("relevant-trigger"))
+    Trace("auto-gen-trigger-debug")
+        << "...processing pattern " << pat << std::endl;
+    Node mpat = pat;
+    // process the pattern: if it has a required polarity, consider it
+    Assert(tinfo.find(pat) != tinfo.end());
+    int rpol = tinfo[pat].d_reqPol;
+    Node rpoleq = tinfo[pat].d_reqPolEq;
+    size_t 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)
+    {
+      Assert(rpol == 1 || rpol == -1);
+      if (Trigger::isRelationalTrigger(pat))
+      {
+        pat = rpol == -1 ? pat.negate() : pat;
+      }
+      else
+      {
+        Assert(Trigger::isAtomicTrigger(pat));
+        if (pat.getType().isBoolean() && rpoleq.isNull())
         {
-          Debug("relevant-trigger")
-              << "Terms based on relevance: " << std::endl;
-          for (const Node& p : patTerms)
+          if (options::literalMatchMode() == options::LiteralMatchMode::USE)
           {
-            Debug("relevant-trigger")
-                << "   " << p << " from " << d_pat_to_mpat[p] << " (";
-            Debug("relevant-trigger")
-                << d_quant_rel->getNumQuantifiersForSymbol(
-                       d_pat_to_mpat[p].getOperator())
-                << ")" << std::endl;
+            pat = pat.eqNode(nm->mkConst(rpol == -1)).negate();
           }
-        }
-      }
-      //now, generate the trigger...
-      Trigger* tr = NULL;
-      if( d_is_single_trigger[ patTerms[0] ] ){
-        tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] );
-        d_single_trigger_gen[ patTerms[0] ] = true;
-      }else{
-        //only generate multi trigger if option set, or if no single triggers exist
-        if( !d_patTerms[0][f].empty() ){
-          if( options::multiTriggerWhenSingle() ){
-            Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl;
-          }else{
-            return;
+          else if (options::literalMatchMode()
+                   != options::LiteralMatchMode::NONE)
+          {
+            pat = pat.eqNode(nm->mkConst(rpol == 1));
           }
         }
-        // if we are re-generating triggers, shuffle based on some method
-        if (d_made_multi_trigger[f])
-        {
-          std::shuffle(patTerms.begin(),
-                       patTerms.end(),
-                       Random::getRandom());  // shuffle randomly
-        }
         else
         {
-          d_made_multi_trigger[f] = true;
-        }
-        //will possibly want to get an old trigger
-        tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, false, Trigger::TR_GET_OLD, d_num_trigger_vars[f] );
-      }
-      if( tr ){
-        addTrigger( tr, f );
-        //if we are generating additional triggers...
-        if( !tr->isMultiTrigger() ){
-          unsigned index = 0;
-          if( index<patTerms.size() ){
-            //Notice() << "check add additional" << std::endl;
-            //check if similar patterns exist, and if so, add them additionally
-            unsigned nqfs_curr = 0;
-            if( options::relevantTriggers() ){
-              nqfs_curr = d_quant_rel->getNumQuantifiersForSymbol(
-                  patTerms[0].getOperator());
+          Assert(!rpoleq.isNull());
+          if (rpol == -1)
+          {
+            if (options::literalMatchMode() != options::LiteralMatchMode::NONE)
+            {
+              // all equivalence classes except rpoleq
+              pat = pat.eqNode(rpoleq).negate();
             }
-            index++;
-            bool success = true;
-            while( success && index<patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
-              success = false;
-              if (!options::relevantTriggers()
-                  || d_quant_rel->getNumQuantifiersForSymbol(
-                         patTerms[index].getOperator())
-                         <= nqfs_curr)
-              {
-                d_single_trigger_gen[ patTerms[index] ] = true;
-                Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] );
-                addTrigger( tr2, f );
-                success = true;
-              }
-              index++;
+          }
+          else if (rpol == 1)
+          {
+            if (options::literalMatchMode() == options::LiteralMatchMode::AGG)
+            {
+              // only equivalence class rpoleq
+              pat = pat.eqNode(rpoleq);
             }
-            //Notice() << "done check add additional" << std::endl;
           }
         }
       }
+      Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
+    }
+    else
+    {
+      if (Trigger::isRelationalTrigger(pat))
+      {
+        // consider both polarities
+        addPatternToPool(f, pat.negate(), num_fv, mpat);
+      }
+    }
+    addPatternToPool(f, pat, num_fv, mpat);
+  }
+  // tinfo not used below this point
+  d_made_multi_trigger[f] = false;
+  if (Trace.isOn("auto-gen-trigger"))
+  {
+    Trace("auto-gen-trigger")
+        << "Single trigger pool for " << f << " : " << std::endl;
+    std::vector<Node>& spats = d_patTerms[0][f];
+    for (size_t i = 0, psize = spats.size(); i < psize; i++)
+    {
+      Trace("auto-gen-trigger") << "   " << spats[i] << std::endl;
+    }
+    std::vector<Node>& mpats = d_patTerms[0][f];
+    if (!mpats.empty())
+    {
+      Trace("auto-gen-trigger")
+          << "Multi-trigger term pool for " << f << " : " << std::endl;
+      for (size_t i = 0, psize = mpats.size(); i < psize; i++)
+      {
+        Trace("auto-gen-trigger") << "   " << mpats[i] << std::endl;
+      }
     }
   }
+  return true;
 }
 
 void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ) {
@@ -573,65 +721,85 @@ void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned n
 
 
 void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
-  if( tr ){
-    if( d_num_trigger_vars[q]<q[0].getNumChildren() ){
-      //partial trigger : generate implication to mark user pattern
-      Node pat =
-          d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables(
-              tr->getInstPattern(), q);
-      Node ipl = NodeManager::currentNM()->mkNode(INST_PATTERN_LIST, pat);
-      Node qq = NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[1][q], NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[0][q], q[1] ), ipl );
-      Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl;
-      Trace("auto-gen-trigger-partial") << "  " << qq << std::endl;
-      Node lem = NodeManager::currentNM()->mkNode( OR, q.negate(), qq );
-      d_quantEngine->addLemma( lem );
-    }else{
-      unsigned tindex;
-      if( tr->isMultiTrigger() ){
-        //disable all other multi triggers
-        for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][q].begin(); it != d_auto_gen_trigger[1][q].end(); ++it ){
-          d_auto_gen_trigger[1][q][ it->first ] = false;
-        }
-        tindex = 1;
-      }else{
-        tindex = 0;
-      }
-      //making it during an instantiation round, so must reset
-      if( d_auto_gen_trigger[tindex][q].find( tr )==d_auto_gen_trigger[tindex][q].end() ){
-        tr->resetInstantiationRound();
-        tr->reset( Node::null() );
-      }
-      d_auto_gen_trigger[tindex][q][tr] = true;
+  if (tr == nullptr)
+  {
+    return;
+  }
+  if (d_num_trigger_vars[q] < q[0].getNumChildren())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    // partial trigger : generate implication to mark user pattern
+    Node pat =
+        d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables(
+            tr->getInstPattern(), q);
+    Node ipl = nm->mkNode(INST_PATTERN_LIST, pat);
+    Node qq = nm->mkNode(FORALL,
+                         d_vc_partition[1][q],
+                         nm->mkNode(FORALL, d_vc_partition[0][q], q[1]),
+                         ipl);
+    Trace("auto-gen-trigger-partial")
+        << "Make partially specified user pattern: " << std::endl;
+    Trace("auto-gen-trigger-partial") << "  " << qq << std::endl;
+    Node lem = nm->mkNode(OR, q.negate(), qq);
+    d_quantEngine->addLemma(lem);
+    return;
+  }
+  unsigned tindex;
+  if (tr->isMultiTrigger())
+  {
+    // disable all other multi triggers
+    std::map<Trigger*, bool>& agt = d_auto_gen_trigger[1][q];
+    for (std::map<Trigger*, bool>::iterator it = agt.begin(); it != agt.end();
+         ++it)
+    {
+      agt[it->first] = false;
     }
+    tindex = 1;
+  }
+  else
+  {
+    tindex = 0;
+  }
+  // making it during an instantiation round, so must reset
+  std::map<Trigger*, bool>& agt = d_auto_gen_trigger[tindex][q];
+  if (agt.find(tr) == agt.end())
+  {
+    tr->resetInstantiationRound();
+    tr->reset(Node::null());
   }
+  agt[tr] = true;
 }
 
 bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
-  if( q.getNumChildren()==3 ){
-    std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q );
-    if( it==d_hasUserPatterns.end() ){
-      bool hasPat = false;
-      for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
-        if( q[2][i].getKind()==INST_PATTERN ){
-          hasPat = true;
-          break;
-        }
-      }
-      d_hasUserPatterns[q] = hasPat;
-      return hasPat;
-    }else{
-      return it->second;
-    }
-  }else{
+  if (q.getNumChildren() != 3)
+  {
     return false;
   }
+  std::map<Node, bool>::iterator it = d_hasUserPatterns.find(q);
+  if (it != d_hasUserPatterns.end())
+  {
+    return it->second;
+  }
+  bool hasPat = false;
+  for (const Node& ip : q[2])
+  {
+    if (ip.getKind() == INST_PATTERN)
+    {
+      hasPat = true;
+      break;
+    }
+  }
+  d_hasUserPatterns[q] = hasPat;
+  return hasPat;
 }
 
 void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
   Assert(pat.getKind() == INST_NO_PATTERN && pat.getNumChildren() == 1);
-  if( std::find( d_user_no_gen[q].begin(), d_user_no_gen[q].end(), pat[0] )==d_user_no_gen[q].end() ){
+  std::vector<Node>& ung = d_user_no_gen[q];
+  if (std::find(ung.begin(), ung.end(), pat[0]) == ung.end())
+  {
     Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << q << std::endl;
-    d_user_no_gen[q].push_back( pat[0] );
+    ung.push_back(pat[0]);
   }
 }
 
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index 45d3db275..701d4ac74 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -47,9 +47,9 @@ public:
   /** add pattern */
   void addUserPattern( Node q, Node pat );
   /** get num patterns */
-  int getNumUserGenerators( Node q ) { return (int)d_user_gen[q].size(); }
+  size_t getNumUserGenerators(Node q) { return d_user_gen[q].size(); }
   /** get user pattern */
-  inst::Trigger* getUserGenerator( Node q, int i ) { return d_user_gen[q][ i ]; }
+  inst::Trigger* getUserGenerator(Node q, size_t i) { return d_user_gen[q][i]; }
   /** identify */
   std::string identify() const override { return std::string("UserPatterns"); }
 };/* class InstStrategyUserPatterns */
@@ -92,8 +92,14 @@ class InstStrategyAutoGenTriggers : public InstStrategy
   /** process functions */
   void processResetInstantiationRound(Theory::Effort effort) override;
   int process(Node q, Theory::Effort effort, int e) override;
-  /** generate triggers */
+  /**
+   * Generate triggers for quantified formula q.
+   */
   void generateTriggers(Node q);
+  /**
+   * Generate pattern terms for quantified formula q.
+   */
+  bool generatePatternTerms(Node q);
   void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat);
   void addTrigger(inst::Trigger* tr, Node f);
   /** has user patterns */
diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp
index 175bb149a..a7bf3499b 100644
--- a/src/theory/quantifiers/quant_relevance.cpp
+++ b/src/theory/quantifiers/quant_relevance.cpp
@@ -50,6 +50,16 @@ void QuantRelevance::computeSymbols(Node n, std::vector<Node>& syms)
   }
 }
 
+size_t QuantRelevance::getNumQuantifiersForSymbol(Node s) const
+{
+  std::map<Node, std::vector<Node> >::const_iterator it = d_syms_quants.find(s);
+  if (it == d_syms_quants.end())
+  {
+    return 0;
+  }
+  return it->second.size();
+}
+
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h
index 3396c2099..a16985d82 100644
--- a/src/theory/quantifiers/quant_relevance.h
+++ b/src/theory/quantifiers/quant_relevance.h
@@ -48,10 +48,7 @@ class QuantRelevance : public QuantifiersUtil
   /** identify */
   std::string identify() const override { return "QuantRelevance"; }
   /** get number of quantifiers for symbol s */
-  unsigned getNumQuantifiersForSymbol(Node s)
-  {
-    return d_syms_quants[s].size();
-  }
+  size_t getNumQuantifiersForSymbol(Node s) const;
 
  private:
   /** map from quantifiers to symbols they contain */