From 08d770f84c3959c076cc693de9e251e910e508a7 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 9 Sep 2021 10:34:43 -0700
Subject: [PATCH] Add Solver::getOutput() (#7162)

Allow access to the Output() macro via the API.
---
 src/api/cpp/cvc5.cpp    | 16 ++++++++++++++++
 src/api/cpp/cvc5.h      |  7 +++++++
 src/options/outputc.cpp |  5 +++++
 src/options/outputc.h   |  1 +
 4 files changed, 29 insertions(+)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d41af938a..b1fb80336 100644
--- 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 a221f3711..e02506d9c 100644
--- 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 e14519123..43c9ced97 100644
--- 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 647b891db..d96468e40 100644
--- 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;
 
-- 
2.30.2