Add Solver::getOutput() (#7162)

Allow access to the Output() macro via the API.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d41af938a7dc090a409f43ee717f18e0cd8e8ed6..b1fb803362d4a32d22e255f49fd083d88a0bb6f9 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -60,6 +60,7 @@
 #include "options/option_exception.h"
 #include "options/options.h"
 #include "options/options_public.h"
+#include "options/outputc.h"
 #include "options/smt_options.h"
 #include "proof/unsat_core.h"
 #include "smt/model.h"
@@ -7937,6 +7938,21 @@ Statistics Solver::getStatistics() const
   return Statistics(d_smtEngine->getStatisticsRegistry());
 }
 
+std::ostream& Solver::getOutput(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 Output(tag);
+  }
+  catch (const cvc5::Exception& e)
+  {
+    throw CVC5ApiException("Invalid output tag " + tag);
+  }
+}
+
 }  // namespace api
 
 }  // namespace cvc5

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index a221f37116763b565e8a4575b5de471d178f5d78..e02506d9c094a83d2bb65ca8b2193d4b395f09c7 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;
 
+  /**
+   * 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.
+   */
+  std::ostream& getOutput(const std::string& tag) const;
+
  private:
   /** @return the node manager of this solver */
   NodeManager* getNodeManager(void) const;

diff --git a/src/options/outputc.cpp b/src/options/outputc.cpp
index e145191237264b497f847f87880c714eeef04a1d..43c9ced97639c6398a5251c2e98bd613af59402f 100644 (file)
--- a/src/options/outputc.cpp
+++ b/src/options/outputc.cpp
@@ -18,6 +18,11 @@ Cvc5ostream OutputC::operator()(const options::OutputTag tag) const
   }
 }
 
+Cvc5ostream OutputC::operator()(const std::string& tag) const
+{
+  return (*this)(options::stringToOutputTag(tag));
+}
+
 bool OutputC::isOn(const options::OutputTag tag) const
 {
   return options::outputTagHolder()[static_cast<size_t>(tag)];

diff --git a/src/options/outputc.h b/src/options/outputc.h
index 647b891db5c18b8b76fa3940ec6c72d1c3d94c0e..d96468e40ffd5173ca611d7cb3fb7b7868693a3f 100644 (file)
--- a/src/options/outputc.h
+++ b/src/options/outputc.h
@@ -17,6 +17,7 @@ class OutputC
   explicit OutputC(std::ostream* os) : d_os(os) {}
 
   Cvc5ostream operator()(const options::OutputTag tag) const;
+  Cvc5ostream operator()(const std::string& tag) const;
 
   bool isOn(const options::OutputTag tag) const;