Simplify instantiation match generator interface (#6121)

12 files changed, 202 insertions, 326 deletions

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 719451d1e..584b3ebbf 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -36,24 +36,23 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
-IMGenerator::IMGenerator(quantifiers::QuantifiersState& qs,
-                         quantifiers::QuantifiersInferenceManager& qim)
-    : d_qstate(qs), d_qim(qim)
+IMGenerator::IMGenerator(Trigger* tparent)
+    : d_tparent(tparent), d_qstate(tparent->d_qstate)
 {
 }
 
-bool IMGenerator::sendInstantiation(Trigger* tparent,
-                                    InstMatch& m,
-                                    InferenceId id)
+bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id)
 {
-  return tparent->sendInstantiation(m, id);
+  return d_tparent->sendInstantiation(m, id);
 }
 
-InstMatchGenerator::InstMatchGenerator(
-    Node pat,
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim)
-    : IMGenerator(qs, qim)
+QuantifiersEngine* IMGenerator::getQuantifiersEngine()
+{
+  return d_tparent->d_quantEngine;
+}
+
+InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat)
+    : IMGenerator(tparent)
 {
   d_cg = nullptr;
   d_needsReset = true;
@@ -85,19 +84,21 @@ void InstMatchGenerator::setActiveAdd(bool val){
   }
 }
 
-int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) {
+int InstMatchGenerator::getActiveScore()
+{
   if( d_match_pattern.isNull() ){
     return -1;
   }
-  else if (TriggerTermInfo::isAtomicTrigger(d_match_pattern))
+  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  if (TriggerTermInfo::isAtomicTrigger(d_match_pattern))
   {
-    Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
-    unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
+    Node f = tdb->getMatchOperator(d_match_pattern);
+    unsigned ngt = tdb->getNumGroundTerms(f);
     Trace("trigger-active-sel-debug") << "Number of ground terms for " << f << " is " << ngt << std::endl;
     return ngt;
   }else if( d_match_pattern.getKind()==INST_CONSTANT ){
     TypeNode tn = d_match_pattern.getType();
-    unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn );
+    unsigned ngtt = tdb->getNumTypeGroundTerms(tn);
     Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl;
     return ngtt;
   }
@@ -105,7 +106,6 @@ int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) {
 }
 
 void InstMatchGenerator::initialize(Node q,
-                                    QuantifiersEngine* qe,
                                     std::vector<InstMatchGenerator*>& gens)
 {
   if (d_pattern.isNull())
@@ -172,7 +172,8 @@ void InstMatchGenerator::initialize(Node q,
   d_match_pattern_type = d_match_pattern.getType();
   Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is "
                           << d_match_pattern << std::endl;
-  d_match_pattern_op = qe->getTermDatabase()->getMatchOperator(d_match_pattern);
+  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  d_match_pattern_op = tdb->getMatchOperator(d_match_pattern);
 
   // now, collect children of d_match_pattern
   Kind mpk = d_match_pattern.getKind();
@@ -195,8 +196,7 @@ void InstMatchGenerator::initialize(Node q,
         }
         else
         {
-          InstMatchGenerator* cimg =
-              getInstMatchGenerator(q, pat, d_qstate, d_qim);
+          InstMatchGenerator* cimg = getInstMatchGenerator(d_tparent, q, pat);
           if (cimg)
           {
             d_children.push_back(cimg);
@@ -216,6 +216,7 @@ void InstMatchGenerator::initialize(Node q,
     }
   }
 
+  QuantifiersEngine* qe = getQuantifiersEngine();
   // create candidate generator
   if (mpk == APPLY_SELECTOR)
   {
@@ -254,7 +255,7 @@ void InstMatchGenerator::initialize(Node q,
   {
     if (d_pattern.getKind() == APPLY_SELECTOR_TOTAL)
     {
-      Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern);
+      Node selectorExpr = tdb->getMatchOperator(d_pattern);
       size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
       const DType& dt = datatypes::utils::datatypeOf(selectorExpr);
       const DTypeConstructor& c = dt[selectorIndex];
@@ -285,8 +286,7 @@ void InstMatchGenerator::initialize(Node q,
 }
 
 /** get match (not modulo equality) */
-int InstMatchGenerator::getMatch(
-    Node f, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent)
+int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
 {
   Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
                     << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
@@ -419,7 +419,7 @@ int InstMatchGenerator::getMatch(
     // we will be requesting candidates for matching terms for each child
     for (size_t i = 0, size = d_children.size(); i < size; i++)
     {
-      if (!d_children[i]->reset(t[d_children_index[i]], qe))
+      if (!d_children[i]->reset(t[d_children_index[i]]))
       {
         success = false;
         break;
@@ -428,8 +428,8 @@ int InstMatchGenerator::getMatch(
     if (success)
     {
       Trace("matching-debug2") << "Continue next " << d_next << std::endl;
-      ret_val = continueNextMatch(
-          f, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING);
+      ret_val =
+          continueNextMatch(f, m, InferenceId::QUANTIFIERS_INST_E_MATCHING);
     }
   }
   if (ret_val < 0)
@@ -444,22 +444,21 @@ int InstMatchGenerator::getMatch(
 
 int InstMatchGenerator::continueNextMatch(Node q,
                                           InstMatch& m,
-                                          QuantifiersEngine* qe,
-                                          Trigger* tparent,
                                           InferenceId id)
 {
   if( d_next!=NULL ){
-    return d_next->getNextMatch(q, m, qe, tparent);
+    return d_next->getNextMatch(q, m);
   }
   if (d_active_add)
   {
-    return sendInstantiation(tparent, m, id) ? 1 : -1;
+    return sendInstantiation(m, id) ? 1 : -1;
   }
   return 1;
 }
 
 /** reset instantiation round */
-void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
+void InstMatchGenerator::resetInstantiationRound()
+{
   if( !d_match_pattern.isNull() ){
     Trace("matching-debug2") << this << " reset instantiation round." << std::endl;
     d_needsReset = true;
@@ -468,12 +467,13 @@ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
     }
   }
   if( d_next ){
-    d_next->resetInstantiationRound( qe );
+    d_next->resetInstantiationRound();
   }
   d_curr_exclude_match.clear();
 }
 
-bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
+bool InstMatchGenerator::reset(Node eqc)
+{
   if (d_cg == nullptr)
   {
     // we did not properly initialize the candidate generator, thus we fail
@@ -506,14 +506,11 @@ bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
   return !d_curr_first_candidate.isNull();
 }
 
-int InstMatchGenerator::getNextMatch(Node f,
-                                     InstMatch& m,
-                                     QuantifiersEngine* qe,
-                                     Trigger* tparent)
+int InstMatchGenerator::getNextMatch(Node f, InstMatch& m)
 {
   if( d_needsReset ){
     Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
-    reset( d_eq_class, qe );
+    reset(d_eq_class);
   }
   d_curr_matched = Node::null();
   Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl;
@@ -527,7 +524,7 @@ int InstMatchGenerator::getNextMatch(Node f,
       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, tparent);
+        success = getMatch(f, t, m);
         if( d_independent_gen && success<0 ){
           Assert(d_eq_class.isNull() || !d_eq_class_rel.isNull());
           d_curr_exclude_match[t] = true;
@@ -546,24 +543,22 @@ int InstMatchGenerator::getNextMatch(Node f,
     Trace("matching-summary") << "..." << d_match_pattern << " failed, reset." << std::endl;
     Trace("matching") << this << " failed, reset " << d_eq_class << std::endl;
     //we failed, must reset
-    reset( d_eq_class, qe );
+    reset(d_eq_class);
   }else{
     Trace("matching-summary") << "..." << d_match_pattern << " success." << std::endl;
   }
   return success;
 }
 
-uint64_t InstMatchGenerator::addInstantiations(Node f,
-                                               QuantifiersEngine* qe,
-                                               Trigger* tparent)
+uint64_t InstMatchGenerator::addInstantiations(Node f)
 {
   //try to add instantiation for each match produced
   uint64_t addedLemmas = 0;
   InstMatch m( f );
-  while (getNextMatch(f, m, qe, tparent) > 0)
+  while (getNextMatch(f, m) > 0)
   {
     if( !d_active_add ){
-      if (sendInstantiation(tparent, m, InferenceId::UNKNOWN))
+      if (sendInstantiation(m, InferenceId::UNKNOWN))
       {
         addedLemmas++;
         if (d_qstate.isInConflict())
@@ -584,31 +579,24 @@ uint64_t InstMatchGenerator::addInstantiations(Node f,
   return addedLemmas;
 }
 
-InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
-    Node q,
-    Node pat,
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim,
-    QuantifiersEngine* qe)
+InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(Trigger* tparent,
+                                                             Node q,
+                                                             Node pat)
 {
   std::vector< Node > pats;
   pats.push_back( pat );
   std::map< Node, InstMatchGenerator * > pat_map_init;
-  return mkInstMatchGenerator(q, pats, qs, qim, qe, pat_map_init);
+  return mkInstMatchGenerator(tparent, q, pats, pat_map_init);
 }
 
 InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti(
-    Node q,
-    std::vector<Node>& pats,
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim,
-    QuantifiersEngine* qe)
+    Trigger* tparent, Node q, std::vector<Node>& pats)
 {
   Assert(pats.size() > 1);
   InstMatchGeneratorMultiLinear* imgm =
-      new InstMatchGeneratorMultiLinear(q, pats, qs, qim);
+      new InstMatchGeneratorMultiLinear(tparent, q, pats);
   std::vector< InstMatchGenerator* > gens;
-  imgm->initialize(q, qe, gens);
+  imgm->initialize(q, gens);
   Assert(gens.size() == pats.size());
   std::vector< Node > patsn;
   std::map< Node, InstMatchGenerator * > pat_map_init;
@@ -618,17 +606,14 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti(
     patsn.push_back( pn );
     pat_map_init[pn] = g;
   }
-  //return mkInstMatchGenerator( q, patsn, qe, pat_map_init );
-  imgm->d_next = mkInstMatchGenerator(q, patsn, qs, qim, qe, pat_map_init);
+  imgm->d_next = mkInstMatchGenerator(tparent, q, patsn, pat_map_init);
   return imgm;
 }
 
 InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
+    Trigger* tparent,
     Node q,
     std::vector<Node>& pats,
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim,
-    QuantifiersEngine* qe,
     std::map<Node, InstMatchGenerator*>& pat_map_init)
 {
   size_t pCounter = 0;
@@ -640,7 +625,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
     InstMatchGenerator* init;
     std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] );
     if( iti==pat_map_init.end() ){
-      init = new InstMatchGenerator(pats[pCounter], qs, qim);
+      init = new InstMatchGenerator(tparent, pats[pCounter]);
     }else{
       init = iti->second;
     }
@@ -654,7 +639,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
       if( prev ){
         prev->d_next = curr;
       }
-      curr->initialize(q, qe, gens);
+      curr->initialize(q, gens);
       prev = curr;
       counter++;
     }
@@ -663,11 +648,9 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
   return oinit;
 }
 
-InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(
-    Node q,
-    Node n,
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim)
+InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
+                                                              Node q,
+                                                              Node n)
 {
   if (n.getKind() != INST_CONSTANT)
   {
@@ -690,13 +673,13 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(
     {
       Node s = PatternTermSelector::getInversion(n, x);
       VarMatchGeneratorTermSubs* vmg =
-          new VarMatchGeneratorTermSubs(x, s, qs, qim);
+          new VarMatchGeneratorTermSubs(tparent, x, s);
       Trace("var-trigger") << "Term substitution trigger : " << n
                            << ", var = " << x << ", subs = " << s << std::endl;
       return vmg;
     }
   }
-  return new InstMatchGenerator(n, qs, qim);
+  return new InstMatchGenerator(tparent, n);
 }
 
 }/* CVC4::theory::inst namespace */
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 7a22a5ded..99414c90d 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -29,7 +29,6 @@ class QuantifiersEngine;
 
 namespace quantifiers {
 class QuantifiersState;
-class QuantifiersInferenceManager;
 }  // namespace quantifiers
 
 namespace inst {
@@ -55,14 +54,13 @@ class Trigger;
 */
 class IMGenerator {
 public:
- IMGenerator(quantifiers::QuantifiersState& qs,
-             quantifiers::QuantifiersInferenceManager& qim);
+ IMGenerator(Trigger* tparent);
  virtual ~IMGenerator() {}
  /** Reset instantiation round.
   *
   * Called once at beginning of an instantiation round.
   */
- virtual void resetInstantiationRound(QuantifiersEngine* qe) {}
+ virtual void resetInstantiationRound() {}
  /** Reset.
   *
   * eqc is the equivalence class to search in (any if eqc=null).
@@ -70,7 +68,7 @@ public:
   * 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; }
+ virtual bool reset(Node eqc) { return true; }
  /** Get the next match.
   *
   * Must call reset( eqc ) before this function. This constructs an
@@ -82,14 +80,8 @@ public:
   *
   * 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
+ virtual int getNextMatch(Node q, InstMatch& m) { 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
@@ -98,32 +90,30 @@ public:
   * It returns the number of instantiations added using calls to calls to
   * Instantiate::addInstantiation(...).
   */
-  virtual uint64_t addInstantiations(Node q,
-                                     QuantifiersEngine* qe,
-                                     Trigger* tparent)
-  {
-    return 0;
-  }
-  /** get active score
+ virtual uint64_t addInstantiations(Node q) { 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, InferenceId id);
-  /** The state of the quantifiers engine */
-  quantifiers::QuantifiersState& d_qstate;
-  /** The quantifiers inference manager */
-  quantifiers::QuantifiersInferenceManager& d_qim;
+ virtual int getActiveScore() { 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(InstMatch& m, InferenceId id);
+ /** The parent trigger that owns this */
+ Trigger* d_tparent;
+ /** The state of the quantifiers engine */
+ quantifiers::QuantifiersState& d_qstate;
+ // !!!!!!!!! temporarily available (project #15)
+ QuantifiersEngine* getQuantifiersEngine();
 };/* class IMGenerator */
 
 class CandidateGenerator;
@@ -206,18 +196,13 @@ class InstMatchGenerator : public IMGenerator {
   ~InstMatchGenerator() override;
 
   /** Reset instantiation round. */
-  void resetInstantiationRound(QuantifiersEngine* qe) override;
+  void resetInstantiationRound() override;
   /** Reset. */
-  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  bool reset(Node eqc) override;
   /** Get the next match. */
-  int getNextMatch(Node q,
-                   InstMatch& m,
-                   QuantifiersEngine* qe,
-                   Trigger* tparent) override;
+  int getNextMatch(Node q, InstMatch& m) override;
   /** Add instantiations. */
-  uint64_t addInstantiations(Node q,
-                             QuantifiersEngine* qe,
-                             Trigger* tparent) override;
+  uint64_t addInstantiations(Node q) override;
 
   /** set active add flag (true by default)
    *
@@ -232,7 +217,7 @@ class InstMatchGenerator : public IMGenerator {
    *
    * See Trigger::getActiveScore for details.
    */
-  int getActiveScore(QuantifiersEngine* qe) override;
+  int getActiveScore() override;
   /** exclude match
    *
    * Exclude matching d_match_pattern with Node n on subsequent calls to
@@ -251,12 +236,9 @@ class InstMatchGenerator : public IMGenerator {
   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,
-      quantifiers::QuantifiersState& qs,
-      quantifiers::QuantifiersInferenceManager& qim,
-      QuantifiersEngine* qe);
+  static InstMatchGenerator* mkInstMatchGenerator(Trigger* tparent,
+                                                  Node q,
+                                                  Node pat);
   /** mkInstMatchGenerator for the multi trigger case
   *
   * This linked list of InstMatchGenerator classes with one
@@ -264,12 +246,9 @@ class InstMatchGenerator : public IMGenerator {
   * InstMatchGenerators corresponding to each unique subterm of pats with
   * free variables.
   */
-  static InstMatchGenerator* mkInstMatchGeneratorMulti(
-      Node q,
-      std::vector<Node>& pats,
-      quantifiers::QuantifiersState& qs,
-      quantifiers::QuantifiersInferenceManager& qim,
-      QuantifiersEngine* qe);
+  static InstMatchGenerator* mkInstMatchGeneratorMulti(Trigger* tparent,
+                                                       Node q,
+                                                       std::vector<Node>& pats);
   /** mkInstMatchGenerator
   *
   * This generates a linked list of InstMatchGenerators for each unique
@@ -284,11 +263,9 @@ class InstMatchGenerator : public IMGenerator {
   * It calls initialize(...) for all InstMatchGenerators generated by this call.
   */
   static InstMatchGenerator* mkInstMatchGenerator(
+      Trigger* tparent,
       Node q,
       std::vector<Node>& pats,
-      quantifiers::QuantifiersState& qs,
-      quantifiers::QuantifiersInferenceManager& qim,
-      QuantifiersEngine* qe,
       std::map<Node, InstMatchGenerator*>& pat_map_init);
   //-------------------------------end construction of inst match generators
 
@@ -298,9 +275,7 @@ class InstMatchGenerator : public IMGenerator {
   * These are intentionally private, and are called during linked list
   * construction in mkInstMatchGenerator.
   */
-  InstMatchGenerator(Node pat,
-                     quantifiers::QuantifiersState& qs,
-                     quantifiers::QuantifiersInferenceManager& qim);
+  InstMatchGenerator(Trigger* tparent, Node pat);
   /** The pattern we are producing matches for.
    *
   * This term and d_match_pattern can be different since this
@@ -399,8 +374,7 @@ class InstMatchGenerator : public IMGenerator {
    * 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);
+  int getMatch(Node q, Node t, InstMatch& m);
   /** Initialize this generator.
    *
    * q is the quantified formula associated with this generator.
@@ -413,7 +387,6 @@ class InstMatchGenerator : public IMGenerator {
    * constructed in this way, it adds them to gens.
    */
   void initialize(Node q,
-                  QuantifiersEngine* qe,
                   std::vector<InstMatchGenerator*>& gens);
   /** Continue next match
    *
@@ -426,8 +399,6 @@ class InstMatchGenerator : public IMGenerator {
   */
   int continueNextMatch(Node q,
                         InstMatch& m,
-                        QuantifiersEngine* qe,
-                        Trigger* tparent,
                         InferenceId id);
   /** Get inst match generator
    *
@@ -435,11 +406,9 @@ class InstMatchGenerator : public IMGenerator {
    * appropriate matching algorithm for n within q
    * within a linked list of InstMatchGenerators.
    */
-  static InstMatchGenerator* getInstMatchGenerator(
-      Node q,
-      Node n,
-      quantifiers::QuantifiersState& qs,
-      quantifiers::QuantifiersInferenceManager& qim);
+  static InstMatchGenerator* getInstMatchGenerator(Trigger* tparent,
+                                                   Node q,
+                                                   Node n);
 };/* class InstMatchGenerator */
 
 }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index a1674e89f..2920be1a2 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -25,13 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
-InstMatchGeneratorMulti::InstMatchGeneratorMulti(
-    Node q,
-    std::vector<Node>& pats,
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim,
-    QuantifiersEngine* qe)
-    : IMGenerator(qs, qim), d_quant(q)
+InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent,
+                                                 Node q,
+                                                 std::vector<Node>& pats)
+    : IMGenerator(tparent), d_quant(q)
 {
   Trace("multi-trigger-cache")
       << "Making smart multi-trigger for " << q << std::endl;
@@ -60,7 +57,7 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(
     Node n = pats[i];
     // make the match generator
     InstMatchGenerator* img =
-        InstMatchGenerator::mkInstMatchGenerator(q, n, qs, qim, qe);
+        InstMatchGenerator::mkInstMatchGenerator(tparent, q, n);
     img->setActiveAdd(false);
     d_children.push_back(img);
     // compute unique/shared variables
@@ -134,20 +131,20 @@ InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
 
 /** reset instantiation round (call this whenever equivalence classes have
  * changed) */
-void InstMatchGeneratorMulti::resetInstantiationRound(QuantifiersEngine* qe)
+void InstMatchGeneratorMulti::resetInstantiationRound()
 {
   for (InstMatchGenerator* c : d_children)
   {
-    c->resetInstantiationRound(qe);
+    c->resetInstantiationRound();
   }
 }
 
 /** reset, eqc is the equivalence class to search in (any if eqc=null) */
-bool InstMatchGeneratorMulti::reset(Node eqc, QuantifiersEngine* qe)
+bool InstMatchGeneratorMulti::reset(Node eqc)
 {
   for (InstMatchGenerator* c : d_children)
   {
-    if (!c->reset(eqc, qe))
+    if (!c->reset(eqc))
     {
       // do not return false here
     }
@@ -155,9 +152,7 @@ bool InstMatchGeneratorMulti::reset(Node eqc, QuantifiersEngine* qe)
   return true;
 }
 
-uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
-                                                    QuantifiersEngine* qe,
-                                                    Trigger* tparent)
+uint64_t InstMatchGeneratorMulti::addInstantiations(Node q)
 {
   uint64_t addedLemmas = 0;
   Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
@@ -166,7 +161,7 @@ uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
     Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
     std::vector<InstMatch> newMatches;
     InstMatch m(q);
-    while (d_children[i]->getNextMatch(q, m, qe, tparent) > 0)
+    while (d_children[i]->getNextMatch(q, m) > 0)
     {
       // m.makeRepresentative( qe );
       newMatches.push_back(InstMatch(&m));
@@ -179,8 +174,8 @@ uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
       Trace("multi-trigger-cache2")
           << "...processing " << j << " / " << newMatches.size()
           << ", #lemmas = " << addedLemmas << std::endl;
-      processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
-      if (qe->getState().isInConflict())
+      processNewMatch(newMatches[j], i, addedLemmas);
+      if (d_qstate.isInConflict())
       {
         return addedLemmas;
       }
@@ -189,15 +184,12 @@ uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
   return addedLemmas;
 }
 
-void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
-                                              Trigger* tparent,
-                                              InstMatch& m,
+void InstMatchGeneratorMulti::processNewMatch(InstMatch& m,
                                               size_t fromChildIndex,
                                               uint64_t& addedLemmas)
 {
   // see if these produce new matches
-  d_children_trie[fromChildIndex].addInstMatch(
-      qe->getState(), d_quant, m.d_vals);
+  d_children_trie[fromChildIndex].addInstMatch(d_qstate, d_quant, m.d_vals);
   // 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
@@ -207,9 +199,7 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
       << "Child " << fromChildIndex << " produced match " << m << std::endl;
   // process new instantiations
   size_t childIndex = (fromChildIndex + 1) % d_children.size();
-  processNewInstantiations(qe,
-                           tparent,
-                           m,
+  processNewInstantiations(m,
                            addedLemmas,
                            d_children_trie[childIndex].getTrie(),
                            0,
@@ -218,9 +208,7 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
                            true);
 }
 
-void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
-                                                       Trigger* tparent,
-                                                       InstMatch& m,
+void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m,
                                                        uint64_t& addedLemmas,
                                                        InstMatchTrie* tr,
                                                        size_t trieIndex,
@@ -228,12 +216,11 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
                                                        size_t endChildIndex,
                                                        bool modEq)
 {
-  Assert(!qe->getState().isInConflict());
+  Assert(!d_qstate.isInConflict());
   if (childIndex == endChildIndex)
   {
     // m is an instantiation
-    if (sendInstantiation(
-            tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
+    if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
     {
       addedLemmas++;
       Trace("multi-trigger-cache-debug")
@@ -253,16 +240,14 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
       {
         InstMatch mn(&m);
         mn.setValue(curr_index, d.first);
-        processNewInstantiations(qe,
-                                 tparent,
-                                 mn,
+        processNewInstantiations(mn,
                                  addedLemmas,
                                  &(d.second),
                                  trieIndex + 1,
                                  childIndex,
                                  endChildIndex,
                                  modEq);
-        if (qe->getState().isInConflict())
+        if (d_qstate.isInConflict())
         {
           break;
         }
@@ -272,9 +257,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
     std::map<Node, InstMatchTrie>::iterator it = tr->d_data.find(n);
     if (it != tr->d_data.end())
     {
-      processNewInstantiations(qe,
-                               tparent,
-                               m,
+      processNewInstantiations(m,
                                addedLemmas,
                                &(it->second),
                                trieIndex + 1,
@@ -286,7 +269,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
     {
       return;
     }
-    quantifiers::QuantifiersState& qs = qe->getState();
+    quantifiers::QuantifiersState& qs = d_qstate;
     // check modulo equality for other possible instantiations
     if (!qs.hasTerm(n))
     {
@@ -301,16 +284,14 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
         std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
         if (itc != tr->d_data.end())
         {
-          processNewInstantiations(qe,
-                                   tparent,
-                                   m,
+          processNewInstantiations(m,
                                    addedLemmas,
                                    &(itc->second),
                                    trieIndex + 1,
                                    childIndex,
                                    endChildIndex,
                                    modEq);
-          if (qe->getState().isInConflict())
+          if (d_qstate.isInConflict())
           {
             break;
           }
@@ -322,9 +303,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
   else
   {
     size_t newChildIndex = (childIndex + 1) % d_children.size();
-    processNewInstantiations(qe,
-                             tparent,
-                             m,
+    processNewInstantiations(m,
                              addedLemmas,
                              d_children_trie[newChildIndex].getTrie(),
                              0,
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
index 53db94c67..85cbff7f0 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
@@ -38,22 +38,16 @@ class InstMatchGeneratorMulti : public IMGenerator
 {
  public:
   /** constructors */
-  InstMatchGeneratorMulti(Node q,
-                          std::vector<Node>& pats,
-                          quantifiers::QuantifiersState& qs,
-                          quantifiers::QuantifiersInferenceManager& qim,
-                          QuantifiersEngine* qe);
+  InstMatchGeneratorMulti(Trigger* tparent, Node q, std::vector<Node>& pats);
   /** destructor */
   ~InstMatchGeneratorMulti() override;
 
   /** Reset instantiation round. */
-  void resetInstantiationRound(QuantifiersEngine* qe) override;
+  void resetInstantiationRound() override;
   /** Reset. */
-  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  bool reset(Node eqc) override;
   /** Add instantiations. */
-  uint64_t addInstantiations(Node q,
-                             QuantifiersEngine* qe,
-                             Trigger* tparent) override;
+  uint64_t addInstantiations(Node q) override;
 
  private:
   /** process new match
@@ -63,9 +57,7 @@ class InstMatchGeneratorMulti : public IMGenerator
    * addedLemmas is how many instantiations we succesfully send
    * via IMGenerator::sendInstantiation(...) calls.
    */
-  void processNewMatch(QuantifiersEngine* qe,
-                       Trigger* tparent,
-                       InstMatch& m,
+  void processNewMatch(InstMatch& m,
                        size_t fromChildIndex,
                        uint64_t& addedLemmas);
   /** helper for process new match
@@ -78,9 +70,7 @@ class InstMatchGeneratorMulti : public IMGenerator
    *                  computed by this function returns to.
    * modEq is whether we are matching modulo equality.
    */
-  void processNewInstantiations(QuantifiersEngine* qe,
-                                Trigger* tparent,
-                                InstMatch& m,
+  void processNewInstantiations(InstMatch& m,
                                 uint64_t& addedLemmas,
                                 InstMatchTrie* tr,
                                 size_t trieIndex,
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
index d70011bfb..ac7bb5f3c 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -25,11 +25,8 @@ namespace theory {
 namespace inst {
 
 InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
-    Node q,
-    std::vector<Node>& pats,
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim)
-    : InstMatchGenerator(Node::null(), qs, qim)
+    Trigger* tparent, Node q, std::vector<Node>& pats)
+    : InstMatchGenerator(tparent, Node::null())
 {
   // order patterns to maximize eager matching failures
   std::map<Node, std::vector<Node> > var_contains;
@@ -105,7 +102,7 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
   {
     Node po = pats_ordered[i];
     Trace("multi-trigger-linear") << "...make for " << po << std::endl;
-    InstMatchGenerator* cimg = getInstMatchGenerator(q, po, qs, qim);
+    InstMatchGenerator* cimg = getInstMatchGenerator(tparent, q, po);
     Assert(cimg != nullptr);
     d_children.push_back(cimg);
     // this could be improved
@@ -116,11 +113,11 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear(
   }
 }
 
-int InstMatchGeneratorMultiLinear::resetChildren(QuantifiersEngine* qe)
+int InstMatchGeneratorMultiLinear::resetChildren()
 {
   for (InstMatchGenerator* c : d_children)
   {
-    if (!c->reset(Node::null(), qe))
+    if (!c->reset(Node::null()))
     {
       return -2;
     }
@@ -128,27 +125,24 @@ int InstMatchGeneratorMultiLinear::resetChildren(QuantifiersEngine* qe)
   return 1;
 }
 
-bool InstMatchGeneratorMultiLinear::reset(Node eqc, QuantifiersEngine* qe)
+bool InstMatchGeneratorMultiLinear::reset(Node eqc)
 {
   Assert(eqc.isNull());
   if (options::multiTriggerLinear())
   {
     return true;
   }
-  return resetChildren(qe) > 0;
+  return resetChildren() > 0;
 }
 
-int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
-                                                InstMatch& m,
-                                                QuantifiersEngine* qe,
-                                                Trigger* tparent)
+int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m)
 {
   Trace("multi-trigger-linear-debug")
       << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
   if (options::multiTriggerLinear())
   {
     // reset everyone
-    int rc_ret = resetChildren(qe);
+    int rc_ret = resetChildren();
     if (rc_ret < 0)
     {
       return rc_ret;
@@ -158,8 +152,8 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
       << "InstMatchGeneratorMultiLinear::getNextMatch : continue match "
       << std::endl;
   Assert(d_next != nullptr);
-  int ret_val = continueNextMatch(
-      q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
+  int ret_val =
+      continueNextMatch(q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
   if (ret_val > 0)
   {
     Trace("multi-trigger-linear")
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
index d83883df9..ce1e79229 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
@@ -68,21 +68,17 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator
 
  public:
   /** Reset. */
-  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  bool reset(Node eqc) override;
   /** Get the next match. */
-  int getNextMatch(Node q,
-                   InstMatch& m,
-                   QuantifiersEngine* qe,
-                   Trigger* tparent) override;
+  int getNextMatch(Node q, InstMatch& m) override;
 
  protected:
   /** reset the children of this generator */
-  int resetChildren(QuantifiersEngine* qe);
+  int resetChildren();
   /** constructor */
-  InstMatchGeneratorMultiLinear(Node q,
-                                std::vector<Node>& pats,
-                                quantifiers::QuantifiersState& qs,
-                                quantifiers::QuantifiersInferenceManager& qim);
+  InstMatchGeneratorMultiLinear(Trigger* tparent,
+                                Node q,
+                                std::vector<Node>& pats);
 };
 
 }  // namespace inst
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 879bd50b9..eaf917545 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -28,13 +28,10 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
-InstMatchGeneratorSimple::InstMatchGeneratorSimple(
-    Node q,
-    Node pat,
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim,
-    QuantifiersEngine* qe)
-    : IMGenerator(qs, qim), d_quant(q), d_match_pattern(pat)
+InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
+                                                   Node q,
+                                                   Node pat)
+    : IMGenerator(tparent), d_quant(q), d_match_pattern(pat)
 {
   if (d_match_pattern.getKind() == NOT)
   {
@@ -68,41 +65,40 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(
     }
     d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
   }
-  d_op = qe->getTermDatabase()->getMatchOperator(d_match_pattern);
+  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  d_op = tdb->getMatchOperator(d_match_pattern);
 }
 
-void InstMatchGeneratorSimple::resetInstantiationRound(QuantifiersEngine* qe) {}
-uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
-                                                     QuantifiersEngine* qe,
-                                                     Trigger* tparent)
+void InstMatchGeneratorSimple::resetInstantiationRound() {}
+uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
 {
-  quantifiers::QuantifiersState& qs = qe->getState();
   uint64_t addedLemmas = 0;
   TNodeTrie* tat;
+  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
   if (d_eqc.isNull())
   {
-    tat = qe->getTermDatabase()->getTermArgTrie(d_op);
+    tat = tdb->getTermArgTrie(d_op);
   }
   else
   {
     if (d_pol)
     {
-      tat = qe->getTermDatabase()->getTermArgTrie(d_eqc, d_op);
+      tat = tdb->getTermArgTrie(d_eqc, d_op);
     }
     else
     {
       // iterate over all classes except r
-      tat = qe->getTermDatabase()->getTermArgTrie(Node::null(), d_op);
-      if (tat && !qs.isInConflict())
+      tat = tdb->getTermArgTrie(Node::null(), d_op);
+      if (tat && !d_qstate.isInConflict())
       {
-        Node r = qs.getRepresentative(d_eqc);
+        Node r = d_qstate.getRepresentative(d_eqc);
         for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
         {
           if (t.first != r)
           {
             InstMatch m(q);
-            addInstantiations(m, qe, addedLemmas, 0, &(t.second), tparent);
-            if (qs.isInConflict())
+            addInstantiations(m, addedLemmas, 0, &(t.second));
+            if (d_qstate.isInConflict())
             {
               break;
             }
@@ -115,20 +111,18 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
   Debug("simple-trigger-debug")
       << "Adding instantiations based on " << tat << " from " << d_op << " "
       << d_eqc << std::endl;
-  if (tat && !qs.isInConflict())
+  if (tat && !d_qstate.isInConflict())
   {
     InstMatch m(q);
-    addInstantiations(m, qe, addedLemmas, 0, tat, tparent);
+    addInstantiations(m, addedLemmas, 0, tat);
   }
   return addedLemmas;
 }
 
 void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
-                                                 QuantifiersEngine* qe,
                                                  uint64_t& addedLemmas,
                                                  size_t argIndex,
-                                                 TNodeTrie* tat,
-                                                 Trigger* tparent)
+                                                 TNodeTrie* tat)
 {
   Debug("simple-trigger-debug")
       << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
@@ -150,15 +144,13 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     }
     // we do not need the trigger parent for simple triggers (no post-processing
     // required)
-    if (sendInstantiation(
-            tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
+    if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
     {
       addedLemmas++;
       Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
     }
     return;
   }
-  quantifiers::QuantifiersState& qs = qe->getState();
   if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
   {
     int v = d_var_num[argIndex];
@@ -173,10 +165,9 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
         if (prev.isNull() || prev == t)
         {
           m.setValue(v, t);
-          addInstantiations(
-              m, qe, addedLemmas, argIndex + 1, &(tt.second), tparent);
+          addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second));
           m.setValue(v, prev);
-          if (qs.isInConflict())
+          if (d_qstate.isInConflict())
           {
             break;
           }
@@ -186,18 +177,19 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     }
     // inst constant from another quantified formula, treat as ground term?
   }
-  Node r = qs.getRepresentative(d_match_pattern[argIndex]);
+  Node r = d_qstate.getRepresentative(d_match_pattern[argIndex]);
   std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
   if (it != tat->d_data.end())
   {
-    addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second), tparent);
+    addInstantiations(m, addedLemmas, argIndex + 1, &(it->second));
   }
 }
 
-int InstMatchGeneratorSimple::getActiveScore(QuantifiersEngine* qe)
+int InstMatchGeneratorSimple::getActiveScore()
 {
-  Node f = qe->getTermDatabase()->getMatchOperator(d_match_pattern);
-  size_t ngt = qe->getTermDatabase()->getNumGroundTerms(f);
+  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  Node f = tdb->getMatchOperator(d_match_pattern);
+  size_t ngt = tdb->getNumGroundTerms(f);
   Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) "
                                     << f << " is " << ngt << std::endl;
   return static_cast<int>(ngt);
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
index dd8746f71..bfb4b6840 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
@@ -49,20 +49,14 @@ class InstMatchGeneratorSimple : public IMGenerator
 {
  public:
   /** constructors */
-  InstMatchGeneratorSimple(Node q,
-                           Node pat,
-                           quantifiers::QuantifiersState& qs,
-                           quantifiers::QuantifiersInferenceManager& qim,
-                           QuantifiersEngine* qe);
+  InstMatchGeneratorSimple(Trigger* tparent, Node q, Node pat);
 
   /** Reset instantiation round. */
-  void resetInstantiationRound(QuantifiersEngine* qe) override;
+  void resetInstantiationRound() override;
   /** Add instantiations. */
-  uint64_t addInstantiations(Node q,
-                             QuantifiersEngine* qe,
-                             Trigger* tparent) override;
+  uint64_t addInstantiations(Node q) override;
   /** Get active score. */
-  int getActiveScore(QuantifiersEngine* qe) override;
+  int getActiveScore() override;
 
  private:
   /** quantified formula for the trigger term */
@@ -101,11 +95,9 @@ class InstMatchGeneratorSimple : public IMGenerator
    * tat is the term index we are currently traversing.
    */
   void addInstantiations(InstMatch& m,
-                         QuantifiersEngine* qe,
                          uint64_t& addedLemmas,
                          size_t argIndex,
-                         TNodeTrie* tat,
-                         Trigger* tparent);
+                         TNodeTrie* tat);
 };
 
 }  // namespace inst
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 7d397403d..62a63a2d5 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -69,19 +69,17 @@ Trigger::Trigger(QuantifiersEngine* qe,
   if( d_nodes.size()==1 ){
     if (TriggerTermInfo::isSimpleTrigger(d_nodes[0]))
     {
-      d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qs, qim, qe);
+      d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]);
       ++(qe->d_statistics.d_triggers);
     }else{
-      d_mg =
-          InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qs, qim, qe);
+      d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]);
       ++(qe->d_statistics.d_simple_triggers);
     }
   }else{
     if( options::multiTriggerCache() ){
-      d_mg = new InstMatchGeneratorMulti(q, d_nodes, qs, qim, qe);
+      d_mg = new InstMatchGeneratorMulti(this, q, d_nodes);
     }else{
-      d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(
-          q, d_nodes, qs, qim, qe);
+      d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes);
     }
     if (Trace.isOn("multi-trigger"))
     {
@@ -101,13 +99,9 @@ Trigger::~Trigger() {
   delete d_mg;
 }
 
-void Trigger::resetInstantiationRound(){
-  d_mg->resetInstantiationRound( d_quantEngine );
-}
+void Trigger::resetInstantiationRound() { d_mg->resetInstantiationRound(); }
 
-void Trigger::reset( Node eqc ){
-  d_mg->reset( eqc, d_quantEngine );
-}
+void Trigger::reset(Node eqc) { d_mg->reset(eqc); }
 
 bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; }
 
@@ -138,7 +132,7 @@ uint64_t Trigger::addInstantiations()
       }
     }
   }
-  uint64_t addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this);
+  uint64_t addedLemmas = d_mg->addInstantiations(d_quant);
   if (Debug.isOn("inst-trigger"))
   {
     if (addedLemmas > 0)
@@ -316,9 +310,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
   return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars);
 }
 
-int Trigger::getActiveScore() {
-  return d_mg->getActiveScore( d_quantEngine );
-}
+int Trigger::getActiveScore() { return d_mg->getActiveScore(); }
 
 Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
                                            Node n,
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 31661e611..b5a271fae 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -247,7 +247,7 @@ class Trigger {
    * This example would fail to match when f(a) is not registered.
    */
   std::vector<Node> d_groundTerms;
-  /** The quantifiers engine associated with this trigger. */
+  // !!!!!!!!!!!!!!!!!! temporarily available (project #15)
   QuantifiersEngine* d_quantEngine;
   /** Reference to the quantifiers state */
   quantifiers::QuantifiersState& d_qstate;
diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
index 20e157808..c8d907bcf 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -23,12 +23,10 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
-VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(
-    Node var,
-    Node subs,
-    quantifiers::QuantifiersState& qs,
-    quantifiers::QuantifiersInferenceManager& qim)
-    : InstMatchGenerator(Node::null(), qs, qim),
+VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Trigger* tparent,
+                                                     Node var,
+                                                     Node subs)
+    : InstMatchGenerator(tparent, Node::null()),
       d_var(var),
       d_subs(subs),
       d_rm_prev(false)
@@ -37,16 +35,13 @@ VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(
   d_var_type = d_var.getType();
 }
 
-bool VarMatchGeneratorTermSubs::reset(Node eqc, QuantifiersEngine* qe)
+bool VarMatchGeneratorTermSubs::reset(Node eqc)
 {
   d_eq_class = eqc;
   return true;
 }
 
-int VarMatchGeneratorTermSubs::getNextMatch(Node q,
-                                            InstMatch& m,
-                                            QuantifiersEngine* qe,
-                                            Trigger* tparent)
+int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m)
 {
   int ret_val = -1;
   if (!d_eq_class.isNull())
@@ -61,14 +56,14 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q,
     d_eq_class = Node::null();
     // if( s.getType().isSubtypeOf( d_var_type ) ){
     d_rm_prev = m.get(d_children_types[0]).isNull();
-    if (!m.set(qe->getState(), d_children_types[0], s))
+    if (!m.set(d_qstate, d_children_types[0], s))
     {
       return -1;
     }
     else
     {
       ret_val = continueNextMatch(
-          q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN);
+          q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN);
       if (ret_val > 0)
       {
         return ret_val;
diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h
index 910dbc79b..591c47958 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.h
+++ b/src/theory/quantifiers/ematching/var_match_generator.h
@@ -31,18 +31,12 @@ namespace inst {
 class VarMatchGeneratorTermSubs : public InstMatchGenerator
 {
  public:
-  VarMatchGeneratorTermSubs(Node var,
-                            Node subs,
-                            quantifiers::QuantifiersState& qs,
-                            quantifiers::QuantifiersInferenceManager& qim);
+  VarMatchGeneratorTermSubs(Trigger* tparent, Node var, Node subs);
 
   /** Reset */
-  bool reset(Node eqc, QuantifiersEngine* qe) override;
+  bool reset(Node eqc) override;
   /** Get the next match. */
-  int getNextMatch(Node q,
-                   InstMatch& m,
-                   QuantifiersEngine* qe,
-                   Trigger* tparent) override;
+  int getNextMatch(Node q, InstMatch& m) override;
 
  private:
   /** variable we are matching (x in the example x+1). */