From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 29 Apr 2022 15:43:55 +0000 (-0500)
Subject: Refactor interfaces for E-matching (#8665)
X-Git-Tag: cvc5-1.0.1~200
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25be5c6148c0e0d9ab4666062c0666fb085eee8a;p=cvc5.git

Refactor interfaces for E-matching (#8665)

InstMatch objects are now fully owned by Triggers. They are passed by reference to InstMatchGenerators.

This also simplifies the interfaces by not passing the quantified formulas.

This is in preparation for making InstMatch objects carry entailment test information.
---

diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp
index af9b184ee..509043b03 100644
--- a/src/theory/quantifiers/ematching/im_generator.cpp
+++ b/src/theory/quantifiers/ematching/im_generator.cpp
@@ -32,9 +32,9 @@ IMGenerator::IMGenerator(Env& env, Trigger* tparent)
 {
 }
 
-bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id)
+bool IMGenerator::sendInstantiation(std::vector<Node>& terms, InferenceId id)
 {
-  return d_tparent->sendInstantiation(m, id);
+  return d_tparent->sendInstantiation(terms, id);
 }
 
 }  // namespace inst
diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h
index cac3fe671..355b29103 100644
--- a/src/theory/quantifiers/ematching/im_generator.h
+++ b/src/theory/quantifiers/ematching/im_generator.h
@@ -77,22 +77,20 @@ class IMGenerator : protected EnvObj
    * 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
+   * @param m the InstMatch object we are generating
+   * @return a value >0 if an instantiation was successfully generated
    */
-  virtual int getNextMatch(Node q, InstMatch& m) { return 0; }
+  virtual int getNextMatch(InstMatch& m) { return 0; }
   /** add instantiations
    *
-   * This adds 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.
+   * This adds all available instantiations for the quantified formula of m
+   * based on the current context using the implemented matching algorithm. It
+   * typically is implemented as a fixed point of getNextMatch above.
    *
    * It returns the number of instantiations added using calls to
    * Instantiate::addInstantiation(...).
    */
-  virtual uint64_t addInstantiations(Node q) { return 0; }
+  virtual uint64_t addInstantiations(InstMatch& m) { return 0; }
   /** get active score
    *
    * A heuristic value indicating how active this generator is.
@@ -102,14 +100,14 @@ class IMGenerator : protected EnvObj
  protected:
   /** send instantiation
    *
-   * This method sends instantiation, specified by m, to the parent trigger
+   * This method sends instantiation, specified by terms, 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);
+  bool sendInstantiation(std::vector<Node>& terms, InferenceId id);
   /** The parent trigger that owns this */
   Trigger* d_tparent;
   /** Reference to the state of the quantifiers engine */
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index e31153bbf..c3d3e17c0 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -282,7 +282,7 @@ void InstMatchGenerator::initialize(Node q,
 }
 
 /** get match (not modulo equality) */
-int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
+int InstMatchGenerator::getMatch(Node t, InstMatch& m)
 {
   Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
                     << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
@@ -309,7 +309,7 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
       Trace("matching-debug2")
           << "Setting " << ct << " to " << t[i] << "..." << std::endl;
       bool addToPrev = m.get(ct).isNull();
-      if (!m.set(d_qstate, ct, t[i]))
+      if (!m.set(ct, t[i]))
       {
         // match is in conflict
         Trace("matching-fail")
@@ -341,7 +341,7 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
   if (d_match_pattern.getKind() == INST_CONSTANT)
   {
     bool addToPrev = m.get(d_children_types[0]).isNull();
-    if (!m.set(d_qstate, d_children_types[0], t))
+    if (!m.set(d_children_types[0], t))
     {
       success = false;
     }
@@ -400,7 +400,7 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
     if (!t_match.isNull())
     {
       bool addToPrev = m.get(v).isNull();
-      if (!m.set(d_qstate, v, t_match))
+      if (!m.set(v, t_match))
       {
         success = false;
       }
@@ -427,8 +427,7 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
     if (success)
     {
       Trace("matching-debug2") << "Continue next " << d_next << std::endl;
-      ret_val =
-          continueNextMatch(f, m, InferenceId::QUANTIFIERS_INST_E_MATCHING);
+      ret_val = continueNextMatch(m, InferenceId::QUANTIFIERS_INST_E_MATCHING);
     }
   }
   if (ret_val < 0)
@@ -441,16 +440,15 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
   return ret_val;
 }
 
-int InstMatchGenerator::continueNextMatch(Node q,
-                                          InstMatch& m,
-                                          InferenceId id)
+int InstMatchGenerator::continueNextMatch(InstMatch& m, InferenceId id)
 {
   if( d_next!=NULL ){
-    return d_next->getNextMatch(q, m);
+    return d_next->getNextMatch(m);
   }
   if (d_active_add)
   {
-    return sendInstantiation(m, id) ? 1 : -1;
+    std::vector<Node> mc = m.get();
+    return sendInstantiation(mc, id) ? 1 : -1;
   }
   return 1;
 }
@@ -505,7 +503,7 @@ bool InstMatchGenerator::reset(Node eqc)
   return !d_curr_first_candidate.isNull();
 }
 
-int InstMatchGenerator::getNextMatch(Node f, InstMatch& m)
+int InstMatchGenerator::getNextMatch(InstMatch& m)
 {
   if( d_needsReset ){
     Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
@@ -523,7 +521,7 @@ int InstMatchGenerator::getNextMatch(Node f, InstMatch& m)
       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);
+        success = getMatch(t, m);
         if( d_independent_gen && success<0 ){
           Assert(d_eq_class.isNull() || !d_eq_class_rel.isNull());
           d_curr_exclude_match[t] = true;
@@ -549,15 +547,16 @@ int InstMatchGenerator::getNextMatch(Node f, InstMatch& m)
   return success;
 }
 
-uint64_t InstMatchGenerator::addInstantiations(Node f)
+uint64_t InstMatchGenerator::addInstantiations(InstMatch& m)
 {
   //try to add instantiation for each match produced
   uint64_t addedLemmas = 0;
-  InstMatch m( f );
-  while (getNextMatch(f, m) > 0)
+  m.resetAll();
+  while (getNextMatch(m) > 0)
   {
     if( !d_active_add ){
-      if (sendInstantiation(m, InferenceId::UNKNOWN))
+      std::vector<Node> mc = m.get();
+      if (sendInstantiation(mc, InferenceId::UNKNOWN))
       {
         addedLemmas++;
         if (d_qstate.isInConflict())
@@ -572,7 +571,7 @@ uint64_t InstMatchGenerator::addInstantiations(Node f)
         break;
       }
     }
-    m.clear();
+    m.resetAll();
   }
   //return number of lemmas added
   return addedLemmas;
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 143a29abd..56e0e8d9e 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -113,9 +113,9 @@ class InstMatchGenerator : public IMGenerator {
   /** Reset. */
   bool reset(Node eqc) override;
   /** Get the next match. */
-  int getNextMatch(Node q, InstMatch& m) override;
+  int getNextMatch(InstMatch& m) override;
   /** Add instantiations. */
-  uint64_t addInstantiations(Node q) override;
+  uint64_t addInstantiations(InstMatch& m) override;
 
   /** set active add flag (true by default)
    *
@@ -290,7 +290,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);
+  int getMatch(Node t, InstMatch& m);
   /** Initialize this generator.
    *
    * q is the quantified formula associated with this generator.
@@ -313,9 +313,7 @@ class InstMatchGenerator : public IMGenerator {
   * value >0 if active add is false).  Its return value has the same semantics
   * as getNextMatch.
   */
-  int continueNextMatch(Node q,
-                        InstMatch& m,
-                        InferenceId id);
+  int continueNextMatch(InstMatch& m, InferenceId id);
   /** Get inst match generator
    *
    * Gets the InstMatchGenerator that implements the
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index a1102feec..f0b01fe63 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -153,7 +153,7 @@ bool InstMatchGeneratorMulti::reset(Node eqc)
   return true;
 }
 
-uint64_t InstMatchGeneratorMulti::addInstantiations(Node q)
+uint64_t InstMatchGeneratorMulti::addInstantiations(InstMatch& m)
 {
   uint64_t addedLemmas = 0;
   Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
@@ -161,8 +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) > 0)
+    while (d_children[i]->getNextMatch(m) > 0)
     {
       Trace("multi-trigger-cache2")
           << "...processing new match, #lemmas = " << addedLemmas << std::endl;
@@ -171,7 +170,7 @@ uint64_t InstMatchGeneratorMulti::addInstantiations(Node q)
       {
         return addedLemmas;
       }
-      m.clear();
+      m.resetAll();
     }
   }
   return addedLemmas;
@@ -213,7 +212,8 @@ void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m,
   if (childIndex == endChildIndex)
   {
     // m is an instantiation
-    if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
+    std::vector<Node> mc = m.get();
+    if (sendInstantiation(mc, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT))
     {
       addedLemmas++;
       Trace("multi-trigger-cache-debug")
@@ -233,7 +233,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m,
       for (std::pair<const Node, InstMatchTrie>& d : tr->d_data)
       {
         // try to set
-        if (!m.set(qs, curr_index, d.first))
+        if (!m.set(curr_index, d.first))
         {
           continue;
         }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
index f55670449..4b03f4e27 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
@@ -52,7 +52,7 @@ class InstMatchGeneratorMulti : public IMGenerator
   /** Reset. */
   bool reset(Node eqc) override;
   /** Add instantiations. */
-  uint64_t addInstantiations(Node q) override;
+  uint64_t addInstantiations(InstMatch& m) override;
 
  private:
   /** process new match
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 d847cffc3..41933f0cf 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -135,7 +135,7 @@ bool InstMatchGeneratorMultiLinear::reset(Node eqc)
   return resetChildren() > 0;
 }
 
-int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m)
+int InstMatchGeneratorMultiLinear::getNextMatch(InstMatch& m)
 {
   Trace("multi-trigger-linear-debug")
       << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
@@ -153,7 +153,7 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m)
       << std::endl;
   Assert(d_next != nullptr);
   int ret_val =
-      continueNextMatch(q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL);
+      continueNextMatch(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 d7122bd5d..9067c689f 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
@@ -72,7 +72,7 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator
   /** Reset. */
   bool reset(Node eqc) override;
   /** Get the next match. */
-  int getNextMatch(Node q, InstMatch& m) override;
+  int getNextMatch(InstMatch& m) override;
 
  protected:
   /** reset the children of this generator */
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index b227df186..dd22f9a06 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -72,7 +72,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Env& env,
 }
 
 void InstMatchGeneratorSimple::resetInstantiationRound() {}
-uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
+uint64_t InstMatchGeneratorSimple::addInstantiations(InstMatch& m)
 {
   uint64_t addedLemmas = 0;
   TNodeTrie* tat;
@@ -98,7 +98,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
         {
           if (t.first != r)
           {
-            InstMatch m(q);
+            m.resetAll();
             addInstantiations(m, addedLemmas, 0, &(t.second));
             if (d_qstate.isInConflict())
             {
@@ -115,7 +115,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
       << d_eqc << std::endl;
   if (tat && !d_qstate.isInConflict())
   {
-    InstMatch m(q);
+    m.resetAll();
     addInstantiations(m, addedLemmas, 0, tat);
   }
   return addedLemmas;
@@ -134,6 +134,8 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     TNode t = tat->getData();
     Trace("simple-trigger") << "Actual term is " << t << std::endl;
     // convert to actual used terms
+    std::vector<Node> terms;
+    terms.resize(d_quant[0].getNumChildren());
     for (const auto& v : d_var_num)
     {
       if (v.second >= 0)
@@ -141,15 +143,17 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
         Assert(v.first < t.getNumChildren());
         Trace("simple-trigger")
             << "...set " << v.second << " " << t[v.first] << std::endl;
-        m.setValue(v.second, t[v.first]);
+        terms[v.second] = t[v.first];
       }
     }
     // we do not need the trigger parent for simple triggers (no post-processing
     // required)
-    if (sendInstantiation(m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
+    if (sendInstantiation(terms,
+                          InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE))
     {
       addedLemmas++;
-      Trace("simple-trigger") << "-> Produced instantiation " << m << std::endl;
+      Trace("simple-trigger")
+          << "-> Produced instantiation " << terms << std::endl;
     }
     return;
   }
@@ -161,18 +165,21 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
       for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
       {
         Node t = tt.first;
-        Node prev = m.get(v);
         // using representatives, just check if equal
         Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
-        if (prev.isNull() || prev == t)
+        bool wasSet = !m.get(v).isNull();
+        if (!m.set(v, t))
         {
-          m.setValue(v, t);
-          addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second));
-          m.setValue(v, prev);
-          if (d_qstate.isInConflict())
-          {
-            break;
-          }
+          continue;
+        }
+        addInstantiations(m, addedLemmas, argIndex + 1, &(tt.second));
+        if (!wasSet)
+        {
+          m.reset(v);
+        }
+        if (d_qstate.isInConflict())
+        {
+          break;
         }
       }
       return;
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
index 451bc766a..7c8a80669 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
@@ -52,7 +52,7 @@ class InstMatchGeneratorSimple : public IMGenerator
   /** Reset instantiation round. */
   void resetInstantiationRound() override;
   /** Add instantiations. */
-  uint64_t addInstantiations(Node q) override;
+  uint64_t addInstantiations(InstMatch& m) override;
   /** Get active score. */
   int getActiveScore() override;
 
diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp
index c3b9a346b..7b1796090 100644
--- a/src/theory/quantifiers/ematching/relational_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp
@@ -63,7 +63,7 @@ bool RelationalMatchGenerator::reset(Node eqc)
   return true;
 }
 
-int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m)
+int RelationalMatchGenerator::getNextMatch(InstMatch& m)
 {
   Trace("relational-match-gen") << "getNextMatch, rel match gen" << std::endl;
   // try (up to) two different terms
@@ -100,11 +100,11 @@ int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m)
     d_counter++;
     Trace("relational-match-gen")
         << "...try set " << s << " for " << checkPol << std::endl;
-    if (m.set(d_qstate, d_vindex, s))
+    if (m.set(d_vindex, s))
     {
       Trace("relational-match-gen") << "...success" << std::endl;
       int ret = continueNextMatch(
-          q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_RELATIONAL);
+          m, InferenceId::QUANTIFIERS_INST_E_MATCHING_RELATIONAL);
       if (ret > 0)
       {
         Trace("relational-match-gen") << "...returned " << ret << std::endl;
diff --git a/src/theory/quantifiers/ematching/relational_match_generator.h b/src/theory/quantifiers/ematching/relational_match_generator.h
index c6119276b..15c38c36e 100644
--- a/src/theory/quantifiers/ematching/relational_match_generator.h
+++ b/src/theory/quantifiers/ematching/relational_match_generator.h
@@ -61,7 +61,7 @@ class RelationalMatchGenerator : public InstMatchGenerator
   /** Reset */
   bool reset(Node eqc) override;
   /** Get the next match. */
-  int getNextMatch(Node q, InstMatch& m) override;
+  int getNextMatch(InstMatch& m) override;
 
  private:
   /** the variable */
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index c0cd6dc53..e441d0616 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -50,7 +50,13 @@ Trigger::Trigger(Env& env,
                  TermRegistry& tr,
                  Node q,
                  std::vector<Node>& nodes)
-    : EnvObj(env), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_quant(q)
+    : EnvObj(env),
+      d_qstate(qs),
+      d_qim(qim),
+      d_qreg(qr),
+      d_treg(tr),
+      d_quant(q),
+      d_instMatch(env, qs, tr, q)
 {
   // We must ensure that the ground subterms of the trigger have been
   // preprocessed.
@@ -159,7 +165,7 @@ uint64_t Trigger::addInstantiations()
       }
     }
   }
-  uint64_t addedLemmas = d_mg->addInstantiations(d_quant);
+  uint64_t addedLemmas = d_mg->addInstantiations(d_instMatch);
   if (TraceIsOn("inst-trigger"))
   {
     if (addedLemmas > 0)
@@ -176,11 +182,6 @@ bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
   return d_qim.getInstantiate()->addInstantiation(d_quant, m, id, d_trNode);
 }
 
-bool Trigger::sendInstantiation(InstMatch& m, InferenceId id)
-{
-  return sendInstantiation(m.get(), id);
-}
-
 int Trigger::getActiveScore() { return d_mg->getActiveScore(); }
 
 Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 77f567a3c..a67953821 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -21,24 +21,25 @@
 #include "expr/node.h"
 #include "smt/env_obj.h"
 #include "theory/inference_id.h"
+#include "theory/quantifiers/inst_match.h"
 
 namespace cvc5::internal {
 namespace theory {
 
-class QuantifiersEngine;
 class Valuation;
 
 namespace quantifiers {
+
 class QuantifiersState;
 class QuantifiersInferenceManager;
 class QuantifiersRegistry;
 class TermRegistry;
-class InstMatch;
 
 namespace inst {
 
 class IMGenerator;
 class InstMatchGenerator;
+
 /** A collection of nodes representing a trigger.
  *
  * This class encapsulates all implementations of E-matching in cvc5.
@@ -161,8 +162,6 @@ class Trigger : protected EnvObj
    * Instantiate::addInstantiation(...).
    */
   virtual bool sendInstantiation(std::vector<Node>& m, InferenceId id);
-  /** inst match version, calls the above method */
-  bool sendInstantiation(InstMatch& m, InferenceId id);
   /**
    * Ensure that all ground subterms of n have been preprocessed. This makes
    * calls to the provided valuation to obtain the preprocessed form of these
@@ -216,6 +215,11 @@ class Trigger : protected EnvObj
   * algorithm associated with this trigger.
   */
   IMGenerator* d_mg;
+  /**
+   * An instantiation match, for building instantiation terms and doing
+   * incremental entailment checking.
+   */
+  InstMatch d_instMatch;
 }; /* class Trigger */
 
 }  // namespace inst
diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
index 03f394ce6..81a980046 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -43,7 +43,7 @@ bool VarMatchGeneratorTermSubs::reset(Node eqc)
   return true;
 }
 
-int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m)
+int VarMatchGeneratorTermSubs::getNextMatch(InstMatch& m)
 {
   size_t index = d_children_types[0];
   int ret_val = -1;
@@ -59,14 +59,14 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m)
     d_eq_class = Node::null();
     // if( s.getType().isSubtypeOf( d_var_type ) ){
     d_rm_prev = m.get(index).isNull();
-    if (!m.set(d_qstate, index, s))
+    if (!m.set(index, s))
     {
       return -1;
     }
     else
     {
       ret_val = continueNextMatch(
-          q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN);
+          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 0852824bc..daaa04c01 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.h
+++ b/src/theory/quantifiers/ematching/var_match_generator.h
@@ -37,7 +37,7 @@ class VarMatchGeneratorTermSubs : public InstMatchGenerator
   /** Reset */
   bool reset(Node eqc) override;
   /** Get the next match. */
-  int getNextMatch(Node q, InstMatch& m) override;
+  int getNextMatch(InstMatch& m) override;
 
  private:
   /** variable we are matching (x in the example x+1). */
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 5445f955f..e9f41e8e7 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -15,13 +15,16 @@
 
 #include "theory/quantifiers/inst_match.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_registry.h"
 
 namespace cvc5::internal {
 namespace theory {
 namespace quantifiers {
 
-InstMatch::InstMatch(TNode q) : d_quant(q)
+InstMatch::InstMatch(Env& env, QuantifiersState& qs, TermRegistry& tr, TNode q)
+    : EnvObj(env), d_qs(qs), d_tr(tr), d_quant(q)
 {
   d_vals.resize(q[0].getNumChildren());
   Assert(!d_vals.empty());
@@ -29,16 +32,6 @@ InstMatch::InstMatch(TNode q) : d_quant(q)
   Assert(d_vals[0].isNull());
 }
 
-void InstMatch::add(InstMatch& m)
-{
-  for (unsigned i = 0, size = d_vals.size(); i < size; i++)
-  {
-    if( d_vals[i].isNull() ){
-      d_vals[i] = m.d_vals[i];
-    }
-  }
-}
-
 void InstMatch::debugPrint( const char* c ){
   for (unsigned i = 0, size = d_vals.size(); i < size; i++)
   {
@@ -91,8 +84,10 @@ bool InstMatch::empty() const
   return true;
 }
 
-void InstMatch::clear() {
-  for( unsigned i=0; i<d_vals.size(); i++ ){
+void InstMatch::resetAll()
+{
+  for (size_t i = 0, nvals = d_vals.size(); i < nvals; i++)
+  {
     d_vals[i] = Node::null();
   }
 }
@@ -103,19 +98,13 @@ Node InstMatch::get(size_t i) const
   return d_vals[i];
 }
 
-void InstMatch::setValue(size_t i, TNode n)
-{
-  Assert(i < d_vals.size());
-  d_vals[i] = n;
-}
-
-bool InstMatch::set(QuantifiersState& qs, size_t i, TNode n)
+bool InstMatch::set(size_t i, TNode n)
 {
   Assert(i < d_vals.size());
   if (!d_vals[i].isNull())
   {
     // if they are equal, we do nothing
-    return qs.areEqual(d_vals[i], n);
+    return d_qs.areEqual(d_vals[i], n);
   }
   // otherwise, we update the value
   d_vals[i] = n;
@@ -128,7 +117,7 @@ void InstMatch::reset(size_t i)
   d_vals[i] = Node::null();
 }
 
-std::vector<Node>& InstMatch::get() { return d_vals; }
+const std::vector<Node>& InstMatch::get() const { return d_vals; }
 
 }  // namespace quantifiers
 }  // namespace theory
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index d31d638ee..d6344860a 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -21,12 +21,14 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5::internal {
 namespace theory {
 namespace quantifiers {
 
 class QuantifiersState;
+class TermRegistry;
 
 /** Inst match
  *
@@ -37,41 +39,44 @@ class QuantifiersState;
  * The values of d_vals may be null, which indicate that the field has
  * yet to be initialized.
  */
-class InstMatch {
+class InstMatch : protected EnvObj
+{
  public:
-  InstMatch(TNode q);
-  /** add match m
-   *
-   * This adds the initialized fields of m to this match for each field that is
-   * not already initialized in this match.
-   */
-  void add(InstMatch& m);
+  InstMatch(Env& env, QuantifiersState& qs, TermRegistry& tr, TNode q);
   /** is this complete, i.e. are all fields non-null? */
   bool isComplete() const;
   /** is this empty, i.e. are all fields the null node? */
   bool empty() const;
-  /** clear the instantiation, i.e. set all fields to the null node */
-  void clear();
+  /**
+   * Clear the instantiation, i.e. set all fields to the null node.
+   */
+  void resetAll();
   /** debug print method */
   void debugPrint(const char* c);
   /** to stream */
   void toStream(std::ostream& out) const;
   /** get the i^th term in the instantiation */
   Node get(size_t i) const;
-  /** set/overwrites the i^th field in the instantiation with n */
-  void setValue(size_t i, TNode n);
   /** set the i^th term in the instantiation to n
    *
-   * This method returns true if the i^th field was previously uninitialized,
-   * or is equivalent to n modulo the equalities given by q.
+   * If the d_vals[i] is not null, then this return true iff it is equal to
+   * n based on the quantifiers state.
+   *
+   * If the d_vals[i] is null, then this sets d_vals[i] to n.
+   */
+  bool set(size_t i, TNode n);
+  /**
+   * Resets index i, which sets d_vals[i] to null.
    */
-  bool set(QuantifiersState& qs, size_t i, TNode n);
-  /** Resets index i */
   void reset(size_t i);
   /** Get the values */
-  std::vector<Node>& get();
+  const std::vector<Node>& get() const;
 
  private:
+  /** Reference to the state */
+  QuantifiersState& d_qs;
+  /** Reference to the term registry */
+  TermRegistry& d_tr;
   /**
    * Ground terms for each variable of the quantified formula, in order.
    * Null nodes indicate the variable has not been set.