Refactor IO stream manipulators (#7555)

This PR consolidates SetLanguage, ExprSetDepth and ExprDag into a single consistent utility. Also, it makes it play more nicely with users setting these options and removes some obsolete code.

4 files changed, 17 insertions, 13 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 283925903..c3ceffc4e 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -26,10 +26,10 @@
 #include "base/check.h"
 #include "base/modal_exception.h"
 #include "base/output.h"
-#include "expr/expr_iomanip.h"
 #include "expr/node.h"
 #include "expr/symbol_manager.h"
 #include "expr/type_node.h"
+#include "options/io_utils.h"
 #include "options/main_options.h"
 #include "options/options.h"
 #include "options/printer_options.h"
@@ -85,9 +85,9 @@ const CommandInterrupted* CommandInterrupted::s_instance =
 std::ostream& operator<<(std::ostream& out, const Command& c)
 {
   c.toStream(out,
-             Node::setdepth::getDepth(out),
-             Node::dag::getDag(out),
-             Node::setlanguage::getLanguage(out));
+             options::ioutils::getNodeDepth(out),
+             options::ioutils::getDagThresh(out),
+             options::ioutils::getOutputLang(out));
   return out;
 }
 
@@ -106,7 +106,7 @@ ostream& operator<<(ostream& out, const Command* c)
 
 std::ostream& operator<<(std::ostream& out, const CommandStatus& s)
 {
-  s.toStream(out, Node::setlanguage::getLanguage(out));
+  s.toStream(out, options::ioutils::getOutputLang(out));
   return out;
 }
 
@@ -1593,7 +1593,8 @@ void GetValueCommand::printResult(std::ostream& out) const
   }
   else
   {
-    expr::ExprDag::Scope scope(out, false);
+    options::ioutils::Scope scope(out);
+    options::ioutils::applyDagThresh(out, 0);
     out << d_result << endl;
   }
 }
@@ -2014,7 +2015,8 @@ void GetInterpolCommand::printResult(std::ostream& out) const
   }
   else
   {
-    expr::ExprDag::Scope scope(out, false);
+    options::ioutils::Scope scope(out);
+    options::ioutils::applyDagThresh(out, 0);
     if (d_resultStatus)
     {
       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
@@ -2103,7 +2105,8 @@ void GetAbductCommand::printResult(std::ostream& out) const
   }
   else
   {
-    expr::ExprDag::Scope scope(out, false);
+    options::ioutils::Scope scope(out);
+    options::ioutils::applyDagThresh(out, 0);
     if (d_resultStatus)
     {
       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index 9a195cb51..5c427fa46 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -15,8 +15,8 @@
 
 #include "smt/model.h"
 
-#include "expr/expr_iomanip.h"
 #include "options/base_options.h"
+#include "options/io_utils.h"
 #include "printer/printer.h"
 
 namespace cvc5 {
@@ -28,7 +28,8 @@ Model::Model(bool isKnownSat, const std::string& inputName)
 }
 
 std::ostream& operator<<(std::ostream& out, const Model& m) {
-  expr::ExprDag::Scope scope(out, false);
+  options::ioutils::Scope scope(out);
+  options::ioutils::applyDagThresh(out, 0);
   Printer::getPrinter(options::outputLanguage())->toStream(out, m);
   return out;
 }
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index 30c338d65..77157625a 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -19,6 +19,7 @@
 #include "context/cdlist.h"
 #include "omt/omt_optimizer.h"
 #include "options/base_options.h"
+#include "options/io_utils.h"
 #include "options/language.h"
 #include "options/smt_options.h"
 #include "smt/assertions.h"
@@ -34,7 +35,7 @@ namespace smt {
 std::ostream& operator<<(std::ostream& out, const OptimizationResult& result)
 {
   // check the output language first
-  Language lang = language::SetLanguage::getLanguage(out);
+  Language lang = options::ioutils::getOutputLang(out);
   if (!language::isLangSmt2(lang))
   {
     Unimplemented()
@@ -68,7 +69,7 @@ std::ostream& operator<<(std::ostream& out,
                          const OptimizationObjective& objective)
 {
   // check the output language first
-  Language lang = language::SetLanguage::getLanguage(out);
+  Language lang = options::ioutils::getOutputLang(out);
   if (!language::isLangSmt2(lang))
   {
     Unimplemented()
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 895e41c96..b2fe2b5d6 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -33,7 +33,6 @@
 #include "options/prop_options.h"
 #include "options/quantifiers_options.h"
 #include "options/sep_options.h"
-#include "options/set_language.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"
 #include "options/theory_options.h"