From: Gereon Kremer Date: Thu, 9 Sep 2021 17:34:43 +0000 (-0700) Subject: Add Solver::getOutput() (#7162) X-Git-Tag: cvc5-1.0.0~1246 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08d770f84c3959c076cc693de9e251e910e508a7;p=cvc5.git 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 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 ` 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(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;