diff options
| -rw-r--r-- | src/printer/printer.cpp | 39 | ||||
| -rw-r--r-- | src/printer/printer.h | 75 |
2 files changed, 63 insertions, 51 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 2ccac5e9f..e8ebadeb8 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -2,9 +2,9 @@ /*! \file printer.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds + ** Morgan Deters, Tim King, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -29,47 +29,52 @@ using namespace std; namespace CVC4 { -Printer* Printer::d_printers[language::output::LANG_MAX]; +unique_ptr<Printer> Printer::d_printers[language::output::LANG_MAX]; -Printer* Printer::makePrinter(OutputLanguage lang) +unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) { using namespace CVC4::language::output; switch(lang) { case LANG_SMTLIB_V1: // TODO the printer - return new printer::smt1::Smt1Printer(); + return unique_ptr<Printer>(new printer::smt1::Smt1Printer()); case LANG_SMTLIB_V2_0: - return new printer::smt2::Smt2Printer(printer::smt2::smt2_0_variant); + return unique_ptr<Printer>( + new printer::smt2::Smt2Printer(printer::smt2::smt2_0_variant)); case LANG_SMTLIB_V2_5: - return new printer::smt2::Smt2Printer(); - + return unique_ptr<Printer>(new printer::smt2::Smt2Printer()); + case LANG_SMTLIB_V2_6: - return new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant); + return unique_ptr<Printer>( + new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); case LANG_TPTP: - return new printer::tptp::TptpPrinter(); + return unique_ptr<Printer>(new printer::tptp::TptpPrinter()); case LANG_CVC4: - return new printer::cvc::CvcPrinter(); + return unique_ptr<Printer>(new printer::cvc::CvcPrinter()); case LANG_Z3STR: - return new printer::smt2::Smt2Printer(printer::smt2::z3str_variant); + return unique_ptr<Printer>( + new printer::smt2::Smt2Printer(printer::smt2::z3str_variant)); case LANG_SYGUS: - return new printer::smt2::Smt2Printer(printer::smt2::sygus_variant); + return unique_ptr<Printer>( + new printer::smt2::Smt2Printer(printer::smt2::sygus_variant)); case LANG_AST: - return new printer::ast::AstPrinter(); + return unique_ptr<Printer>(new printer::ast::AstPrinter()); case LANG_CVC3: - return new printer::cvc::CvcPrinter(/* cvc3-mode = */ true); + return unique_ptr<Printer>( + new printer::cvc::CvcPrinter(/* cvc3-mode = */ true)); default: Unhandled(lang); } -}/* Printer::makePrinter() */ +} void Printer::toStreamSygus(std::ostream& out, TNode n) const { @@ -121,7 +126,7 @@ Printer* Printer::getPrinter(OutputLanguage lang) if(d_printers[lang] == NULL) { d_printers[lang] = makePrinter(lang); } - return d_printers[lang]; + return d_printers[lang].get(); } diff --git a/src/printer/printer.h b/src/printer/printer.h index f5e05a848..29d4f5598 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -2,9 +2,9 @@ /*! \file printer.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Paul Meng + ** Morgan Deters, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -30,37 +30,15 @@ namespace CVC4 { -class Printer { - /** Printers for each OutputLanguage */ - static Printer* d_printers[language::output::LANG_MAX]; - - /** Make a Printer for a given OutputLanguage */ - static Printer* makePrinter(OutputLanguage lang); - - // disallow copy, assignment - Printer(const Printer&) CVC4_UNDEFINED; - Printer& operator=(const Printer&) CVC4_UNDEFINED; - -protected: - // derived classes can construct, but no one else. - Printer() {} - virtual ~Printer() {} - - /** write model response to command */ - virtual void toStream(std::ostream& out, - const Model& m, - const Command* c) const = 0; - - /** write model response to command using another language printer */ - void toStreamUsing(OutputLanguage lang, - std::ostream& out, - const Model& m, - const Command* c) const - { - getPrinter(lang)->toStream(out, m, c); - } - +class Printer +{ public: + /** + * Since the printers are managed as unique_ptr, we need public acces to + * the virtual destructor. + */ + virtual ~Printer() {} + /** Get the Printer for a given OutputLanguage */ static Printer* getPrinter(OutputLanguage lang); @@ -102,8 +80,37 @@ protected: */ virtual void toStreamSygus(std::ostream& out, TNode n) const; -};/* class Printer */ + protected: + /** Derived classes can construct, but no one else. */ + Printer() {} + + /** write model response to command */ + virtual void toStream(std::ostream& out, + const Model& m, + const Command* c) const = 0; + + /** write model response to command using another language printer */ + void toStreamUsing(OutputLanguage lang, + std::ostream& out, + const Model& m, + const Command* c) const + { + getPrinter(lang)->toStream(out, m, c); + } + + private: + /** Disallow copy, assignment */ + Printer(const Printer&) CVC4_UNDEFINED; + Printer& operator=(const Printer&) CVC4_UNDEFINED; + + /** Make a Printer for a given OutputLanguage */ + static std::unique_ptr<Printer> makePrinter(OutputLanguage lang); + + /** Printers for each OutputLanguage */ + static std::unique_ptr<Printer> d_printers[language::output::LANG_MAX]; + +}; /* class Printer */ -}/* CVC4 namespace */ +} // namespace CVC4 #endif /* __CVC4__PRINTER__PRINTER_H */ |