diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 2 | ||||
-rw-r--r-- | src/printer/printer.cpp | 56 | ||||
-rw-r--r-- | src/printer/printer.h | 15 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
-rw-r--r-- | src/printer/tptp/tptp_printer.cpp | 6 |
5 files changed, 41 insertions, 40 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 11959f37b..b42304ecc 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -929,7 +929,7 @@ void CvcPrinter::toStreamNode(std::ostream& out, } toStreamNode(out, n[i], -1, false, lbind); out << ":"; - n[i].getType().toStream(out, language::output::LANG_CVC); + n[i].getType().toStream(out, Language::LANG_CVC); } out << ')'; return; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 69727e1a2..59122cf3d 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -31,32 +31,32 @@ using namespace std; namespace cvc5 { -unique_ptr<Printer> Printer::d_printers[language::output::LANG_MAX]; +unique_ptr<Printer> + Printer::d_printers[static_cast<size_t>(Language::LANG_MAX)]; -unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) +unique_ptr<Printer> Printer::makePrinter(Language lang) { - using namespace cvc5::language::output; - switch(lang) { - case LANG_SMTLIB_V2_6: - return unique_ptr<Printer>( - new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); + case Language::LANG_SMTLIB_V2_6: + return unique_ptr<Printer>( + new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); - case LANG_TPTP: - return unique_ptr<Printer>(new printer::tptp::TptpPrinter()); + case Language::LANG_TPTP: + return unique_ptr<Printer>(new printer::tptp::TptpPrinter()); - case LANG_CVC: return unique_ptr<Printer>(new printer::cvc::CvcPrinter()); + case Language::LANG_CVC: + return unique_ptr<Printer>(new printer::cvc::CvcPrinter()); - case LANG_SYGUS_V2: - // sygus version 2.0 does not have discrepancies with smt2, hence we use - // a normal smt2 variant here. - return unique_ptr<Printer>( - new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); + case Language::LANG_SYGUS_V2: + // sygus version 2.0 does not have discrepancies with smt2, hence we use + // a normal smt2 variant here. + return unique_ptr<Printer>( + new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); - case LANG_AST: - return unique_ptr<Printer>(new printer::ast::AstPrinter()); + case Language::LANG_AST: + return unique_ptr<Printer>(new printer::ast::AstPrinter()); - default: Unhandled() << lang; + default: Unhandled() << lang; } } @@ -83,7 +83,7 @@ void Printer::toStream(std::ostream& out, const smt::Model& m) const }/* Printer::toStream(Model) */ -void Printer::toStreamUsing(OutputLanguage lang, +void Printer::toStreamUsing(Language lang, std::ostream& out, const smt::Model& m) const { @@ -140,9 +140,9 @@ void Printer::toStream(std::ostream& out, const SkolemList& sks) const out << ")" << std::endl; } -Printer* Printer::getPrinter(OutputLanguage lang) +Printer* Printer::getPrinter(Language lang) { - if (lang == language::output::LANG_AUTO) + if (lang == Language::LANG_AUTO) { // Infer the language to use for output. // @@ -154,22 +154,22 @@ Printer* Printer::getPrinter(OutputLanguage lang) { lang = options::outputLanguage(); } - if (lang == language::output::LANG_AUTO + if (lang == Language::LANG_AUTO && Options::current().base.inputLanguageWasSetByUser) { - lang = language::toOutputLanguage(options::inputLanguage()); + lang = options::inputLanguage(); } } - if (lang == language::output::LANG_AUTO) + if (lang == Language::LANG_AUTO) { - lang = language::output::LANG_SMTLIB_V2_6; // default + lang = Language::LANG_SMTLIB_V2_6; // default } } - if (d_printers[lang] == nullptr) + if (d_printers[static_cast<size_t>(lang)] == nullptr) { - d_printers[lang] = makePrinter(lang); + d_printers[static_cast<size_t>(lang)] = makePrinter(lang); } - return d_printers[lang].get(); + return d_printers[static_cast<size_t>(lang)].get(); } void Printer::printUnknownCommand(std::ostream& out, diff --git a/src/printer/printer.h b/src/printer/printer.h index 6c00ebad5..05ac8879b 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -42,8 +42,8 @@ class Printer */ virtual ~Printer() {} - /** Get the Printer for a given OutputLanguage */ - static Printer* getPrinter(OutputLanguage lang); + /** Get the Printer for a given Language */ + static Printer* getPrinter(Language lang); /** Write a Node out to a stream with this Printer. */ virtual void toStream(std::ostream& out, @@ -286,7 +286,7 @@ class Printer Node n) const = 0; /** write model response to command using another language printer */ - void toStreamUsing(OutputLanguage lang, + void toStreamUsing(Language lang, std::ostream& out, const smt::Model& m) const; @@ -301,11 +301,12 @@ class Printer Printer(const Printer&) = delete; Printer& operator=(const Printer&) = delete; - /** Make a Printer for a given OutputLanguage */ - static std::unique_ptr<Printer> makePrinter(OutputLanguage lang); + /** Make a Printer for a given Language */ + static std::unique_ptr<Printer> makePrinter(Language lang); - /** Printers for each OutputLanguage */ - static std::unique_ptr<Printer> d_printers[language::output::LANG_MAX]; + /** Printers for each Language */ + static std::unique_ptr<Printer> + d_printers[static_cast<size_t>(Language::LANG_MAX)]; }; /* class Printer */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ba03a4fe8..b7f32123d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1204,7 +1204,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) void Smt2Printer::toStreamType(std::ostream& out, TypeNode tn) const { // we currently must call TypeNode::toStream here. - tn.toStream(out, language::output::LANG_SMTLIB_V2_6); + tn.toStream(out, Language::LANG_SMTLIB_V2_6); } template <class T> diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index 14bc6f220..bb8df120e 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -38,12 +38,12 @@ void TptpPrinter::toStream(std::ostream& out, int toDepth, size_t dag) const { - n.toStream(out, toDepth, dag, language::output::LANG_SMTLIB_V2_6); + n.toStream(out, toDepth, dag, Language::LANG_SMTLIB_V2_6); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const { - s->toStream(out, language::output::LANG_SMTLIB_V2_6); + s->toStream(out, Language::LANG_SMTLIB_V2_6); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const smt::Model& m) const @@ -52,7 +52,7 @@ void TptpPrinter::toStream(std::ostream& out, const smt::Model& m) const : "CandidateFiniteModel"); out << "% SZS output start " << statusName << " for " << m.getInputName() << endl; - this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_6, out, m); + this->Printer::toStreamUsing(Language::LANG_SMTLIB_V2_6, out, m); out << "% SZS output end " << statusName << " for " << m.getInputName() << endl; } |