Split inst match generator into multiple files (#5805)

No code changes on this PR, only move + format.

12 files changed, 1171 insertions, 853 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 60e79fbe3..53420d395 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -658,6 +658,12 @@ libcvc4_add_sources(
   theory/quantifiers/ematching/ho_trigger.h
   theory/quantifiers/ematching/inst_match_generator.cpp
   theory/quantifiers/ematching/inst_match_generator.h
+  theory/quantifiers/ematching/inst_match_generator_multi.cpp
+  theory/quantifiers/ematching/inst_match_generator_multi.h
+  theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+  theory/quantifiers/ematching/inst_match_generator_multi_linear.h
+  theory/quantifiers/ematching/inst_match_generator_simple.cpp
+  theory/quantifiers/ematching/inst_match_generator_simple.h
   theory/quantifiers/ematching/inst_strategy.h
   theory/quantifiers/ematching/inst_strategy_e_matching.cpp
   theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -669,6 +675,8 @@ libcvc4_add_sources(
   theory/quantifiers/ematching/trigger.h
   theory/quantifiers/ematching/trigger_trie.cpp
   theory/quantifiers/ematching/trigger_trie.h
+  theory/quantifiers/ematching/var_match_generator.cpp
+  theory/quantifiers/ematching/var_match_generator.h
   theory/quantifiers/equality_infer.cpp
   theory/quantifiers/equality_infer.h
   theory/quantifiers/equality_query.cpp
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index c8e821dd7..91da843b3 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -9,16 +9,19 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** \brief Implementation of inst match generator class
  **/
+
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 
-#include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
+#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
+#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
+#include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 #include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/ematching/var_match_generator.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
@@ -656,612 +659,6 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n)
   return new InstMatchGenerator(n);
 }
 
-VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) :
-  InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){
-  d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute()));
-  d_var_type = d_var.getType();
-}
-
-int VarMatchGeneratorTermSubs::getNextMatch(Node q,
-                                            InstMatch& m,
-                                            QuantifiersEngine* qe,
-                                            Trigger* tparent)
-{
-  int ret_val = -1;
-  if( !d_eq_class.isNull() ){
-    Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl;
-    TNode tvar = d_var;
-    Node s = d_subs.substitute(tvar, d_eq_class);
-    s = Rewriter::rewrite( s );
-    Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl;
-    d_eq_class = Node::null();
-    //if( s.getType().isSubtypeOf( d_var_type ) ){
-    d_rm_prev = m.get(d_children_types[0]).isNull();
-    if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
-    {
-      return -1;
-    }else{
-      ret_val = continueNextMatch(q, m, qe, tparent);
-      if( ret_val>0 ){
-        return ret_val;
-      }
-    }
-  }
-  if( d_rm_prev ){
-    m.d_vals[d_children_types[0]] = Node::null();
-    d_rm_prev = false;
-  }
-  return -1;
-}
-
-InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) {
-  //order patterns to maximize eager matching failures
-  std::map< Node, std::vector< Node > > var_contains;
-  for (const Node& pat : pats)
-  {
-    quantifiers::TermUtil::computeInstConstContainsForQuant(
-        q, pat, var_contains[pat]);
-  }
-  std::map< Node, std::vector< Node > > var_to_node;
-  for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
-  {
-    for (const Node& n : vc.second)
-    {
-      var_to_node[n].push_back(vc.first);
-    }
-  }
-  std::vector< Node > pats_ordered;
-  std::vector< bool > pats_ordered_independent;
-  std::map< Node, bool > var_bound;
-  size_t patsSize = pats.size();
-  while (pats_ordered.size() < patsSize)
-  {
-    // score is lexographic ( bound vars, shared vars )
-    int score_max_1 = -1;
-    int score_max_2 = -1;
-    unsigned score_index = 0;
-    bool set_score_index = false;
-    for (size_t i = 0; i < patsSize; i++)
-    {
-      Node p = pats[i];
-      if( std::find( pats_ordered.begin(), pats_ordered.end(), p )==pats_ordered.end() ){
-        int score_1 = 0;
-        int score_2 = 0;
-        for( unsigned j=0; j<var_contains[p].size(); j++ ){
-          Node v = var_contains[p][j];
-          if( var_bound.find( v )!=var_bound.end() ){
-            score_1++;
-          }else if( var_to_node[v].size()>1 ){
-            score_2++;
-          }
-        }
-        if (!set_score_index || score_1 > score_max_1
-            || (score_1 == score_max_1 && score_2 > score_max_2))
-        {
-          score_index = i;
-          set_score_index = true;
-          score_max_1 = score_1;
-          score_max_2 = score_2;
-        }
-      }
-    }
-    Assert(set_score_index);
-    //update the variable bounds
-    Node mp = pats[score_index];
-    std::vector<Node>& vcm = var_contains[mp];
-    for (const Node& vc : vcm)
-    {
-      var_bound[vc] = true;
-    }
-    pats_ordered.push_back( mp );
-    pats_ordered_independent.push_back( score_max_1==0 );
-  }
-  
-  Trace("multi-trigger-linear") << "Make children for linear multi trigger." << std::endl;
-  for (size_t i = 0, poSize = pats_ordered.size(); i < poSize; i++)
-  {
-    Node po = pats_ordered[i];
-    Trace("multi-trigger-linear") << "...make for " << po << std::endl;
-    InstMatchGenerator* cimg = getInstMatchGenerator(q, po);
-    Assert(cimg != nullptr);
-    d_children.push_back( cimg );
-    // this could be improved
-    if (i == 0)
-    {
-      cimg->setIndependent();
-    }
-  }
-}
-
-int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){
-  for (InstMatchGenerator* c : d_children)
-  {
-    if (!c->reset(Node::null(), qe))
-    {
-      return -2;
-    }
-  }
-  return 1;
-}
-
-bool InstMatchGeneratorMultiLinear::reset( Node eqc, QuantifiersEngine* qe ) {
-  Assert(eqc.isNull());
-  if( options::multiTriggerLinear() ){
-    return true;
-  }
-  return resetChildren(qe) > 0;
-}
-
-int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
-                                                InstMatch& m,
-                                                QuantifiersEngine* qe,
-                                                Trigger* tparent)
-{
-  Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
-  if( options::multiTriggerLinear() ){
-    //reset everyone
-    int rc_ret = resetChildren( qe );
-    if( rc_ret<0 ){
-      return rc_ret;
-    }
-  }
-  Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl;
-  Assert(d_next != nullptr);
-  int ret_val = continueNextMatch(q, m, qe, tparent);
-  if( ret_val>0 ){
-    Trace("multi-trigger-linear") << "Successful multi-trigger instantiation." << std::endl;
-    if( options::multiTriggerLinear() ){
-      // now, restrict everyone
-      for (size_t i = 0, csize = d_children.size(); i < csize; i++)
-      {
-        Node mi = d_children[i]->getCurrentMatch();
-        Trace("multi-trigger-linear") << "   child " << i << " match : " << mi << std::endl;
-        d_children[i]->excludeMatch( mi );
-      }
-    }
-  }
-  return ret_val;
-}
-
-
-/** constructors */
-InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q,
-                                                 std::vector<Node>& pats,
-                                                 QuantifiersEngine* qe)
-    : d_quant(q)
-{
-  Trace("multi-trigger-cache") << "Making smart multi-trigger for " << q << std::endl;
-  std::map< Node, std::vector< Node > > var_contains;
-  for (const Node& pat : pats)
-  {
-    quantifiers::TermUtil::computeInstConstContainsForQuant(
-        q, pat, var_contains[pat]);
-  }
-  //convert to indicies
-  for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
-  {
-    Trace("multi-trigger-cache") << "Pattern " << vc.first << " contains: ";
-    for (const Node& vcn : vc.second)
-    {
-      Trace("multi-trigger-cache") << vcn << " ";
-      uint64_t index = vcn.getAttribute(InstVarNumAttribute());
-      d_var_contains[vc.first].push_back(index);
-      d_var_to_node[index].push_back(vc.first);
-    }
-    Trace("multi-trigger-cache") << std::endl;
-  }
-  size_t patsSize = pats.size();
-  for (size_t i = 0; i < patsSize; i++)
-  {
-    Node n = pats[i];
-    //make the match generator
-    InstMatchGenerator* img =
-        InstMatchGenerator::mkInstMatchGenerator(q, n, qe);
-    img->setActiveAdd(false);
-    d_children.push_back(img);
-    //compute unique/shared variables
-    std::vector<uint64_t> unique_vars;
-    std::map<uint64_t, bool> shared_vars;
-    unsigned numSharedVars = 0;
-    std::vector<uint64_t>& vctn = d_var_contains[n];
-    for (size_t j = 0, vctnSize = vctn.size(); j < vctnSize; j++)
-    {
-      if (d_var_to_node[vctn[j]].size() == 1)
-      {
-        Trace("multi-trigger-cache")
-            << "Var " << vctn[j] << " is unique to " << pats[i] << std::endl;
-        unique_vars.push_back(vctn[j]);
-      }else{
-        shared_vars[vctn[j]] = true;
-        numSharedVars++;
-      }
-    }
-    //we use the latest shared variables, then unique variables
-    std::vector<uint64_t> vars;
-    size_t index = i == 0 ? pats.size() - 1 : (i - 1);
-    while( numSharedVars>0 && index!=i ){
-      for (std::pair<const uint64_t, bool>& sv : shared_vars)
-      {
-        if (sv.second)
-        {
-          std::vector<uint64_t>& vctni = d_var_contains[pats[index]];
-          if (std::find(vctni.begin(), vctni.end(), sv.first) != vctni.end())
-          {
-            vars.push_back(sv.first);
-            shared_vars[sv.first] = false;
-            numSharedVars--;
-          }
-        }
-      }
-      index = index == 0 ? patsSize - 1 : (index - 1);
-    }
-    vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
-    if (Trace.isOn("multi-trigger-cache"))
-    {
-      Trace("multi-trigger-cache") << "   Index[" << i << "]: ";
-      for (uint64_t v : vars)
-      {
-        Trace("multi-trigger-cache") << v << " ";
-      }
-      Trace("multi-trigger-cache") << std::endl;
-    }
-    //make ordered inst match trie
-    d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
-    d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() );
-    d_children_trie.push_back( InstMatchTrieOrdered( d_imtio[i] ) );
-  }
-}
-
-InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
-{
-  for (size_t i = 0, csize = d_children.size(); i < csize; i++)
-  {
-    delete d_children[i];
-  }
-  for (std::pair<const size_t, InstMatchTrie::ImtIndexOrder*>& i : d_imtio)
-  {
-    delete i.second;
-  }
-}
-
-/** reset instantiation round (call this whenever equivalence classes have changed) */
-void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
-  for (InstMatchGenerator* c : d_children)
-  {
-    c->resetInstantiationRound(qe);
-  }
-}
-
-/** reset, eqc is the equivalence class to search in (any if eqc=null) */
-bool InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
-  for (InstMatchGenerator* c : d_children)
-  {
-    if (!c->reset(eqc, qe))
-    {
-      // do not return false here
-    }
-  }
-  return true;
-}
-
-uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
-                                                    QuantifiersEngine* qe,
-                                                    Trigger* tparent)
-{
-  uint64_t addedLemmas = 0;
-  Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
-  for (size_t i = 0, csize = d_children.size(); i < csize; i++)
-  {
-    Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
-    std::vector< InstMatch > newMatches;
-    InstMatch m( q );
-    while (d_children[i]->getNextMatch(q, m, qe, tparent) > 0)
-    {
-      //m.makeRepresentative( qe );
-      newMatches.push_back( InstMatch( &m ) );
-      m.clear();
-    }
-    Trace("multi-trigger-cache") << "Made " << newMatches.size() << " new matches for index " << i << std::endl;
-    for (size_t j = 0, nmatches = newMatches.size(); j < nmatches; j++)
-    {
-      Trace("multi-trigger-cache2") << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl;
-      processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
-      if( qe->inConflict() ){
-        return addedLemmas;
-      }
-    }
-  }
-  return addedLemmas;
-}
-
-void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
-                                              Trigger* tparent,
-                                              InstMatch& m,
-                                              size_t fromChildIndex,
-                                              uint64_t& addedLemmas)
-{
-  //see if these produce new matches
-  d_children_trie[fromChildIndex].addInstMatch(qe, d_quant, m);
-  //possibly only do the following if we know that new matches will be produced?
-  //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
-  // we can safely skip the following lines, even when we have already produced this match.
-  Trace("multi-trigger-cache-debug") << "Child " << fromChildIndex << " produced match " << m << std::endl;
-  //process new instantiations
-  size_t childIndex = (fromChildIndex + 1) % d_children.size();
-  processNewInstantiations(qe,
-                           tparent,
-                           m,
-                           addedLemmas,
-                           d_children_trie[childIndex].getTrie(),
-                           0,
-                           childIndex,
-                           fromChildIndex,
-                           true);
-}
-
-void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
-                                                       Trigger* tparent,
-                                                       InstMatch& m,
-                                                       uint64_t& addedLemmas,
-                                                       InstMatchTrie* tr,
-                                                       size_t trieIndex,
-                                                       size_t childIndex,
-                                                       size_t endChildIndex,
-                                                       bool modEq)
-{
-  Assert(!qe->inConflict());
-  if( childIndex==endChildIndex ){
-    // m is an instantiation
-    if (sendInstantiation(tparent, m))
-    {
-      addedLemmas++;
-      Trace("multi-trigger-cache-debug") << "-> Produced instantiation " << m
-                                         << std::endl;
-    }
-    return;
-  }
-  InstMatchTrie::ImtIndexOrder* iio = d_children_trie[childIndex].getOrdering();
-  if (trieIndex < iio->d_order.size())
-  {
-    size_t curr_index = iio->d_order[trieIndex];
-    // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant,
-    // curr_index );
-    Node n = m.get( curr_index );
-    if( n.isNull() ){
-      // add to InstMatch
-      for (std::pair<const Node, InstMatchTrie>& d : tr->d_data)
-      {
-        InstMatch mn(&m);
-        mn.setValue(curr_index, d.first);
-        processNewInstantiations(qe,
-                                 tparent,
-                                 mn,
-                                 addedLemmas,
-                                 &(d.second),
-                                 trieIndex + 1,
-                                 childIndex,
-                                 endChildIndex,
-                                 modEq);
-        if (qe->inConflict())
-        {
-          break;
-        }
-      }
-    }
-    // shared and set variable, try to merge
-    std::map<Node, InstMatchTrie>::iterator it = tr->d_data.find(n);
-    if (it != tr->d_data.end())
-    {
-      processNewInstantiations(qe,
-                               tparent,
-                               m,
-                               addedLemmas,
-                               &(it->second),
-                               trieIndex + 1,
-                               childIndex,
-                               endChildIndex,
-                               modEq);
-    }
-    if (!modEq)
-    {
-      return;
-    }
-    eq::EqualityEngine* ee = qe->getEqualityQuery()->getEngine();
-    // check modulo equality for other possible instantiations
-    if (!ee->hasTerm(n))
-    {
-      return;
-    }
-    eq::EqClassIterator eqc(ee->getRepresentative(n), ee);
-    while (!eqc.isFinished())
-    {
-      Node en = (*eqc);
-      if (en != n)
-      {
-        std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
-        if (itc != tr->d_data.end())
-        {
-          processNewInstantiations(qe,
-                                   tparent,
-                                   m,
-                                   addedLemmas,
-                                   &(itc->second),
-                                   trieIndex + 1,
-                                   childIndex,
-                                   endChildIndex,
-                                   modEq);
-          if (qe->inConflict())
-          {
-            break;
-          }
-        }
-      }
-      ++eqc;
-    }
-  }else{
-    size_t newChildIndex = (childIndex + 1) % d_children.size();
-    processNewInstantiations(qe,
-                             tparent,
-                             m,
-                             addedLemmas,
-                             d_children_trie[newChildIndex].getTrie(),
-                             0,
-                             newChildIndex,
-                             endChildIndex,
-                             modEq);
-  }
-}
-
-InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q,
-                                                   Node pat,
-                                                   QuantifiersEngine* qe)
-    : d_quant(q), d_match_pattern(pat)
-{
-  if( d_match_pattern.getKind()==NOT ){
-    d_match_pattern = d_match_pattern[0];
-    d_pol = false;
-  }else{
-    d_pol = true;
-  }
-  if( d_match_pattern.getKind()==EQUAL ){
-    d_eqc = d_match_pattern[1];
-    d_match_pattern = d_match_pattern[0];
-    Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc));
-  }
-  Assert(Trigger::isSimpleTrigger(d_match_pattern));
-  for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
-  {
-    if( d_match_pattern[i].getKind()==INST_CONSTANT ){
-      if( !options::cegqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
-        d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
-      }else{
-        d_var_num[i] = -1;
-      }
-    }
-    d_match_pattern_arg_types.push_back( d_match_pattern[i].getType() );
-  }
-  d_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
-}
-
-void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) {
-  
-}
-uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
-                                                     QuantifiersEngine* qe,
-                                                     Trigger* tparent)
-{
-  uint64_t addedLemmas = 0;
-  TNodeTrie* tat;
-  if( d_eqc.isNull() ){
-    tat = qe->getTermDatabase()->getTermArgTrie( d_op );
-  }else{
-    if( d_pol ){
-      tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
-    }else{
-      //iterate over all classes except r
-      tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op );
-      if (tat && !qe->inConflict())
-      {
-        Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
-        for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
-        {
-          if (t.first != r)
-          {
-            InstMatch m( q );
-            addInstantiations(m, qe, addedLemmas, 0, &(t.second));
-            if( qe->inConflict() ){
-              break;
-            }
-          }
-        }
-      }
-      tat = nullptr;
-    }
-  }
-  Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
-  if (tat && !qe->inConflict())
-  {
-    InstMatch m( q );
-    addInstantiations( m, qe, addedLemmas, 0, tat );
-  }
-  return addedLemmas;
-}
-
-void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
-                                                 QuantifiersEngine* qe,
-                                                 uint64_t& addedLemmas,
-                                                 size_t argIndex,
-                                                 TNodeTrie* tat)
-{
-  Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
-  if (argIndex == d_match_pattern.getNumChildren())
-  {
-    Assert(!tat->d_data.empty());
-    TNode t = tat->getData();
-    Debug("simple-trigger") << "Actual term is " << t << std::endl;
-    //convert to actual used terms
-    for (const std::pair<unsigned, int>& v : d_var_num)
-    {
-      if (v.second >= 0)
-      {
-        Assert(v.first < t.getNumChildren());
-        Debug("simple-trigger")
-            << "...set " << v.second << " " << t[v.first] << std::endl;
-        m.setValue(v.second, t[v.first]);
-      }
-    }
-    // we do not need the trigger parent for simple triggers (no post-processing
-    // required)
-    if (qe->getInstantiate()->addInstantiation(d_quant, m))
-    {
-      addedLemmas++;
-      Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
-    }
-    return;
-  }
-  if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
-  {
-    int v = d_var_num[argIndex];
-    if (v != -1)
-    {
-      for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
-      {
-        Node t = tt.first;
-        Node prev = m.get(v);
-        // using representatives, just check if equal
-        Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
-        if (prev.isNull() || prev == t)
-        {
-          m.setValue(v, t);
-          addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
-          m.setValue(v, prev);
-          if (qe->inConflict())
-          {
-            break;
-          }
-        }
-      }
-      return;
-    }
-    // inst constant from another quantified formula, treat as ground term TODO:
-    // remove this?
-  }
-  Node r = qe->getEqualityQuery()->getRepresentative(d_match_pattern[argIndex]);
-  std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
-  if (it != tat->d_data.end())
-  {
-    addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second));
-  }
-}
-
-int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) {
-  Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
-  size_t ngt = qe->getTermDatabase()->getNumGroundTerms(f);
-  Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " << f << " is " << ngt << std::endl;
-  return static_cast<int>(ngt);
-}
-
-
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 99816c040..f03d1cf20 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -416,250 +416,6 @@ class InstMatchGenerator : public IMGenerator {
   static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
 };/* class InstMatchGenerator */
 
-/** match generator for purified terms
-* This handles the special case of invertible terms like x+1 (see
-* Trigger::getTermInversionVariable).
-*/
-class VarMatchGeneratorTermSubs : public InstMatchGenerator {
-public:
-  VarMatchGeneratorTermSubs( Node var, Node subs );
-
-  /** Reset */
-  bool reset(Node eqc, QuantifiersEngine* qe) override
-  {
-    d_eq_class = eqc;
-    return true;
-  }
-  /** Get the next match. */
-  int getNextMatch(Node q,
-                   InstMatch& m,
-                   QuantifiersEngine* qe,
-                   Trigger* tparent) override;
-
- private:
-  /** variable we are matching (x in the example x+1). */
-  Node d_var;
-  /** cache of d_var.getType() */
-  TypeNode d_var_type;
-  /** The substitution for what we match (x-1 in the example x+1). */
-  Node d_subs;
-  /** stores whether we have written a value for d_var in the current match. */
-  bool d_rm_prev;
-};
-
-/** InstMatchGeneratorMultiLinear class
-*
-* This is the default implementation of multi-triggers.
-*
-* Handling multi-triggers using this class is done by constructing a linked
-* list of InstMatchGenerator classes (see mkInstMatchGeneratorMulti), with one
-* InstMatchGeneratorMultiLinear at the head and a list of trailing
-* InstMatchGenerators.
-*
-* CVC4 employs techniques that ensure that the number of instantiations
-* is worst-case polynomial wrt the number of ground terms, where this class
-* lifts this policy to multi-triggers. In particular consider
-*
-*  multi-trigger : { f( x1 ), f( x2 ), f( x3 ), f( x4 ) }
-*
-* For this multi-trigger, we insist that for each i=1...4, and each ground term
-* t, there is at most 1 instantiation added as a result of matching
-*    ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
-* against ground terms of the form
-*    ( s_1, s_2, s_3, s_4 ) where t = s_i for i=1,...,4.
-* Meaning we add instantiations for the multi-trigger
-* ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) based on matching pairwise against:
-*   ( f( c_i11 ), f( c_i21 ), f( c_i31 ), f( c_i41 ) )
-*   ( f( c_i12 ), f( c_i22 ), f( c_i32 ), f( c_i42 ) )
-*   ( f( c_i13 ), f( c_i23 ), f( c_i33 ), f( c_i43 ) )
-* Where we require c_i{jk} != c_i{jl} for each i=1...4, k != l.
-*
-* For example, we disallow adding instantiations based on matching against both
-* ( f( c_1 ), f( c_2 ), f( c_4 ), f( c_6 ) ) and
-* ( f( c_1 ), f( c_3 ), f( c_5 ), f( c_7 ) )
-* against ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ), since f( c_1 ) is matched
-* against f( x1 ) twice.
-*
-* This policy can be disabled by --no-multi-trigger-linear.
-*
-*/
-class InstMatchGeneratorMultiLinear : public InstMatchGenerator {
-  friend class InstMatchGenerator;
-
- public:
-  /** Reset. */
-  bool reset(Node eqc, QuantifiersEngine* qe) override;
-  /** Get the next match. */
-  int getNextMatch(Node q,
-                   InstMatch& m,
-                   QuantifiersEngine* qe,
-                   Trigger* tparent) override;
-
- protected:
-  /** reset the children of this generator */
-  int resetChildren(QuantifiersEngine* qe);
-  /** constructor */
-  InstMatchGeneratorMultiLinear(Node q,
-                                std::vector<Node>& pats,
-                                QuantifiersEngine* qe);
-};/* class InstMatchGeneratorMulti */
-
-/** InstMatchGeneratorMulti
-*
-* This is an earlier implementation of multi-triggers
-* that is enabled by --multi-trigger-cache.
-* This generator takes the product of instantiations
-* found by single trigger matching, and does
-* not have the guarantee that the number of
-* instantiations is polynomial wrt the number of
-* ground terms.
-*/
-class InstMatchGeneratorMulti : public IMGenerator {
- public:
-  /** constructors */
-  InstMatchGeneratorMulti(Node q,
-                          std::vector<Node>& pats,
-                          QuantifiersEngine* qe);
-  /** destructor */
-  ~InstMatchGeneratorMulti() override;
-
-  /** Reset instantiation round. */
-  void resetInstantiationRound(QuantifiersEngine* qe) override;
-  /** Reset. */
-  bool reset(Node eqc, QuantifiersEngine* qe) override;
-  /** Add instantiations. */
-  uint64_t addInstantiations(Node q,
-                             QuantifiersEngine* qe,
-                             Trigger* tparent) override;
-
- private:
-  /** process new match
-   *
-   * Called during addInstantiations(...).
-   * Indicates we produced a match m for child fromChildIndex
-   * addedLemmas is how many instantiations we succesfully send
-   * via IMGenerator::sendInstantiation(...) calls.
-   */
-  void processNewMatch(QuantifiersEngine* qe,
-                       Trigger* tparent,
-                       InstMatch& m,
-                       size_t fromChildIndex,
-                       uint64_t& addedLemmas);
-  /** helper for process new match
-   * tr is the inst match trie (term index) we are currently traversing.
-   * trieIndex is depth we are in trie tr.
-   * childIndex is the index of the term in the multi trigger we are currently
-   *               processing.
-   * endChildIndex is the index of the term in the multi trigger that generated
-   *                  a new term, and hence we will end when the product
-   *                  computed by this function returns to.
-   * modEq is whether we are matching modulo equality.
-   */
-  void processNewInstantiations(QuantifiersEngine* qe,
-                                Trigger* tparent,
-                                InstMatch& m,
-                                uint64_t& addedLemmas,
-                                InstMatchTrie* tr,
-                                size_t trieIndex,
-                                size_t childIndex,
-                                size_t endChildIndex,
-                                bool modEq);
-  /** Map from pattern nodes to indices of variables they contain. */
-  std::map<Node, std::vector<uint64_t> > d_var_contains;
-  /** Map from variable indices to pattern nodes that contain them. */
-  std::map<uint64_t, std::vector<Node> > d_var_to_node;
-  /** quantified formula we are producing matches for */
-  Node d_quant;
-  /** children generators
-   * These are inst match generators for each term in the multi trigger.
-   */
-  std::vector< InstMatchGenerator* > d_children;
-  /** variable orderings
-   * Stores a heuristically determined variable ordering (unique
-   * variables first) for each term in the multi trigger.
-   */
-  std::map<size_t, InstMatchTrie::ImtIndexOrder*> d_imtio;
-  /** inst match tries for each child node
-   * This data structure stores all InstMatch objects generated
-   * by matching for each term in the multi trigger.
-   */
-  std::vector< InstMatchTrieOrdered > d_children_trie;
-};/* class InstMatchGeneratorMulti */
-
-/** InstMatchGeneratorSimple class
-*
-* This is the default generator class for simple single triggers.
-* For example, { f( x, a ) }, { f( x, x ) } and { f( x, y ) } are simple single
-* triggers. In practice, around 70-90% of triggers are simple single triggers.
-*
-* Notice that simple triggers also can have an attached polarity.
-* For example, { P( x ) = false }, { f( x, y ) = a } and { ~f( a, x ) = b } are
-* simple single triggers.
-*
-* The implementation traverses the term indices in TermDatabase for adding
-* instantiations, which is more efficient than the techniques required for
-* handling non-simple single triggers.
-*
-* In contrast to other instantiation generators, it does not call
-* IMGenerator::sendInstantiation and for performance reasons instead calls
-* qe->getInstantiate()->addInstantiation(...) directly.
-*/
-class InstMatchGeneratorSimple : public IMGenerator {
- public:
-  /** constructors */
-  InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe);
-
-  /** Reset instantiation round. */
-  void resetInstantiationRound(QuantifiersEngine* qe) override;
-  /** Add instantiations. */
-  uint64_t addInstantiations(Node q,
-                             QuantifiersEngine* qe,
-                             Trigger* tparent) override;
-  /** Get active score. */
-  int getActiveScore(QuantifiersEngine* qe) override;
-
- private:
-  /** quantified formula for the trigger term */
-  Node d_quant;
-  /** the trigger term */
-  Node d_match_pattern;
-  /** equivalence class polarity information
-   *
-  * This stores the required polarity/equivalence class with this trigger.
-  * If d_eqc is non-null, we only produce matches { x->t } such that
-  * our context does not entail
-  *   ( d_match_pattern*{ x->t } = d_eqc) if d_pol = true, or
-  *   ( d_match_pattern*{ x->t } != d_eqc) if d_pol = false.
-  * where * denotes application of substitution.
-  */
-  bool d_pol;
-  Node d_eqc;
-  /** Match pattern arg types.
-   * Cached values of d_match_pattern[i].getType().
-   */
-  std::vector< TypeNode > d_match_pattern_arg_types;
-  /** The match operator d_match_pattern (see TermDb::getMatchOperator). */
-  Node d_op;
-  /**
-   * Map from child number of d_match_pattern to variable index, or -1 if the
-   * child is not a variable.
-   */
-  std::map<size_t, int> d_var_num;
-  /** add instantiations, helper function.
-   *
-   * m is the current match we are building,
-   * addedLemmas is the number of lemmas we have added via calls to
-   *                qe->getInstantiate()->aaddInstantiation(...),
-   * argIndex is the argument index in d_match_pattern we are currently
-   *              matching,
-   * tat is the term index we are currently traversing.
-   */
-  void addInstantiations(InstMatch& m,
-                         QuantifiersEngine* qe,
-                         uint64_t& addedLemmas,
-                         size_t argIndex,
-                         TNodeTrie* tat);
-};/* class InstMatchGeneratorSimple */
 }
 }
 }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
new file mode 100644
index 000000000..b4a7457a3
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -0,0 +1,333 @@
+/*********************                                                        */
+/*! \file inst_match_generator_multi.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief multi inst match generator class
+ **/
+
+#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
+
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q,
+                                                 std::vector<Node>& pats,
+                                                 QuantifiersEngine* qe)
+    : d_quant(q)
+{
+  Trace("multi-trigger-cache")
+      << "Making smart multi-trigger for " << q << std::endl;
+  std::map<Node, std::vector<Node> > var_contains;
+  for (const Node& pat : pats)
+  {
+    quantifiers::TermUtil::computeInstConstContainsForQuant(
+        q, pat, var_contains[pat]);
+  }
+  // convert to indicies
+  for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
+  {
+    Trace("multi-trigger-cache") << "Pattern " << vc.first << " contains: ";
+    for (const Node& vcn : vc.second)
+    {
+      Trace("multi-trigger-cache") << vcn << " ";
+      uint64_t index = vcn.getAttribute(InstVarNumAttribute());
+      d_var_contains[vc.first].push_back(index);
+      d_var_to_node[index].push_back(vc.first);
+    }
+    Trace("multi-trigger-cache") << std::endl;
+  }
+  size_t patsSize = pats.size();
+  for (size_t i = 0; i < patsSize; i++)
+  {
+    Node n = pats[i];
+    // make the match generator
+    InstMatchGenerator* img =
+        InstMatchGenerator::mkInstMatchGenerator(q, n, qe);
+    img->setActiveAdd(false);
+    d_children.push_back(img);
+    // compute unique/shared variables
+    std::vector<uint64_t> unique_vars;
+    std::map<uint64_t, bool> shared_vars;
+    unsigned numSharedVars = 0;
+    std::vector<uint64_t>& vctn = d_var_contains[n];
+    for (size_t j = 0, vctnSize = vctn.size(); j < vctnSize; j++)
+    {
+      if (d_var_to_node[vctn[j]].size() == 1)
+      {
+        Trace("multi-trigger-cache")
+            << "Var " << vctn[j] << " is unique to " << pats[i] << std::endl;
+        unique_vars.push_back(vctn[j]);
+      }
+      else
+      {
+        shared_vars[vctn[j]] = true;
+        numSharedVars++;
+      }
+    }
+    // we use the latest shared variables, then unique variables
+    std::vector<uint64_t> vars;
+    size_t index = i == 0 ? pats.size() - 1 : (i - 1);
+    while (numSharedVars > 0 && index != i)
+    {
+      for (std::pair<const uint64_t, bool>& sv : shared_vars)
+      {
+        if (sv.second)
+        {
+          std::vector<uint64_t>& vctni = d_var_contains[pats[index]];
+          if (std::find(vctni.begin(), vctni.end(), sv.first) != vctni.end())
+          {
+            vars.push_back(sv.first);
+            shared_vars[sv.first] = false;
+            numSharedVars--;
+          }
+        }
+      }
+      index = index == 0 ? patsSize - 1 : (index - 1);
+    }
+    vars.insert(vars.end(), unique_vars.begin(), unique_vars.end());
+    if (Trace.isOn("multi-trigger-cache"))
+    {
+      Trace("multi-trigger-cache") << "   Index[" << i << "]: ";
+      for (uint64_t v : vars)
+      {
+        Trace("multi-trigger-cache") << v << " ";
+      }
+      Trace("multi-trigger-cache") << std::endl;
+    }
+    // make ordered inst match trie
+    d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
+    d_imtio[i]->d_order.insert(
+        d_imtio[i]->d_order.begin(), vars.begin(), vars.end());
+    d_children_trie.push_back(InstMatchTrieOrdered(d_imtio[i]));
+  }
+}
+
+InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
+{
+  for (size_t i = 0, csize = d_children.size(); i < csize; i++)
+  {
+    delete d_children[i];
+  }
+  for (std::pair<const size_t, InstMatchTrie::ImtIndexOrder*>& i : d_imtio)
+  {
+    delete i.second;
+  }
+}
+
+/** reset instantiation round (call this whenever equivalence classes have
+ * changed) */
+void InstMatchGeneratorMulti::resetInstantiationRound(QuantifiersEngine* qe)
+{
+  for (InstMatchGenerator* c : d_children)
+  {
+    c->resetInstantiationRound(qe);
+  }
+}
+
+/** reset, eqc is the equivalence class to search in (any if eqc=null) */
+bool InstMatchGeneratorMulti::reset(Node eqc, QuantifiersEngine* qe)
+{
+  for (InstMatchGenerator* c : d_children)
+  {
+    if (!c->reset(eqc, qe))
+    {
+      // do not return false here
+    }
+  }
+  return true;
+}
+
+uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
+                                                    QuantifiersEngine* qe,
+                                                    Trigger* tparent)
+{
+  uint64_t addedLemmas = 0;
+  Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
+  for (size_t i = 0, csize = d_children.size(); i < csize; i++)
+  {
+    Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
+    std::vector<InstMatch> newMatches;
+    InstMatch m(q);
+    while (d_children[i]->getNextMatch(q, m, qe, tparent) > 0)
+    {
+      // m.makeRepresentative( qe );
+      newMatches.push_back(InstMatch(&m));
+      m.clear();
+    }
+    Trace("multi-trigger-cache") << "Made " << newMatches.size()
+                                 << " new matches for index " << i << std::endl;
+    for (size_t j = 0, nmatches = newMatches.size(); j < nmatches; j++)
+    {
+      Trace("multi-trigger-cache2")
+          << "...processing " << j << " / " << newMatches.size()
+          << ", #lemmas = " << addedLemmas << std::endl;
+      processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
+      if (qe->inConflict())
+      {
+        return addedLemmas;
+      }
+    }
+  }
+  return addedLemmas;
+}
+
+void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
+                                              Trigger* tparent,
+                                              InstMatch& m,
+                                              size_t fromChildIndex,
+                                              uint64_t& addedLemmas)
+{
+  // see if these produce new matches
+  d_children_trie[fromChildIndex].addInstMatch(qe, d_quant, m);
+  // possibly only do the following if we know that new matches will be
+  // produced? the issue is that instantiations are filtered in quantifiers
+  // engine, and so there is no guarentee that
+  // we can safely skip the following lines, even when we have already produced
+  // this match.
+  Trace("multi-trigger-cache-debug")
+      << "Child " << fromChildIndex << " produced match " << m << std::endl;
+  // process new instantiations
+  size_t childIndex = (fromChildIndex + 1) % d_children.size();
+  processNewInstantiations(qe,
+                           tparent,
+                           m,
+                           addedLemmas,
+                           d_children_trie[childIndex].getTrie(),
+                           0,
+                           childIndex,
+                           fromChildIndex,
+                           true);
+}
+
+void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
+                                                       Trigger* tparent,
+                                                       InstMatch& m,
+                                                       uint64_t& addedLemmas,
+                                                       InstMatchTrie* tr,
+                                                       size_t trieIndex,
+                                                       size_t childIndex,
+                                                       size_t endChildIndex,
+                                                       bool modEq)
+{
+  Assert(!qe->inConflict());
+  if (childIndex == endChildIndex)
+  {
+    // m is an instantiation
+    if (sendInstantiation(tparent, m))
+    {
+      addedLemmas++;
+      Trace("multi-trigger-cache-debug")
+          << "-> Produced instantiation " << m << std::endl;
+    }
+    return;
+  }
+  InstMatchTrie::ImtIndexOrder* iio = d_children_trie[childIndex].getOrdering();
+  if (trieIndex < iio->d_order.size())
+  {
+    size_t curr_index = iio->d_order[trieIndex];
+    // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant,
+    // curr_index );
+    Node n = m.get(curr_index);
+    if (n.isNull())
+    {
+      // add to InstMatch
+      for (std::pair<const Node, InstMatchTrie>& d : tr->d_data)
+      {
+        InstMatch mn(&m);
+        mn.setValue(curr_index, d.first);
+        processNewInstantiations(qe,
+                                 tparent,
+                                 mn,
+                                 addedLemmas,
+                                 &(d.second),
+                                 trieIndex + 1,
+                                 childIndex,
+                                 endChildIndex,
+                                 modEq);
+        if (qe->inConflict())
+        {
+          break;
+        }
+      }
+    }
+    // shared and set variable, try to merge
+    std::map<Node, InstMatchTrie>::iterator it = tr->d_data.find(n);
+    if (it != tr->d_data.end())
+    {
+      processNewInstantiations(qe,
+                               tparent,
+                               m,
+                               addedLemmas,
+                               &(it->second),
+                               trieIndex + 1,
+                               childIndex,
+                               endChildIndex,
+                               modEq);
+    }
+    if (!modEq)
+    {
+      return;
+    }
+    eq::EqualityEngine* ee = qe->getEqualityQuery()->getEngine();
+    // check modulo equality for other possible instantiations
+    if (!ee->hasTerm(n))
+    {
+      return;
+    }
+    eq::EqClassIterator eqc(ee->getRepresentative(n), ee);
+    while (!eqc.isFinished())
+    {
+      Node en = (*eqc);
+      if (en != n)
+      {
+        std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
+        if (itc != tr->d_data.end())
+        {
+          processNewInstantiations(qe,
+                                   tparent,
+                                   m,
+                                   addedLemmas,
+                                   &(itc->second),
+                                   trieIndex + 1,
+                                   childIndex,
+                                   endChildIndex,
+                                   modEq);
+          if (qe->inConflict())
+          {
+            break;
+          }
+        }
+      }
+      ++eqc;
+    }
+  }
+  else
+  {
+    size_t newChildIndex = (childIndex + 1) % d_children.size();
+    processNewInstantiations(qe,
+                             tparent,
+                             m,
+                             addedLemmas,
+                             d_children_trie[newChildIndex].getTrie(),
+                             0,
+                             newChildIndex,
+                             endChildIndex,
+                             modEq);
+  }
+}
+
+}  // namespace inst
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
new file mode 100644
index 000000000..b68d362cc
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
@@ -0,0 +1,113 @@
+/*********************                                                        */
+/*! \file inst_match_generator_multi.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief multi inst match generator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
+#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
+
+#include <map>
+#include <vector>
+#include "expr/node_trie.h"
+#include "theory/quantifiers/ematching/inst_match_generator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+/** InstMatchGeneratorMulti
+ *
+ * This is an earlier implementation of multi-triggers that is enabled by
+ * --multi-trigger-cache. This generator takes the product of instantiations
+ * found by single trigger matching, and does not have the guarantee that the
+ * number of instantiations is polynomial wrt the number of ground terms.
+ */
+class InstMatchGeneratorMulti : public IMGenerator
+{
+ public:
+  /** constructors */
+  InstMatchGeneratorMulti(Node q,
+                          std::vector<Node>& pats,
+                          QuantifiersEngine* qe);
+  /** destructor */
+  ~InstMatchGeneratorMulti() override;
+
+  /** Reset instantiation round. */
+  void resetInstantiationRound(QuantifiersEngine* qe) override;
+  /** Reset. */
+  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  /** Add instantiations. */
+  uint64_t addInstantiations(Node q,
+                             QuantifiersEngine* qe,
+                             Trigger* tparent) override;
+
+ private:
+  /** process new match
+   *
+   * Called during addInstantiations(...).
+   * Indicates we produced a match m for child fromChildIndex
+   * addedLemmas is how many instantiations we succesfully send
+   * via IMGenerator::sendInstantiation(...) calls.
+   */
+  void processNewMatch(QuantifiersEngine* qe,
+                       Trigger* tparent,
+                       InstMatch& m,
+                       size_t fromChildIndex,
+                       uint64_t& addedLemmas);
+  /** helper for process new match
+   * tr is the inst match trie (term index) we are currently traversing.
+   * trieIndex is depth we are in trie tr.
+   * childIndex is the index of the term in the multi trigger we are currently
+   *               processing.
+   * endChildIndex is the index of the term in the multi trigger that generated
+   *                  a new term, and hence we will end when the product
+   *                  computed by this function returns to.
+   * modEq is whether we are matching modulo equality.
+   */
+  void processNewInstantiations(QuantifiersEngine* qe,
+                                Trigger* tparent,
+                                InstMatch& m,
+                                uint64_t& addedLemmas,
+                                InstMatchTrie* tr,
+                                size_t trieIndex,
+                                size_t childIndex,
+                                size_t endChildIndex,
+                                bool modEq);
+  /** Map from pattern nodes to indices of variables they contain. */
+  std::map<Node, std::vector<uint64_t> > d_var_contains;
+  /** Map from variable indices to pattern nodes that contain them. */
+  std::map<uint64_t, std::vector<Node> > d_var_to_node;
+  /** quantified formula we are producing matches for */
+  Node d_quant;
+  /** children generators
+   * These are inst match generators for each term in the multi trigger.
+   */
+  std::vector<InstMatchGenerator*> d_children;
+  /** variable orderings
+   * Stores a heuristically determined variable ordering (unique
+   * variables first) for each term in the multi trigger.
+   */
+  std::map<size_t, InstMatchTrie::ImtIndexOrder*> d_imtio;
+  /** inst match tries for each child node
+   * This data structure stores all InstMatch objects generated
+   * by matching for each term in the multi trigger.
+   */
+  std::vector<InstMatchTrieOrdered> d_children_trie;
+};
+
+}  // namespace inst
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
new file mode 100644
index 000000000..1eb9ccdad
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -0,0 +1,176 @@
+/*********************                                                        */
+/*! \file inst_match_generator_multi_linear.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of multi-linear inst match generator class
+ **/
+#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
+
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
+    Node q, std::vector<Node>& pats, QuantifiersEngine* qe)
+{
+  // order patterns to maximize eager matching failures
+  std::map<Node, std::vector<Node> > var_contains;
+  for (const Node& pat : pats)
+  {
+    quantifiers::TermUtil::computeInstConstContainsForQuant(
+        q, pat, var_contains[pat]);
+  }
+  std::map<Node, std::vector<Node> > var_to_node;
+  for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
+  {
+    for (const Node& n : vc.second)
+    {
+      var_to_node[n].push_back(vc.first);
+    }
+  }
+  std::vector<Node> pats_ordered;
+  std::vector<bool> pats_ordered_independent;
+  std::map<Node, bool> var_bound;
+  size_t patsSize = pats.size();
+  while (pats_ordered.size() < patsSize)
+  {
+    // score is lexographic ( bound vars, shared vars )
+    int score_max_1 = -1;
+    int score_max_2 = -1;
+    unsigned score_index = 0;
+    bool set_score_index = false;
+    for (size_t i = 0; i < patsSize; i++)
+    {
+      Node p = pats[i];
+      if (std::find(pats_ordered.begin(), pats_ordered.end(), p)
+          == pats_ordered.end())
+      {
+        int score_1 = 0;
+        int score_2 = 0;
+        for (unsigned j = 0; j < var_contains[p].size(); j++)
+        {
+          Node v = var_contains[p][j];
+          if (var_bound.find(v) != var_bound.end())
+          {
+            score_1++;
+          }
+          else if (var_to_node[v].size() > 1)
+          {
+            score_2++;
+          }
+        }
+        if (!set_score_index || score_1 > score_max_1
+            || (score_1 == score_max_1 && score_2 > score_max_2))
+        {
+          score_index = i;
+          set_score_index = true;
+          score_max_1 = score_1;
+          score_max_2 = score_2;
+        }
+      }
+    }
+    Assert(set_score_index);
+    // update the variable bounds
+    Node mp = pats[score_index];
+    std::vector<Node>& vcm = var_contains[mp];
+    for (const Node& vc : vcm)
+    {
+      var_bound[vc] = true;
+    }
+    pats_ordered.push_back(mp);
+    pats_ordered_independent.push_back(score_max_1 == 0);
+  }
+
+  Trace("multi-trigger-linear")
+      << "Make children for linear multi trigger." << std::endl;
+  for (size_t i = 0, poSize = pats_ordered.size(); i < poSize; i++)
+  {
+    Node po = pats_ordered[i];
+    Trace("multi-trigger-linear") << "...make for " << po << std::endl;
+    InstMatchGenerator* cimg = getInstMatchGenerator(q, po);
+    Assert(cimg != nullptr);
+    d_children.push_back(cimg);
+    // this could be improved
+    if (i == 0)
+    {
+      cimg->setIndependent();
+    }
+  }
+}
+
+int InstMatchGeneratorMultiLinear::resetChildren(QuantifiersEngine* qe)
+{
+  for (InstMatchGenerator* c : d_children)
+  {
+    if (!c->reset(Node::null(), qe))
+    {
+      return -2;
+    }
+  }
+  return 1;
+}
+
+bool InstMatchGeneratorMultiLinear::reset(Node eqc, QuantifiersEngine* qe)
+{
+  Assert(eqc.isNull());
+  if (options::multiTriggerLinear())
+  {
+    return true;
+  }
+  return resetChildren(qe) > 0;
+}
+
+int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
+                                                InstMatch& m,
+                                                QuantifiersEngine* qe,
+                                                Trigger* tparent)
+{
+  Trace("multi-trigger-linear-debug")
+      << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
+  if (options::multiTriggerLinear())
+  {
+    // reset everyone
+    int rc_ret = resetChildren(qe);
+    if (rc_ret < 0)
+    {
+      return rc_ret;
+    }
+  }
+  Trace("multi-trigger-linear-debug")
+      << "InstMatchGeneratorMultiLinear::getNextMatch : continue match "
+      << std::endl;
+  Assert(d_next != nullptr);
+  int ret_val = continueNextMatch(q, m, qe, tparent);
+  if (ret_val > 0)
+  {
+    Trace("multi-trigger-linear")
+        << "Successful multi-trigger instantiation." << std::endl;
+    if (options::multiTriggerLinear())
+    {
+      // now, restrict everyone
+      for (size_t i = 0, csize = d_children.size(); i < csize; i++)
+      {
+        Node mi = d_children[i]->getCurrentMatch();
+        Trace("multi-trigger-linear")
+            << "   child " << i << " match : " << mi << std::endl;
+        d_children[i]->excludeMatch(mi);
+      }
+    }
+  }
+  return ret_val;
+}
+
+}  // namespace inst
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
new file mode 100644
index 000000000..245b3d794
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
@@ -0,0 +1,91 @@
+/*********************                                                        */
+/*! \file inst_match_generator_multi_linear.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief multi-linear inst match generator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
+#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/quantifiers/ematching/inst_match_generator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+/** InstMatchGeneratorMultiLinear class
+ *
+ * This is the default implementation of multi-triggers.
+ *
+ * Handling multi-triggers using this class is done by constructing a linked
+ * list of InstMatchGenerator classes (see mkInstMatchGeneratorMulti), with one
+ * InstMatchGeneratorMultiLinear at the head and a list of trailing
+ * InstMatchGenerators.
+ *
+ * CVC4 employs techniques that ensure that the number of instantiations
+ * is worst-case polynomial wrt the number of ground terms, where this class
+ * lifts this policy to multi-triggers. In particular consider
+ *
+ *  multi-trigger : { f( x1 ), f( x2 ), f( x3 ), f( x4 ) }
+ *
+ * For this multi-trigger, we insist that for each i=1...4, and each ground term
+ * t, there is at most 1 instantiation added as a result of matching
+ *    ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
+ * against ground terms of the form
+ *    ( s_1, s_2, s_3, s_4 ) where t = s_i for i=1,...,4.
+ * Meaning we add instantiations for the multi-trigger
+ * ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) based on matching pairwise against:
+ *   ( f( c_i11 ), f( c_i21 ), f( c_i31 ), f( c_i41 ) )
+ *   ( f( c_i12 ), f( c_i22 ), f( c_i32 ), f( c_i42 ) )
+ *   ( f( c_i13 ), f( c_i23 ), f( c_i33 ), f( c_i43 ) )
+ * Where we require c_i{jk} != c_i{jl} for each i=1...4, k != l.
+ *
+ * For example, we disallow adding instantiations based on matching against both
+ * ( f( c_1 ), f( c_2 ), f( c_4 ), f( c_6 ) ) and
+ * ( f( c_1 ), f( c_3 ), f( c_5 ), f( c_7 ) )
+ * against ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ), since f( c_1 ) is matched
+ * against f( x1 ) twice.
+ *
+ * This policy can be disabled by --no-multi-trigger-linear.
+ *
+ */
+class InstMatchGeneratorMultiLinear : public InstMatchGenerator
+{
+  friend class InstMatchGenerator;
+
+ public:
+  /** Reset. */
+  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  /** Get the next match. */
+  int getNextMatch(Node q,
+                   InstMatch& m,
+                   QuantifiersEngine* qe,
+                   Trigger* tparent) override;
+
+ protected:
+  /** reset the children of this generator */
+  int resetChildren(QuantifiersEngine* qe);
+  /** constructor */
+  InstMatchGeneratorMultiLinear(Node q,
+                                std::vector<Node>& pats,
+                                QuantifiersEngine* qe);
+};
+
+}  // namespace inst
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
new file mode 100644
index 000000000..995888ba2
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -0,0 +1,193 @@
+/*********************                                                        */
+/*! \file inst_match_generator_simple.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief  simple inst match generator class
+ **/
+#include "theory/quantifiers/ematching/inst_match_generator_simple.h"
+
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q,
+                                                   Node pat,
+                                                   QuantifiersEngine* qe)
+    : d_quant(q), d_match_pattern(pat)
+{
+  if (d_match_pattern.getKind() == NOT)
+  {
+    d_match_pattern = d_match_pattern[0];
+    d_pol = false;
+  }
+  else
+  {
+    d_pol = true;
+  }
+  if (d_match_pattern.getKind() == EQUAL)
+  {
+    d_eqc = d_match_pattern[1];
+    d_match_pattern = d_match_pattern[0];
+    Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc));
+  }
+  Assert(Trigger::isSimpleTrigger(d_match_pattern));
+  for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
+  {
+    if (d_match_pattern[i].getKind() == INST_CONSTANT)
+    {
+      if (!options::cegqi()
+          || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]) == q)
+      {
+        d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
+      }
+      else
+      {
+        d_var_num[i] = -1;
+      }
+    }
+    d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
+  }
+  d_op = qe->getTermDatabase()->getMatchOperator(d_match_pattern);
+}
+
+void InstMatchGeneratorSimple::resetInstantiationRound(QuantifiersEngine* qe) {}
+uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
+                                                     QuantifiersEngine* qe,
+                                                     Trigger* tparent)
+{
+  uint64_t addedLemmas = 0;
+  TNodeTrie* tat;
+  if (d_eqc.isNull())
+  {
+    tat = qe->getTermDatabase()->getTermArgTrie(d_op);
+  }
+  else
+  {
+    if (d_pol)
+    {
+      tat = qe->getTermDatabase()->getTermArgTrie(d_eqc, d_op);
+    }
+    else
+    {
+      // iterate over all classes except r
+      tat = qe->getTermDatabase()->getTermArgTrie(Node::null(), d_op);
+      if (tat && !qe->inConflict())
+      {
+        Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
+        for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
+        {
+          if (t.first != r)
+          {
+            InstMatch m(q);
+            addInstantiations(m, qe, addedLemmas, 0, &(t.second));
+            if (qe->inConflict())
+            {
+              break;
+            }
+          }
+        }
+      }
+      tat = nullptr;
+    }
+  }
+  Debug("simple-trigger-debug")
+      << "Adding instantiations based on " << tat << " from " << d_op << " "
+      << d_eqc << std::endl;
+  if (tat && !qe->inConflict())
+  {
+    InstMatch m(q);
+    addInstantiations(m, qe, addedLemmas, 0, tat);
+  }
+  return addedLemmas;
+}
+
+void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
+                                                 QuantifiersEngine* qe,
+                                                 uint64_t& addedLemmas,
+                                                 size_t argIndex,
+                                                 TNodeTrie* tat)
+{
+  Debug("simple-trigger-debug")
+      << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
+  if (argIndex == d_match_pattern.getNumChildren())
+  {
+    Assert(!tat->d_data.empty());
+    TNode t = tat->getData();
+    Debug("simple-trigger") << "Actual term is " << t << std::endl;
+    // convert to actual used terms
+    for (const std::pair<unsigned, int>& v : d_var_num)
+    {
+      if (v.second >= 0)
+      {
+        Assert(v.first < t.getNumChildren());
+        Debug("simple-trigger")
+            << "...set " << v.second << " " << t[v.first] << std::endl;
+        m.setValue(v.second, t[v.first]);
+      }
+    }
+    // we do not need the trigger parent for simple triggers (no post-processing
+    // required)
+    if (qe->getInstantiate()->addInstantiation(d_quant, m))
+    {
+      addedLemmas++;
+      Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
+    }
+    return;
+  }
+  if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
+  {
+    int v = d_var_num[argIndex];
+    if (v != -1)
+    {
+      for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
+      {
+        Node t = tt.first;
+        Node prev = m.get(v);
+        // using representatives, just check if equal
+        Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
+        if (prev.isNull() || prev == t)
+        {
+          m.setValue(v, t);
+          addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
+          m.setValue(v, prev);
+          if (qe->inConflict())
+          {
+            break;
+          }
+        }
+      }
+      return;
+    }
+    // inst constant from another quantified formula, treat as ground term?
+  }
+  Node r = qe->getEqualityQuery()->getRepresentative(d_match_pattern[argIndex]);
+  std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
+  if (it != tat->d_data.end())
+  {
+    addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second));
+  }
+}
+
+int InstMatchGeneratorSimple::getActiveScore(QuantifiersEngine* qe)
+{
+  Node f = qe->getTermDatabase()->getMatchOperator(d_match_pattern);
+  size_t ngt = qe->getTermDatabase()->getNumGroundTerms(f);
+  Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) "
+                                    << f << " is " << ngt << std::endl;
+  return static_cast<int>(ngt);
+}
+
+}  // namespace inst
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
new file mode 100644
index 000000000..243050772
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
@@ -0,0 +1,110 @@
+/*********************                                                        */
+/*! \file inst_match_generator_simple.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief simple inst match generator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
+#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node_trie.h"
+#include "theory/quantifiers/ematching/inst_match_generator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+/** InstMatchGeneratorSimple class
+ *
+ * This is the default generator class for simple single triggers.
+ * For example, { f( x, a ) }, { f( x, x ) } and { f( x, y ) } are simple single
+ * triggers. In practice, around 70-90% of triggers are simple single triggers.
+ *
+ * Notice that simple triggers also can have an attached polarity.
+ * For example, { P( x ) = false }, { f( x, y ) = a } and { ~f( a, x ) = b } are
+ * simple single triggers.
+ *
+ * The implementation traverses the term indices in TermDatabase for adding
+ * instantiations, which is more efficient than the techniques required for
+ * handling non-simple single triggers.
+ *
+ * In contrast to other instantiation generators, it does not call
+ * IMGenerator::sendInstantiation and for performance reasons instead calls
+ * qe->getInstantiate()->addInstantiation(...) directly.
+ */
+class InstMatchGeneratorSimple : public IMGenerator
+{
+ public:
+  /** constructors */
+  InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe);
+
+  /** Reset instantiation round. */
+  void resetInstantiationRound(QuantifiersEngine* qe) override;
+  /** Add instantiations. */
+  uint64_t addInstantiations(Node q,
+                             QuantifiersEngine* qe,
+                             Trigger* tparent) override;
+  /** Get active score. */
+  int getActiveScore(QuantifiersEngine* qe) override;
+
+ private:
+  /** quantified formula for the trigger term */
+  Node d_quant;
+  /** the trigger term */
+  Node d_match_pattern;
+  /** equivalence class polarity information
+   *
+   * This stores the required polarity/equivalence class with this trigger.
+   * If d_eqc is non-null, we only produce matches { x->t } such that
+   * our context does not entail
+   *   ( d_match_pattern*{ x->t } = d_eqc) if d_pol = true, or
+   *   ( d_match_pattern*{ x->t } != d_eqc) if d_pol = false.
+   * where * denotes application of substitution.
+   */
+  bool d_pol;
+  Node d_eqc;
+  /** Match pattern arg types.
+   * Cached values of d_match_pattern[i].getType().
+   */
+  std::vector<TypeNode> d_match_pattern_arg_types;
+  /** The match operator d_match_pattern (see TermDb::getMatchOperator). */
+  Node d_op;
+  /**
+   * Map from child number of d_match_pattern to variable index, or -1 if the
+   * child is not a variable.
+   */
+  std::map<size_t, int> d_var_num;
+  /** add instantiations, helper function.
+   *
+   * m is the current match we are building,
+   * addedLemmas is the number of lemmas we have added via calls to
+   *                qe->getInstantiate()->aaddInstantiation(...),
+   * argIndex is the argument index in d_match_pattern we are currently
+   *              matching,
+   * tat is the term index we are currently traversing.
+   */
+  void addInstantiations(InstMatch& m,
+                         QuantifiersEngine* qe,
+                         uint64_t& addedLemmas,
+                         size_t argIndex,
+                         TNodeTrie* tat);
+};
+
+}  // namespace inst
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 4d6dd9f58..34f413b71 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -19,6 +19,9 @@
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
+#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
+#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
+#include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
new file mode 100644
index 000000000..0553c1745
--- /dev/null
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -0,0 +1,78 @@
+/*********************                                                        */
+/*! \file var_match_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of variable match generator class
+ **/
+#include "theory/quantifiers/ematching/var_match_generator.h"
+
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Node var, Node subs)
+    : InstMatchGenerator(), d_var(var), d_subs(subs), d_rm_prev(false)
+{
+  d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute()));
+  d_var_type = d_var.getType();
+}
+
+bool VarMatchGeneratorTermSubs::reset(Node eqc, QuantifiersEngine* qe)
+{
+  d_eq_class = eqc;
+  return true;
+}
+
+int VarMatchGeneratorTermSubs::getNextMatch(Node q,
+                                            InstMatch& m,
+                                            QuantifiersEngine* qe,
+                                            Trigger* tparent)
+{
+  int ret_val = -1;
+  if (!d_eq_class.isNull())
+  {
+    Trace("var-trigger-matching") << "Matching " << d_eq_class << " against "
+                                  << d_var << " in " << d_subs << std::endl;
+    TNode tvar = d_var;
+    Node s = d_subs.substitute(tvar, d_eq_class);
+    s = Rewriter::rewrite(s);
+    Trace("var-trigger-matching")
+        << "...got " << s << ", " << s.getKind() << std::endl;
+    d_eq_class = Node::null();
+    // if( s.getType().isSubtypeOf( d_var_type ) ){
+    d_rm_prev = m.get(d_children_types[0]).isNull();
+    if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
+    {
+      return -1;
+    }
+    else
+    {
+      ret_val = continueNextMatch(q, m, qe, tparent);
+      if (ret_val > 0)
+      {
+        return ret_val;
+      }
+    }
+  }
+  if (d_rm_prev)
+  {
+    m.d_vals[d_children_types[0]] = Node::null();
+    d_rm_prev = false;
+  }
+  return -1;
+}
+
+}  // namespace inst
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h
new file mode 100644
index 000000000..c1030e11d
--- /dev/null
+++ b/src/theory/quantifiers/ematching/var_match_generator.h
@@ -0,0 +1,60 @@
+/*********************                                                        */
+/*! \file var_match_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief variable match generator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
+#define CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
+
+#include <map>
+#include "expr/node.h"
+#include "theory/quantifiers/ematching/inst_match_generator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+/** match generator for purified terms
+ * This handles the special case of invertible terms like x+1 (see
+ * Trigger::getTermInversionVariable).
+ */
+class VarMatchGeneratorTermSubs : public InstMatchGenerator
+{
+ public:
+  VarMatchGeneratorTermSubs(Node var, Node subs);
+
+  /** Reset */
+  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  /** Get the next match. */
+  int getNextMatch(Node q,
+                   InstMatch& m,
+                   QuantifiersEngine* qe,
+                   Trigger* tparent) override;
+
+ private:
+  /** variable we are matching (x in the example x+1). */
+  Node d_var;
+  /** cache of d_var.getType() */
+  TypeNode d_var_type;
+  /** The substitution for what we match (x-1 in the example x+1). */
+  Node d_subs;
+  /** stores whether we have written a value for d_var in the current match. */
+  bool d_rm_prev;
+};
+
+}  // namespace inst
+}  // namespace theory
+}  // namespace CVC4
+
+#endif