diff options
Diffstat (limited to 'src/options/outputc.cpp')
| -rw-r--r-- | src/options/outputc.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
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)]; |