Initial cleaning of triggers (#5795)

In preparation for splitting trigger.h/cpp into multiple files.

This updates the code to conform to guidelines. No major changes, apart from a heuristic related to "pure theory triggers" is deleted and simplified.

6 files changed, 435 insertions, 402 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 9027e7a94..3499da7de 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -264,14 +264,6 @@ header = "options/quantifiers_options.h"
   help       = "purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1"
 
 [[option]]
-  name       = "pureThTriggers"
-  category   = "regular"
-  long       = "pure-th-triggers"
-  type       = "bool"
-  default    = "false"
-  help       = "use pure theory terms as single triggers"
-
-[[option]]
   name       = "partialTriggers"
   category   = "regular"
   long       = "partial-triggers"
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 4672c10c7..cdfb9c85c 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -186,12 +186,12 @@ void HigherOrderTrigger::collectHoVarApplyTerms(
   }
 }
 
-int HigherOrderTrigger::addInstantiations()
+uint64_t HigherOrderTrigger::addInstantiations()
 {
   // call the base class implementation
-  int addedFoLemmas = Trigger::addInstantiations();
+  uint64_t addedFoLemmas = Trigger::addInstantiations();
   // also adds predicate lemms to force app completion
-  int addedHoLemmas = addHoTypeMatchPredicateLemmas();
+  uint64_t addedHoLemmas = addHoTypeMatchPredicateLemmas();
   return addedHoLemmas + addedFoLemmas;
 }
 
@@ -460,14 +460,14 @@ bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m,
   }
 }
 
-int HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
+uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
 {
   if (d_ho_var_types.empty())
   {
     return 0;
   }
   Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
-  unsigned numLemmas = 0;
+  uint64_t numLemmas = 0;
   // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
   quantifiers::TermDb* tdb = d_quantEngine->getTermDatabase();
   unsigned size = tdb->getNumOperators();
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index a369aa7c5..d9636cd65 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -122,7 +122,7 @@ class HigherOrderTrigger : public Trigger
    * Extends Trigger::addInstantiations to also send
    * lemmas based on addHoTypeMatchPredicateLemmas.
    */
-  int addInstantiations() override;
+  uint64_t addInstantiations() override;
 
  protected:
   /**
@@ -158,7 +158,7 @@ class HigherOrderTrigger : public Trigger
    *
    * TODO: we may eliminate this based on how github issue #1115 is resolved.
    */
-  int addHoTypeMatchPredicateLemmas();
+  uint64_t addHoTypeMatchPredicateLemmas();
   /** send instantiation
    *
   * Sends an instantiation that is equivalent to m via
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 513897cc9..7dcb9b797 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -561,7 +561,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
 void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ) {
   d_pat_to_mpat[pat] = mpat;
   unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren();
-  if( num_fv==num_vars && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
+  if (num_fv == num_vars)
+  {
     d_patTerms[0][q].push_back( pat );
     d_is_single_trigger[ pat ] = true;
   }else{
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index a111e0221..4d6dd9f58 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -67,8 +67,10 @@ Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
   if( d_nodes.size()==1 ){
     if( isSimpleTrigger( d_nodes[0] ) ){
       d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qe);
+      ++(qe->d_statistics.d_triggers);
     }else{
       d_mg = InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qe);
+      ++(qe->d_statistics.d_simple_triggers);
     }
   }else{
     if( options::multiTriggerCache() ){
@@ -76,17 +78,13 @@ Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
     }else{
       d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(q, d_nodes, qe);
     }
-  }
-  if( d_nodes.size()==1 ){
-    if( isSimpleTrigger( d_nodes[0] ) ){
-      ++(qe->d_statistics.d_triggers);
-    }else{
-      ++(qe->d_statistics.d_simple_triggers);
-    }
-  }else{
-    Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl;
-    for( unsigned i=0; i<d_nodes.size(); i++ ){
-      Trace("multi-trigger") << "   " << d_nodes[i] << std::endl;
+    if (Trace.isOn("multi-trigger"))
+    {
+      Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl;
+      for (const Node& nc : d_nodes)
+      {
+        Trace("multi-trigger") << "   " << nc << std::endl;
+      }
     }
     ++(qe->d_statistics.d_multi_triggers);
   }
@@ -107,23 +105,22 @@ void Trigger::reset( Node eqc ){
   d_mg->reset( eqc, d_quantEngine );
 }
 
-Node Trigger::getInstPattern(){
+bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; }
+
+Node Trigger::getInstPattern() const
+{
   return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
 }
 
-int Trigger::addInstantiations()
+uint64_t Trigger::addInstantiations()
 {
-  int addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this);
-  if( addedLemmas>0 ){
-    if (Debug.isOn("inst-trigger"))
+  uint64_t addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this);
+  if (Debug.isOn("inst-trigger"))
+  {
+    if (addedLemmas > 0)
     {
       Debug("inst-trigger") << "Added " << addedLemmas
-                            << " lemmas, trigger was ";
-      for (unsigned i = 0; i < d_nodes.size(); i++)
-      {
-        Debug("inst-trigger") << d_nodes[i] << " ";
-      }
-      Debug("inst-trigger") << std::endl;
+                            << " lemmas, trigger was " << d_nodes << std::endl;
     }
   }
   return addedLemmas;
@@ -134,7 +131,11 @@ bool Trigger::sendInstantiation(InstMatch& m)
   return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
 }
 
-bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
+bool Trigger::mkTriggerTerms(Node q,
+                             std::vector<Node>& nodes,
+                             size_t nvars,
+                             std::vector<Node>& trNodes)
+{
   //only take nodes that contribute variables to the trigger when added
   std::vector< Node > temp;
   temp.insert( temp.begin(), nodes.begin(), nodes.end() );
@@ -147,10 +148,12 @@ bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_var
     quantifiers::TermUtil::computeInstConstContainsForQuant(
         q, pat, varContains[pat]);
   }
-  for( unsigned i=0; i<temp.size(); i++ ){
+  for (const Node& t : temp)
+  {
+    const std::vector<Node>& vct = varContains[t];
     bool foundVar = false;
-    for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
-      Node v = varContains[ temp[i] ][j];
+    for (const Node& v : vct)
+    {
       Assert(quantifiers::TermUtil::getInstConstAttr(v) == q);
       if( vars.find( v )==vars.end() ){
         varCount++;
@@ -159,63 +162,74 @@ bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_var
       }
     }
     if( foundVar ){
-      trNodes.push_back( temp[i] );
-      for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
-        Node v = varContains[ temp[i] ][j];
-        patterns[ v ].push_back( temp[i] );
+      trNodes.push_back(t);
+      for (const Node& v : vct)
+      {
+        patterns[v].push_back(t);
       }
     }
-    if( varCount==n_vars ){
+    if (varCount == nvars)
+    {
       break;
     }
   }
-  if( varCount<n_vars ){
+  if (varCount < nvars)
+  {
     Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl;
-    for( unsigned i=0; i<nodes.size(); i++) {
-      Trace("trigger-debug") << nodes[i] << " ";
-    }
-    Trace("trigger-debug") << std::endl;
-
+    Trace("trigger-debug") << nodes << std::endl;
     //do not generate multi-trigger if it does not contain all variables
     return false;
-  }else{
-    //now, minimize the trigger
-    for( unsigned i=0; i<trNodes.size(); i++ ){
-      bool keepPattern = false;
-      Node n = trNodes[i];
-      for( unsigned j=0; j<varContains[ n ].size(); j++ ){
-        Node v = varContains[ n ][j];
-        if( patterns[v].size()==1 ){
-          keepPattern = true;
-          break;
-        }
+  }
+  // now, minimize the trigger
+  for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
+  {
+    bool keepPattern = false;
+    Node n = trNodes[i];
+    const std::vector<Node>& vcn = varContains[n];
+    for (const Node& v : vcn)
+    {
+      if (patterns[v].size() == 1)
+      {
+        keepPattern = true;
+        break;
       }
-      if( !keepPattern ){
-        //remove from pattern vector
-        for( unsigned j=0; j<varContains[ n ].size(); j++ ){
-          Node v = varContains[ n ][j];
-          for( unsigned k=0; k<patterns[v].size(); k++ ){
-            if( patterns[v][k]==n ){
-              patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
-              break;
-            }
+    }
+    if (!keepPattern)
+    {
+      // remove from pattern vector
+      for (const Node& v : vcn)
+      {
+        std::vector<Node>& pv = patterns[v];
+        for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
+        {
+          if (pv[k] == n)
+          {
+            pv.erase(pv.begin() + k, pv.begin() + k + 1);
+            break;
           }
         }
-        //remove from trigger nodes
-        trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
-        i--;
       }
+      // remove from trigger nodes
+      trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
+      i--;
     }
   }
   return true;
 }
 
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, bool keepAll, int trOption, unsigned use_n_vars ){
+Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+                            Node f,
+                            std::vector<Node>& nodes,
+                            bool keepAll,
+                            int trOption,
+                            size_t useNVars)
+{
   std::vector< Node > trNodes;
   if( !keepAll ){
-    unsigned n_vars = use_n_vars==0 ? f[0].getNumChildren() : use_n_vars;
-    if( !mkTriggerTerms( f, nodes, n_vars, trNodes ) ){
-      return NULL;
+    size_t nvars = useNVars == 0 ? f[0].getNumChildren() : useNVars;
+    if (!mkTriggerTerms(f, nodes, nvars, trNodes))
+    {
+      return nullptr;
     }
   }else{
     trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
@@ -229,7 +243,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
         //just return old trigger
         return t;
       }else{
-        return NULL;
+        return nullptr;
       }
     }
   }
@@ -255,42 +269,54 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
   return t;
 }
 
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll, int trOption, unsigned use_n_vars ){
+Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+                            Node f,
+                            Node n,
+                            bool keepAll,
+                            int trOption,
+                            size_t useNVars)
+{
   std::vector< Node > nodes;
   nodes.push_back( n );
-  return mkTrigger( qe, f, nodes, keepAll, trOption, use_n_vars );
+  return mkTrigger(qe, f, nodes, keepAll, trOption, useNVars);
 }
 
 bool Trigger::isUsable( Node n, Node q ){
-  if( quantifiers::TermUtil::getInstConstAttr(n)==q ){
-    if( isAtomicTrigger( n ) ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( !isUsable( n[i], q ) ){
-          return false;
-        }
-      }
-      return true;
-    }else if( n.getKind()==INST_CONSTANT ){
-      return true;
-    }else{
-      std::map< Node, Node > coeffs;
-      if (options::purifyTriggers())
+  if (quantifiers::TermUtil::getInstConstAttr(n) != q)
+  {
+    return true;
+  }
+  if (isAtomicTrigger(n))
+  {
+    for (const Node& nc : n)
+    {
+      if (!isUsable(nc, q))
       {
-        Node x = getInversionVariable( n );
-        if( !x.isNull() ){
-          return true;
-        }
+        return false;
       }
     }
-    return false;
-  }else{
     return true;
   }
+  else if (n.getKind() == INST_CONSTANT)
+  {
+    return true;
+  }
+  std::map<Node, Node> coeffs;
+  if (options::purifyTriggers())
+  {
+    Node x = getInversionVariable(n);
+    if (!x.isNull())
+    {
+      return true;
+    }
+  }
+  return false;
 }
 
 Node Trigger::getIsUsableEq( Node q, Node n ) {
   Assert(isRelationalTrigger(n));
-  for( unsigned i=0; i<2; i++) {
+  for (size_t i = 0; i < 2; i++)
+  {
     if( isUsableEqTerms( q, n[i], n[1-i] ) ){
       if( i==1 && n.getKind()==EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0]) ){
         return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );  
@@ -349,8 +375,9 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) {
     pol = !pol;
     n = n[0];
   }
+  NodeManager* nm = NodeManager::currentNM();
   if( n.getKind()==INST_CONSTANT ){
-    return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+    return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
   }else if( isRelationalTrigger( n ) ){
     Node rtr = getIsUsableEq( q, n );
     if( rtr.isNull() && n[0].getType().isReal() ){
@@ -388,11 +415,15 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) {
       Trace("relational-trigger") << "    return : " << rtr2 << std::endl;
       return rtr2;
     }
-  }else{
-    Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermUtil::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
-    if( isUsableAtomicTrigger( n, q ) ){
-      return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
-    }
+    return Node::null();
+  }
+  Trace("trigger-debug") << n << " usable : "
+                         << (quantifiers::TermUtil::getInstConstAttr(n) == q)
+                         << " " << isAtomicTrigger(n) << " " << isUsable(n, q)
+                         << std::endl;
+  if (isUsableAtomicTrigger(n, q))
+  {
+    return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
   }
   return Node::null();
 }
@@ -437,19 +468,23 @@ bool Trigger::isSimpleTrigger( Node n ){
       t = t[0];
     }
   }
-  if( isAtomicTrigger( t ) ){
-    for( unsigned i=0; i<t.getNumChildren(); i++ ){
-      if( t[i].getKind()!=INST_CONSTANT && quantifiers::TermUtil::hasInstConstAttr(t[i]) ){
-        return false;
-      }
-    }
-    if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
+  if (!isAtomicTrigger(t))
+  {
+    return false;
+  }
+  for (const Node& tc : t)
+  {
+    if (tc.getKind() != INST_CONSTANT
+        && quantifiers::TermUtil::hasInstConstAttr(tc))
     {
       return false;
     }
-    return true;
   }
-  return false;
+  if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
+  {
+    return false;
+  }
+  return true;
 }
 
 //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
@@ -467,131 +502,167 @@ void Trigger::collectPatTerms2(Node q,
                                bool knowIsUsable)
 {
   std::map< Node, std::vector< Node > >::iterator itv = visited.find( n );
-  if( itv==visited.end() ){
-    visited[ n ].clear();
-    Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
-    if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){
-      Node nu;
-      bool nu_single = false;
-      if( knowIsUsable ){
-        nu = n;
-      }else if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
-        nu = getIsUsableTrigger( n, q );
-        if( !nu.isNull() && nu!=n ){
-          collectPatTerms2( q, nu, visited, tinfo, tstrt, exclude, added, pol, hasPol, epol, hasEPol, true );
-          // copy to n
-          visited[n].insert( visited[n].end(), added.begin(), added.end() );
-          return;
-        }
+  if (itv != visited.end())
+  {
+    // already visited
+    for (const Node& t : itv->second)
+    {
+      if (std::find(added.begin(), added.end(), t) == added.end())
+      {
+        added.push_back(t);
       }
-      if( !nu.isNull() ){
-        Assert(nu == n);
-        Assert(nu.getKind() != NOT);
-        Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
-        Node reqEq;
-        if( nu.getKind()==EQUAL ){
-          if( isAtomicTrigger( nu[0] ) && !quantifiers::TermUtil::hasInstConstAttr(nu[1]) ){
-            if( hasPol ){
-              reqEq = nu[1];
-            }
-            nu = nu[0];
-          }
+    }
+    return;
+  }
+  visited[n].clear();
+  Trace("auto-gen-trigger-debug2")
+      << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol
+      << " " << hasEPol << std::endl;
+  Kind nk = n.getKind();
+  if (nk == FORALL || nk == INST_CONSTANT)
+  {
+    // do not traverse beneath quantified formulas
+    return;
+  }
+  Node nu;
+  bool nu_single = false;
+  if (knowIsUsable)
+  {
+    nu = n;
+  }
+  else if (nk != NOT
+           && std::find(exclude.begin(), exclude.end(), n) == exclude.end())
+  {
+    nu = getIsUsableTrigger(n, q);
+    if (!nu.isNull() && nu != n)
+    {
+      collectPatTerms2(q,
+                       nu,
+                       visited,
+                       tinfo,
+                       tstrt,
+                       exclude,
+                       added,
+                       pol,
+                       hasPol,
+                       epol,
+                       hasEPol,
+                       true);
+      // copy to n
+      visited[n].insert(visited[n].end(), added.begin(), added.end());
+      return;
+    }
+  }
+  if (!nu.isNull())
+  {
+    Assert(nu == n);
+    Assert(nu.getKind() != NOT);
+    Trace("auto-gen-trigger-debug2")
+        << "...found usable trigger : " << nu << std::endl;
+    Node reqEq;
+    if (nu.getKind() == EQUAL)
+    {
+      if (isAtomicTrigger(nu[0])
+          && !quantifiers::TermUtil::hasInstConstAttr(nu[1]))
+      {
+        if (hasPol)
+        {
+          reqEq = nu[1];
         }
-        Assert(reqEq.isNull()
-               || !quantifiers::TermUtil::hasInstConstAttr(reqEq));
-        Assert(isUsableTrigger(nu, q));
-        //tinfo.find( nu )==tinfo.end()
-        Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
-        tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
-        nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
+        nu = nu[0];
       }
-      Node nrec = nu.isNull() ? n : nu;
-      std::vector< Node > added2;
-      for( unsigned i=0; i<nrec.getNumChildren(); i++ ){
-        bool newHasPol, newPol;
-        bool newHasEPol, newEPol;
-        QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol );
-        QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
-        collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol );
-      }
-      // if this is not a usable trigger, don't worry about caching the results, since triggers do not contain non-usable subterms
-      if( !nu.isNull() ){
-        bool rm_nu = false;
-        for( unsigned i=0; i<added2.size(); i++ ){
-          Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i << " : " << added2[i] << std::endl;
-          Assert(added2[i] != nu);
-          // if child was not already removed
-          if( tinfo.find( added2[i] )!=tinfo.end() ){
-            if (tstrt == options::TriggerSelMode::MAX
-                || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX
-                    && !nu_single))
-            {
-              // discard all subterms
-              // do not remove if it has smaller weight
-              if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
-              {
-                Trace("auto-gen-trigger-debug2")
-                    << "......remove it." << std::endl;
-                visited[added2[i]].clear();
-                tinfo.erase(added2[i]);
-              }
-            }
-            else
-            {
-              if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
-                if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
-                {
-                  // discard if we added a subterm as a trigger with all
-                  // variables that nu has
-                  Trace("auto-gen-trigger-debug2")
-                      << "......subsumes parent " << tinfo[nu].d_weight << " "
-                      << tinfo[added2[i]].d_weight << "." << std::endl;
-                  rm_nu = true;
-                }
-              }
-              if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){
-                added.push_back( added2[i] );
-              }
-            }
-          }
-        }
-        if (rm_nu
-            && (tstrt == options::TriggerSelMode::MIN
-                || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL
-                    && nu_single)))
+    }
+    Assert(reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr(reqEq));
+    Assert(isUsableTrigger(nu, q));
+    // tinfo.find( nu )==tinfo.end()
+    Trace("auto-gen-trigger-debug2")
+        << "...add usable trigger : " << nu << std::endl;
+    tinfo[nu].init(q, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
+    nu_single = tinfo[nu].d_fv.size() == q[0].getNumChildren();
+  }
+  Node nrec = nu.isNull() ? n : nu;
+  std::vector<Node> added2;
+  for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++)
+  {
+    bool newHasPol, newPol;
+    bool newHasEPol, newEPol;
+    QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol);
+    QuantPhaseReq::getEntailPolarity(
+        nrec, i, hasEPol, epol, newHasEPol, newEPol);
+    collectPatTerms2(q,
+                     nrec[i],
+                     visited,
+                     tinfo,
+                     tstrt,
+                     exclude,
+                     added2,
+                     newPol,
+                     newHasPol,
+                     newEPol,
+                     newHasEPol);
+  }
+  // if this is not a usable trigger, don't worry about caching the results,
+  // since triggers do not contain non-usable subterms
+  if (nu.isNull())
+  {
+    return;
+  }
+  bool rm_nu = false;
+  for (size_t i = 0, asize = added2.size(); i < asize; i++)
+  {
+    Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i
+                                     << " : " << added2[i] << std::endl;
+    Assert(added2[i] != nu);
+    // if child was not already removed
+    if (tinfo.find(added2[i]) != tinfo.end())
+    {
+      if (tstrt == options::TriggerSelMode::MAX
+          || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX && !nu_single))
+      {
+        // discard all subterms
+        // do not remove if it has smaller weight
+        if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
         {
-          tinfo.erase( nu );
+          Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
+          visited[added2[i]].clear();
+          tinfo.erase(added2[i]);
         }
-        else
+      }
+      else
+      {
+        if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size())
         {
-          if( std::find( added.begin(), added.end(), nu )==added.end() ){
-            added.push_back( nu );
+          if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
+          {
+            // discard if we added a subterm as a trigger with all
+            // variables that nu has
+            Trace("auto-gen-trigger-debug2")
+                << "......subsumes parent " << tinfo[nu].d_weight << " "
+                << tinfo[added2[i]].d_weight << "." << std::endl;
+            rm_nu = true;
           }
         }
-        visited[n].insert( visited[n].end(), added.begin(), added.end() );
-      }
-    }
-  }else{
-    for( unsigned i=0; i<itv->second.size(); ++i ){
-      Node t = itv->second[i];
-      if( std::find( added.begin(), added.end(), t )==added.end() ){
-        added.push_back( t );
+        if (std::find(added.begin(), added.end(), added2[i]) == added.end())
+        {
+          added.push_back(added2[i]);
+        }
       }
     }
   }
-}
-
-bool Trigger::isPureTheoryTrigger( Node n ) {
-  if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){  //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){
-    return false;
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !isPureTheoryTrigger( n[i] ) ){
-        return false;
-      }
+  if (rm_nu
+      && (tstrt == options::TriggerSelMode::MIN
+          || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL && nu_single)))
+  {
+    tinfo.erase(nu);
+  }
+  else
+  {
+    if (std::find(added.begin(), added.end(), nu) == added.end())
+    {
+      added.push_back(nu);
     }
-    return true;
   }
+  visited[n].insert(visited[n].end(), added.begin(), added.end());
 }
 
 int Trigger::getTriggerWeight( Node n ) {
@@ -606,38 +677,6 @@ int Trigger::getTriggerWeight( Node n ) {
   return 2;
 }
 
-bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
-  if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
-    if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){
-      bool hasVar = false;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( n[i].getKind()==INST_CONSTANT ){
-          hasVar = true;
-          if( std::find( vars.begin(), vars.end(), n[i] )==vars.end() ){
-            vars.push_back( n[i] );
-          }else{
-            //do not allow duplicate variables
-            return false;
-          }
-        }else{
-          //do not allow nested function applications
-          return false;
-        }
-      }
-      if( hasVar ){
-        patTerms.push_back( n );
-      }
-    }
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !isLocalTheoryExt( n[i], vars, patTerms ) ){
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
 void Trigger::collectPatTerms(Node q,
                               Node n,
                               std::vector<Node>& patTerms,
@@ -698,15 +737,16 @@ void Trigger::collectPatTerms(Node q,
   }
   std::vector< Node > added;
   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 ){
-    patTerms.push_back( it->first );
+  for (const std::pair<const Node, TriggerTermInfo>& t : tinfo)
+  {
+    patTerms.push_back(t.first);
   }
 }
 
 int Trigger::isTriggerInstanceOf(Node n1,
                                  Node n2,
-                                 std::vector<Node>& fv1,
-                                 std::vector<Node>& fv2)
+                                 const std::vector<Node>& fv1,
+                                 const std::vector<Node>& fv2)
 {
   Assert(n1 != n2);
   int status = 0;
@@ -726,73 +766,72 @@ int Trigger::isTriggerInstanceOf(Node n1,
   {
     cur = visit.back();
     visit.pop_back();
-    if (visited.find(cur) == visited.end())
+    if (visited.find(cur) != visited.end())
     {
-      visited.insert(cur);
-      cur1 = cur.first;
-      cur2 = cur.second;
-      Assert(cur1 != cur2);
-      // recurse if they have the same operator
-      if (cur1.hasOperator() && cur2.hasOperator()
-          && cur1.getNumChildren() == cur2.getNumChildren()
-          && cur1.getOperator() == cur2.getOperator()
-          && cur1.getOperator().getKind()!=INST_CONSTANT)
+      continue;
+    }
+    visited.insert(cur);
+    cur1 = cur.first;
+    cur2 = cur.second;
+    Assert(cur1 != cur2);
+    // recurse if they have the same operator
+    if (cur1.hasOperator() && cur2.hasOperator()
+        && cur1.getNumChildren() == cur2.getNumChildren()
+        && cur1.getOperator() == cur2.getOperator()
+        && cur1.getOperator().getKind() != INST_CONSTANT)
+    {
+      visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
+      for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++)
       {
-        visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
-        for (unsigned i = 0, size = cur1.getNumChildren(); i < size; i++)
+        if (cur1[i] != cur2[i])
         {
-          if (cur1[i] != cur2[i])
-          {
-            visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
-          }
-          else if (cur1[i].getKind() == INST_CONSTANT)
+          visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
+        }
+        else if (cur1[i].getKind() == INST_CONSTANT)
+        {
+          if (subs_vars.find(cur1[i]) != subs_vars.end())
           {
-            if (subs_vars.find(cur1[i]) != subs_vars.end())
-            {
-              return 0;
-            }
-            // the variable must map to itself in the substitution
-            subs_vars.insert(cur1[i]);
+            return 0;
           }
+          // the variable must map to itself in the substitution
+          subs_vars.insert(cur1[i]);
         }
       }
-      else
+      continue;
+    }
+    bool success = false;
+    // check if we are in a unifiable instance case
+    // must be only this case
+    for (unsigned r = 0; r < 2; r++)
+    {
+      if (status == 0 || ((status == 1) == (r == 0)))
       {
-        bool success = false;
-        // check if we are in a unifiable instance case
-        // must be only this case
-        for (unsigned r = 0; r < 2; r++)
+        TNode curi = r == 0 ? cur1 : cur2;
+        if (curi.getKind() == INST_CONSTANT
+            && subs_vars.find(curi) == subs_vars.end())
         {
-          if (status == 0 || ((status == 1) == (r == 0)))
+          TNode curj = r == 0 ? cur2 : cur1;
+          // RHS must be a simple trigger
+          if (getTriggerWeight(curj) == 0)
           {
-            TNode curi = r == 0 ? cur1 : cur2;
-            if (curi.getKind() == INST_CONSTANT
-                && subs_vars.find(curi) == subs_vars.end())
+            // must occur in the free variables in the other
+            const std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
+            if (std::find(free_vars.begin(), free_vars.end(), curi)
+                != free_vars.end())
             {
-              TNode curj = r == 0 ? cur2 : cur1;
-              // RHS must be a simple trigger
-              if (getTriggerWeight(curj) == 0)
-              {
-                // must occur in the free variables in the other
-                std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
-                if (std::find(free_vars.begin(), free_vars.end(), curi)
-                    != free_vars.end())
-                {
-                  status = r == 0 ? 1 : -1;
-                  subs_vars.insert(curi);
-                  success = true;
-                  break;
-                }
-              }
+              status = r == 0 ? 1 : -1;
+              subs_vars.insert(curi);
+              success = true;
+              break;
             }
           }
         }
-        if (!success)
-        {
-          return 0;
-        }
       }
     }
+    if (!success)
+    {
+      return 0;
+    }
   } while (!visit.empty());
   return status;
 }
@@ -800,41 +839,43 @@ int Trigger::isTriggerInstanceOf(Node n1,
 void Trigger::filterTriggerInstances(std::vector<Node>& nodes)
 {
   std::map<unsigned, std::vector<Node> > fvs;
-  for (unsigned i = 0, size = nodes.size(); i < size; i++)
+  for (size_t i = 0, size = nodes.size(); i < size; i++)
   {
     quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
   }
   std::vector<bool> active;
   active.resize(nodes.size(), true);
-  for (unsigned i = 0, size = nodes.size(); i < size; i++)
+  for (size_t i = 0, size = nodes.size(); i < size; i++)
   {
     std::vector<Node>& fvsi = fvs[i];
-    if (active[i])
+    if (!active[i])
     {
-      for (unsigned j = i + 1, size2 = nodes.size(); j < size2; j++)
+      continue;
+    }
+    for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++)
+    {
+      if (!active[j])
       {
-        if (active[j])
-        {
-          int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
-          if (result == 1)
-          {
-            Trace("filter-instances") << nodes[j] << " is an instance of "
-                                      << nodes[i] << std::endl;
-            active[i] = false;
-            break;
-          }
-          else if (result == -1)
-          {
-            Trace("filter-instances") << nodes[i] << " is an instance of "
-                                      << nodes[j] << std::endl;
-            active[j] = false;
-          }
-        }
+        continue;
+      }
+      int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
+      if (result == 1)
+      {
+        Trace("filter-instances")
+            << nodes[j] << " is an instance of " << nodes[i] << std::endl;
+        active[i] = false;
+        break;
+      }
+      else if (result == -1)
+      {
+        Trace("filter-instances")
+            << nodes[i] << " is an instance of " << nodes[j] << std::endl;
+        active[j] = false;
       }
     }
   }
   std::vector<Node> temp;
-  for (unsigned i = 0; i < nodes.size(); i++)
+  for (size_t i = 0, nsize = nodes.size(); i < nsize; i++)
   {
     if (active[i])
     {
@@ -846,14 +887,20 @@ void Trigger::filterTriggerInstances(std::vector<Node>& nodes)
 }
 
 Node Trigger::getInversionVariable( Node n ) {
-  if( n.getKind()==INST_CONSTANT ){
+  Kind nk = n.getKind();
+  if (nk == INST_CONSTANT)
+  {
     return n;
-  }else if( n.getKind()==PLUS || n.getKind()==MULT ){
+  }
+  else if (nk == PLUS || nk == MULT)
+  {
     Node ret;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
+    for (const Node& nc : n)
+    {
+      if (quantifiers::TermUtil::hasInstConstAttr(nc))
+      {
         if( ret.isNull() ){
-          ret = getInversionVariable( n[i] );
+          ret = getInversionVariable(nc);
           if( ret.isNull() ){
             Trace("var-trigger-debug") << "No : multiple variables " << n << std::endl;
             return Node::null();
@@ -861,52 +908,59 @@ Node Trigger::getInversionVariable( Node n ) {
         }else{
           return Node::null();
         }
-      }else if( n.getKind()==MULT ){
-        if( !n[i].isConst() ){
+      }
+      else if (nk == MULT)
+      {
+        if (!nc.isConst())
+        {
           Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl;
           return Node::null();
         }
-        /*
-        else if( n.getType().isInteger() ){
-          Rational r = n[i].getConst<Rational>();
-          if( r!=Rational(-1) && r!=Rational(1) ){
-            Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl;
-            return Node::null();
-          }
-        }
-        */
       }
     }
     return ret;
-  }else{
-    Trace("var-trigger-debug") << "No : unsupported operator " << n << "." << std::endl;
   }
+  Trace("var-trigger-debug")
+      << "No : unsupported operator " << n << "." << std::endl;
   return Node::null();
 }
 
 Node Trigger::getInversion( Node n, Node x ) {
-  if( n.getKind()==INST_CONSTANT ){
+  Kind nk = n.getKind();
+  if (nk == INST_CONSTANT)
+  {
     return x;
-  }else if( n.getKind()==PLUS || n.getKind()==MULT ){
+  }
+  else if (nk == PLUS || nk == MULT)
+  {
+    NodeManager* nm = NodeManager::currentNM();
     int cindex = -1;
     bool cindexSet = false;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
-        if( n.getKind()==PLUS ){
-          x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] );
-        }else if( n.getKind()==MULT ){
-          Assert(n[i].isConst());
+    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+    {
+      Node nc = n[i];
+      if (!quantifiers::TermUtil::hasInstConstAttr(nc))
+      {
+        if (nk == PLUS)
+        {
+          x = nm->mkNode(MINUS, x, nc);
+        }
+        else if (nk == MULT)
+        {
+          Assert(nc.isConst());
           if( x.getType().isInteger() ){
-            Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>().abs() );
-            if( !n[i].getConst<Rational>().abs().isOne() ){
-              x = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, x, coeff );
+            Node coeff = nm->mkConst(nc.getConst<Rational>().abs());
+            if (!nc.getConst<Rational>().abs().isOne())
+            {
+              x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
             }
-            if( n[i].getConst<Rational>().sgn()<0 ){
-              x = NodeManager::currentNM()->mkNode( UMINUS, x );
+            if (nc.getConst<Rational>().sgn() < 0)
+            {
+              x = nm->mkNode(UMINUS, x);
             }
           }else{
-            Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
-            x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
+            Node coeff = nm->mkConst(Rational(1) / nc.getConst<Rational>());
+            x = nm->mkNode(MULT, x, coeff);
           }
         }
         x = Rewriter::rewrite( x );
@@ -942,6 +996,11 @@ int Trigger::getActiveScore() {
   return d_mg->getActiveScore( d_quantEngine );
 }
 
+void Trigger::debugPrint(const char* c) const
+{
+  Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl;
+}
+
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 890811c8b..201d4258b 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -187,16 +187,16 @@ class Trigger {
   * produce instantiations beyond what is produced by the match generator
   * (for example, see theory/quantifiers/ematching/ho_trigger.h).
   */
-  virtual int addInstantiations();
+  virtual uint64_t addInstantiations();
   /** Return whether this is a multi-trigger. */
-  bool isMultiTrigger() { return d_nodes.size()>1; }
+  bool isMultiTrigger() const;
   /** Get instantiation pattern list associated with this trigger.
    *
   * An instantiation pattern list is the node representation of a trigger, in
   * particular, it is the third argument of quantified formulas which have user
   * (! ... :pattern) attributes.
   */
-  Node getInstPattern();
+  Node getInstPattern() const;
   /* A heuristic value indicating how active this generator is.
    *
   * This returns the number of ground terms for the match operators in terms
@@ -205,19 +205,7 @@ class Trigger {
   */
   int getActiveScore();
   /** print debug information for the trigger */
-  void debugPrint(const char* c)
-  {
-    Trace(c) << "TRIGGER( ";
-    for (int i = 0; i < (int)d_nodes.size(); i++)
-    {
-      if (i > 0)
-      {
-        Trace(c) << ", ";
-      }
-      Trace(c) << d_nodes[i];
-    }
-    Trace(c) << " )";
-  }
+  void debugPrint(const char* c) const;
   /** mkTrigger method
    *
    * This makes an instance of a trigger object.
@@ -227,8 +215,8 @@ class Trigger {
    *  keepAll: don't remove unneeded patterns;
    *  trOption : policy for dealing with triggers that already exist
    *             (see below)
-   *  use_n_vars : number of variables that should be bound by the trigger
-   *               typically, the number of quantified variables in q.
+   *  useNVars : number of variables that should be bound by the trigger
+   *             typically, the number of quantified variables in q.
    */
   enum{
     TR_MAKE_NEW,    //make new trigger even if it already may exist
@@ -240,14 +228,14 @@ class Trigger {
                             std::vector<Node>& nodes,
                             bool keepAll = true,
                             int trOption = TR_MAKE_NEW,
-                            unsigned use_n_vars = 0);
+                            size_t useNVars = 0);
   /** single trigger version that calls the above function */
   static Trigger* mkTrigger(QuantifiersEngine* qe,
                             Node q,
                             Node n,
                             bool keepAll = true,
                             int trOption = TR_MAKE_NEW,
-                            unsigned use_n_vars = 0);
+                            size_t useNVars = 0);
   /** make trigger terms
    *
    * This takes a set of eligible trigger terms and stores a subset of them in
@@ -259,7 +247,7 @@ class Trigger {
    */
   static bool mkTriggerTerms(Node q,
                              std::vector<Node>& nodes,
-                             unsigned n_vars,
+                             size_t nvars,
                              std::vector<Node>& trNodes);
   /** collect pattern terms
    *
@@ -319,8 +307,6 @@ class Trigger {
   static bool isRelationalTriggerKind( Kind k );
   /** is n a simple trigger (see inst_match_generator.h)? */
   static bool isSimpleTrigger( Node n );
-  /** is n a pure theory trigger, e.g. head( x )? */
-  static bool isPureTheoryTrigger( Node n );
   /** get trigger weight
    *
    * Intutively, this function classifies how difficult it is to handle the
@@ -331,11 +317,6 @@ class Trigger {
    * Returns 2 otherwise.
    */
   static int getTriggerWeight( Node n );
-  /** Returns whether n is a trigger term with a local theory extension
-  * property from Bansal et al., CAV 2015.
-  */
-  static bool isLocalTheoryExt( Node n, std::vector< Node >& vars,
-                                std::vector< Node >& patTerms );
   /** get the variable associated with an inversion for n
    *
    * A term n with an inversion variable x has the following property :
@@ -422,8 +403,8 @@ class Trigger {
    */
   static int isTriggerInstanceOf(Node n1,
                                  Node n2,
-                                 std::vector<Node>& fv1,
-                                 std::vector<Node>& fv2);
+                                 const std::vector<Node>& fv1,
+                                 const std::vector<Node>& fv2);
 
   /** add an instantiation (called by InstMatchGenerator)
    *