(proof-new) Instantiation list utility (#5768)

This is in preparation for refactoring the printing of instantiations. We will migrate the printing of instantiations (currently done in the Instantiate module within quantifiers engine) to somewhere more high level e.g. the SmtEngine or in the command layer. This will make the infrastructure for dumping instantiations much more flexible, as implemented on proof-new.

2 files changed, 36 insertions, 1 deletions

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index be43a07cf..4e464f829 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -26,6 +26,7 @@
 #include "proof/unsat_core.h"
 #include "smt/command.h"
 #include "smt/node_command.h"
+#include "theory/quantifiers/instantiation_list.h"
 
 using namespace std;
 
@@ -110,6 +111,33 @@ void Printer::toStream(std::ostream& out, const UnsatCore& core) const
   }
 }/* Printer::toStream(UnsatCore) */
 
+void Printer::toStream(std::ostream& out, const InstantiationList& is) const
+{
+  out << "(instantiations " << is.d_quant << std::endl;
+  for (const std::vector<Node>& i : is.d_inst)
+  {
+    out << "  ( ";
+    for (const Node& n : i)
+    {
+      out << n << " ";
+    }
+    out << ")" << std::endl;
+  }
+  out << ")" << std::endl;
+}
+
+void Printer::toStream(std::ostream& out, const SkolemList& sks) const
+{
+  out << "(skolem " << sks.d_quant << std::endl;
+  out << "  ( ";
+  for (const Node& n : sks.d_sks)
+  {
+    out << n << " ";
+  }
+  out << ")" << std::endl;
+  out << ")" << std::endl;
+}
+
 Printer* Printer::getPrinter(OutputLanguage lang)
 {
   if(lang == language::output::LANG_AUTO) {
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 3c53e34e6..835dbe798 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -32,8 +32,9 @@ namespace CVC4 {
 
 class Command;
 class CommandStatus;
-class NodeCommand;
 class UnsatCore;
+class InstantiationList;
+class SkolemList;
 
 class Printer
 {
@@ -62,6 +63,12 @@ class Printer
   /** Write an UnsatCore out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const UnsatCore& core) const;
 
+  /** Write an instantiation list out to a stream with this Printer. */
+  virtual void toStream(std::ostream& out, const InstantiationList& is) const;
+
+  /** Write a skolem list out to a stream with this Printer. */
+  virtual void toStream(std::ostream& out, const SkolemList& sks) const;
+
   /** Print empty command */
   virtual void toStreamCmdEmpty(std::ostream& out,
                                 const std::string& name) const;