Support the SMT-LIB Unicode string standard by default (#4378)

[cvc5.git] / src / printer / printer.h

diff --git a/src/printer/printer.h b/src/printer/printer.h
index f5e05a848d8813e200d190d2bc421fd6bd1b1e9d..85b7d498f53b387d2bb54527d37f6a6157a96fb3 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
+ **   Tim King, Morgan Deters, 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-2019 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
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PRINTER__PRINTER_H
-#define __CVC4__PRINTER__PRINTER_H
+#ifndef CVC4__PRINTER__PRINTER_H
+#define CVC4__PRINTER__PRINTER_H
 
 #include <map>
 #include <string>
@@ -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&) = delete;
+  Printer& operator=(const Printer&) = delete;
+
+  /** 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 */
+#endif /* CVC4__PRINTER__PRINTER_H */