Add printing methods for some commands. (#7557)

This PR is a step towards enabling -o raw-benchmark. It adds printing methods for some of the new commands and fixes some other miscellaneous issues.

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index ec0fdeda1c06ece731a8e023d6d05969f4297235..cc9df91f45d0ac744defceaf8fd147e6016ab585 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -411,7 +411,8 @@ void Printer::toStreamCmdGetAbduct(std::ostream& out,
 }
 
 void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
-                                                  Node n) const
+                                                  Node n,
+                                                  bool doFull) const
 {
   printUnknownCommand(out, "get-quantifier-elimination");
 }

diff --git a/src/printer/printer.h b/src/printer/printer.h
index 8c8118aa933b5e24ce2b332d205d1e8898bb8007..485cd70e6973cedc18880b5e8d2f4c579c25b5b9 100644 (file)
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -179,11 +179,11 @@ class Printer
   virtual void toStreamCmdGetModel(std::ostream& out) const;
 
   /** Print block-model command */
-  void toStreamCmdBlockModel(std::ostream& out) const;
+  virtual void toStreamCmdBlockModel(std::ostream& out) const;
 
   /** Print block-model-values command */
-  void toStreamCmdBlockModelValues(std::ostream& out,
-                                   const std::vector<Node>& nodes) const;
+  virtual void toStreamCmdBlockModelValues(
+      std::ostream& out, const std::vector<Node>& nodes) const;
 
   /** Print get-proof command */
   virtual void toStreamCmdGetProof(std::ostream& out) const;
@@ -192,10 +192,10 @@ class Printer
   void toStreamCmdGetInstantiations(std::ostream& out) const;
 
   /** Print get-interpol command */
-  void toStreamCmdGetInterpol(std::ostream& out,
-                              const std::string& name,
-                              Node conj,
-                              TypeNode sygusType) const;
+  virtual void toStreamCmdGetInterpol(std::ostream& out,
+                                      const std::string& name,
+                                      Node conj,
+                                      TypeNode sygusType) const;
 
   /** Print get-abduct command */
   virtual void toStreamCmdGetAbduct(std::ostream& out,
@@ -204,7 +204,9 @@ class Printer
                                     TypeNode sygusType) const;
 
   /** Print get-quantifier-elimination command */
-  void toStreamCmdGetQuantifierElimination(std::ostream& out, Node n) const;
+  virtual void toStreamCmdGetQuantifierElimination(std::ostream& out,
+                                                   Node n,
+                                                   bool doFull) const;
 
   /** Print get-unsat-assumptions command */
   virtual void toStreamCmdGetUnsatAssumptions(std::ostream& out) const;

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 171f8e524e815a6822a08eb3f0f5d2da73c90d65..d6e6fc4eb466e62f828da037e67cd3602c2a05da 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1199,7 +1199,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::SEP_STAR: return "sep";
   case kind::SEP_PTO: return "pto";
   case kind::SEP_WAND: return "wand";
-  case kind::SEP_EMP: return "emp";
+  case kind::SEP_EMP: return "sep.emp";
 
   // quantifiers
   case kind::FORALL: return "forall";
@@ -1437,6 +1437,23 @@ void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out,
   out << ") " << type << ')' << std::endl;
 }
 
+void Smt2Printer::toStreamCmdDeclarePool(
+    std::ostream& out,
+    const std::string& id,
+    TypeNode type,
+    const std::vector<Node>& initValue) const
+{
+  out << "(declare-pool " << cvc5::quoteSymbol(id) << ' ' << type << " (";
+  for (size_t i = 0, n = initValue.size(); i < n; ++i)
+  {
+    if (i != 0) {
+      out << ' ';
+    }
+    out << initValue[i];
+  }
+  out << "))" << std::endl;
+}
+
 void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out,
                                             const std::string& id,
                                             const std::vector<Node>& formals,
@@ -1577,6 +1594,26 @@ void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const
   out << "(get-model)" << std::endl;
 }
 
+void Smt2Printer::toStreamCmdBlockModel(std::ostream& out) const
+{
+  out << "(block-model)" << std::endl;
+}
+
+void Smt2Printer::toStreamCmdBlockModelValues(
+    std::ostream& out, const std::vector<Node>& nodes) const
+{
+  out << "(block-model-values (";
+  for (size_t i = 0, n = nodes.size(); i < n; ++i)
+  {
+    if (i != 0)
+    {
+      out << ' ';
+    }
+    out << nodes[i];
+  }
+  out << "))" << std::endl;
+}
+
 void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const
 {
   out << "(get-assignment)" << std::endl;
@@ -1858,6 +1895,20 @@ void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const
   out << "(check-synth)" << std::endl;
 }
 
+void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out,
+                                         const std::string& name,
+                                         Node conj,
+                                         TypeNode sygusType) const
+{
+  out << "(get-interpol " << cvc5::quoteSymbol(name) << ' ' << conj;
+  if (!sygusType.isNull())
+  {
+    out << ' ';
+    toStreamSygusGrammar(out, sygusType);
+  }
+  out << ')' << std::endl;
+}
+
 void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
                                        const std::string& name,
                                        Node conj,
@@ -1875,6 +1926,14 @@ void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
   out << ')' << std::endl;
 }
 
+void Smt2Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
+                                                      Node n,
+                                                      bool doFull) const
+{
+  out << '(' << (doFull ? "get-qe" : "get-qe-disjunct") << ' ' << n << ')'
+      << std::endl;
+}
+
 /*
    --------------------------------------------------------------------------
     End of Handling SyGuS commands

diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index e0b6fedbc31b3da03415285eba158188359d76a1..2af17ed5954118382d37e2e53b497ccbc81b8795 100644 (file)
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -74,9 +74,14 @@ class Smt2Printer : public cvc5::Printer
                                   const std::string& id,
                                   TypeNode type) const override;
 
+  /** Print declare-pool command */
+  void toStreamCmdDeclarePool(std::ostream& out,
+                                      const std::string& id,
+                                      TypeNode type,
+                                      const std::vector<Node>& initValue) const override;
+
   /** Print declare-sort command */
-  void toStreamCmdDeclareType(std::ostream& out,
-                              TypeNode type) const override;
+  void toStreamCmdDeclareType(std::ostream& out, TypeNode type) const override;
 
   /** Print define-sort command */
   void toStreamCmdDefineType(std::ostream& out,
@@ -114,11 +119,12 @@ class Smt2Printer : public cvc5::Printer
                              TypeNode type) const override;
 
   /** Print synth-fun command */
-  void toStreamCmdSynthFun(std::ostream& out,
-                           Node f,
-                           const std::vector<Node>& vars,
-                           bool isInv,
-                           TypeNode sygusType = TypeNode::null()) const override;
+  void toStreamCmdSynthFun(
+      std::ostream& out,
+      Node f,
+      const std::vector<Node>& vars,
+      bool isInv,
+      TypeNode sygusType = TypeNode::null()) const override;
 
   /** Print constraint command */
   void toStreamCmdConstraint(std::ostream& out, Node n) const override;
@@ -149,15 +155,33 @@ class Smt2Printer : public cvc5::Printer
   /** Print get-model command */
   void toStreamCmdGetModel(std::ostream& out) const override;
 
+  /** Print block-model command */
+  void toStreamCmdBlockModel(std::ostream& out) const override;
+
+  /** Print block-model-values command */
+  void toStreamCmdBlockModelValues(
+      std::ostream& out, const std::vector<Node>& nodes) const override;
+
   /** Print get-proof command */
   void toStreamCmdGetProof(std::ostream& out) const override;
 
+  /** Print get-interpol command */
+  void toStreamCmdGetInterpol(std::ostream& out,
+                              const std::string& name,
+                              Node conj,
+                              TypeNode sygusType) const override;
+
   /** Print get-abduct command */
   void toStreamCmdGetAbduct(std::ostream& out,
                             const std::string& name,
                             Node conj,
                             TypeNode sygusType) const override;
 
+  /** Print get-quantifier-elimination command */
+  void toStreamCmdGetQuantifierElimination(std::ostream& out,
+                                           Node n,
+                                           bool doFull) const override;
+
   /** Print get-unsat-assumptions command */
   void toStreamCmdGetUnsatAssumptions(std::ostream& out) const override;
 

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 419b925c4e1a735c63bc396db51678c03afdf32b..c2aa1c5f9d1f3dee981cbc9b8fbce8481ca60ea1 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1168,8 +1168,8 @@ void DeclareFunctionCommand::toStream(std::ostream& out,
                                       size_t dag,
                                       Language language) const
 {
-  Printer::getPrinter(language)->toStreamCmdDeclareFunction(out,
-                                                            termToNode(d_func));
+  Printer::getPrinter(language)->toStreamCmdDeclareFunction(
+      out, d_symbol, sortToTypeNode(d_func.getSort()));
 }
 
 /* -------------------------------------------------------------------------- */
@@ -2221,7 +2221,7 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out,
                                                Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
-      out, termToNode(d_term));
+      out, termToNode(d_term), d_doFull);
 }
 
 /* -------------------------------------------------------------------------- */