1 files changed, 84 insertions, 3 deletions

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()