Printers are now managed as unique_ptr (fix mem leak). (#1654)

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 2ccac5e9f9b0fc912a0ebcd455492f3e9c068a46..e8ebadeb87179b2565580c967ecbf0c04e2d89c9 100644 (file)
--- 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 f5e05a848d8813e200d190d2bc421fd6bd1b1e9d..29d4f5598a670bea92ca8c0e9d8199b6ad63ec61 100644 (file)
--- 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 */