Add Solver::isOutputOn() (#7187)

This PR adds a new api::Solver::isOutputOn() method, including unit tests for both isOutputOn() and getOutput().

2 files changed, 22 insertions, 0 deletions

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
@@ -4353,6 +4353,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
    * when an invalid tag is given.