Ho instantiation (#1204)

* Higher-order instantiation.

* Add missing files.

* Document inst match generators, make collectHoVarApplyTerms iterative.

* More documentation.

* More documentation.

* More documentation.

* More documentation

* Refactoring, documentation.

* More documentation.

* Fix comment, reference issue.

* More documentation. Fix ho trigger for the changes from master.

* Minor

* More documentation.

* More documentation.

* More

* More documentation, make indexing and lookup in TriggerTrie iterative instead of recursive.

* More

* Minor improvements to comments.

* Remove an unimplemented optimization from an old version of cached multi-trigger matching. Update and improve documentation in inst match generator.

* Improve documentation for ho_trigger.

* Update ho trigger to not access now private member of TermDb.

* Address comments.

* Address

* Clang format

8 files changed, 2099 insertions, 487 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index acd94a90a..f5694dc71 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -391,6 +391,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/fun_def_engine.h \
 	theory/quantifiers/fun_def_process.cpp \
 	theory/quantifiers/fun_def_process.h \
+	theory/quantifiers/ho_trigger.cpp \
+	theory/quantifiers/ho_trigger.h \
 	theory/quantifiers/inst_match.cpp \
 	theory/quantifiers/inst_match.h \
 	theory/quantifiers/inst_match_generator.cpp \
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index a19555987..6274269ce 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -87,19 +87,65 @@ enum QcfMode {
   QCF_PARTIAL,
 };
 
-enum UserPatMode {
-  /** use but do not trust */
+/** User pattern mode.
+*
+* These modes determine how user provided patterns (triggers) are
+* used during E-matching. The modes vary on when instantiation based on
+* user-provided triggers is combined with instantiation based on
+* automatically selected triggers.
+*/
+enum UserPatMode
+{
+  /** First instantiate based on user-provided triggers. If no instantiations
+  * are produced, use automatically selected triggers.
+  */
   USER_PAT_MODE_USE,
-  /** default, if patterns are supplied for a quantifier, use only those */
+  /** Default, if triggers are supplied for a quantifier, use only those. */
   USER_PAT_MODE_TRUST,
-  /** resort to user patterns only when necessary */
+  /** Resort to user triggers only when no instantiations are
+  * produced by automatically selected triggers
+  */
   USER_PAT_MODE_RESORT,
-  /** ignore user patterns */
+  /** Ignore user patterns. */
   USER_PAT_MODE_IGNORE,
-  /** interleave use/resort for user patterns */
+  /** Interleave use/resort modes for quantified formulas with user patterns. */
   USER_PAT_MODE_INTERLEAVE,
 };
 
+/** Trigger selection mode.
+*
+* These modes are used for determining which terms to select
+* as triggers for quantified formulas, when necessary, during E-matching.
+* In the following, note the following terminology. A trigger is a set of terms,
+* where a single trigger is a singleton set and a multi-trigger is a set of more
+* than one term.
+*
+* TRIGGER_SEL_MIN selects single triggers of minimal term size.
+* TRIGGER_SEL_MAX selects single triggers of maximal term size.
+*
+* For example, consider the quantified formula :
+*   forall xy. P( f( g( x, y ) ) ) V Q( f( x ), y )
+*
+* TRIGGER_SEL_MIN will select g( x, y ) and Q( f( x ), y ).
+* TRIGGER_SEL_MAX will select P( f( g( x ) ) ) and Q( f( x ), y ).
+*
+* The remaining three trigger selections make a difference for multi-triggers
+* only. For quantified formulas that require multi-triggers, we build a set of
+* partial triggers that don't contain all variables, call this set S. Then,
+* multi-triggers are built by taking a random subset of S that collectively
+* contains all variables.
+*
+* Consider the quantified formula :
+*   forall xyz. P( h( x ), y ) V Q( y, z )
+*
+* For TRIGGER_SEL_ALL and TRIGGER_SEL_MIN_SINGLE_ALL,
+*   S = { h( x ), P( h( x ), y ), Q( y, z ) }.
+* For TRIGGER_SEL_MIN_SINGLE_MAX,
+*   S = { P( h( x ), y ), Q( y, z ) }.
+*
+* Furthermore, TRIGGER_SEL_MIN_SINGLE_ALL and TRIGGER_SEL_MIN_SINGLE_MAX, when
+* selecting single triggers, only select terms of minimal size.
+*/
 enum TriggerSelMode {
   /** only consider minimal terms for triggers */
   TRIGGER_SEL_MIN,
diff --git a/src/theory/quantifiers/ho_trigger.cpp b/src/theory/quantifiers/ho_trigger.cpp
new file mode 100644
index 000000000..b0ac02a25
--- /dev/null
+++ b/src/theory/quantifiers/ho_trigger.cpp
@@ -0,0 +1,447 @@
+/*********************                                                        */
+/*! \file ho_trigger.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 higher-order trigger class
+ **/
+
+#include <stack>
+
+#include "theory/quantifiers/ho_trigger.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/theory_uf_rewriter.h"
+#include "util/hash.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+HigherOrderTrigger::HigherOrderTrigger(
+    QuantifiersEngine* qe,
+    Node q,
+    std::vector<Node>& nodes,
+    std::map<Node, std::vector<Node> >& ho_apps)
+    : Trigger(qe, q, nodes), d_ho_var_apps(ho_apps)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  // process the higher-order variable applications
+  for (std::pair<const Node, std::vector<Node> >& as : d_ho_var_apps)
+  {
+    Node n = as.first;
+    d_ho_var_list.push_back(n);
+    TypeNode tn = n.getType();
+    Assert(tn.isFunction());
+    if (Trace.isOn("ho-quant-trigger"))
+    {
+      Trace("ho-quant-trigger") << "  have " << as.second.size();
+      Trace("ho-quant-trigger") << " patterns with variable operator " << n
+                                << ":" << std::endl;
+      for (unsigned j = 0; j < as.second.size(); j++)
+      {
+        Trace("ho-quant-trigger") << "  " << as.second[j] << std::endl;
+      }
+    }
+    if (d_ho_var_types.find(tn) == d_ho_var_types.end())
+    {
+      Trace("ho-quant-trigger") << "  type " << tn
+                                << " needs higher-order matching." << std::endl;
+      d_ho_var_types.insert(tn);
+    }
+    // make the bound variable lists
+    d_ho_var_bvl[n] = nm->getBoundVarListForFunctionType(tn);
+    for (const Node& nc : d_ho_var_bvl[n])
+    {
+      d_ho_var_bvs[n].push_back(nc);
+    }
+  }
+}
+
+HigherOrderTrigger::~HigherOrderTrigger() {}
+void HigherOrderTrigger::collectHoVarApplyTerms(
+    Node q, TNode n, std::map<Node, std::vector<Node> >& apps)
+{
+  std::vector<Node> ns;
+  ns.push_back(n);
+  collectHoVarApplyTerms(q, ns, apps);
+}
+
+void HigherOrderTrigger::collectHoVarApplyTerms(
+    Node q, std::vector<Node>& ns, std::map<Node, std::vector<Node> >& apps)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  // whether the visited node is a child of a HO_APPLY chain
+  std::unordered_map<TNode, bool, TNodeHashFunction> withinApply;
+  std::stack<TNode> visit;
+  TNode cur;
+  for (unsigned i = 0; i < ns.size(); i++)
+  {
+    visit.push(ns[i]);
+    withinApply[ns[i]] = false;
+    do
+    {
+      cur = visit.top();
+      visit.pop();
+
+      if (visited.find(cur) == visited.end())
+      {
+        visited.insert(cur);
+        bool curWithinApply = withinApply[cur];
+        if (!curWithinApply)
+        {
+          TNode op;
+          if (cur.getKind() == kind::APPLY_UF)
+          {
+            // could be a fully applied function variable
+            op = cur.getOperator();
+          }
+          else if (cur.getKind() == kind::HO_APPLY)
+          {
+            op = cur;
+            while (op.getKind() == kind::HO_APPLY)
+            {
+              op = op[0];
+            }
+          }
+          if (!op.isNull())
+          {
+            if (op.getKind() == kind::INST_CONSTANT)
+            {
+              Assert(quantifiers::TermUtil::getInstConstAttr(cur) == q);
+              Trace("ho-quant-trigger-debug")
+                  << "Ho variable apply term : " << cur << " with head " << op
+                  << std::endl;
+              Node app = cur;
+              if (app.getKind() == kind::APPLY_UF)
+              {
+                // for consistency, convert to HO_APPLY if fully applied
+                app = uf::TheoryUfRewriter::getHoApplyForApplyUf(app);
+              }
+              apps[op].push_back(cur);
+            }
+            if (cur.getKind() == kind::HO_APPLY)
+            {
+              curWithinApply = true;
+            }
+          }
+        }
+        else
+        {
+          if (cur.getKind() != HO_APPLY)
+          {
+            curWithinApply = false;
+          }
+        }
+        // do not look in nested quantifiers
+        if (cur.getKind() != FORALL)
+        {
+          for (unsigned i = 0, size = cur.getNumChildren(); i < size; i++)
+          {
+            withinApply[cur[i]] = curWithinApply && i == 0;
+            visit.push(cur[i]);
+          }
+        }
+      }
+    } while (!visit.empty());
+  }
+}
+
+int HigherOrderTrigger::addInstantiations(InstMatch& baseMatch)
+{
+  // call the base class implementation
+  int addedFoLemmas = Trigger::addInstantiations(baseMatch);
+  // also adds predicate lemms to force app completion
+  int addedHoLemmas = addHoTypeMatchPredicateLemmas();
+  return addedHoLemmas + addedFoLemmas;
+}
+
+bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
+{
+  if (options::hoMatching())
+  {
+    // get substitution corresponding to m
+    std::vector<TNode> vars;
+    std::vector<TNode> subs;
+    for (unsigned i = 0, size = d_f[0].getNumChildren(); i < size; i++)
+    {
+      subs.push_back(m.d_vals[i]);
+      vars.push_back(
+          d_quantEngine->getTermUtil()->getInstantiationConstant(d_f, i));
+    }
+
+    Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl;
+
+    // get the substituted form of all variable-operator ho application terms
+    std::map<TNode, std::vector<Node> > ho_var_apps_subs;
+    for (std::pair<const Node, std::vector<Node> >& ha : d_ho_var_apps)
+    {
+      TNode var = ha.first;
+      for (unsigned j = 0, size = ha.second.size(); j < size; j++)
+      {
+        TNode app = ha.second[j];
+        Node sapp =
+            app.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+        ho_var_apps_subs[var].push_back(sapp);
+        Trace("ho-unif-debug") << "  app[" << var << "] : " << app << " -> "
+                               << sapp << std::endl;
+      }
+    }
+
+    // compute argument vectors for each variable
+    d_lchildren.clear();
+    d_arg_to_arg_rep.clear();
+    d_arg_vector.clear();
+    EqualityQuery* eq = d_quantEngine->getEqualityQuery();
+    for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
+    {
+      TNode var = ha.first;
+      unsigned vnum = var.getAttribute(InstVarNumAttribute());
+      Node value = m.d_vals[vnum];
+      Trace("ho-unif-debug") << "  val[" << var << "] = " << value << std::endl;
+
+      Trace("ho-unif-debug2") << "initialize lambda information..."
+                              << std::endl;
+      // initialize the lambda children
+      d_lchildren[vnum].push_back(value);
+      std::map<TNode, std::vector<Node> >::iterator ithb =
+          d_ho_var_bvs.find(var);
+      Assert(ithb != d_ho_var_bvs.end());
+      d_lchildren[vnum].insert(
+          d_lchildren[vnum].end(), ithb->second.begin(), ithb->second.end());
+
+      Trace("ho-unif-debug2") << "compute fixed arguments..." << std::endl;
+      // compute for each argument if it is only applied to a fixed value modulo
+      // equality
+      std::map<unsigned, Node> fixed_vals;
+      for (unsigned i = 0; i < ha.second.size(); i++)
+      {
+        std::vector<TNode> args;
+        Node f = uf::TheoryUfRewriter::decomposeHoApply(ha.second[i], args);
+        // Assert( f==value );
+        for (unsigned k = 0, size = args.size(); k < size; k++)
+        {
+          Node val = args[k];
+          std::map<unsigned, Node>::iterator itf = fixed_vals.find(k);
+          if (itf == fixed_vals.end())
+          {
+            fixed_vals[k] = val;
+          }
+          else if (!itf->second.isNull())
+          {
+            if (!eq->areEqual(itf->second, args[k]))
+            {
+              if (!d_quantEngine->getTermDatabase()->isEntailed(
+                      itf->second.eqNode(args[k]), true, eq))
+              {
+                fixed_vals[k] = Node::null();
+              }
+            }
+          }
+        }
+      }
+      if (Trace.isOn("ho-unif-debug"))
+      {
+        for (std::map<unsigned, Node>::iterator itf = fixed_vals.begin();
+             itf != fixed_vals.end();
+             ++itf)
+        {
+          Trace("ho-unif-debug") << "  arg[" << var << "][" << itf->first
+                                 << "] : " << itf->second << std::endl;
+        }
+      }
+
+      // now construct argument vectors
+      Trace("ho-unif-debug2") << "compute argument vectors..." << std::endl;
+      std::map<Node, unsigned> arg_to_rep;
+      for (unsigned index = 0, size = ithb->second.size(); index < size;
+           index++)
+      {
+        Node bv_at_index = ithb->second[index];
+        std::map<unsigned, Node>::iterator itf = fixed_vals.find(index);
+        Trace("ho-unif-debug") << "  * arg[" << var << "][" << index << "]";
+        if (itf != fixed_vals.end())
+        {
+          if (!itf->second.isNull())
+          {
+            Node r = eq->getRepresentative(itf->second);
+            std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r);
+            if (itfr != arg_to_rep.end())
+            {
+              d_arg_to_arg_rep[vnum][index] = itfr->second;
+              // function applied to equivalent values at multiple arguments,
+              // can permute variables
+              d_arg_vector[vnum][itfr->second].push_back(bv_at_index);
+              Trace("ho-unif-debug") << " = { self } ++ arg[" << var << "]["
+                                     << itfr->second << "]" << std::endl;
+            }
+            else
+            {
+              arg_to_rep[r] = index;
+              // function applied to single value, can either use variable or
+              // value at this argument position
+              d_arg_vector[vnum][index].push_back(bv_at_index);
+              d_arg_vector[vnum][index].push_back(itf->second);
+              if (!options::hoMatchingVarArgPriority())
+              {
+                std::reverse(d_arg_vector[vnum][index].begin(),
+                             d_arg_vector[vnum][index].end());
+              }
+              Trace("ho-unif-debug") << " = { self, " << itf->second << " } "
+                                     << std::endl;
+            }
+          }
+          else
+          {
+            // function is applied to disequal values, can only use variable at
+            // this argument position
+            d_arg_vector[vnum][index].push_back(bv_at_index);
+            Trace("ho-unif-debug") << " = { self } (disequal)" << std::endl;
+          }
+        }
+        else
+        {
+          // argument is irrelevant to matching, assume identity variable
+          d_arg_vector[vnum][index].push_back(bv_at_index);
+          Trace("ho-unif-debug") << " = { self } (irrelevant)" << std::endl;
+        }
+      }
+      Trace("ho-unif-debug2") << "finished." << std::endl;
+    }
+
+    return sendInstantiation(m, 0);
+  }
+  else
+  {
+    // do not run higher-order matching
+    return d_quantEngine->addInstantiation(d_f, m);
+  }
+}
+
+// recursion depth limited by number of arguments of higher order variables
+// occurring as pattern operators (very small)
+bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index)
+{
+  if (var_index == d_ho_var_list.size())
+  {
+    // we now have an instantiation to try
+    return d_quantEngine->addInstantiation(d_f, m);
+  }
+  else
+  {
+    Node var = d_ho_var_list[var_index];
+    unsigned vnum = var.getAttribute(InstVarNumAttribute());
+    Assert(vnum < m.d_vals.size());
+    Node value = m.d_vals[vnum];
+    Assert(d_lchildren[vnum][0] == value);
+    Assert(d_ho_var_bvl.find(var) != d_ho_var_bvl.end());
+
+    // now, recurse on arguments to enumerate equivalent matching lambda
+    // expressions
+    bool ret =
+        sendInstantiationArg(m, var_index, vnum, 0, d_ho_var_bvl[var], false);
+
+    // reset the value
+    m.d_vals[vnum] = value;
+
+    return ret;
+  }
+}
+
+bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m,
+                                              unsigned var_index,
+                                              unsigned vnum,
+                                              unsigned arg_index,
+                                              Node lbvl,
+                                              bool arg_changed)
+{
+  if (arg_index == lbvl.getNumChildren())
+  {
+    // construct the lambda
+    if (arg_changed)
+    {
+      Node body =
+          NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_lchildren[vnum]);
+      Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, lbvl, body);
+      m.d_vals[vnum] = lam;
+      Trace("ho-unif-debug2") << "  try " << vnum << " -> " << lam << std::endl;
+    }
+    return sendInstantiation(m, var_index + 1);
+  }
+  else
+  {
+    std::map<unsigned, unsigned>::iterator itr =
+        d_arg_to_arg_rep[vnum].find(arg_index);
+    unsigned rindex =
+        itr != d_arg_to_arg_rep[vnum].end() ? itr->second : arg_index;
+    std::map<unsigned, std::vector<Node> >::iterator itv =
+        d_arg_vector[vnum].find(rindex);
+    Assert(itv != d_arg_vector[vnum].end());
+    Node prev = lbvl[arg_index];
+    bool ret = false;
+    // try each argument in the vector
+    for (unsigned i = 0, size = itv->second.size(); i < size; i++)
+    {
+      bool new_arg_changed = arg_changed || prev != itv->second[i];
+      d_lchildren[vnum][arg_index + 1] = itv->second[i];
+      if (sendInstantiationArg(
+              m, var_index, vnum, arg_index + 1, lbvl, new_arg_changed))
+      {
+        ret = true;
+        break;
+      }
+    }
+    // clean up
+    d_lchildren[vnum][arg_index + 1] = prev;
+    return ret;
+  }
+}
+
+int HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
+{
+  unsigned numLemmas = 0;
+  if (!d_ho_var_types.empty())
+  {
+    // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
+    unsigned size = d_quantEngine->getTermDatabase()->getNumOperators();
+    for (unsigned j = 0; j < size; j++)
+    {
+      Node f = d_quantEngine->getTermDatabase()->getOperator(j);
+      if (f.isVar())
+      {
+        TypeNode tn = f.getType();
+        if (d_ho_var_types.find(tn) != d_ho_var_types.end())
+        {
+          Node u = d_quantEngine->getTermUtil()->getHoTypeMatchPredicate(tn);
+          Node au = NodeManager::currentNM()->mkNode(kind::APPLY_UF, u, f);
+          if (d_quantEngine->addLemma(au))
+          {
+            // this forces f to be a first-class member of the quantifier-free
+            // equality engine,
+            //  which in turn forces the quantifier-free theory solver to expand
+            //  it to HO_APPLY
+            Trace("ho-quant") << "Added ho match predicate lemma : " << au
+                              << std::endl;
+            numLemmas++;
+          }
+        }
+      }
+    }
+  }
+  return numLemmas;
+}
+
+} /* CVC4::theory::inst namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/ho_trigger.h b/src/theory/quantifiers/ho_trigger.h
new file mode 100644
index 000000000..16d676353
--- /dev/null
+++ b/src/theory/quantifiers/ho_trigger.h
@@ -0,0 +1,276 @@
+/*********************                                                        */
+/*! \file ho_trigger.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 higher-order trigger class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
+#define __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
+
+#include <map>
+#include <unordered_set>
+
+#include "expr/node.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/trigger.h"
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+class Trigger;
+
+/** HigherOrder trigger
+ *
+ * This extends the trigger class with techniques that post-process
+ * instantiations, specified by InstMatch objects, according to a variant of
+ * Huet's algorithm. For details, see Chapter 16 of the Handbook of Automated
+ * Reasoning (vol. 2), by Gilles Dowek.
+ *
+ * The main difference between HigherOrderTrigger and Trigger is the function
+ * sendInstantiation(...). Recall that this function is called when its
+ * underlying IMGenerator generates an InstMatch m using E-matching technique.
+ * We enumerate additional instantiations based on m, when the domain of m
+ * contains variables of function type.
+ *
+ * Examples below (f, x, y are universal variables):
+ *
+ * (EX1): (f x y) matches (k 0 1) in standard E-matching with:
+ *
+ * f -> k, x -> 0, y -> 1
+ *
+ * This match is extended to four possible solutions by this class:
+ *
+ * f -> \ xy. (k x y), x -> 0, y -> 1
+ * f -> \ xy. (k 0 y), x -> 0, y -> 1
+ * f -> \ xy. (k x 1), x -> 0, y -> 1
+ * f -> \ xy. (k 0 1), x -> 0, y -> 1
+ *
+ *
+ * (EX2): Similarly, (f x y) matches (k 0 0) with possible solutions:
+ *
+ * f -> \ xy. (k x x), x -> 0, y -> 0
+ * f -> \ xy. (k y x), x -> 0, y -> 0
+ * f -> \ xy. (k 0 x), x -> 0, y -> 0
+ * f -> \ xy. (k x y), x -> 0, y -> 0
+ * f -> \ xy. (k y y), x -> 0, y -> 0
+ * f -> \ xy. (k 0 y), x -> 0, y -> 0
+ * f -> \ xy. (k x 0), x -> 0, y -> 0
+ * f -> \ xy. (k y 0), x -> 0, y -> 0
+ * f -> \ xy. (k 0 0), x -> 0, y -> 0
+ *
+ *
+ * (EX3): (f x y), (f x z) simultaneously match (k 0 1), (k 0 2) with possible
+ * solutions:
+ *
+ * f -> \ xy. (k x y), x -> 0, y -> 1, z -> 2
+ * f -> \ xy. (k 0 y), x -> 0, y -> 1, z -> 2
+ *
+ *
+ * This class enumerates the lists above until one instantiation of that form is
+ * successfully added via a call to Instantiate::addInstantiation(...)
+ *
+ *
+ * It also implements a way of forcing APPLY_UF to expand to curried HO_APPLY to
+ * handle a corner case where there are no matchable ground terms
+ * (addHoTypeMatchPredicateLemmas).
+ *
+ */
+class HigherOrderTrigger : public Trigger
+{
+  friend class Trigger;
+
+ private:
+  HigherOrderTrigger(QuantifiersEngine* qe,
+                     Node q,
+                     std::vector<Node>& nodes,
+                     std::map<Node, std::vector<Node> >& ho_apps);
+  virtual ~HigherOrderTrigger();
+
+ public:
+  /** Collect higher order var apply terms
+   *
+   * Collect all top-level HO_APPLY terms in n whose head is a variable in
+   * quantified formula q. Append all such terms in apps.
+   */
+  static void collectHoVarApplyTerms(Node q,
+                                     TNode n,
+                                     std::map<Node, std::vector<Node> >& apps);
+  /** Collect higher order var apply terms
+   *
+   * Collect all top-level HO_APPLY terms in terms ns whose head is a variable
+   * in quantified formula q, store in apps.
+   */
+  static void collectHoVarApplyTerms(Node q,
+                                     std::vector<Node>& ns,
+                                     std::map<Node, std::vector<Node> >& apps);
+  /** add all available instantiations, based on the current context
+   *
+   * Extends Trigger::addInstantiations to also send
+   * lemmas based on addHoTypeMatchPredicateLemmas.
+   */
+  virtual int addInstantiations(InstMatch& baseMatch) override;
+
+ protected:
+  /**
+   * Map from function-typed variables to their applications in the quantified
+   * formula d_f (member of Trigger).
+   */
+  std::map<Node, std::vector<Node> > d_ho_var_apps;
+  /**
+   * List of all function-typed variables that occur as the head of function
+   * applications in d_f.
+   */
+  std::vector<Node> d_ho_var_list;
+  /**
+   * Cached bound variables and bound variable list for each variable of
+   * function type. These are used for constructing lambda terms in
+   * instantiations.
+   */
+  std::map<TNode, std::vector<Node> > d_ho_var_bvs;
+  std::map<TNode, Node> d_ho_var_bvl;
+  /** the set of types of ho variables */
+  std::unordered_set<TypeNode, TypeNodeHashFunction> d_ho_var_types;
+  /** add higher-order type predicate lemmas
+   *
+   * Adds lemmas of the form P( f ), where P is the predicate
+   * returned by TermUtil::getHoTypeMatchPredicate( f.getType() ).
+   * These lemmas force certain functions f of type tn to appear as
+   * first-class terms in the quantifier-free UF solver, where recall a
+   * first-class term is one that occurs as an (external) term in its equality
+   * engine. These functions f are all operators that have at least one
+   * term f(t1...tn) indexed by TermDabatase and are such that
+   * f's type is the same as a function-typed variable we
+   * are considering in this class (in d_ho_var_apps).
+   *
+   * TODO: we may eliminate this based on how github issue #1115 is resolved.
+   */
+  int addHoTypeMatchPredicateLemmas();
+  /** send instantiation
+   *
+  * Sends an instantiation that is equivalent to m via
+  * Instantiate::addInstantiation(...). This method may modify m based on
+  * imitations and projections (Huet's algorithm), if m was generated by
+  * matching ground terms to function applications with variable heads.
+  * See examples (EX1)-(EX3) above.
+  */
+  virtual bool sendInstantiation(InstMatch& m);
+
+ private:
+  //-------------------- current information about the match
+  /**
+   * Map from variable position to the arguments of the lambda we generated
+   * for that variable.
+   *
+   * For example (EX4), take a quantified formula:
+   *   forall x f1 y f2. (...)
+   * Say we generated the match:
+   *   x -> 0
+   *   f1 -> k1
+   *   y -> 1
+   *   f2 -> k2
+   *   z -> 0
+   * where we matched
+   *   (f1 x y) with (k1 0 1) and
+   *   (f2 x z)  with (k2 0 0)
+   * Then the algorithm implemented by this class may modify the match to:
+   *   x -> 0
+   *   f1 -> (\ x1 x2. (k1 x1 1))
+   *   y -> 1
+   *   f2 -> (\ x1 x2. (k2 0 x1))
+   *   z -> 0
+   *
+   * In the above (modified) match, the contents of d_lchildren are:
+   *   1 -> { k1, x1, 1 }
+   *   3 -> { k2, 0, x1 }
+   */
+  std::map<unsigned, std::vector<Node> > d_lchildren;
+  /** map from variable position to the representative variable position.
+  * Used when two argument positions of a match are mapped to equal terms.
+  *
+  * In the above example (EX4), the first and second arguments of
+  * the match for f2 are equal.  Thus, in the above example,
+  * we have that d_arg_to_arg_rep is:
+  *   1 -> { 0 -> 0, 1 -> 1 }
+  *   3 -> { 0 -> 0, 1 -> 0 }
+  * In other words, the first argument
+  */
+  std::map<unsigned, std::map<unsigned, unsigned> > d_arg_to_arg_rep;
+  /** map from representative argument positions to the equivalence class
+   * of argument positions. In the above example (EX4), d_arg_vector is:
+   *   1 -> { 0 -> { 0 }, 1 -> { 1 } }
+   *   3 -> { 0 -> { 0, 1 } }
+   */
+  std::map<unsigned, std::map<unsigned, std::vector<Node> > > d_arg_vector;
+  //-------------------- end current information about the match
+
+  /** higher-order pattern unification algorithm
+   *
+  * Sends an instantiation that is equivalent to m via
+  * d_quantEngine->addInstantiation(...),
+  * based on Huet's algorithm.
+  *
+  * This is a helper function of sendInstantiation( m ) above.
+  *
+  * var_index is the index of the variable in m that we are currently processing
+  *   i.e. we are processing the var_index^{th} higher-order variable.
+  *
+  * For example, say we are processing the match from (EX4) above.
+  *   when var_index = 0,1, we are processing possibilities for
+  *    instantiation of f1,f2 respectively.
+  */
+  bool sendInstantiation(InstMatch& m, unsigned var_index);
+  /** higher-order pattern unification algorithm
+   * Sends an instantiation that is equivalent to m via
+   * d_quantEngine->addInstantiation(...).
+   * This is a helper function of sendInstantiation( m, var_index ) above.
+   *
+   * var_index is the index of the variable in m that we are currently
+   * processing
+   *   i.e. we are processing the var_index^{th} higher-order variable.
+   * vnum maps var_index to the actual variable number in m
+   * arg_index is the argument of the lambda term we are currently considering
+   * lbvl is the bound variable list associated with the term in m we are
+   * currently modifying
+   * arg_changed is whether we have modified m.
+   *
+   * For example, say we have modified our match from (EX4) to:
+   *   x -> 0
+   *   f1 -> (\ x1 x2. (k1 x1 1))
+   *   y -> 1
+   *   f2 -> (\ x1 x2. (k2 0 ?))
+   *   z -> 0
+   * That is, we are currently considering possibilities for the second
+   * argument of the body for f2.
+   * Then:
+   *   var_index = 1,
+   *   vnum = 3 (f2 is the 3^rd variable of our quantified formula)
+   *   arg_index = 1,
+   *   lbvl is d_ho_var_bvl[f2], and
+   *   arg_changed is true, since we modified at least one previous
+   *     argument of f1 or f2.
+   */
+  bool sendInstantiationArg(InstMatch& m,
+                            unsigned var_index,
+                            unsigned vnum,
+                            unsigned arg_index,
+                            Node lbvl,
+                            bool arg_changed);
+};
+
+} /* CVC4::theory::inst namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 31bd1d517..a8942326c 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -33,10 +33,15 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
+bool IMGenerator::sendInstantiation(Trigger* tparent, InstMatch& m)
+{
+  return tparent->sendInstantiation(m);
+}
+
 InstMatchGenerator::InstMatchGenerator( Node pat ){
   d_cg = NULL;
   d_needsReset = true;
-  d_active_add = false;
+  d_active_add = true;
   Assert( quantifiers::TermUtil::hasInstConstAttr(pat) );
   d_pattern = pat;
   d_match_pattern = pat;
@@ -49,7 +54,7 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){
 InstMatchGenerator::InstMatchGenerator() {
   d_cg = NULL;
   d_needsReset = true;
-  d_active_add = false;
+  d_active_add = true;
   d_next = NULL;
   d_matchPolicy = MATCH_GEN_DEFAULT;
   d_independent_gen = false;
@@ -127,29 +132,44 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
     d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
 
     //now, collect children of d_match_pattern
-    for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
-      Node qa = quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]);
-      if( !qa.isNull() ){
-        InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( q, d_match_pattern[i] );
-        if( cimg ){
-          d_children.push_back( cimg );
-          d_children_index.push_back( i );
-          d_children_types.push_back( 1 );
-        }else{
-          if( d_match_pattern[i].getKind()==INST_CONSTANT && qa==q ){
-            d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
-            d_children_types.push_back( 0 );
+    if (d_match_pattern.getKind() == INST_CONSTANT)
+    {
+      d_var_num[0] = d_match_pattern.getAttribute(InstVarNumAttribute());
+    }
+    else
+    {
+      for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size;
+           i++)
+      {
+        Node qa = quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]);
+        if (!qa.isNull())
+        {
+          InstMatchGenerator* cimg =
+              getInstMatchGenerator(q, d_match_pattern[i]);
+          if (cimg)
+          {
+            d_children.push_back(cimg);
+            d_children_index.push_back(i);
+            d_children_types.push_back(1);
           }else{
-            d_children_types.push_back( -1 );
+            if (d_match_pattern[i].getKind() == INST_CONSTANT && qa == q)
+            {
+              d_var_num[i] =
+                  d_match_pattern[i].getAttribute(InstVarNumAttribute());
+              d_children_types.push_back(0);
+            }
+            else
+            {
+              d_children_types.push_back(-1);
+            }
           }
         }
-      }else{
-        d_children_types.push_back( -1 );
+        else
+        {
+          d_children_types.push_back(-1);
+        }
       }
     }
-    if( d_match_pattern.getKind()==INST_CONSTANT ){
-      d_var_num[0] = d_match_pattern.getAttribute(InstVarNumAttribute());
-    }
 
     //create candidate generator
     if( Trigger::isAtomicTrigger( d_match_pattern ) ){
@@ -192,7 +212,9 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
 }
 
 /** get match (not modulo equality) */
-int InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){
+int InstMatchGenerator::getMatch(
+    Node f, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent)
+{
   Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
                     << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
   Assert( !d_match_pattern.isNull() );
@@ -294,7 +316,7 @@ int InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngin
       }
       if( success ){
         Trace("matching-debug2") << "Continue next " << d_next << std::endl;
-        ret_val = continueNextMatch( f, m, qe );
+        ret_val = continueNextMatch(f, m, qe, tparent);
       }
     }
     if( ret_val<0 ){
@@ -307,12 +329,16 @@ int InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngin
   }
 }
 
-int InstMatchGenerator::continueNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
+int InstMatchGenerator::continueNextMatch(Node f,
+                                          InstMatch& m,
+                                          QuantifiersEngine* qe,
+                                          Trigger* tparent)
+{
   if( d_next!=NULL ){
-    return d_next->getNextMatch( f, m, qe );
+    return d_next->getNextMatch(f, m, qe, tparent);
   }else{
     if( d_active_add ){
-      return qe->addInstantiation( f, m ) ? 1 : -1;
+      return sendInstantiation(tparent, m) ? 1 : -1;
     }else{
       return 1;
     }
@@ -362,7 +388,11 @@ bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
   return !d_curr_first_candidate.isNull();
 }
 
-int InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
+int InstMatchGenerator::getNextMatch(Node f,
+                                     InstMatch& m,
+                                     QuantifiersEngine* qe,
+                                     Trigger* tparent)
+{
   if( d_needsReset ){
     Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
     reset( d_eq_class, qe );
@@ -378,7 +408,7 @@ int InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* q
       if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
         Assert( t.getType().isComparableTo( d_match_pattern_type ) );
         Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl;
-        success = getMatch( f, t, m, qe );
+        success = getMatch(f, t, m, qe, tparent);
         if( d_independent_gen && success<0 ){
           Assert( d_eq_class.isNull() );
           d_curr_exclude_match[t] = true;
@@ -404,16 +434,20 @@ int InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* q
   return success;
 }
 
-
-
-int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
+int InstMatchGenerator::addInstantiations(Node f,
+                                          InstMatch& baseMatch,
+                                          QuantifiersEngine* qe,
+                                          Trigger* tparent)
+{
   //try to add instantiation for each match produced
   int addedLemmas = 0;
   InstMatch m( f );
-  while( getNextMatch( f, m, qe )>0 ){
+  while (getNextMatch(f, m, qe, tparent) > 0)
+  {
     if( !d_active_add ){
       m.add( baseMatch );
-      if( qe->addInstantiation( f, m ) ){
+      if (sendInstantiation(tparent, m))
+      {
         addedLemmas++;
         if( qe->inConflict() ){
           break;
@@ -491,12 +525,48 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, std::vecto
   return oinit;
 }
 
+InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n)
+{
+  if (n.getKind() == INST_CONSTANT)
+  {
+    return NULL;
+  }
+  Trace("var-trigger-debug") << "Is " << n << " a variable trigger?"
+                             << std::endl;
+  if (Trigger::isBooleanTermTrigger(n))
+  {
+    VarMatchGeneratorBooleanTerm* vmg =
+        new VarMatchGeneratorBooleanTerm(n[0], n[1]);
+    Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0]
+                         << std::endl;
+    return vmg;
+  }
+  Node x;
+  if (options::purifyTriggers())
+  {
+    x = Trigger::getInversionVariable(n);
+  }
+  if (!x.isNull())
+  {
+    Node s = Trigger::getInversion(n, x);
+    VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs(x, s);
+    Trace("var-trigger") << "Term substitution trigger : " << n
+                         << ", var = " << x << ", subs = " << s << std::endl;
+    return vmg;
+  }
+  return new InstMatchGenerator(n);
+}
+
 VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) :
   InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) {
   d_var_num[0] = var.getAttribute(InstVarNumAttribute());
 }
 
-int VarMatchGeneratorBooleanTerm::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) {
+int VarMatchGeneratorBooleanTerm::getNextMatch(Node q,
+                                               InstMatch& m,
+                                               QuantifiersEngine* qe,
+                                               Trigger* tparent)
+{
   int ret_val = -1;
   if( !d_eq_class.isNull() ){
     Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern ));
@@ -505,7 +575,7 @@ int VarMatchGeneratorBooleanTerm::getNextMatch( Node q, InstMatch& m, Quantifier
     if( !m.set( qe, d_var_num[0], s ) ){
       return -1;
     }else{
-      ret_val = continueNextMatch( q, m, qe );
+      ret_val = continueNextMatch(q, m, qe, tparent);
       if( ret_val>0 ){
         return ret_val;
       }
@@ -524,7 +594,11 @@ VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) :
   d_var_type = d_var.getType();
 }
 
-int VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) {
+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;
@@ -537,7 +611,7 @@ int VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersEn
     if( !m.set( qe, d_var_num[0], s ) ){
       return -1;
     }else{
-      ret_val = continueNextMatch( q, m, qe );
+      ret_val = continueNextMatch(q, m, qe, tparent);
       if( ret_val>0 ){
         return ret_val;
       }
@@ -600,7 +674,7 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto
   Trace("multi-trigger-linear") << "Make children for linear multi trigger." << std::endl;
   for( unsigned i=0; i<pats_ordered.size(); i++ ){
     Trace("multi-trigger-linear") << "...make for " << pats_ordered[i] << std::endl;
-    InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( q, pats_ordered[i] );
+    InstMatchGenerator* cimg = getInstMatchGenerator(q, pats_ordered[i]);
     Assert( cimg!=NULL );
     d_children.push_back( cimg );
     if( i==0 ){  //TODO : improve
@@ -631,7 +705,11 @@ bool InstMatchGeneratorMultiLinear::reset( Node eqc, QuantifiersEngine* qe ) {
   }
 }
 
-int InstMatchGeneratorMultiLinear::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) {
+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
@@ -642,13 +720,13 @@ int InstMatchGeneratorMultiLinear::getNextMatch( Node q, InstMatch& m, Quantifie
   }
   Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl;
   Assert( d_next!=NULL );
-  int ret_val = continueNextMatch( q, m, qe ); 
+  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( unsigned i=0; i<d_children.size(); i++ ){
-        Node mi = d_children[i]->d_curr_matched;
+        Node mi = d_children[i]->getCurrentMatch();
         Trace("multi-trigger-linear") << "   child " << i << " match : " << mi << std::endl;
         d_children[i]->excludeMatch( mi );
       }
@@ -659,8 +737,11 @@ int InstMatchGeneratorMultiLinear::getNextMatch( Node q, InstMatch& m, Quantifie
 
 
 /** constructors */
-InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) :
-d_f( q ){
+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;
   qe->getTermUtil()->getVarContains( q, pats, var_contains );
@@ -678,7 +759,10 @@ d_f( q ){
   for( unsigned i=0; i<pats.size(); i++ ){
     Node n = pats[i];
     //make the match generator
-    d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(q, n, qe ) );
+    InstMatchGenerator* img =
+        InstMatchGenerator::mkInstMatchGenerator(q, n, qe);
+    img->setActiveAdd(false);
+    d_children.push_back(img);
     //compute unique/shared variables
     std::vector< int > unique_vars;
     std::map< int, bool > shared_vars;
@@ -747,14 +831,19 @@ bool InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
   return true;
 }
 
-int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
+int InstMatchGeneratorMulti::addInstantiations(Node q,
+                                               InstMatch& baseMatch,
+                                               QuantifiersEngine* qe,
+                                               Trigger* tparent)
+{
   int addedLemmas = 0;
   Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
   for( unsigned i=0; i<d_children.size(); 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 )>0 ){
+    while (d_children[i]->getNextMatch(q, m, qe, tparent) > 0)
+    {
       //m.makeRepresentative( qe );
       newMatches.push_back( InstMatch( &m ) );
       m.clear();
@@ -762,7 +851,7 @@ int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, Qu
     Trace("multi-trigger-cache") << "Made " << newMatches.size() << " new matches for index " << i << std::endl;
     for( unsigned j=0; j<newMatches.size(); j++ ){
       Trace("multi-trigger-cache2") << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl;
-      processNewMatch( qe, newMatches[j], i, addedLemmas );
+      processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
       if( qe->inConflict() ){
         return addedLemmas;
       }
@@ -771,120 +860,144 @@ int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, Qu
   return addedLemmas;
 }
 
-void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){
+void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
+                                              Trigger* tparent,
+                                              InstMatch& m,
+                                              int fromChildIndex,
+                                              int& addedLemmas)
+{
   //see if these produce new matches
-  d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m );
+  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
   int childIndex = (fromChildIndex+1)%(int)d_children.size();
-  std::vector< IndexedTrie > unique_var_tries;
-  processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),
-                            unique_var_tries, 0, childIndex, fromChildIndex, true );
+  processNewInstantiations(qe,
+                           tparent,
+                           m,
+                           addedLemmas,
+                           d_children_trie[childIndex].getTrie(),
+                           0,
+                           childIndex,
+                           fromChildIndex,
+                           true);
 }
 
-void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
-                                                        std::vector< IndexedTrie >& unique_var_tries,
-                                                        int trieIndex, int childIndex, int endChildIndex, bool modEq ){
+void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
+                                                       Trigger* tparent,
+                                                       InstMatch& m,
+                                                       int& addedLemmas,
+                                                       InstMatchTrie* tr,
+                                                       int trieIndex,
+                                                       int childIndex,
+                                                       int endChildIndex,
+                                                       bool modEq)
+{
   Assert( !qe->inConflict() );
   if( childIndex==endChildIndex ){
-    //now, process unique variables
-    processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
+    // m is an instantiation
+    if (sendInstantiation(tparent, m))
+    {
+      addedLemmas++;
+      Trace("multi-trigger-cache-debug") << "-> Produced instantiation " << m
+                                         << std::endl;
+    }
   }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
     int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
-    //Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_f, curr_index );
+    // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant,
+    // curr_index );
     Node n = m.get( curr_index );
     if( n.isNull() ){
-      //if( d_var_to_node[ curr_index ].size()==1 ){    //FIXME
-      //  //unique variable(s), defer calculation
-      //  unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );
-      //  int newChildIndex = (childIndex+1)%(int)d_children.size();
-      //  processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
-      //                            0, newChildIndex, endChildIndex, modEq );
-      //}else{
-        //shared and non-set variable, add to InstMatch
-        for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
-          InstMatch mn( &m );
-          mn.setValue( curr_index, it->first);
-          processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,
-                                    trieIndex+1, childIndex, endChildIndex, modEq );
-          if( qe->inConflict() ){
-            break;
-          }
+      // 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;
         }
-      //}
-    }else{
-      //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, m, addedLemmas, &(it->second), unique_var_tries,
-                                  trieIndex+1, childIndex, endChildIndex, modEq );
       }
-      if( modEq ){
-        //check modulo equality for other possible instantiations
-        if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
-          eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
-                                   qe->getEqualityQuery()->getEngine() );
-          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, m, addedLemmas, &(itc->second), unique_var_tries,
-                                          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)
+    {
+      // check modulo equality for other possible instantiations
+      if (qe->getEqualityQuery()->getEngine()->hasTerm(n))
+      {
+        eq::EqClassIterator eqc(
+            qe->getEqualityQuery()->getEngine()->getRepresentative(n),
+            qe->getEqualityQuery()->getEngine());
+        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;
           }
+          ++eqc;
         }
       }
     }
   }else{
     int newChildIndex = (childIndex+1)%(int)d_children.size();
-    processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
-                              0, newChildIndex, endChildIndex, modEq );
-  }
-}
-
-void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
-                                                         std::vector< IndexedTrie >& unique_var_tries,
-                                                         int uvtIndex, InstMatchTrie* tr, int trieIndex ){
-  if( uvtIndex<(int)unique_var_tries.size() ){
-    int childIndex = unique_var_tries[uvtIndex].first.first;
-    if( !tr ){
-      tr = unique_var_tries[uvtIndex].second;
-      trieIndex = unique_var_tries[uvtIndex].first.second;
-    }
-    if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
-      int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
-      //Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_f, curr_index );
-      //unique non-set variable, add to InstMatch
-      for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
-        InstMatch mn( &m );
-        mn.setValue( curr_index, it->first);
-        processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
-        if( qe->inConflict() ){
-          break;
-        }
-      }
-    }else{
-      processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );
-    }
-  }else{
-    //m is an instantiation
-    if( qe->addInstantiation( d_f, m ) ){
-      addedLemmas++;
-      Trace("multi-trigger-cache-debug") << "-> Produced instantiation " << m << std::endl;
-    }
+    processNewInstantiations(qe,
+                             tparent,
+                             m,
+                             addedLemmas,
+                             d_children_trie[newChildIndex].getTrie(),
+                             0,
+                             newChildIndex,
+                             endChildIndex,
+                             modEq);
   }
 }
 
-InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ) : d_f( q ), d_match_pattern( pat ) {
+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;
@@ -913,8 +1026,11 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, Quantifier
 void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) {
   
 }
-
-int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
+int InstMatchGeneratorSimple::addInstantiations(Node q,
+                                                InstMatch& baseMatch,
+                                                QuantifiersEngine* qe,
+                                                Trigger* tparent)
+{
   int addedLemmas = 0;
   quantifiers::TermArgTrie* tat;
   if( d_eqc.isNull() ){
@@ -950,9 +1066,15 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q
   return addedLemmas;
 }
 
-void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
+void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
+                                                 QuantifiersEngine* qe,
+                                                 int& addedLemmas,
+                                                 unsigned argIndex,
+                                                 quantifiers::TermArgTrie* tat)
+{
   Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
-  if( argIndex==(int)d_match_pattern.getNumChildren() ){
+  if (argIndex == d_match_pattern.getNumChildren())
+  {
     Assert( !tat->d_data.empty() );
     TNode t = tat->getNodeData();
     Debug("simple-trigger") << "Actual term is " << t << std::endl;
@@ -963,7 +1085,10 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
         m.setValue( it->second, t[it->first] );
       }
     }
-    if( qe->addInstantiation( d_f, m ) ){
+    // we do not need the trigger parent for simple triggers (no post-processing
+    // required)
+    if (qe->addInstantiation(d_quant, m))
+    {
       addedLemmas++;
       Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
     }
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 882d786fb..a74035076 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -30,249 +30,684 @@ namespace quantifiers{
 
 namespace inst {
 
-/** base class for producing InstMatch objects */
+class Trigger;
+
+/** IMGenerator class
+*
+* Virtual base class for generating InstMatch objects, which correspond to
+* quantifier instantiations. The main use of this class is as a backend utility
+* to Trigger (see theory/quantifiers/trigger.h).
+*
+* Some functions below take as argument a pointer to the current quantifiers
+* engine, which is used for making various queries about what terms and
+* equalities exist in the current context.
+*
+* Some functions below take a pointer to a parent Trigger object, which is used
+* to post-process and finalize the instantiations through
+* sendInstantiation(...), where the parent trigger will make calls to
+* qe->getInstantiate()->addInstantiation(...). The latter function is the entry
+* point in which instantiate lemmas are enqueued to be sent on the output
+* channel.
+*/
 class IMGenerator {
 public:
   virtual ~IMGenerator() {}
-  /** reset instantiation round (call this at beginning of instantiation round) */
-  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  virtual bool reset( Node eqc, QuantifiersEngine* qe ) = 0;
-  /** get the next match.  must call reset( eqc ) before this function. */
-  virtual int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) = 0;
-  /** add instantiations directly */
-  virtual int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
-  /** set active add */
-  virtual void setActiveAdd( bool val ) {}
-  /** get active score */
+  /** Reset instantiation round.
+  *
+  * Called once at beginning of an instantiation round.
+  */
+  virtual void resetInstantiationRound(QuantifiersEngine* qe) {}
+  /** Reset.
+  *
+  * eqc is the equivalence class to search in (any if eqc=null).
+  * Returns true if this generator can produce instantiations, and false
+  * otherwise. An example of when it returns false is if it can be determined
+  * that no appropriate matchable terms occur based on eqc.
+  */
+  virtual bool reset(Node eqc, QuantifiersEngine* qe) { return true; }
+  /** Get the next match.
+  *
+  * Must call reset( eqc ) before this function. This constructs an
+  * instantiation, which it populates in data structure m,
+  * based on the current context using the implemented matching algorithm.
+  *
+  * q is the quantified formula we are adding instantiations for
+  * m is the InstMatch object we are generating
+  *
+  * Returns a value >0 if an instantiation was successfully generated
+  */
+  virtual int getNextMatch(Node q,
+                           InstMatch& m,
+                           QuantifiersEngine* qe,
+                           Trigger* tparent)
+  {
+    return 0;
+  }
+  /** add instantiations
+  *
+  * This add all available instantiations for q based on the current context
+  * using the implemented matching algorithm. It typically is implemented as a
+  * fixed point of getNextMatch above.
+  *
+  * baseMatch is a mapping of default values that should be used for variables
+  * that are not bound by this (not frequently used). (TODO remove #1389)
+  *
+  * It returns the number of instantiations added using calls to calls to
+  * Instantiate::addInstantiation(...).
+  */
+  virtual int addInstantiations(Node q,
+                                InstMatch& baseMatch,
+                                QuantifiersEngine* qe,
+                                Trigger* tparent)
+  {
+    return 0;
+  }
+  /** get active score
+  *
+  * A heuristic value indicating how active this generator is.
+  */
   virtual int getActiveScore( QuantifiersEngine * qe ) { return 0; }
+ protected:
+  /** send instantiation
+   *
+   * This method sends instantiation, specified by m, to the parent trigger
+   * object, which will in turn make a call to
+   * Instantiate::addInstantiation(...). This method returns true if a
+   * call to Instantiate::addInstantiation(...) was successfully made,
+   * indicating that an instantiation was enqueued in the quantifier engine's
+   * lemma cache.
+   */
+  bool sendInstantiation(Trigger* tparent, InstMatch& m);
 };/* class IMGenerator */
 
 class CandidateGenerator;
 
+/** InstMatchGenerator class
+*
+* This is the default generator class for non-simple single triggers, that is,
+* triggers composed of a single term with nested term applications.
+* For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple
+* triggers.
+*
+* Handling non-simple triggers is done by constructing a linked list of
+* InstMatchGenerator classes (see mkInstMatchGenerator), where each
+* InstMatchGenerator has a "d_next" pointer.  If d_next is NULL,
+* then this is the end of the InstMatchGenerator and the last
+* InstMatchGenerator is responsible for finalizing the instantiation.
+*
+* For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list:
+*
+* [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL
+*
+* In a call to getNextMatch,
+* if we match against a ground term f( b, c ), then the first InstMatchGenerator
+* in this list binds y to b, and tells the InstMatchGenerator [ f( x, a ) ] to
+* match f-applications in the equivalence class of c.
+*
+* CVC4 employs techniques that ensure that the number of instantiations
+* is worst-case polynomial wrt the number of ground terms.
+* Consider the axiom/pattern/context (EX2) :
+*
+*          axiom : forall x1 x2 x3 x4. F[ x1...x4 ]
+*
+*        trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
+*
+* ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 )
+*
+* If E-matching were applied exhaustively, then x1, x2, x3, x4 would be
+* instantiated with all combinations of c_1, ... c_100, giving 100^4
+* instantiations.
+*
+* Instead, we enforce that at most 1 instantiation is produced for a
+* ( pattern, ground term ) pair per round. Meaning, only one instantiation is
+* generated when matching P( a, a, a, a ) against the generator
+* [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of
+* Reynolds, Vampire 2016.
+*
+* To enforce these policies, we use a flag "d_active_add" which dictates the
+* behavior of the last element in the linked list. If d_active_add is
+*   true -> a call to getNextMatch(...) returns 1 only if adding the
+*           instantiation via a call to IMGenerator::sendInstantiation(...)
+*           successfully enqueues a lemma via a call to
+*           Instantiate::addInstantiation(...). This call may fail e.g. if we
+*           have already added the instantiation, or the instantiation is
+*           entailed.
+*   false -> a call to getNextMatch(...) returns 1 whenever an m is
+*            constructed, where typically the caller would use m.
+* This is important since a return value >0 signals that the current matched
+* terms should be flushed. Consider the above example (EX1), where
+* [ f(y,f(x,a)) ] is being matched against f(b,c),
+* [ f(x,a) ] is being matched against f(d,a) where c=f(d,a)
+* A successfully added instantiation { x->d, y->b } here signals we should
+* not produce further instantiations that match f(y,f(x,a)) with f(b,c).
+*
+* A number of special cases of triggers are covered by this generator (see
+* implementation of initialize), including :
+*   Literal triggers, e.g. x >= a, ~x = y
+*   Selector triggers, e.g. head( x )
+*   Triggers with invertible subterms, e.g. f( x+1 )
+*   Variable triggers, e.g. x
+*
+* All triggers above can be in the context of an equality, e.g.
+* { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to
+* ground terms in the equivalence class of b.
+* { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any
+* ground terms not in the equivalence class of b.
+*/
 class InstMatchGenerator : public IMGenerator {
-protected:
-  bool d_needsReset;
-  /** candidate generator */
-  CandidateGenerator* d_cg;
-  /** policy to use for matching */
-  int d_matchPolicy;
-  /** children generators */
-  std::vector< InstMatchGenerator* > d_children;
-  std::vector< int > d_children_index;
-  /** the next generator in order */
-  InstMatchGenerator* d_next;
-  /** eq class */
-  Node d_eq_class;
-  Node d_eq_class_rel;
-  /** variable numbers */
-  std::map< int, int > d_var_num;
-  /** excluded matches */
-  std::map< Node, bool > d_curr_exclude_match;
-  /** first candidate */
-  Node d_curr_first_candidate;
-  /** indepdendent generate (failures should be cached) */
-  bool d_independent_gen;
-  /** initialize pattern */
-  void initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens );
-  /** children types 0 : variable, 1 : child term, -1 : ground term */
-  std::vector< int > d_children_types;
-  /** continue */
-  int continueNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
-public:
-  enum {
-    //options for producing matches
-    MATCH_GEN_DEFAULT = 0,
-    //others (internally used)
-    MATCH_GEN_INTERNAL_ERROR,
-  };
 public:
-  /** get the match against ground term or formula t.
-      d_match_pattern and t should have the same shape.
-      only valid for use where !d_match_pattern.isNull().
-  */
-  int getMatch( Node q, Node t, InstMatch& m, QuantifiersEngine* qe );
+ /** destructor */
+ virtual ~InstMatchGenerator() throw();
+ enum
+ {
+   // options for producing matches
+   MATCH_GEN_DEFAULT = 0,
+   // others (internally used)
+   MATCH_GEN_INTERNAL_ERROR,
+ };
 
-  /** constructors */
-  InstMatchGenerator( Node pat );
-  InstMatchGenerator();
-  /** destructor */
-  virtual ~InstMatchGenerator() throw();
-  /** The pattern we are producing matches for.
-      If null, this is a multi trigger that is merging matches from d_children.
-  */
-  Node d_pattern;
-  /** match pattern */
-  Node d_match_pattern;
-  /** match pattern type */
-  TypeNode d_match_pattern_type;
-  /** match pattern op */
-  Node d_match_pattern_op;
-  /** what matched */
-  Node d_curr_matched;
-public:
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  void resetInstantiationRound( QuantifiersEngine* qe );
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  bool reset( Node eqc, QuantifiersEngine* qe );
-  /** get the next match.  must call reset( eqc ) before this function. */
-  int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
-  /** add instantiations */
-  int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
+ /** Reset instantiation round. */
+ void resetInstantiationRound(QuantifiersEngine* qe) override;
+ /** Reset. */
+ bool reset(Node eqc, QuantifiersEngine* qe) override;
+ /** Get the next match. */
+ int getNextMatch(Node q,
+                  InstMatch& m,
+                  QuantifiersEngine* qe,
+                  Trigger* tparent) override;
+ /** Add instantiations. */
+ int addInstantiations(Node q,
+                       InstMatch& baseMatch,
+                       QuantifiersEngine* qe,
+                       Trigger* tparent) override;
 
-  bool d_active_add;
-  void setActiveAdd( bool val );
-  int getActiveScore( QuantifiersEngine * qe );
-  void excludeMatch( Node n ) { d_curr_exclude_match[n] = true; }
-  void setIndependent() { d_independent_gen = true; }
+ /** set active add flag (true by default)
+  *
+ * If active add is true, we call sendInstantiation in calls to getNextMatch,
+ * instead of returning the match. This is necessary so that we can ensure
+ * policies that are dependent upon knowing when instantiations are
+ * successfully added to the output channel through
+ * Instantiate::addInstantiation(...).
+ */
+ void setActiveAdd(bool val);
+ /** Get active score for this inst match generator
+  *
+  * See Trigger::getActiveScore for details.
+  */
+ int getActiveScore(QuantifiersEngine* qe);
+ /** exclude match
+  *
+  * Exclude matching d_match_pattern with Node n on subsequent calls to
+  * getNextMatch.
+  */
+ void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
+ /** Get current match.
+  * Returns the term we are currently matching.
+  */
+ Node getCurrentMatch() { return d_curr_matched; }
+ /** set that this match generator is independent
+  *
+ * A match generator is indepndent when this generator fails to produce a
+ * match in a call to getNextMatch, the overall matching fails.
+ */
+ void setIndependent() { d_independent_gen = true; }
+ //-------------------------------construction of inst match generators
+ /** mkInstMatchGenerator for single triggers, calls the method below */
+ static InstMatchGenerator* mkInstMatchGenerator(Node q,
+                                                 Node pat,
+                                                 QuantifiersEngine* qe);
+ /** mkInstMatchGenerator for the multi trigger case
+ *
+ * This linked list of InstMatchGenerator classes with one
+ * InstMatchGeneratorMultiLinear at the head and a list of trailing
+ * InstMatchGenerators corresponding to each unique subterm of pats with
+ * free variables.
+ */
+ static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q,
+                                                      std::vector<Node>& pats,
+                                                      QuantifiersEngine* qe);
+ /** mkInstMatchGenerator
+ *
+ * This generates a linked list of InstMatchGenerators for each unique
+ * subterm of pats with free variables.
+ *
+ * q is the quantified formula associated with the generator we are making
+ * pats is a set of terms we are making InstMatchGenerator nodes for
+ * qe is a pointer to the quantifiers engine (used for querying necessary
+ * information during initialization) pat_map_init maps from terms to
+ * generators we have already made for them.
+ *
+ * It calls initialize(...) for all InstMatchGenerators generated by this call.
+ */
+ static InstMatchGenerator* mkInstMatchGenerator(
+     Node q,
+     std::vector<Node>& pats,
+     QuantifiersEngine* qe,
+     std::map<Node, InstMatchGenerator*>& pat_map_init);
+ //-------------------------------end construction of inst match generators
 
-  static InstMatchGenerator* mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe );
-  static InstMatchGenerator* mkInstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
-  static InstMatchGenerator* mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe, 
-                                                   std::map< Node, InstMatchGenerator * >& pat_map_init );
+protected:
+ /** constructors
+  *
+ * These are intentionally private, and are called during linked list
+ * construction in mkInstMatchGenerator.
+ */
+ InstMatchGenerator(Node pat);
+ InstMatchGenerator();
+ /** The pattern we are producing matches for.
+  *
+ * This term and d_match_pattern can be different since this
+ * term may involve  information regarding phase and (dis)equality entailment,
+ * or other special cases of Triggers.
+ *
+ * For example, for the trigger for P( x ) = false, which matches P( x ) with
+ * P( t ) in the equivalence class of false,
+ *   P( x ) = false is d_pattern
+ *   P( x ) is d_match_pattern
+ * Another example, for pure theory triggers like head( x ), we have
+ *   head( x ) is d_pattern
+ *   x is d_match_pattern
+ * since head( x ) can match any (List) datatype term x.
+ *
+ * If null, this is a multi trigger that is merging matches from d_children,
+ * which is used in InstMatchGeneratorMulti.
+ */
+ Node d_pattern;
+ /** The match pattern
+  * This is the term that is matched against ground terms,
+  * see examples above.
+  */
+ Node d_match_pattern;
+ /** The current term we are matching. */
+ Node d_curr_matched;
+ /** do we need to call reset on this generator? */
+ bool d_needsReset;
+ /** candidate generator
+  * This is the back-end utility for InstMatchGenerator.
+  * It generates a stream of candidate terms to match against d_match_pattern
+  * below, dependending upon what kind of term we are matching
+  * (e.g. a matchable term, a variable, a relation, etc.).
+  */
+ CandidateGenerator* d_cg;
+ /** policy to use for matching
+  * This is one of MATCH_GEN_* above.
+  * TODO: this can be simplified/removed (#1283).
+  */
+ int d_matchPolicy;
+ /** children generators
+  * These match generators correspond to the children of the term
+  * we are matching with this generator.
+  * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
+  * in the example (EX1) above.
+  */
+ std::vector<InstMatchGenerator*> d_children;
+ /** for each child, the index in the term
+  * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
+  * in the example (EX1) above, indicating it is the 2nd child
+  * of the term.
+  */
+ std::vector<int> d_children_index;
+ /** children types 0 : variable, 1 : child term, -1 : ground term */
+ std::vector<int> d_children_types;
+ /** The next generator in the linked list
+  * that this generator is a part of.
+  */
+ InstMatchGenerator* d_next;
+ /** The equivalence class we are currently matching in. */
+ Node d_eq_class;
+ /** If non-null, then this is a relational trigger of the form x ~
+  * d_eq_class_rel. */
+ Node d_eq_class_rel;
+ /** For each child index of this node, the variable numbers of the children.
+ * For example, if this is generator is for the term f( x3, a, x1, x2 )
+ *  the quantified formula
+ *    forall x1 x2 x3. (...).
+ * Then d_var_num[0] = 2, d_var_num[2] = 0 and d_var_num[3] = 1.
+ */
+ std::map<int, int> d_var_num;
+ /** Excluded matches
+ * Stores the terms we are not allowed to match.
+ * These can for instance be specified by the smt2
+ * extended syntax (! ... :no-pattern).
+ */
+ std::map<Node, bool> d_curr_exclude_match;
+ /** Current first candidate
+ * Used in a key fail-quickly optimization which generates
+ * the first candidate term to match during reset().
+ */
+ Node d_curr_first_candidate;
+ /** Indepdendent generate
+ * If this flag is true, failures to match should be cached.
+ */
+ bool d_independent_gen;
+ /** active add flag, described above. */
+ bool d_active_add;
+ /** cached value of d_match_pattern.getType() */
+ TypeNode d_match_pattern_type;
+ /** the match operator for d_match_pattern
+  *
+  * See TermDatabase::getMatchOperator for details on match operators.
+  */
+ Node d_match_pattern_op;
+ /** get the match against ground term or formula t.
+  *
+  * d_match_pattern and t should have the same shape, that is,
+  * their match operator (see TermDatabase::getMatchOperator) is the same.
+  * only valid for use where !d_match_pattern.isNull().
+  */
+ int getMatch(
+     Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent);
+ /** Initialize this generator.
+  *
+  * q is the quantified formula associated with this generator.
+  *
+  * This constructs the appropriate information about what
+  * patterns we are matching and children generators.
+  *
+  * It may construct new (child) generators needed to implement
+  * the matching algorithm for this term. For each new generator
+  * constructed in this way, it adds them to gens.
+  */
+ void initialize(Node q,
+                 QuantifiersEngine* qe,
+                 std::vector<InstMatchGenerator*>& gens);
+ /** Continue next match
+  *
+ * This is called during getNextMatch when the current generator in the linked
+ * list succesfully satisfies its matching constraint. This function either
+ * calls getNextMatch of the next element in the linked list, or finalizes the
+ * match (calling sendInstantiation(...) if active add is true, or returning a
+ * value >0 if active add is false).  Its return value has the same semantics
+ * as getNextMatch.
+ */
+ int continueNextMatch(Node q,
+                       InstMatch& m,
+                       QuantifiersEngine* qe,
+                       Trigger* tparent);
+ /** Get inst match generator
+  *
+  * Gets the InstMatchGenerator that implements the
+  * appropriate matching algorithm for n within q
+  * within a linked list of InstMatchGenerators.
+  */
+ static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
 };/* class InstMatchGenerator */
 
-//match generator for boolean term ITEs
+/** match generator for Boolean term ITEs
+* This handles the special case of triggers that look like ite( x, BV1, BV0 ).
+*/
 class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
 public:
   VarMatchGeneratorBooleanTerm( Node var, Node comp );
   virtual ~VarMatchGeneratorBooleanTerm() throw() {}
-  Node d_comp;
-  bool d_rm_prev;
-  /** reset instantiation round (call this at beginning of instantiation round) */
-  void resetInstantiationRound( QuantifiersEngine* qe ){}
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  bool reset( Node eqc, QuantifiersEngine* qe ){ 
+  /** Reset */
+  bool reset(Node eqc, QuantifiersEngine* qe) override
+  {
     d_eq_class = eqc; 
     return true;
   }
-  /** get the next match.  must call reset( eqc ) before this function. */
-  int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
-  /** add instantiations directly */
-  int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; }
+  /** Get the next match. */
+  int getNextMatch(Node q,
+                   InstMatch& m,
+                   QuantifiersEngine* qe,
+                   Trigger* tparent) override;
+
+ private:
+  /** stores the true branch of the Boolean ITE */
+  Node d_comp;
+  /** stores whether we have written a value for var in the current match. */
+  bool d_rm_prev;
 };
 
-//match generator for purified terms (matched term is substituted into d_subs)
+/** 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 );
   virtual ~VarMatchGeneratorTermSubs() throw() {}
+  /** 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). */
   TNode 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;
-  /** reset instantiation round (call this at beginning of instantiation round) */
-  void resetInstantiationRound( QuantifiersEngine* qe ){}
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  bool reset( Node eqc, QuantifiersEngine* qe ){ 
-    d_eq_class = eqc; 
-    return true;
-  }
-  /** get the next match.  must call reset( eqc ) before this function. */
-  int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
-  /** add instantiations directly */
-  int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; }
 };
 
-
-/** smart multi-trigger implementation */
+/** 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 {
-private:
-  int resetChildren( QuantifiersEngine* qe );
-public:
-  /** constructors */
-  InstMatchGeneratorMultiLinear( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
+  friend class InstMatchGenerator;
+
+ public:
   /** destructor */
   virtual ~InstMatchGeneratorMultiLinear() throw();
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  bool reset( Node eqc, QuantifiersEngine* qe );
-  /** get the next match.  must call reset( eqc ) before this function.*/
-  int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
-};/* class InstMatchGeneratorMulti */
 
+  /** Reset. */
+  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  /** Get the next match. */
+  int getNextMatch(Node q,
+                   InstMatch& m,
+                   QuantifiersEngine* qe,
+                   Trigger* tparent) override;
 
-/** smart multi-trigger implementation */
+ 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 {
-private:
+ public:
+  /** constructors */
+  InstMatchGeneratorMulti(Node q,
+                          std::vector<Node>& pats,
+                          QuantifiersEngine* qe);
+  /** destructor */
+  virtual ~InstMatchGeneratorMulti() throw();
+
+  /** Reset instantiation round. */
+  void resetInstantiationRound(QuantifiersEngine* qe) override;
+  /** Reset. */
+  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  /** Add instantiations. */
+  int addInstantiations(Node q,
+                        InstMatch& baseMatch,
+                        QuantifiersEngine* qe,
+                        Trigger* tparent) override;
+
+ private:
   /** indexed trie */
   typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
-  /** process new match */
-  void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
-  /** process new instantiations */
-  void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
-                                 std::vector< IndexedTrie >& unique_var_tries,
-                                 int trieIndex, int childIndex, int endChildIndex, bool modEq );
-  /** process new instantiations 2 */
-  void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
-                                  std::vector< IndexedTrie >& unique_var_tries,
-                                  int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
-private:
-  /** var contains (variable indices) for each pattern node */
+  /** 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,
+                       int fromChildIndex,
+                       int& 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,
+                                int& addedLemmas,
+                                InstMatchTrie* tr,
+                                int trieIndex,
+                                int childIndex,
+                                int endChildIndex,
+                                bool modEq);
+  /** Map from pattern nodes to indices of variables they contain. */
   std::map< Node, std::vector< int > > d_var_contains;
-  /** variable indices contained to pattern nodes */
+  /** Map from variable indices to pattern nodes that contain them. */
   std::map< int, std::vector< Node > > d_var_to_node;
-  /** quantifier to use */
-  Node d_f;
-  /** policy to use for matching */
-  int d_matchPolicy;
-  /** children generators */
+  /** 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;
-  /** order */
+  /** variable orderings
+   * Stores a heuristically determined variable ordering (unique
+   * variables first) for each term in the multi trigger.
+   */
   std::map< unsigned, InstMatchTrie::ImtIndexOrder* > d_imtio;
-  /** inst match tries for each child */
+  /** 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;
-  /** calculate matches */
-  void calculateMatches( QuantifiersEngine* qe );
-public:
-  /** constructors */
-  InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
-  /** destructor */
-  virtual ~InstMatchGeneratorMulti() throw();
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  void resetInstantiationRound( QuantifiersEngine* qe );
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  bool reset( Node eqc, QuantifiersEngine* qe );
-  /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
-  int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return -1; }
-  /** add instantiations */
-  int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
 };/* class InstMatchGeneratorMulti */
 
-/** smart (single)-trigger implementation */
+/** 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 {
-private:
-  /** quantifier for match term */
-  Node d_f;
-  /** match term */
+ public:
+  /** constructors */
+  InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe);
+  /** destructor */
+  ~InstMatchGeneratorSimple() throw() {}
+  /** Reset instantiation round. */
+  void resetInstantiationRound(QuantifiersEngine* qe) override;
+  /** Add instantiations. */
+  int addInstantiations(Node q,
+                        InstMatch& baseMatch,
+                        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 */
+  /** 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 */
+  /** Match pattern arg types.
+   * Cached values of d_match_pattern[i].getType().
+   */
   std::vector< TypeNode > d_match_pattern_arg_types;
-  /** operator */
+  /** The match operator d_match_pattern (see TermDb::getMatchOperator). */
   Node d_op;
-  /** to indicies */
+  /** Map from child number to variable index. */
   std::map< int, int > d_var_num;
-  /** add instantiations */
-  void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
-public:
-  /** constructors */
-  InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe );
-  /** destructor */
-  ~InstMatchGeneratorSimple() throw() {}
-  /** reset instantiation round (call this whenever equivalence classes have changed) */
-  void resetInstantiationRound( QuantifiersEngine* qe );
-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-  bool reset( Node eqc, QuantifiersEngine* qe ) { return true; }
-  /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
-  int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return -1; }
-  /** add instantiations */
-  int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** get active score */
-  int getActiveScore( QuantifiersEngine * qe );
+  /** 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,
+                         int& addedLemmas,
+                         unsigned argIndex,
+                         quantifiers::TermArgTrie* tat);
 };/* class InstMatchGeneratorSimple */
-
 }
 }
 }
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 01cf655ac..b72f6c8cb 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/trigger.h"
 #include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/ho_trigger.h"
 #include "theory/quantifiers/inst_match_generator.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
@@ -22,7 +23,6 @@
 #include "theory/uf/equality_engine.h"
 #include "util/hash.h"
 
-
 using namespace std;
 using namespace CVC4::kind;
 using namespace CVC4::context;
@@ -56,17 +56,13 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
       d_mg = new InstMatchGeneratorSimple( f, d_nodes[0], qe );
     }else{
       d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe );
-      d_mg->setActiveAdd(true);
     }
   }else{
     if( options::multiTriggerCache() ){
       d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
     }else{
       d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti( f, d_nodes, qe );
-      d_mg->setActiveAdd(true);
     }
-    //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
-    //d_mg->setActiveAdd();
   }
   if( d_nodes.size()==1 ){
     if( isSimpleTrigger( d_nodes[0] ) ){
@@ -81,6 +77,7 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
     }
     ++(qe->d_statistics.d_multi_triggers);
   }
+
   //Notice() << "Trigger : " << (*this) << "  for " << f << std::endl;
   Trace("trigger-debug") << "Finished making trigger." << std::endl;
 }
@@ -97,27 +94,34 @@ void Trigger::reset( Node eqc ){
   d_mg->reset( eqc, d_quantEngine );
 }
 
-bool Trigger::getNextMatch( Node f, InstMatch& m ){
-  int retVal = d_mg->getNextMatch( f, m, d_quantEngine );
-  return retVal>0;
-}
-
 Node Trigger::getInstPattern(){
   return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
 }
 
-int Trigger::addInstantiations( InstMatch& baseMatch ){
-  int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine );
+int Trigger::addInstantiations(InstMatch& baseMatch)
+{
+  int addedLemmas =
+      d_mg->addInstantiations(d_f, baseMatch, d_quantEngine, this);
   if( addedLemmas>0 ){
-    Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was ";
-    for( int i=0; i<(int)d_nodes.size(); i++ ){
-      Debug("inst-trigger") << d_nodes[i] << " ";
+    if (Debug.isOn("inst-trigger"))
+    {
+      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;
     }
-    Debug("inst-trigger") << std::endl;
   }
   return addedLemmas;
 }
 
+bool Trigger::sendInstantiation(InstMatch& m)
+{
+  return d_quantEngine->addInstantiation(d_f, m);
+}
+
 bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
   //only take nodes that contribute variables to the trigger when added
   std::vector< Node > temp;
@@ -213,7 +217,21 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
       }
     }
   }
-  Trigger* t = new Trigger( qe, f, trNodes );
+
+  // check if higher-order
+  Trace("trigger") << "Collect higher-order variable triggers..." << std::endl;
+  std::map<Node, std::vector<Node> > ho_apps;
+  HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
+  Trigger* t;
+  if (!ho_apps.empty())
+  {
+    t = new HigherOrderTrigger(qe, f, trNodes, ho_apps);
+  }
+  else
+  {
+    t = new Trigger(qe, f, trNodes);
+  }
+
   qe->getTriggerDatabase()->addTrigger( trNodes, t );
   return t;
 }
@@ -352,10 +370,11 @@ bool Trigger::isAtomicTrigger( Node n ){
 }
 
 bool Trigger::isAtomicTriggerKind( Kind k ) {
-  return k==APPLY_UF || k==SELECT || k==STORE ||
-         k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
-         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || 
-         k==SEP_PTO || k==BITVECTOR_TO_NAT || k==INT_TO_BITVECTOR;
+  return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
+         || k == APPLY_SELECTOR_TOTAL || k == APPLY_TESTER || k == UNION
+         || k == INTERSECTION || k == SUBSET || k == SETMINUS || k == MEMBER
+         || k == SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT
+         || k == INT_TO_BITVECTOR || k == HO_APPLY;
 }
 
 bool Trigger::isRelationalTrigger( Node n ) {
@@ -392,6 +411,10 @@ bool Trigger::isSimpleTrigger( Node n ){
     if( options::purifyDtTriggers() && t.getKind()==APPLY_SELECTOR_TOTAL ){
       return false;
     }
+    if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
+    {
+      return false;
+    }
     return true;
   }else{
     return false;
@@ -695,76 +718,23 @@ Node Trigger::getInversion( Node n, Node x ) {
   return Node::null();
 }
 
-void Trigger::getTriggerVariables( Node icn, Node q, std::vector< Node >& t_vars ) {
+void Trigger::getTriggerVariables(Node n, Node q, std::vector<Node>& t_vars)
+{
   std::vector< Node > patTerms;
   std::map< Node, TriggerTermInfo > tinfo;
-  //collect all patterns from icn
+  // collect all patterns from n
   std::vector< Node > exclude;
-  collectPatTerms( q, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo );
+  collectPatTerms(q, n, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo);
   //collect all variables from all patterns in patTerms, add to t_vars
   for( unsigned i=0; i<patTerms.size(); i++ ){
     quantifiers::TermUtil::getVarContainsNode( q, patTerms[i], t_vars );
   }
 }
 
-InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) {
-  if( n.getKind()==INST_CONSTANT ){
-    return NULL;
-  }else{
-    Trace("var-trigger-debug") << "Is " << n << " a variable trigger?" << std::endl;
-    if( isBooleanTermTrigger( n ) ){
-      VarMatchGeneratorBooleanTerm* vmg = new VarMatchGeneratorBooleanTerm( n[0], n[1] );
-      Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0] << std::endl;
-      return vmg;
-    }else{
-      Node x;
-      if( options::purifyTriggers() ){
-        x = getInversionVariable( n );
-      }
-      if( !x.isNull() ){
-        Node s = getInversion( n, x );
-        VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs( x, s );
-        Trace("var-trigger") << "Term substitution trigger : " << n << ", var = " << x << ", subs = " << s << std::endl;
-        return vmg;
-      }else{
-        return new InstMatchGenerator( n );
-      }
-    }
-  }
-}
-
 int Trigger::getActiveScore() {
   return d_mg->getActiveScore( d_quantEngine );
 }
 
-Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
-  if( nodes.empty() ){
-    return d_tr.empty() ? NULL : d_tr[0];
-  }else{
-    Node n = nodes.back();
-    nodes.pop_back();
-    if( d_children.find( n )!=d_children.end() ){
-      return d_children[n]->getTrigger2( nodes );
-    }else{
-      return NULL;
-    }
-  }
-}
-
-void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
-  if( nodes.empty() ){
-    d_tr.push_back( t );
-  }else{
-    Node n = nodes.back();
-    nodes.pop_back();
-    if( d_children.find( n )==d_children.end() ){
-      d_children[n] = new TriggerTrie;
-    }
-    d_children[n]->addTrigger2( nodes, t );
-  }
-}
-
-
 TriggerTrie::TriggerTrie()
 {}
 
@@ -781,6 +751,50 @@ TriggerTrie::~TriggerTrie() {
   }
 }
 
+inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
+{
+  std::vector<Node> temp;
+  temp.insert(temp.begin(), nodes.begin(), nodes.end());
+  std::sort(temp.begin(), temp.end());
+  TriggerTrie* tt = this;
+  for (const Node& n : temp)
+  {
+    std::map<TNode, TriggerTrie*>::iterator itt = tt->d_children.find(n);
+    if (itt == tt->d_children.end())
+    {
+      return NULL;
+    }
+    else
+    {
+      tt = itt->second;
+    }
+  }
+  return tt->d_tr.empty() ? NULL : tt->d_tr[0];
+}
+
+void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
+{
+  std::vector<Node> temp;
+  temp.insert(temp.begin(), nodes.begin(), nodes.end());
+  std::sort(temp.begin(), temp.end());
+  TriggerTrie* tt = this;
+  for (const Node& n : temp)
+  {
+    std::map<TNode, TriggerTrie*>::iterator itt = tt->d_children.find(n);
+    if (itt == tt->d_children.end())
+    {
+      TriggerTrie* ttn = new TriggerTrie;
+      tt->d_children[n] = ttn;
+      tt = ttn;
+    }
+    else
+    {
+      tt = itt->second;
+    }
+  }
+  tt->d_tr.push_back(t);
+}
+
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index afab98cee..105878df1 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -23,7 +23,6 @@
 #include "theory/quantifiers/inst_match.h"
 #include "options/quantifiers_options.h"
 
-// Forward declarations for defining the Trigger and TriggerTrie.
 namespace CVC4 {
 namespace theory {
 
@@ -33,147 +32,415 @@ namespace inst {
 
 class IMGenerator;
 class InstMatchGenerator;
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-
-namespace CVC4 {
-namespace theory {
-namespace inst {
 
+/** Information about a node used in a trigger.
+*
+* This information includes:
+* 1. the free variables of the node, and
+* 2. information about which terms are useful for matching.
+*
+* As an example, consider the trigger
+*   { f( x ), g( y ), P( y, z ) }
+* for quantified formula
+*   forall xy. ( f( x ) != b => ( P( x, g( y ) ) V P( y, z ) ) )
+*
+* Notice that it is only useful to match f( x ) to f-applications not in the
+* equivalence class of b, and P( y, z ) to P-applications not in the equivalence
+* class of true, as such instances will always be entailed by the ground
+* equalities and disequalities the current context. Entailed instances are
+* typically not helpful, and are discarded in Instantiate::addInstantiation(...)
+* unless the option --no-inst-no-entail is enabled. For more details, see page
+* 10 of "Congruence Closure with Free Variables", Barbosa et al., TACAS 2017.
+*
+* This example is referenced for each of the functions below.
+*/
 class TriggerTermInfo {
 public:
   TriggerTermInfo() : d_reqPol(0){}
   ~TriggerTermInfo(){}
+  /** The free variables in the node
+  *
+  * In the trigger term info for f( x ) in the above example, d_fv = { x }
+  * In the trigger term info for g( y ) in the above example, d_fv = { y }
+  * In the trigger term info for P( y, z ) in the above example, d_fv = { y, z }
+  */
   std::vector< Node > d_fv;
+  /** Required polarity:  1 for equality, -1 for disequality, 0 for none
+  *
+  * In the trigger term info for f( x ) in the above example, d_reqPol = -1
+  * In the trigger term info for g( y ) in the above example, d_reqPol = 0
+  * In the trigger term info for P( y, z ) in the above example,  d_reqPol = 1
+  */
   int d_reqPol;
+  /** Required polarity equal term
+  *
+  * If d_reqPolEq is not null,
+  *   if d_reqPol = 1, then this trigger term must be matched to terms in the
+  *                    equivalence class of d_reqPolEq,
+  *   if d_reqPol = -1, then this trigger term must be matched to terms *not* in
+  *                     the equivalence class of d_reqPolEq.
+  *
+  * This information is typically chosen by analyzing the entailed equalities
+  * and disequalities of quantified formulas.
+  * In the trigger term info for f( x ) in the above example, d_reqPolEq = b
+  * In the trigger term info for g( y ) in the above example,
+  *   d_reqPolEq = Node::null()
+  * In the trigger term info for P( y, z ) in the above example,
+  *   d_reqPolEq = false
+  */
   Node d_reqPolEq;
+  /** Initialize this information class (can be called more than once).
+  * q is the quantified formula that n is a trigger term for
+  * n is the trigger term
+  * reqPol/reqPolEq are described above
+  */
   void init( Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null() );
 };
 
-/** A collect of nodes representing a trigger. */
+/** A collection of nodes representing a trigger.
+*
+* This class encapsulates all implementations of E-matching in CVC4.
+* Its primary use is as a utility of the quantifiers module InstantiationEngine
+* (see theory/quantifiers/instantiation_engine.h) which uses Trigger to make
+* appropriate calls to Instantiate::addInstantiation(...)
+* (see theory/instantiate.h) for the instantiate utility of the quantifiers
+* engine (d_quantEngine) associated with this trigger.  These calls
+* queue instantiation lemmas to the output channel of TheoryQuantifiers during
+* a full effort check.
+*
+* Concretely, a Trigger* t is used in the following way during a full effort
+* check. Assume that t is associated with quantified formula q (see field d_f).
+* We call :
+*
+* // setup initial information
+* t->resetInstantiationRound();
+* // will produce instantiations based on matching with all terms
+* t->reset( Node::null() );
+* InstMatch baseMatch;
+* // add all instantiations based on E-matching with this trigger and the
+* // current context
+* t->addInstantiations( baseMatch );
+*
+* This will result in (a set of) calls to
+* Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn),
+* where m1...mn are InstMatch objects. These calls add the corresponding
+* instantiation lemma for (q,mi) on the output channel associated with
+* d_quantEngine.
+*
+* The Trigger class is wrapper around an underlying IMGenerator class, which
+* implements various forms of E-matching for its set of nodes (d_nodes), which
+* is refered to in the literature as a "trigger". A trigger is a set of terms
+* whose free variables are the bound variables of a quantified formula q,
+* and that is used to guide instantiations for q (for example, see "Efficient
+* E-Matching for SMT Solvers" by de Moura et al).
+*
+* For example of an instantiation lemma produced by E-matching :
+*
+* quantified formula : forall x. P( x )
+*            trigger : P( x )
+*     ground context : ~P( a )
+*
+* Then E-matching matches P( x ) and P( a ), resulting in the match { x -> a }
+* which is used to generate the instantiation lemma :
+*   (forall x. P( x )) => P( a )
+*
+* Terms that are provided as input to a Trigger class via mkTrigger
+* should be in "instantiation constant form", see TermUtil::getInstConstantNode.
+* Say we have quantified formula q whose AST is the Node
+*   (FORALL
+*     (BOUND_VAR_LIST x)
+*     (NOT (P x))
+*     (INST_PATTERN_LIST (INST_PATTERN (P x))))
+* then TermUtil::getInstConstantNode( q, (P x) ) = (P IC) where
+* IC = TermUtil::getInstantiationConstant( q, i ).
+* Trigger expects as input (P IC) to represent the Trigger (P x). This form
+* ensures that references to bound variables are unique to quantified formulas,
+* which is required to ensure the correctness of instantiation lemmas we
+* generate.
+*
+*/
 class Trigger {
- public:
-  ~Trigger();
+  friend class IMGenerator;
 
+ public:
+  virtual ~Trigger();
+  /** get the generator associated with this trigger */
   IMGenerator* getGenerator() { return d_mg; }
-
-  /** reset instantiation round (call this whenever equivalence
-   * classes have changed) */
+  /** Reset instantiation round.
+   *
+  * Called once at beginning of an instantiation round.
+  */
   void resetInstantiationRound();
-  /** reset, eqc is the equivalence class to search in (search in any
-   * if eqc=null) */
+  /** Reset the trigger.
+   *
+  * eqc is the equivalence class from which to match ground terms. If eqc is
+  * Node::null(), then we match ground terms from all equivalence classes.
+  */
   void reset( Node eqc );
-  /** get next match.  must call reset( eqc ) once before this function. */
-  bool getNextMatch( Node f, InstMatch& m );
-  /** return whether this is a multi-trigger */
+  /** add all available instantiations, based on the current context
+  *
+  * This function makes the appropriate calls to d_qe->addInstantiation(...)
+  * based on the current ground terms and equalities in the current context,
+  * via queries to functions in d_qe. This calls the addInstantiations function
+  * of the underlying match generator. It can be extended to
+  * produce instantiations beyond what is produced by the match generator
+  * (for example, see theory/quantifiers/ho_trigger.h).
+  *
+  * baseMatch : a mapping of default values that should be used for variables
+  *             that are not bound as a result of matching terms from this
+  *             trigger. These default values are not frequently used in
+  *             instantiations.  (TODO : remove #1389)
+  */
+  virtual int addInstantiations(InstMatch& baseMatch);
+  /** Return whether this is a multi-trigger. */
   bool isMultiTrigger() { return d_nodes.size()>1; }
-  /** get inst pattern list */
+  /** 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();
-
-  /** add all available instantiations exhaustively, in any equivalence class
-      if limitInst>0, limitInst is the max # of instantiations to try */
-  int addInstantiations( InstMatch& baseMatch );
-  /** mkTrigger method
-     ie     : quantifier engine;
-     f      : forall something ....
-     nodes  : (multi-)trigger
-     keepAll: don't remove unneeded patterns;
-     trOption : policy for dealing with triggers that already existed
-                (see below)
+  /* A heuristic value indicating how active this generator is.
+   *
+  * This returns the number of ground terms for the match operators in terms
+  * from d_nodes. This score is only used with the experimental option
+  *   --trigger-active-sel.
   */
+  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) << " )";
+  }
+  /** mkTrigger method
+   *
+   * This makes an instance of a trigger object.
+   *  qe     : pointer to the quantifier engine;
+   *  q      : the quantified formula we are making a trigger for
+   *  nodes  : the nodes comprising the (multi-)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.
+   */
   enum{
     TR_MAKE_NEW,    //make new trigger even if it already may exist
     TR_GET_OLD,     //return a previous trigger if it had already been created
     TR_RETURN_NULL  //return null if a duplicate is found
   };
-  //nodes input, trNodes output
-  static bool mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes );
-  static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
-                             bool keepAll = true, int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 );
-  static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll = true,
-                             int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 );
+  static Trigger* mkTrigger(QuantifiersEngine* qe,
+                            Node q,
+                            std::vector<Node>& nodes,
+                            bool keepAll = true,
+                            int trOption = TR_MAKE_NEW,
+                            unsigned use_n_vars = 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);
+  /** make trigger terms
+   *
+   * This takes a set of eligible trigger terms and stores a subset of them in
+   * trNodes, such that :
+   *   (1) the terms in trNodes contain at least n_vars of the quantified
+   *       variables in quantified formula q, and
+   *   (2) the set trNodes is minimal, i.e. removing one term from trNodes
+   *       always violates (1).
+   */
+  static bool mkTriggerTerms(Node q,
+                             std::vector<Node>& nodes,
+                             unsigned n_vars,
+                             std::vector<Node>& trNodes);
+  /** collect pattern terms
+   *
+   * This collects all terms that are eligible for triggers for quantified
+   * formula q in term n and adds them to patTerms.
+   *   tstrt : the selection strategy (see options/quantifiers_mode.h),
+   *   exclude :  a set of terms that *cannot* be selected as triggers,
+   *   tinfo : stores the result of the collection, mapping terms to the
+   *           information they are associated with,
+   *   filterInst : flag that when true, we discard terms that have instances
+   *     in the vector we are returning, e.g. we do not return f( x ) if we are
+   *     also returning f( f( x ) ). TODO: revisit this (issue #1211)
+   */
   static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt,
                                std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo,
                                bool filterInst = false );
-  /** is usable trigger */
+  /** Is n a usable trigger in quantified formula q?
+   *
+   * A usable trigger is one that is matchable and contains free variables only
+   * from q.
+   */
   static bool isUsableTrigger( Node n, Node q );
+  /** get is usable trigger
+   *
+   * Return the associated node of n that is a usable trigger in quantified
+   * formula q. This may be different than n in several cases :
+   * (1) Polarity information is explicitly converted to equalities, e.g.
+   *      getIsUsableTrigger( (not (P x )), q ) may return (= (P x) false)
+   * (2) Relational triggers are put into solved form, e.g.
+   *      getIsUsableTrigger( (= (+ x a) 5), q ) may return (= x (- 5 a)).
+   */
   static Node getIsUsableTrigger( Node n, Node q );
+  /** Is n a usable atomic trigger?
+   *
+   * A usable atomic trigger is a term that is both a useable trigger and an
+   * atomic trigger.
+   */
   static bool isUsableAtomicTrigger( Node n, Node q );
+  /** is n an atomic trigger?
+  *
+  * An atomic trigger is one whose kind is an atomic trigger kind.
+  */
   static bool isAtomicTrigger( Node n );
+  /** Is k an atomic trigger kind?
+   *
+  * An atomic trigger kind is one for which term indexing/matching is possible.
+  */
   static bool isAtomicTriggerKind( Kind k );
+  /** is n a relational trigger, e.g. like x >= a ? */
   static bool isRelationalTrigger( Node n );
+  /** Is k a relational trigger kind? */
   static bool isRelationalTriggerKind( Kind k );
+  /** Is k a kind for which counterexample-guided instantiation is possible?
+   *
+  * This typically corresponds to kinds that correspond to operators that
+  * have total interpretations and are a part of the signature of
+  * satisfaction complete theories (see Reynolds et al., CAV 2015).
+  */
   static bool isCbqiKind( Kind k );
+  /** is n a simple trigger (see inst_match_generator.h)? */
   static bool isSimpleTrigger( Node n );
+  /** is n a Boolean term trigger, e.g. ite( x, BV1, BV0 )? */
   static bool isBooleanTermTrigger( Node n );
+  /** is n a pure theory trigger, e.g. head( x )? */
   static bool isPureTheoryTrigger( Node n );
+  /** get trigger weight
+   *
+   * Returns 0 for triggers that are easy to process and 1 otherwise.
+   * A trigger is easy to process if it is an atomic trigger, or a relational
+   * trigger of the form x ~ g for ~ \in { =, >=, > }.
+   */
   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 );
-  /** return data structure for producing matches for this trigger. */
-  static InstMatchGenerator* getInstMatchGenerator( Node q, Node n );
+  /** get the variable associated with an inversion for n
+   *
+   * A term n with an inversion variable x has the following property :
+   *   There exists a closed function f such that for all terms t
+   *   |= (n = t) <=> (x = f(t))
+   * For example, getInversionVariable( x+1 ) returns x since for all terms t,
+   *   |= x+1 = t <=> x = (\y. y-1)(t)
+   * We call f the inversion function for n.
+   */
   static Node getInversionVariable( Node n );
-  static Node getInversion( Node n, Node x );
-  /** get all variables that E-matching can possibly handle */
-  static void getTriggerVariables( Node icn, Node f, std::vector< Node >& t_vars );
+  /** Get the body of the inversion function for n whose argument is y.
+   * e.g. getInversion( x+1, y ) returns y-1
+   */
+  static Node getInversion(Node n, Node y);
+  /** get all variables that E-matching can instantiate from a subterm n.
+   *
+   * This returns the union of all free variables in usable triggers that are
+   * subterms of n.
+   */
+  static void getTriggerVariables(Node n, Node f, std::vector<Node>& t_vars);
 
-  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) << " )";
-  }
-  int getActiveScore();
-private:
-  /** trigger constructor */
+ protected:
+  /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
   Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes );
-
-  /** is subterm of trigger usable */
+  /** is subterm of trigger usable (helper function for isUsableTrigger) */
   static bool isUsable( Node n, Node q );
+  /** returns an equality that is equivalent to the equality eq and
+  * is a usable trigger for q if one exists, otherwise returns Node::null().
+  */
   static Node getIsUsableEq( Node q, Node eq );
+  /** returns whether n1 == n2 is a usable (relational) trigger for q. */
   static bool isUsableEqTerms( Node q, Node n1, Node n2 );
-  /** collect all APPLY_UF pattern terms for f in n */
+  /** recursive helper function for collectPatTerms
+   *
+   * This collects the usable trigger terms in the subterm n of the body of
+   * quantified formula q.
+   *   visited : cache of the trigger terms collected for each visited node,
+   *   tinfo : cache of trigger term info for each visited node,
+   *   tstrat : the selection strategy (see options/quantifiers_mode.h)
+   *   exclude :  a set of terms that *cannot* be selected as triggers
+   *   pol/hasPol : the polarity of node n in q
+   *                (see QuantPhaseReq theory/quantifiers/quant_util.h)
+   *   epol/hasEPol : the entailed polarity of node n in q
+   *                  (see QuantPhaseReq theory/quantifiers/quant_util.h)
+   *   knowIsUsable : whether we know that n is a usable trigger.
+   *
+   * We add the triggers we collected recursively in n into added.
+   */
   static void collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
                                 quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
                                 bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false );
 
+  /** add an instantiation (called by InstMatchGenerator)
+   *
+   * This calls Instantiate::addInstantiation(...) for instantiations
+   * associated with m. Typically, m is associated with a single instantiation,
+   * but in some cases (e.g. higher-order) we may modify m before calling
+   * Instantiate::addInstantiation(...).
+   */
+  virtual bool sendInstantiation(InstMatch& m);
+  /** The nodes comprising this trigger. */
   std::vector< Node > d_nodes;
-
-  /** the quantifiers engine */
+  /** The quantifiers engine associated with this trigger. */
   QuantifiersEngine* d_quantEngine;
-  /** the quantifier this trigger is for */
+  /** The quantified formula this trigger is for. */
   Node d_f;
-  /** match generators */
+  /** match generator
+   *
+  * This is the back-end utility that implements the underlying matching
+  * algorithm associated with this trigger.
+  */
   IMGenerator* d_mg;
 }; /* class Trigger */
 
-/** a trie of triggers */
+/** A trie of triggers.
+*
+* This class is used to cache all Trigger objects that are generated in the
+* current context. We index Triggers in this data structure based on the
+* value of Trigger::d_nodes. When a Trigger is added to this data structure,
+* this Trie assumes responsibility for deleting it.
+*/
 class TriggerTrie {
 public:
   TriggerTrie();
   ~TriggerTrie();
+  /** get trigger
+  * This returns a Trigger t that is indexed by nodes,
+  * or NULL otherwise.
+  */
+  Trigger* getTrigger(std::vector<Node>& nodes);
+  /** add trigger
+  * This adds t to the trie, indexed by nodes.
+  * In typical use cases, nodes is t->d_nodes.
+  */
+  void addTrigger(std::vector<Node>& nodes, Trigger* t);
 
-  inst::Trigger* getTrigger( std::vector< Node >& nodes ){
-    std::vector< Node > temp;
-    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
-    std::sort( temp.begin(), temp.end() );
-    return getTrigger2( temp );
-  }
-  void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){
-    std::vector< Node > temp;
-    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
-    std::sort( temp.begin(), temp.end() );
-    return addTrigger2( temp, t );
-  }
-private:
-  inst::Trigger* getTrigger2( std::vector< Node >& nodes );
-  void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
-
-  std::vector< inst::Trigger* > d_tr;
+ private:
+  /** The trigger at this node in the trie. */
+  std::vector<Trigger*> d_tr;
+  /** The children of this node in the trie. */
   std::map< TNode, TriggerTrie* > d_children;
 };/* class inst::Trigger::TriggerTrie */