Add Solver::isOutputOn() (#7187)

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

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index b1fb803362d4a32d22e255f49fd083d88a0bb6f9..1aa9a740fa452d571c601ffa8092f0a68c5ad651 100644 (file)
--- 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 e02506d9c094a83d2bb65ca8b2193d4b395f09c7..9324e42091a96cda3e7a34f5ee9c873425984ff9 100644 (file)
--- 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 43c9ced97639c6398a5251c2e98bd613af59402f..d9b7b346b35cd861706e8b3c0d2cfaa8ac4010e7 100644 (file)
--- 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 d96468e40ffd5173ca611d7cb3fb7b7868693a3f..7ad7cea7668669fc9c89235edc1c4b235711c295 100644 (file)
--- 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 e7d7c0bb4d8c6570e52e996247b951a0803bad18..75cd970607432c3566cbbe55bef719593f39a4dd 100644 (file)
--- 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