Push output language inside the printing code (#7683)

This PR pushes the explicit specification of the output language further inside the printing methods.
The general way to specify the output language is to attach it to the output stream. The changes simplify the interface, while we still allow printing in another output language via using a scope (as used in the lfsc and tptp printers).

diff --git a/src/expr/node.h b/src/expr/node.h
index bd5f8c605f66de8b390a5da9252a38647d32e72e..3a4706e1e95108a73090c1e47fbd0fa3be5560e0 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -817,11 +817,10 @@ public:
    */
   inline void toStream(std::ostream& out,
                        int toDepth = -1,
-                       size_t dagThreshold = 1,
-                       Language language = Language::LANG_AUTO) const
+                       size_t dagThreshold = 1) const
   {
     assertTNodeNotExpired();
-    d_nv->toStream(out, toDepth, dagThreshold, language);
+    d_nv->toStream(out, toDepth, dagThreshold);
   }
 
   void constToStream(std::ostream& out) const
@@ -865,8 +864,7 @@ public:
 inline std::ostream& operator<<(std::ostream& out, TNode n) {
   n.toStream(out,
              options::ioutils::getNodeDepth(out),
-             options::ioutils::getDagThresh(out),
-             options::ioutils::getOutputLang(out));
+             options::ioutils::getDagThresh(out));
   return out;
 }
 

diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 3d51cbbbe6581de4cbe7c073259e457f607a2085..d38447f2140f5ee2bea8501ffd1897aa5fdbe457 100644 (file)
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -25,6 +25,7 @@
 #include "expr/metakind.h"
 #include "expr/node.h"
 #include "options/base_options.h"
+#include "options/io_utils.h"
 #include "options/language.h"
 #include "options/options.h"
 #include "printer/printer.h"
@@ -36,23 +37,20 @@ namespace expr {
 
 string NodeValue::toString() const {
   stringstream ss;
-
-  Language outlang =
-      (this == &null()) ? Language::LANG_AUTO : options::outputLanguage();
-  toStream(ss, -1, false, outlang);
+  toStream(ss, -1, false);
   return ss.str();
 }
 
 void NodeValue::toStream(std::ostream& out,
                          int toDepth,
-                         size_t dag,
-                         Language language) const
+                         size_t dag) const
 {
   // Ensure that this node value is live for the length of this call.
   // It really breaks things badly if we don't have a nonzero ref
   // count, even just for printing.
   RefCountGuard guard(this);
 
+  auto language = options::ioutils::getOutputLang(out);
   Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, dag);
 }
 
@@ -98,8 +96,7 @@ std::ostream& operator<<(std::ostream& out, const NodeValue& nv)
 {
   nv.toStream(out,
               options::ioutils::getNodeDepth(out),
-              options::ioutils::getDagThresh(out),
-              options::ioutils::getOutputLang(out));
+              options::ioutils::getDagThresh(out));
   return out;
 }
 

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index cf24a207d77f918d227a884b381f8564a24d5d78..a0237a10673fd983f8a753cfac1b6caba87f2458 100644 (file)
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -230,8 +230,7 @@ class NodeValue
 
   void toStream(std::ostream& out,
                 int toDepth = -1,
-                size_t dag = 1,
-                Language = Language::LANG_AUTO) const;
+                size_t dag = 1) const;
 
   void printAst(std::ostream& out, int indent = 0) const;
 

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index c8a0d9ce26be3a24a79a0c76b568b6b24fcf8912..e94d4733e9a1e283c2126bbe8e4680296b59a218 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -660,9 +660,7 @@ bool TypeNode::isSygusDatatype() const
 
 std::string TypeNode::toString() const {
   std::stringstream ss;
-  Language outlang =
-      (this == &s_null) ? Language::LANG_AUTO : options::outputLanguage();
-  d_nv->toStream(ss, -1, 0, outlang);
+  d_nv->toStream(ss, -1, 0);
   return ss.str();
 }
 

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 95b3895eee500596a8c65df1cb363d3dab921b22..33d698163fe088bd908e9a0d6c7d85e9802e396f 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -374,10 +374,9 @@ private:
    * @param out the stream to serialize this node to
    * @param language the language in which to output
    */
-  inline void toStream(std::ostream& out,
-                       Language language = Language::LANG_AUTO) const
+  inline void toStream(std::ostream& out) const
   {
-    d_nv->toStream(out, -1, 0, language);
+    d_nv->toStream(out, -1, 0);
   }
 
   /**
@@ -729,7 +728,7 @@ private:
  * @return the stream
  */
 inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
-  n.toStream(out, options::ioutils::getOutputLang(out));
+  n.toStream(out);
   return out;
 }
 

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index fe464a8bdd47617f798bdfdc1daa71eb5c725a9f..13477b7923449a9912242c8323f585c805d6962a 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1220,7 +1220,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
 void Smt2Printer::toStreamType(std::ostream& out, TypeNode tn) const
 {
   // we currently must call TypeNode::toStream here.
-  tn.toStream(out, Language::LANG_SMTLIB_V2_6);
+  tn.toStream(out);
 }
 
 template <class T>

diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index fe44becb64f0b714130903ef3e7bf7c5a3d28b18..ef94bf54f2d812d827560c5d12e002fb6132aa0a 100644 (file)
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -37,7 +37,9 @@ void TptpPrinter::toStream(std::ostream& out,
                            int toDepth,
                            size_t dag) const
 {
-  n.toStream(out, toDepth, dag, Language::LANG_SMTLIB_V2_6);
+  options::ioutils::Scope scope(out);
+  options::ioutils::applyOutputLang(out, Language::LANG_SMTLIB_V2_6);
+  n.toStream(out, toDepth, dag);
 }/* TptpPrinter::toStream() */
 
 void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 7f1d9e192c9c3f25b12c5d9c83cf9e3bd77a5d20..6eab9b0368832427d327844578f6a4c5ed3f16f5 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -531,7 +531,8 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
     if (tnn.isNull())
     {
       std::stringstream ss;
-      tn.toStream(ss, Language::LANG_SMTLIB_V2_6);
+      options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
+      tn.toStream(ss);
       if (tn.isSort() || (tn.isDatatype() && !tn.isTuple()))
       {
         std::stringstream sss;

diff --git a/src/proof/lfsc/lfsc_print_channel.cpp b/src/proof/lfsc/lfsc_print_channel.cpp
index 36fd8831b7acf5ec7d90c85675e8f8580dd8f775..47961062ef7847d196e91a7850371401f0e9d4cc 100644 (file)
--- a/src/proof/lfsc/lfsc_print_channel.cpp
+++ b/src/proof/lfsc/lfsc_print_channel.cpp
@@ -79,7 +79,8 @@ void LfscPrintChannelOut::printNodeInternal(std::ostream& out, Node n)
 {
   // due to use of special names in the node converter, we must clean symbols
   std::stringstream ss;
-  n.toStream(ss, -1, 0, Language::LANG_SMTLIB_V2_6);
+  options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
+  n.toStream(ss, -1, 0);
   std::string s = ss.str();
   cleanSymbols(s);
   out << s;
@@ -89,7 +90,8 @@ void LfscPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn)
 {
   // due to use of special names in the node converter, we must clean symbols
   std::stringstream ss;
-  tn.toStream(ss, Language::LANG_SMTLIB_V2_6);
+  options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
+  tn.toStream(ss);
   std::string s = ss.str();
   cleanSymbols(s);
   out << s;

diff --git a/src/util/result.cpp b/src/util/result.cpp
index f424558be94652130c9d2f7c9c96f1ea0a2f6c00..20c0beae511ba8c7fa15e48d943086dc35b0c4d3 100644 (file)
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -289,7 +289,20 @@ ostream& operator<<(ostream& out, enum Result::UnknownExplanation e)
 }
 
 ostream& operator<<(ostream& out, const Result& r) {
-  r.toStream(out, options::ioutils::getOutputLang(out));
+  Language language = options::ioutils::getOutputLang(out);
+  switch (language) {
+    case Language::LANG_SYGUS_V2: r.toStreamSmt2(out); break;
+    case Language::LANG_TPTP: r.toStreamTptp(out); break;
+    default:
+      if (language::isLangSmt2(language))
+      {
+        r.toStreamSmt2(out);
+      }
+      else
+      {
+        r.toStreamDefault(out);
+      }
+  };
   return out;
 } /* operator<<(ostream&, const Result&) */
 
@@ -354,22 +367,4 @@ void Result::toStreamTptp(std::ostream& out) const {
   out << " for " << getInputName();
 }
 
-void Result::toStream(std::ostream& out, Language language) const
-{
-  switch (language) {
-    case Language::LANG_SYGUS_V2: toStreamSmt2(out); break;
-    case Language::LANG_TPTP: toStreamTptp(out); break;
-    default:
-      if (language::isLangSmt2(language))
-      {
-        toStreamSmt2(out);
-      }
-      else
-      {
-        toStreamDefault(out);
-      }
-      break;
-  };
-}
-
 }  // namespace cvc5

diff --git a/src/util/result.h b/src/util/result.h
index 251d3454881d249fae217c0c9abde694df866915..9bdc99319d0ea7ab49dfdd4c96a3819c7f0d1fa4 100644 (file)
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -119,11 +119,6 @@ class Result
 
   std::string getInputName() const { return d_inputName; }
 
-  /**
-   * Write a Result out to a stream in this language.
-   */
-  void toStream(std::ostream& out, Language language) const;
-
   /**
    * This is mostly the same the default
    * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN,