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

5 files changed, 132 insertions, 3 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index dd944f929..632adae1e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -694,10 +694,10 @@ libcvc4_add_sources(
   theory/quantifiers/inst_match_trie.h
   theory/quantifiers/inst_strategy_enumerative.cpp
   theory/quantifiers/inst_strategy_enumerative.h
-  theory/quantifiers/sygus_inst.cpp
-  theory/quantifiers/sygus_inst.h
   theory/quantifiers/instantiate.cpp
   theory/quantifiers/instantiate.h
+  theory/quantifiers/instantiation_list.cpp
+  theory/quantifiers/instantiation_list.h
   theory/quantifiers/lazy_trie.cpp
   theory/quantifiers/lazy_trie.h
   theory/quantifiers/proof_checker.cpp
@@ -808,6 +808,8 @@ libcvc4_add_sources(
   theory/quantifiers/sygus/type_node_id_trie.h
   theory/quantifiers/sygus/transition_inference.cpp
   theory/quantifiers/sygus/transition_inference.h
+  theory/quantifiers/sygus_inst.cpp
+  theory/quantifiers/sygus_inst.h
   theory/quantifiers/sygus_sampler.cpp
   theory/quantifiers/sygus_sampler.h
   theory/quantifiers/term_database.cpp
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;
diff --git a/src/theory/quantifiers/instantiation_list.cpp b/src/theory/quantifiers/instantiation_list.cpp
new file mode 100644
index 000000000..4bf17ebc2
--- /dev/null
+++ b/src/theory/quantifiers/instantiation_list.cpp
@@ -0,0 +1,34 @@
+/*********************                                                        */
+/*! \file instantiation_list.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief list of instantiations
+ **/
+
+#include "theory/quantifiers/instantiation_list.h"
+
+#include "options/base_options.h"
+#include "printer/printer.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist)
+{
+  Printer::getPrinter(options::outputLanguage())->toStream(out, ilist);
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out, const SkolemList& skl)
+{
+  Printer::getPrinter(options::outputLanguage())->toStream(out, skl);
+  return out;
+}
+
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h
new file mode 100644
index 000000000..6ef8e4784
--- /dev/null
+++ b/src/theory/quantifiers/instantiation_list.h
@@ -0,0 +1,58 @@
+/*********************                                                        */
+/*! \file instantiation_list.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief list of instantiations
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
+#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
+
+#include <iosfwd>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+/** A list of instantiations for a quantified formula */
+struct InstantiationList
+{
+  InstantiationList(Node q, const std::vector<std::vector<Node> >& inst)
+      : d_quant(q), d_inst(inst)
+  {
+  }
+  /** The quantified formula */
+  Node d_quant;
+  /** The instantiation list */
+  std::vector<std::vector<Node> > d_inst;
+};
+
+/** Print the instantiation list to stream out */
+std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist);
+
+/** The list of skolemization for a quantified formula */
+struct SkolemList
+{
+  SkolemList(Node q, const std::vector<Node>& sks) : d_quant(q), d_sks(sks) {}
+  /** The quantified formula */
+  Node d_quant;
+  /** The list of skolems for the quantified formula */
+  std::vector<Node> d_sks;
+};
+
+/** Print the skolem list to stream out */
+std::ostream& operator<<(std::ostream& out, const SkolemList& skl);
+
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */