Simplify interface to instantiate (#5926)

Does not support InstMatch interfaces anymore, which are spurious.

11 files changed, 107 insertions, 247 deletions

diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 4c606a273..875c74aa4 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -368,7 +368,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
   else
   {
     // do not run higher-order matching
-    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
+    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
   }
 }
 
@@ -381,7 +381,7 @@ 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->getInstantiate()->addInstantiation(d_quant, m);
+    return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
   }
   else
   {
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index f03d1cf20..b5c81b766 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -19,7 +19,7 @@
 
 #include <map>
 #include "expr/node_trie.h"
-#include "theory/quantifiers/inst_match_trie.h"
+#include "theory/quantifiers/inst_match.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index 4f393bc4f..e4fb3fc41 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -191,7 +191,8 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
                                               uint64_t& addedLemmas)
 {
   // see if these produce new matches
-  d_children_trie[fromChildIndex].addInstMatch(qe->getState(), d_quant, m);
+  d_children_trie[fromChildIndex].addInstMatch(
+      qe->getState(), 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
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
index b68d362cc..2007e652d 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
@@ -21,6 +21,7 @@
 #include <vector>
 #include "expr/node_trie.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
+#include "theory/quantifiers/inst_match_trie.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index b5ef7792d..a46eb12ce 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -140,7 +140,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     }
     // we do not need the trigger parent for simple triggers (no post-processing
     // required)
-    if (qe->getInstantiate()->addInstantiation(d_quant, m))
+    if (qe->getInstantiate()->addInstantiation(d_quant, m.d_vals))
     {
       addedLemmas++;
       Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index ac43d3bc9..8d9cfd3a3 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -143,7 +143,7 @@ uint64_t Trigger::addInstantiations()
 
 bool Trigger::sendInstantiation(InstMatch& m)
 {
-  return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
+  return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
 }
 
 bool Trigger::mkTriggerTerms(Node q,
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 1c0a74013..4ca820709 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -291,7 +291,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           triedLemmas++;
           //add as instantiation
-          if (inst->addInstantiation(f, m, true))
+          if (inst->addInstantiation(f, m.d_vals, true))
           {
             addedLemmas++;
             if (d_qstate.isInConflict())
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index a42823845..993fad90a 100644
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Implementation of inst match class
+ ** \brief Implementation of inst match trie class
  **/
 
 #include "theory/quantifiers/inst_match_trie.h"
@@ -26,9 +26,19 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
+bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
+                                    Node q,
+                                    const std::vector<Node>& m,
+                                    bool modEq,
+                                    ImtIndexOrder* imtio,
+                                    unsigned index)
+{
+  return !addInstMatch(qs, q, m, modEq, imtio, true, index);
+}
+
 bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
                                  Node f,
-                                 std::vector<Node>& m,
+                                 const std::vector<Node>& m,
                                  bool modEq,
                                  ImtIndexOrder* imtio,
                                  bool onlyExist,
@@ -84,7 +94,7 @@ bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
 }
 
 bool InstMatchTrie::removeInstMatch(Node q,
-                                    std::vector<Node>& m,
+                                    const std::vector<Node>& m,
                                     ImtIndexOrder* imtio,
                                     unsigned index)
 {
@@ -108,49 +118,27 @@ bool InstMatchTrie::removeInstMatch(Node q,
 
 void InstMatchTrie::print(std::ostream& out,
                           Node q,
-                          std::vector<TNode>& terms,
-                          bool useActive,
-                          std::vector<Node>& active) const
+                          std::vector<TNode>& terms) const
 {
   if (terms.size() == q[0].getNumChildren())
   {
-    bool print;
-    if (useActive)
+    out << "  ( ";
+    for (unsigned i = 0, size = terms.size(); i < size; i++)
     {
-      if (hasInstLemma())
-      {
-        Node lem = getInstLemma();
-        print = std::find(active.begin(), active.end(), lem) != active.end();
-      }
-      else
+      if (i > 0)
       {
-        print = false;
+        out << ", ";
       }
+      out << terms[i];
     }
-    else
-    {
-      print = true;
-    }
-    if (print)
-    {
-      out << "  ( ";
-      for (unsigned i = 0, size = terms.size(); i < size; i++)
-      {
-        if (i > 0)
-        {
-          out << ", ";
-        }
-        out << terms[i];
-      }
-      out << " )" << std::endl;
-    }
+    out << " )" << std::endl;
   }
   else
   {
     for (const std::pair<const Node, InstMatchTrie>& d : d_data)
     {
       terms.push_back(d.first);
-      d.second.print(out, q, terms, useActive, active);
+      d.second.print(out, q, terms);
       terms.pop_back();
     }
   }
@@ -182,6 +170,14 @@ void InstMatchTrie::getInstantiations(Node q,
   }
 }
 
+void InstMatchTrie::clear() { d_data.clear(); }
+
+void InstMatchTrie::print(std::ostream& out, Node q) const
+{
+  std::vector<TNode> terms;
+  print(out, q, terms);
+}
+
 CDInstMatchTrie::~CDInstMatchTrie()
 {
   for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
@@ -192,9 +188,18 @@ CDInstMatchTrie::~CDInstMatchTrie()
   d_data.clear();
 }
 
+bool CDInstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
+                                      Node q,
+                                      const std::vector<Node>& m,
+                                      bool modEq,
+                                      unsigned index)
+{
+  return !addInstMatch(qs, q, m, modEq, index, true);
+}
+
 bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
                                    Node f,
-                                   std::vector<Node>& m,
+                                   const std::vector<Node>& m,
                                    bool modEq,
                                    unsigned index,
                                    bool onlyExist)
@@ -262,7 +267,7 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
 }
 
 bool CDInstMatchTrie::removeInstMatch(Node q,
-                                      std::vector<Node>& m,
+                                      const std::vector<Node>& m,
                                       unsigned index)
 {
   if (index == q[0].getNumChildren())
@@ -284,48 +289,26 @@ bool CDInstMatchTrie::removeInstMatch(Node q,
 
 void CDInstMatchTrie::print(std::ostream& out,
                             Node q,
-                            std::vector<TNode>& terms,
-                            bool useActive,
-                            std::vector<Node>& active) const
+                            std::vector<TNode>& terms) const
 {
   if (d_valid.get())
   {
     if (terms.size() == q[0].getNumChildren())
     {
-      bool print;
-      if (useActive)
-      {
-        if (hasInstLemma())
-        {
-          Node lem = getInstLemma();
-          print = std::find(active.begin(), active.end(), lem) != active.end();
-        }
-        else
-        {
-          print = false;
-        }
-      }
-      else
-      {
-        print = true;
-      }
-      if (print)
+      out << "  ( ";
+      for (unsigned i = 0; i < terms.size(); i++)
       {
-        out << "  ( ";
-        for (unsigned i = 0; i < terms.size(); i++)
-        {
-          if (i > 0) out << " ";
-          out << terms[i];
-        }
-        out << " )" << std::endl;
+        if (i > 0) out << " ";
+        out << terms[i];
       }
+      out << " )" << std::endl;
     }
     else
     {
       for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
       {
         terms.push_back(d.first);
-        d.second->print(out, q, terms, useActive, active);
+        d.second->print(out, q, terms);
         terms.pop_back();
       }
     }
@@ -362,6 +345,28 @@ void CDInstMatchTrie::getInstantiations(Node q,
   }
 }
 
+void CDInstMatchTrie::print(std::ostream& out, Node q) const
+{
+  std::vector<TNode> terms;
+  print(out, q, terms);
+}
+
+bool InstMatchTrieOrdered::addInstMatch(quantifiers::QuantifiersState& qs,
+                                        Node q,
+                                        const std::vector<Node>& m,
+                                        bool modEq)
+{
+  return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
+}
+
+bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs,
+                                           Node q,
+                                           const std::vector<Node>& m,
+                                           bool modEq)
+{
+  return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
+}
+
 } /* CVC4::theory::inst namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index c8d0214b6..c45badc38 100644
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief inst match class
+ ** \brief inst match trie class
  **/
 
 #include "cvc4_private.h"
@@ -22,14 +22,13 @@
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "expr/node.h"
-#include "theory/quantifiers/inst_match.h"
 
 namespace CVC4 {
 namespace theory {
 
 class QuantifiersEngine;
 
-namespace {
+namespace quantifiers {
 class QuantifiersState;
 }
 
@@ -65,23 +64,10 @@ class InstMatchTrie
    */
   bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
-                       InstMatch& m,
+                       const std::vector<Node>& m,
                        bool modEq = false,
-                       ImtIndexOrder* imtio = NULL,
-                       unsigned index = 0)
-  {
-    return !addInstMatch(qs, q, m, modEq, imtio, true, index);
-  }
-  /** exists inst match, vector version */
-  bool existsInstMatch(quantifiers::QuantifiersState& qs,
-                       Node q,
-                       std::vector<Node>& m,
-                       bool modEq = false,
-                       ImtIndexOrder* imtio = NULL,
-                       unsigned index = 0)
-  {
-    return !addInstMatch(qs, q, m, modEq, imtio, true, index);
-  }
+                       ImtIndexOrder* imtio = nullptr,
+                       unsigned index = 0);
   /** add inst match
    *
    * This method adds (the suffix of) m starting at the given index to this
@@ -91,21 +77,10 @@ class InstMatchTrie
    * equalities in the equality engine of qs.
    */
   bool addInstMatch(quantifiers::QuantifiersState& qs,
-                    Node q,
-                    InstMatch& m,
-                    bool modEq = false,
-                    ImtIndexOrder* imtio = NULL,
-                    bool onlyExist = false,
-                    unsigned index = 0)
-  {
-    return addInstMatch(qs, q, m.d_vals, modEq, imtio, onlyExist, index);
-  }
-  /** add inst match, vector version */
-  bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node f,
-                    std::vector<Node>& m,
+                    const std::vector<Node>& m,
                     bool modEq = false,
-                    ImtIndexOrder* imtio = NULL,
+                    ImtIndexOrder* imtio = nullptr,
                     bool onlyExist = false,
                     unsigned index = 0);
   /** remove inst match
@@ -115,8 +90,8 @@ class InstMatchTrie
    * The domain of m is the bound variables of quantified formula q.
    */
   bool removeInstMatch(Node f,
-                       std::vector<Node>& m,
-                       ImtIndexOrder* imtio = NULL,
+                       const std::vector<Node>& m,
+                       ImtIndexOrder* imtio = nullptr,
                        unsigned index = 0);
   /**
    * Adds the instantiations for q into insts.
@@ -124,16 +99,9 @@ class InstMatchTrie
   void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
 
   /** clear the data of this class */
-  void clear() { d_data.clear(); }
+  void clear();
   /** print this class */
-  void print(std::ostream& out,
-             Node q,
-             bool useActive,
-             std::vector<Node>& active) const
-  {
-    std::vector<TNode> terms;
-    print(out, q, terms, useActive, active);
-  }
+  void print(std::ostream& out, Node q) const;
   /** the data */
   std::map<Node, InstMatchTrie> d_data;
 
@@ -145,21 +113,7 @@ class InstMatchTrie
   /** helper for print
    * terms accumulates the path we are on in the trie.
    */
-  void print(std::ostream& out,
-             Node q,
-             std::vector<TNode>& terms,
-             bool useActive,
-             std::vector<Node>& active) const;
-  /** set instantiation lemma at this node in the trie */
-  void setInstLemma(Node n)
-  {
-    d_data.clear();
-    d_data[n].clear();
-  }
-  /** does this node of the trie store an instantiation lemma? */
-  bool hasInstLemma() const { return !d_data.empty(); }
-  /** get the instantiation lemma stored in this node of the trie */
-  Node getInstLemma() const { return d_data.begin()->first; }
+  void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
 };
 
 /** trie for InstMatch objects
@@ -183,21 +137,9 @@ class CDInstMatchTrie
    */
   bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
-                       InstMatch& m,
+                       const std::vector<Node>& m,
                        bool modEq = false,
-                       unsigned index = 0)
-  {
-    return !addInstMatch(qs, q, m, modEq, index, true);
-  }
-  /** exists inst match, vector version */
-  bool existsInstMatch(quantifiers::QuantifiersState& qs,
-                       Node q,
-                       std::vector<Node>& m,
-                       bool modEq = false,
-                       unsigned index = 0)
-  {
-    return !addInstMatch(qs, q, m, modEq, index, true);
-  }
+                       unsigned index = 0);
   /** add inst match
    *
    * This method adds (the suffix of) m starting at the given index to this
@@ -209,17 +151,7 @@ class CDInstMatchTrie
    */
   bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node q,
-                    InstMatch& m,
-                    bool modEq = false,
-                    unsigned index = 0,
-                    bool onlyExist = false)
-  {
-    return addInstMatch(qs, q, m.d_vals, modEq, index, onlyExist);
-  }
-  /** add inst match, vector version */
-  bool addInstMatch(quantifiers::QuantifiersState& qs,
-                    Node q,
-                    std::vector<Node>& m,
+                    const std::vector<Node>& m,
                     bool modEq = false,
                     unsigned index = 0,
                     bool onlyExist = false);
@@ -229,67 +161,28 @@ class CDInstMatchTrie
    * It returns true if and only if this entry existed in this trie.
    * The domain of m is the bound variables of quantified formula q.
    */
-  bool removeInstMatch(Node q, std::vector<Node>& m, unsigned index = 0);
+  bool removeInstMatch(Node q, const std::vector<Node>& m, unsigned index = 0);
   /**
    * Adds the instantiations for q into insts.
    */
   void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
 
   /** print this class */
-  void print(std::ostream& out,
-             Node q,
-             bool useActive,
-             std::vector<Node>& active) const
-  {
-    std::vector<TNode> terms;
-    print(out, q, terms, useActive, active);
-  }
+  void print(std::ostream& out, Node q) const;
 
  private:
   /** Helper for getInstantiations.*/
   void getInstantiations(Node q,
                          std::vector<std::vector<Node>>& insts,
                          std::vector<Node>& terms) const;
+  /** helper for print
+   * terms accumulates the path we are on in the trie.
+   */
+  void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
   /** the data */
   std::map<Node, CDInstMatchTrie*> d_data;
   /** is valid */
   context::CDO<bool> d_valid;
-  /** helper for print
-   * terms accumulates the path we are on in the trie.
-   */
-  void print(std::ostream& out,
-             Node q,
-             std::vector<TNode>& terms,
-             bool useActive,
-             std::vector<Node>& active) const;
-  /** helper for get instantiations
-   * terms accumulates the path we are on in the trie.
-   */
-  void getInstantiations(std::vector<Node>& insts,
-                         Node q,
-                         std::vector<Node>& terms,
-                         QuantifiersEngine* qe,
-                         bool useActive,
-                         std::vector<Node>& active) const;
-  /** helper for get explanation for inst lemma
-   * terms accumulates the path we are on in the trie.
-   */
-  void getExplanationForInstLemmas(
-      Node q,
-      std::vector<Node>& terms,
-      const std::vector<Node>& lems,
-      std::map<Node, Node>& quant,
-      std::map<Node, std::vector<Node> >& tvec) const;
-  /** set instantiation lemma at this node in the trie */
-  void setInstLemma(Node n)
-  {
-    d_data.clear();
-    d_data[n] = NULL;
-  }
-  /** does this node of the trie store an instantiation lemma? */
-  bool hasInstLemma() const { return !d_data.empty(); }
-  /** get the instantiation lemma stored in this node of the trie */
-  Node getInstLemma() const { return d_data.begin()->first; }
 };
 
 /** inst match trie ordered
@@ -314,11 +207,8 @@ class InstMatchTrieOrdered
    */
   bool addInstMatch(quantifiers::QuantifiersState& qs,
                     Node q,
-                    InstMatch& m,
-                    bool modEq = false)
-  {
-    return d_imt.addInstMatch(qs, q, m, modEq, d_imtio);
-  }
+                    const std::vector<Node>& m,
+                    bool modEq = false);
   /** returns true if this trie contains m
    *
    * This method returns true if the match m exists in this
@@ -327,11 +217,8 @@ class InstMatchTrieOrdered
    */
   bool existsInstMatch(quantifiers::QuantifiersState& qs,
                        Node q,
-                       InstMatch& m,
-                       bool modEq = false)
-  {
-    return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio);
-  }
+                       const std::vector<Node>& m,
+                       bool modEq = false);
 
  private:
   /** the ordering */
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 729dd6100..232499fbf 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -97,13 +97,6 @@ void Instantiate::addRewriter(InstantiationRewriter* ir)
 }
 
 bool Instantiate::addInstantiation(
-    Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts)
-{
-  Assert(q[0].getNumChildren() == m.d_vals.size());
-  return addInstantiation(q, m.d_vals, mkRep, modEq, doVts);
-}
-
-bool Instantiate::addInstantiation(
     Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts)
 {
   // For resource-limiting (also does a time check).
@@ -142,7 +135,7 @@ bool Instantiate::addInstantiation(
     }
 #ifdef CVC4_ASSERTIONS
     bool bad_inst = false;
-    if (quantifiers::TermUtil::containsUninterpretedConstant(terms[i]))
+    if (TermUtil::containsUninterpretedConstant(terms[i]))
     {
       Trace("inst") << "***& inst contains uninterpreted constant : "
                     << terms[i] << std::endl;
@@ -157,7 +150,7 @@ bool Instantiate::addInstantiation(
     }
     else if (options::cegqi())
     {
-      Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
+      Node icf = TermUtil::getInstConstAttr(terms[i]);
       if (!icf.isNull())
       {
         if (icf == q)
@@ -254,7 +247,7 @@ bool Instantiate::addInstantiation(
   Node body = getInstantiation(q, d_qreg.d_vars[q], terms, doVts, pfTmp.get());
   Node orig_body = body;
   // now preprocess, storing the trust node for the rewrite
-  TrustNode tpBody = quantifiers::QuantifiersRewriter::preprocess(body, true);
+  TrustNode tpBody = QuantifiersRewriter::preprocess(body, true);
   if (!tpBody.isNull())
   {
     Assert(tpBody.getKind() == TrustNodeKind::REWRITE);
@@ -462,13 +455,6 @@ Node Instantiate::getInstantiation(Node q,
   return body;
 }
 
-Node Instantiate::getInstantiation(Node q, InstMatch& m, bool doVts)
-{
-  Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
-  Assert(m.d_vals.size() == q[0].getNumChildren());
-  return getInstantiation(q, d_qreg.d_vars[q], m.d_vals, doVts);
-}
-
 Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
 {
   Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 4188311ec..c9911785f 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -120,7 +120,7 @@ class Instantiate : public QuantifiersUtil
   /** do instantiation specified by m
    *
    * This function returns true if the instantiation lemma for quantified
-   * formula q for the substitution specified by m is successfully enqueued
+   * formula q for the substitution specified by terms is successfully enqueued
    * via a call to QuantifiersInferenceManager::addPendingLemma.
    *   mkRep : whether to take the representatives of the terms in the range of
    *           the substitution m,
@@ -142,25 +142,10 @@ class Instantiate : public QuantifiersUtil
    *
    */
   bool addInstantiation(Node q,
-                        InstMatch& m,
-                        bool mkRep = false,
-                        bool modEq = false,
-                        bool doVts = false);
-  /** add instantiation
-   *
-   * Same as above, but the substitution we are considering maps the variables
-   * of q to the vector terms, in order.
-   */
-  bool addInstantiation(Node q,
                         std::vector<Node>& terms,
                         bool mkRep = false,
                         bool modEq = false,
                         bool doVts = false);
-  /** remove pending instantiation
-   *
-   * Removes the instantiation lemma lem from the instantiation trie.
-   */
-  bool removeInstantiation(Node q, Node lem, std::vector<Node>& terms);
   /** record instantiation
    *
    * Explicitly record that q has been instantiated with terms. This is the
@@ -196,11 +181,6 @@ class Instantiate : public QuantifiersUtil
                         LazyCDProof* pf = nullptr);
   /** get instantiation
    *
-   * Same as above, but with vars/terms specified by InstMatch m.
-   */
-  Node getInstantiation(Node q, InstMatch& m, bool doVts = false);
-  /** get instantiation
-   *
    * Same as above but with vars equal to the bound variables of q.
    */
   Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false);