From: Gereon Kremer Date: Tue, 23 Nov 2021 19:04:46 +0000 (-0800) Subject: Push output language inside the printing code (#7683) X-Git-Tag: cvc5-1.0.0~782 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=20e2df18b5427bdc3b59ade5b0711c78b677cef9;p=cvc5.git 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 bd5f8c605..3a4706e1e 100644 --- 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 3d51cbbbe..d38447f21 100644 --- 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 cf24a207d..a0237a106 100644 --- 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 c8a0d9ce2..e94d4733e 100644 --- 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 95b3895ee..33d698163 100644 --- 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 fe464a8bd..13477b792 100644 --- 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 diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index fe44becb6..ef94bf54f 100644 --- 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 7f1d9e192..6eab9b036 100644 --- 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 36fd8831b..47961062e 100644 --- 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 f424558be..20c0beae5 100644 --- 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 251d34548..9bdc99319 100644 --- 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,