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

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index dd944f929d1adf194fdcd46655ede3c4619fcc0c..632adae1e0fbb59b134cb76a591e09f1bb6a1ea2 100644 (file)
--- 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 be43a07cf7b626ed4bff23f568d31790376f645c..4e464f8299f4caf58da0609f3036da25b3dbbde8 100644 (file)
--- 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 3c53e34e6c2929cbe5d6031bfb1dc62bed4586a3..835dbe798e58dd9630c68cf94a95c0299a9aeeb7 100644 (file)
--- 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 (file)
index 0000000..4bf17eb
--- /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 (file)
index 0000000..6ef8e47
--- /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 */