4 files changed, 30 insertions, 34 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 6206b24a7..4cdce940e 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/theory_uf_rewriter.h"
@@ -236,7 +237,6 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
     d_lchildren.clear();
     d_arg_to_arg_rep.clear();
     d_arg_vector.clear();
-    QuantifiersState& qs = d_quantEngine->getState();
     for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
     {
       TNode var = ha.first;
@@ -288,9 +288,9 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
           }
           else if (!itf->second.isNull())
           {
-            if (!qs.areEqual(itf->second, args[k]))
+            if (!d_qstate.areEqual(itf->second, args[k]))
             {
-              if (!d_quantEngine->getTermDatabase()->isEntailed(
+              if (!d_treg.getTermDatabase()->isEntailed(
                       itf->second.eqNode(args[k]), true))
               {
                 fixed_vals[k] = Node::null();
@@ -323,7 +323,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
         {
           if (!itf->second.isNull())
           {
-            Node r = qs.getRepresentative(itf->second);
+            Node r = d_qstate.getRepresentative(itf->second);
             std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r);
             if (itfr != arg_to_rep.end())
             {
@@ -375,7 +375,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
   else
   {
     // do not run higher-order matching
-    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
+    return d_qim.getInstantiate()->addInstantiation(d_quant, m, id);
   }
 }
 
@@ -389,7 +389,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m,
   if (var_index == d_ho_var_list.size())
   {
     // we now have an instantiation to try
-    return d_quantEngine->getInstantiate()->addInstantiation(
+    return d_qim.getInstantiate()->addInstantiation(
         d_quant, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_HO);
   }
   else
@@ -476,7 +476,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
   Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
   uint64_t numLemmas = 0;
   // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
-  TermDb* tdb = d_quantEngine->getTermDatabase();
+  TermDb* tdb = d_treg.getTermDatabase();
   unsigned size = tdb->getNumOperators();
   NodeManager* nm = NodeManager::currentNM();
   for (unsigned j = 0; j < size; j++)
diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h
index 0d0f9498d..efc65cdef 100644
--- a/src/theory/quantifiers/ematching/im_generator.h
+++ b/src/theory/quantifiers/ematching/im_generator.h
@@ -36,22 +36,22 @@ namespace inst {
 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/ematching/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.
-*/
+ *
+ * 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/ematching/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
+ * Instantiate::addInstantiation(...). The latter function is the entry
+ * point in which instantiate lemmas are enqueued to be sent on the output
+ * channel.
+ */
 class IMGenerator {
 public:
  IMGenerator(Trigger* tparent);
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
index ad48d9c91..6ae2f915b 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
@@ -41,10 +41,6 @@ namespace inst {
  * 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
 {
@@ -88,12 +84,12 @@ class InstMatchGeneratorSimple : public IMGenerator
   std::map<size_t, int> d_var_num;
   /** add instantiations, helper function.
    *
-   * m is the current match we are building,
-   * addedLemmas is the number of lemmas we have added via calls to
-   *                qe->getInstantiate()->aaddInstantiation(...),
-   * argIndex is the argument index in d_match_pattern we are currently
-   *              matching,
-   * tat is the term index we are currently traversing.
+   * @param m the current match we are building,
+   * @param addedLemmas the number of lemmas we have added via calls to
+   * Instantiate::addInstantiation(...),
+   * @param argIndex the argument index in d_match_pattern we are currently
+   * matching,
+   * @param tat the term index we are currently traversing.
    */
   void addInstantiations(InstMatch& m,
                          uint64_t& addedLemmas,
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index af0a0bfbc..c93e1a99b 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -154,7 +154,7 @@ uint64_t Trigger::addInstantiations()
 
 bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
 {
-  return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id);
+  return d_qim.getInstantiate()->addInstantiation(d_quant, m, id);
 }
 
 bool Trigger::sendInstantiation(InstMatch& m, InferenceId id)