From 3a67082f2155760917e72efbd08d15af9d06ab13 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Mon, 13 Sep 2021 21:21:50 +0200
Subject: [PATCH] Add Solver::isOutputOn() (#7187)

This PR adds a new api::Solver::isOutputOn() method, including unit tests for both isOutputOn() and getOutput().
---
 src/api/cpp/cvc5.cpp           | 15 +++++++++++++++
 src/api/cpp/cvc5.h             |  7 +++++++
 src/options/outputc.cpp        |  4 ++++
 src/options/outputc.h          |  1 +
 test/unit/api/solver_black.cpp | 12 ++++++++++++
 5 files changed, 39 insertions(+)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index b1fb80336..1aa9a740f 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7938,6 +7938,21 @@ Statistics Solver::getStatistics() const
   return Statistics(d_smtEngine->getStatisticsRegistry());
 }
 
+bool Solver::isOutputOn(const std::string& tag) const
+{
+  // `Output(tag)` may raise an `OptionException`, which we do not want to
+  // forward as such. We thus do not use the standard exception handling macros
+  // here but roll our own.
+  try
+  {
+    return cvc5::OutputChannel.isOn(tag);
+  }
+  catch (const cvc5::Exception& e)
+  {
+    throw CVC5ApiException("Invalid output tag " + tag);
+  }
+}
+
 std::ostream& Solver::getOutput(const std::string& tag) const
 {
   // `Output(tag)` may raise an `OptionException`, which we do not want to
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index e02506d9c..9324e4209 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4352,6 +4352,13 @@ class CVC5_EXPORT Solver
    */
   Statistics getStatistics() const;
 
+  /**
+   * Whether the output stream for the given tag is enabled. Tags can be enabled
+   * with the `output` option (and `-o <tag>` on the command line). Raises an
+   * exception when an invalid tag is given.
+   */
+  bool isOutputOn(const std::string& tag) const;
+
   /**
    * Returns an output stream for the given tag. Tags can be enabled with the
    * `output` option (and `-o <tag>` on the command line). Raises an exception
diff --git a/src/options/outputc.cpp b/src/options/outputc.cpp
index 43c9ced97..d9b7b346b 100644
--- a/src/options/outputc.cpp
+++ b/src/options/outputc.cpp
@@ -27,5 +27,9 @@ bool OutputC::isOn(const options::OutputTag tag) const
 {
   return options::outputTagHolder()[static_cast<size_t>(tag)];
 }
+bool OutputC::isOn(const std::string& tag) const
+{
+  return (*this).isOn(options::stringToOutputTag(tag));
+}
 
 }  // namespace cvc5
diff --git a/src/options/outputc.h b/src/options/outputc.h
index d96468e40..7ad7cea76 100644
--- a/src/options/outputc.h
+++ b/src/options/outputc.h
@@ -20,6 +20,7 @@ class OutputC
   Cvc5ostream operator()(const std::string& tag) const;
 
   bool isOn(const options::OutputTag tag) const;
+  bool isOn(const std::string& tag) const;
 
  private:
   std::ostream* d_os;
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index e7d7c0bb4..75cd97060 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -16,6 +16,7 @@
 #include <algorithm>
 
 #include "test_api.h"
+#include "base/output.h"
 
 namespace cvc5 {
 
@@ -2474,5 +2475,16 @@ TEST_F(TestApiBlackSolver, tupleProject)
       projection.toString());
 }
 
+TEST_F(TestApiBlackSolver, Output)
+{
+  ASSERT_THROW(d_solver.isOutputOn("foo-invalid"), CVC5ApiException);
+  ASSERT_THROW(d_solver.getOutput("foo-invalid"), CVC5ApiException);
+  ASSERT_FALSE(d_solver.isOutputOn("inst"));
+  ASSERT_EQ(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf());
+  d_solver.setOption("output", "inst");
+  ASSERT_TRUE(d_solver.isOutputOn("inst"));
+  ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf());
+}
+
 }  // namespace test
 }  // namespace cvc5
-- 
2.30.2