summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/cvc/cvc_printer.cpp2
-rw-r--r--src/printer/printer.cpp56
-rw-r--r--src/printer/printer.h15
-rw-r--r--src/printer/smt2/smt2_printer.cpp2
-rw-r--r--src/printer/tptp/tptp_printer.cpp6
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback