2 files changed, 46 insertions, 0 deletions
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index c77b8cfba..0ffe1c4b9 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -135,6 +135,27 @@ const Printer& Env::getPrinter()
 
 std::ostream& Env::getDumpOut() { return *d_options.base.out; }
 
+bool Env::isOutputOn(options::OutputTag tag) const
+{
+  return d_options.base.outputTagHolder[static_cast<size_t>(tag)];
+}
+bool Env::isOutputOn(const std::string& tag) const
+{
+  return isOutputOn(options::stringToOutputTag(tag));
+}
+std::ostream& Env::getOutput(options::OutputTag tag) const
+{
+  if (isOutputOn(tag))
+  {
+    return *d_options.base.out;
+  }
+  return cvc5::null_os;
+}
+std::ostream& Env::getOutput(const std::string& tag) const
+{
+  return getOutput(options::stringToOutputTag(tag));
+}
+
 Node Env::evaluate(TNode n,
                    const std::vector<Node>& args,
                    const std::vector<Node>& vals,
diff --git a/src/smt/env.h b/src/smt/env.h
index 2f2fe19ce..426749f5c 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -21,6 +21,7 @@
 
 #include <memory>
 
+#include "options/base_options.h"
 #include "options/options.h"
 #include "proof/method_id.h"
 #include "theory/logic_info.h"
@@ -139,6 +140,30 @@ class Env
    */
   std::ostream& getDumpOut();
 
+  /**
+   * Check whether the output for the given output tag is enabled. Output tags
+   * are enabled via the `output` option (or `-o` on the command line).
+   */
+  bool isOutputOn(options::OutputTag tag) const;
+  /**
+   * Check whether the output for the given output tag (as a string) is enabled.
+   * Output tags are enabled via the `output` option (or `-o` on the command
+   * line).
+   */
+  bool isOutputOn(const std::string& tag) const;
+  /**
+   * Return the output stream for the given output tag. If the output tag is
+   * enabled, this returns the output stream from the `out` option. Otherwise,
+   * a null stream (`cvc5::null_os`) is returned.
+   */
+  std::ostream& getOutput(options::OutputTag tag) const;
+  /**
+   * Return the output stream for the given output tag (as a string). If the
+   * output tag is enabled, this returns the output stream from the `out`
+   * option. Otherwise, a null stream (`cvc5::null_os`) is returned.
+   */
+  std::ostream& getOutput(const std::string& tag) const;
+
   /* Rewrite helpers--------------------------------------------------------- */
   /**
    * Evaluate node n under the substitution args -> vals. For details, see