(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5814)

This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).

Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.

14 files changed, 188 insertions, 254 deletions

diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml
index db2f3d6c9..1f27326a0 100644
--- a/src/options/printer_options.toml
+++ b/src/options/printer_options.toml
@@ -43,3 +43,26 @@ header = "options/printer_options.h"
   type       = "bool"
   default    = "false"
   help       = "print (binary) application chains in a flattened way, e.g. (a b c) rather than ((a b) c)"
+
+[[option]]
+  name       = "printInstMode"
+  category   = "regular"
+  long       = "print-inst=MODE"
+  type       = "PrintInstMode"
+  default    = "LIST"
+  help       = "print format for printing instantiations"
+  help_mode  = "Print format for printing instantiations."
+[[option.mode.LIST]]
+  name = "list"
+  help = "Print the list of instantiations per quantified formula, when non-empty."
+[[option.mode.NUM]]
+  name = "num"
+  help = "Print the total number of instantiations per quantified formula, when non-zero."
+
+[[option]]
+  name       = "printInstFull"
+  category   = "regular"
+  long       = "print-inst-full"
+  type       = "bool"
+  default    = "false"
+  help       = "print instantiations for formulas that do not have given identifiers"
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index d3b3502fc..4b98cb84d 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1889,29 +1889,6 @@ header = "options/quantifiers_options.h"
 ### Output options
 
 [[option]]
-  name       = "printInstMode"
-  category   = "regular"
-  long       = "print-inst=MODE"
-  type       = "PrintInstMode"
-  default    = "LIST"
-  help       = "print format for printing instantiations"
-  help_mode  = "Print format for printing instantiations."
-[[option.mode.LIST]]
-  name = "list"
-  help = "Print the list of instantiations per quantified formula, when non-empty."
-[[option.mode.NUM]]
-  name = "num"
-  help = "Print the total number of instantiations per quantified formula, when non-zero."
-
-[[option]]
-  name       = "printInstFull"
-  category   = "regular"
-  long       = "print-inst-full"
-  type       = "bool"
-  default    = "false"
-  help       = "print instantiations for formulas that do not have given identifiers"
-
-[[option]]
   name       = "debugInst"
   category   = "regular"
   long       = "debug-inst"
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 4636cf17a..d1d86b5e0 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -19,6 +19,7 @@
 #include "smt/smt_solver.h"
 #include "theory/quantifiers/cegqi/nested_qe.h"
 #include "theory/quantifiers/extended_rewrite.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
@@ -58,6 +59,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
   Assert(te != nullptr);
   te->setUserAttribute(
       doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
+  QuantifiersEngine* qe = te->getQuantifiersEngine();
   n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
   n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr);
   std::vector<Node> children;
@@ -88,7 +90,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
     // that the (single) quantified formula is preprocessed, rewritten
     // version of the input quantified formula q.
     std::vector<Node> inst_qs;
-    te->getInstantiatedQuantifiedFormulas(inst_qs);
+    qe->getInstantiatedQuantifiedFormulas(inst_qs);
     Assert(inst_qs.size() <= 1);
     Node ret;
     if (inst_qs.size() == 1)
@@ -98,7 +100,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
       Trace("smt-qe") << "Get qe based on preprocessed quantified formula "
                       << topq << std::endl;
       std::vector<std::vector<Node>> insts;
-      te->getInstantiationTermVectors(topq, insts);
+      qe->getInstantiationTermVectors(topq, insts);
       std::vector<Node> vars(ne[0].begin(), ne[0].end());
       std::vector<Node> conjs;
       // apply the instantiation on the original body
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6f775f6b5..19fa8dc34 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -53,10 +53,12 @@
 #include "smt/smt_engine_stats.h"
 #include "smt/smt_solver.h"
 #include "smt/sygus_solver.h"
+#include "theory/quantifiers/instantiation_list.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 #include "theory/theory_engine.h"
+#include "theory/quantifiers_engine.h"
 #include "util/random.h"
 #include "util/resource_manager.h"
 
@@ -1533,13 +1535,90 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   }
   TheoryEngine* te = getTheoryEngine();
   Assert(te != nullptr);
-  te->printInstantiations(out);
+  QuantifiersEngine* qe = te->getQuantifiersEngine();
+
+  // First, extract and print the skolemizations
+  bool printed = false;
+  bool reqNames = !options::printInstFull();
+  // only print when in list mode
+  if (options::printInstMode() == options::PrintInstMode::LIST)
+  {
+    std::map<Node, std::vector<Node>> sks;
+    qe->getSkolemTermVectors(sks);
+    for (const std::pair<const Node, std::vector<Node>>& s : sks)
+    {
+      Node name;
+      if (!qe->getNameForQuant(s.first, name, reqNames))
+      {
+        // did not have a name and we are only printing formulas with names
+        continue;
+      }
+      SkolemList slist(name, s.second);
+      out << slist;
+      printed = true;
+    }
+  }
+
+  // Second, extract and print the instantiations
+  std::map<Node, std::vector<std::vector<Node>>> insts;
+  getInstantiationTermVectors(insts);
+  for (const std::pair<const Node, std::vector<std::vector<Node>>>& i : insts)
+  {
+    if (i.second.empty())
+    {
+      // no instantiations, skip
+      continue;
+    }
+    Node name;
+    if (!qe->getNameForQuant(i.first, name, reqNames))
+    {
+      // did not have a name and we are only printing formulas with names
+      continue;
+    }
+    // must have a name
+    if (options::printInstMode() == options::PrintInstMode::NUM)
+    {
+      out << "(num-instantiations " << name << " " << i.second.size() << ")"
+          << std::endl;
+    }
+    else
+    {
+      Assert(options::printInstMode() == options::PrintInstMode::LIST);
+      InstantiationList ilist(name, i.second);
+      out << ilist;
+    }
+    printed = true;
+  }
+  // if we did not print anything, we indicate this
+  if (!printed)
+  {
+    out << "No instantiations" << std::endl;
+  }
   if (options::instFormatMode() == options::InstFormatMode::SZS)
   {
     out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
   }
 }
 
+void SmtEngine::getInstantiationTermVectors(
+    std::map<Node, std::vector<std::vector<Node>>>& insts)
+{
+  SmtScope smts(this);
+  finishInit();
+  if (options::proofNew() && getSmtMode() == SmtMode::UNSAT)
+  {
+    // TODO (project #37): minimize instantiations based on proof manager
+  }
+  else
+  {
+    TheoryEngine* te = getTheoryEngine();
+    Assert(te != nullptr);
+    QuantifiersEngine* qe = te->getQuantifiersEngine();
+    // otherwise, just get the list of all instantiations
+    qe->getInstantiationTermVectors(insts);
+  }
+}
+
 void SmtEngine::printSynthSolution( std::ostream& out ) {
   SmtScope smts(this);
   finishInit();
@@ -1609,7 +1688,8 @@ void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
   SmtScope smts(this);
   TheoryEngine* te = getTheoryEngine();
   Assert(te != nullptr);
-  te->getInstantiatedQuantifiedFormulas(qs);
+  QuantifiersEngine* qe = te->getQuantifiersEngine();
+  qe->getInstantiatedQuantifiedFormulas(qs);
 }
 
 void SmtEngine::getInstantiationTermVectors(
@@ -1618,7 +1698,8 @@ void SmtEngine::getInstantiationTermVectors(
   SmtScope smts(this);
   TheoryEngine* te = getTheoryEngine();
   Assert(te != nullptr);
-  te->getInstantiationTermVectors(q, tvecs);
+  QuantifiersEngine* qe = te->getQuantifiersEngine();
+  qe->getInstantiationTermVectors(q, tvecs);
 }
 
 std::vector<Node> SmtEngine::getAssertions()
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 558bd2b40..a392e8c42 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -675,6 +675,14 @@ class CVC4_PUBLIC SmtEngine
    */
   void getInstantiationTermVectors(Node q,
                                    std::vector<std::vector<Node>>& tvecs);
+  /**
+   * Get instantiation term vectors, which maps each instantiated quantified
+   * formula to the list of instantiations for that quantified formula. This
+   * list is minimized if proofs are enabled, and this call is immediately
+   * preceded by an UNSAT or ENTAILED query
+   */
+  void getInstantiationTermVectors(
+      std::map<Node, std::vector<std::vector<Node>>>& insts);
 
   /**
    * Get an unsatisfiable core (only if immediately preceded by an UNSAT or
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index ed02c6b32..3bbe15b8c 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/instantiate.h"
 
 #include "expr/node_algorithm.h"
+#include "options/printer_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
@@ -559,107 +560,6 @@ Node Instantiate::getTermForType(TypeNode tn)
   return d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
 }
 
-bool Instantiate::printInstantiations(std::ostream& out)
-{
-  if (options::printInstMode() == options::PrintInstMode::NUM)
-  {
-    return printInstantiationsNum(out);
-  }
-  Assert(options::printInstMode() == options::PrintInstMode::LIST);
-  return printInstantiationsList(out);
-}
-
-bool Instantiate::printInstantiationsList(std::ostream& out)
-{
-  bool useUnsatCore = false;
-  std::vector<Node> active_lemmas;
-  if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas))
-  {
-    useUnsatCore = true;
-  }
-  bool printed = false;
-  bool isFull = options::printInstFull();
-  if (options::incrementalSolving())
-  {
-    for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
-    {
-      std::stringstream qout;
-      if (!printQuant(t.first, qout, isFull))
-      {
-        continue;
-      }
-      std::stringstream sout;
-      t.second->print(sout, t.first, useUnsatCore, active_lemmas);
-      if (!sout.str().empty())
-      {
-        out << "(instantiations " << qout.str() << std::endl;
-        out << sout.str();
-        out << ")" << std::endl;
-        printed = true;
-      }
-    }
-  }
-  else
-  {
-    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
-    {
-      std::stringstream qout;
-      if (!printQuant(t.first, qout, isFull))
-      {
-        continue;
-      }
-      std::stringstream sout;
-      t.second.print(sout, t.first, useUnsatCore, active_lemmas);
-      if (!sout.str().empty())
-      {
-        out << "(instantiations " << qout.str() << std::endl;
-        out << sout.str();
-        out << ")" << std::endl;
-        printed = true;
-      }
-    }
-  }
-  return printed;
-}
-
-bool Instantiate::printInstantiationsNum(std::ostream& out)
-{
-  if (d_total_inst_debug.empty())
-  {
-    return false;
-  }
-  bool isFull = options::printInstFull();
-  for (NodeUIntMap::iterator it = d_total_inst_debug.begin();
-       it != d_total_inst_debug.end();
-       ++it)
-  {
-    std::stringstream ss;
-    if (printQuant((*it).first, ss, isFull))
-    {
-      out << "(num-instantiations " << ss.str() << " " << (*it).second << ")"
-          << std::endl;
-    }
-  }
-  return true;
-}
-
-bool Instantiate::printQuant(Node q, std::ostream& out, bool isFull)
-{
-  if (isFull)
-  {
-    out << q;
-    return true;
-  }
-  quantifiers::QuantAttributes* qa = d_qe->getQuantAttributes();
-  Node name = qa->getQuantName(q);
-  if (name.isNull())
-  {
-    return false;
-  }
-  out << name;
-  return true;
-}
-
 void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
 {
   if (options::incrementalSolving())
@@ -902,15 +802,15 @@ void Instantiate::debugPrint(std::ostream& out)
   }
   if (options::debugInst())
   {
-    bool isFull = options::printInstFull();
+    bool req = !options::printInstFull();
     for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
     {
-      std::stringstream ss;
-      if (!printQuant(i.first, ss, isFull))
+      Node name;
+      if (!d_qe->getNameForQuant(i.first, name, req))
       {
         continue;
       }
-      out << "(num-instantiations " << ss.str() << " " << i.second << ")"
+      out << "(num-instantiations " << name << " " << i.second << ")"
           << std::endl;
     }
   }
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 3a51c8904..bbb1a0a44 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -223,13 +223,6 @@ class Instantiate : public QuantifiersUtil
   void debugPrintModel();
 
   //--------------------------------------user-level interface utilities
-  /** print instantiations
-   *
-   * Print all instantiations for all quantified formulas on out,
-   * returns true if at least one instantiation was printed. The type of output
-   * (list, num, etc.) is determined by printInstMode.
-   */
-  bool printInstantiations(std::ostream& out);
   /** get instantiated quantified formulas
    *
    * Get the list of quantified formulas that were instantiated in the current
@@ -274,11 +267,11 @@ class Instantiate : public QuantifiersUtil
   Node getInstantiatedConjunction(Node q);
   /** get unsat core lemmas
    *
-   * If this method returns true, then it appends to active_lemmas all lemmas
+   * If this method returns true, then it appends to activeLemmas all lemmas
    * that are in the unsat core that originated from the theory of quantifiers.
    * This method returns false if the unsat core is not available.
    */
-  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
+  bool getUnsatCoreLemmas(std::vector<Node>& activeLemmas);
   /** get explanation for instantiation lemmas
    *
    *
@@ -328,16 +321,6 @@ class Instantiate : public QuantifiersUtil
    * if possible.
    */
   static Node ensureType(Node n, TypeNode tn);
-  /** print instantiations in list format */
-  bool printInstantiationsList(std::ostream& out);
-  /** print instantiations in num format */
-  bool printInstantiationsNum(std::ostream& out);
-  /**
-   * Print quantified formula q on output out. If isFull is false, then we print
-   * the identifier of the quantified formula if it has one, or print
-   * nothing and return false otherwise.
-   */
-  bool printQuant(Node q, std::ostream& out, bool isFull);
 
   /** pointer to the quantifiers engine */
   QuantifiersEngine* d_qe;
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 901b7ad82..3ddfc4c9f 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -378,29 +378,18 @@ bool Skolemize::isInductionTerm(Node n)
   return false;
 }
 
-bool Skolemize::printSkolemization(std::ostream& out)
+void Skolemize::getSkolemTermVectors(
+    std::map<Node, std::vector<Node> >& sks) const
 {
-  bool printed = false;
-  for (NodeNodeMap::iterator it = d_skolemized.begin();
-       it != d_skolemized.end();
-       ++it)
+  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::const_iterator
+      itk;
+  for (const std::pair<const Node, Node>& p : d_skolemized)
   {
-    Node q = (*it).first;
-    printed = true;
-    out << "(skolem " << q << std::endl;
-    out << "  ( ";
-    for (unsigned i = 0; i < d_skolem_constants[q].size(); i++)
-    {
-      if (i > 0)
-      {
-        out << " ";
-      }
-      out << d_skolem_constants[q][i];
-    }
-    out << " )" << std::endl;
-    out << ")" << std::endl;
+    Node q = p.first;
+    itk = d_skolem_constants.find(q);
+    Assert(itk != d_skolem_constants.end());
+    sks[q].insert(sks[q].end(), itk->second.begin(), itk->second.end());
   }
-  return printed;
 }
 
 bool Skolemize::isProofEnabled() const { return d_epg != nullptr; }
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index 8cf3e3176..b28854baf 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -108,15 +108,18 @@ class Skolemize
   Node getSkolemizedBody(Node q);
   /** is n a variable that we can apply inductive strenghtening to? */
   static bool isInductionTerm(Node n);
-  /** print all skolemizations
+  /**
+   * Get skolemization vectors, where for each quantified formula that was
+   * skolemized, this is the list of skolems that were used to witness the
+   * negation of that quantified formula (which is equivalent to an existential
+   * one).
+   *
    * This is used for the command line option
    *   --dump-instantiations
-   * which prints an informal justification
-   * of steps taken by the quantifiers module.
-   * Returns true if we printed at least one
-   * skolemization.
+   * which prints an informal justification of steps taken by the quantifiers
+   * module.
    */
-  bool printSkolemization(std::ostream& out);
+  void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const;
 
  private:
   /** Are proofs enabled? */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 94f70a2d9..7cec8721c 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers_engine.h"
 
+#include "options/printer_options.h"
 #include "options/quantifiers_options.h"
 #include "options/uf_options.h"
 #include "smt/smt_engine_scope.h"
@@ -979,26 +980,6 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector
   d_instantiate->getInstantiationTermVectors(insts);
 }
 
-void QuantifiersEngine::printInstantiations( std::ostream& out ) {
-  bool printed = false;
-  // print the skolemizations
-  if (options::printInstMode() == options::PrintInstMode::LIST)
-  {
-    if (d_skolemize->printSkolemization(out))
-    {
-      printed = true;
-    }
-  }
-  // print the instantiations
-  if (d_instantiate->printInstantiations(out))
-  {
-    printed = true;
-  }
-  if( !printed ){
-    out << "No instantiations" << std::endl;
-  }
-}
-
 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
   if (d_qmodules->d_synth_e)
   {
@@ -1008,10 +989,17 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
   }
 }
 
-void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
+void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
+{
   d_instantiate->getInstantiatedQuantifiedFormulas(qs);
 }
 
+void QuantifiersEngine::getSkolemTermVectors(
+    std::map<Node, std::vector<Node> >& sks) const
+{
+  d_skolemize->getSkolemTermVectors(sks);
+}
+
 QuantifiersEngine::Statistics::Statistics()
     : d_time("theory::QuantifiersEngine::time"),
       d_qcf_time("theory::QuantifiersEngine::time_qcf"),
@@ -1088,6 +1076,23 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
   return d_eq_query->getInternalRepresentative(a, q, index);
 }
 
+Node QuantifiersEngine::getNameForQuant(Node q) const
+{
+  Node name = d_quant_attr->getQuantName(q);
+  if (!name.isNull())
+  {
+    return name;
+  }
+  return q;
+}
+
+bool QuantifiersEngine::getNameForQuant(Node q, Node& name, bool req) const
+{
+  name = getNameForQuant(q);
+  // if we have a name, or we did not require one
+  return name != q || !req;
+}
+
 bool QuantifiersEngine::getSynthSolutions(
     std::map<Node, std::map<Node, Node> >& sol_map)
 {
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d09090da3..126fca01f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -258,11 +258,19 @@ public:
   * guided instantiation.
   */
  Node getInternalRepresentative(Node a, Node q, int index);
+ /**
+  * Get quantifiers name, which returns a variable corresponding to the name of
+  * quantified formula q if q has a name, or otherwise returns q itself.
+  */
+ Node getNameForQuant(Node q) const;
+ /**
+  * Get name for quantified formula. Returns true if q has a name or if req
+  * is false. Sets name to the result of the above method.
+  */
+ bool getNameForQuant(Node q, Node& name, bool req = true) const;
 
 public:
  //----------user interface for instantiations (see quantifiers/instantiate.h)
- /** print instantiations */
- void printInstantiations(std::ostream& out);
  /** print solution for synthesis conjectures */
  void printSynthSolution(std::ostream& out);
  /** get list of quantified formulas that were instantiated */
@@ -272,6 +280,12 @@ public:
                                   std::vector<std::vector<Node> >& tvecs);
  void getInstantiationTermVectors(
      std::map<Node, std::vector<std::vector<Node> > >& insts);
+ /**
+  * Get skolemization vectors, where for each quantified formula that was
+  * skolemized, this is the list of skolems that were used to witness the
+  * negation of that quantified formula.
+  */
+ void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const;
 
  /** get synth solutions
   *
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 16d68ea5c..ba65fe69d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1175,15 +1175,6 @@ Node TheoryEngine::getPreprocessedTerm(TNode n)
   return d_propEngine->getPreprocessedTerm(rewritten);
 }
 
-void TheoryEngine::printInstantiations( std::ostream& out ) {
-  if( d_quantEngine ){
-    d_quantEngine->printInstantiations( out );
-  }else{
-    out << "Internal error : instantiations not available when quantifiers are not present." << std::endl;
-    Assert(false);
-  }
-}
-
 void TheoryEngine::printSynthSolution( std::ostream& out ) {
   if( d_quantEngine ){
     d_quantEngine->printSynthSolution( out );
@@ -1193,30 +1184,6 @@ void TheoryEngine::printSynthSolution( std::ostream& out ) {
   }
 }
 
-void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
-  if( d_quantEngine ){
-    d_quantEngine->getInstantiatedQuantifiedFormulas( qs );
-  }else{
-    Assert(false);
-  }
-}
-
-void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
-  if( d_quantEngine ){
-    d_quantEngine->getInstantiationTermVectors( q, tvecs );
-  }else{
-    Assert(false);
-  }
-}
-
-void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
-  if( d_quantEngine ){
-    d_quantEngine->getInstantiationTermVectors( insts );
-  }else{
-    Assert(false);
-  }
-}
-
 TrustNode TheoryEngine::getExplanation(TNode node)
 {
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0be511e47..747c1ccc9 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -663,30 +663,11 @@ class TheoryEngine {
    */
   Node getPreprocessedTerm(TNode n);
   /**
-   * Print all instantiations made by the quantifiers module.
-   */
-  void printInstantiations( std::ostream& out );
-
-  /**
    * Print solution for synthesis conjectures found by ce_guided_instantiation module
    */
   void printSynthSolution( std::ostream& out );
 
   /**
-   * Get list of quantified formulas that were instantiated
-   */
-  void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
-
-  /**
-   * Get instantiation methods
-   *   the first given forall x.q[x] returns ( a, ..., z )
-   *   the second returns mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] )
-   * , ... , forall x.qn[x] -> ( qn[a]...qn[z] )
-   */
-  void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
-  void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
-
-  /**
    * Forwards an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
    */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 52bdd6854..a3eaeee57 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1711,7 +1711,6 @@ set(regress_1_tests
   regress1/quantifiers/constfunc.cvc
   regress1/quantifiers/dt-tc-opt-small.smt2
   regress1/quantifiers/dump-inst-i.smt2
-  regress1/quantifiers/dump-inst-proof.smt2
   regress1/quantifiers/dump-inst.smt2
   regress1/quantifiers/eqrange_ex_1.smt2
   regress1/quantifiers/ext-ex-deq-trigger.smt2
@@ -2491,6 +2490,8 @@ set(regression_disabled_tests
   regress1/quantifiers/anti-sk-simp.smt2
   # no longer support snorm option
   regress1/quantifiers/arith-snorm.smt2
+  # until we have support for minimizing instantiations based on unsat core
+  regress1/quantifiers/dump-inst-proof.smt2
   # ajreynol: different error messages on production and debug:
   regress1/quantifiers/macro-subtype-param.smt2
   # times out with competition build, ok with other builds: