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 a6156ad161a1541631e8797b1c7c263ffdb3493d..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, Andrew Reynolds
+ **   Tim King, Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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,58 +30,87 @@
 
 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) throw();
-
-  // disallow copy, assignment
-  Printer(const Printer&) CVC4_UNDEFINED;
-  Printer& operator=(const Printer&) CVC4_UNDEFINED;
-
-protected:
-  // derived classes can construct, but no one else.
-  Printer() throw() {}
+class Printer
+{
+ public:
+  /**
+   * Since the printers are managed as unique_ptr, we need public acces to
+   * the virtual destructor.
+   */
   virtual ~Printer() {}
 
-  /** write model response to command */
-  virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0;
-
-  /** write model response to command using another language printer */
-  void toStreamUsing(OutputLanguage lang, std::ostream& out, const Model& m, const Command* c) const throw() {
-    getPrinter(lang)->toStream(out, m, c);
-  }
-
-public:
   /** Get the Printer for a given OutputLanguage */
-  static Printer* getPrinter(OutputLanguage lang) throw();
+  static Printer* getPrinter(OutputLanguage lang);
 
   /** Write a Node out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, TNode n,
-                        int toDepth, bool types, size_t dag) const throw() = 0;
+  virtual void toStream(std::ostream& out,
+                        TNode n,
+                        int toDepth,
+                        bool types,
+                        size_t dag) const = 0;
 
   /** Write a Command out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, const Command* c,
-                        int toDepth, bool types, size_t dag) const throw() = 0;
+  virtual void toStream(std::ostream& out,
+                        const Command* c,
+                        int toDepth,
+                        bool types,
+                        size_t dag) const = 0;
 
   /** Write a CommandStatus out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
-
-
+  virtual void toStream(std::ostream& out, const CommandStatus* s) const = 0;
 
   /** Write a Model out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, const Model& m) const throw();
+  virtual void toStream(std::ostream& out, const Model& m) const;
 
   /** Write an UnsatCore out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, const UnsatCore& core) const throw();
+  virtual void toStream(std::ostream& out, const UnsatCore& core) const;
+
+  /**
+   * Write the term that sygus datatype term n
+   * encodes to a stream with this Printer.
+   * For example, consider the datatype term
+   *   (C_plus (C_minus C_x C_0) C_y)
+   * where C_plus, C_minus, C_x, C_0, C_y are constructors
+   * whose sygus operators are PLUS, MINUS, x, 0, y.
+   * In this case, this method is equivalent to printing
+   * the integer term:
+   *   (PLUS (MINUS x 0) y)
+   * This method may make calls to sygus printing callback
+   * methods stored in sygus datatype constructors.
+   */
+  virtual void toStreamSygus(std::ostream& out, TNode n) const;
+
+ protected:
+  /** Derived classes can construct, but no one else. */
+  Printer() {}
 
-  /** Write an UnsatCore out to a stream with this Printer. */
-  virtual void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
+  /** 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 */
+}; /* class Printer */
 
-}/* CVC4 namespace */
+}  // namespace CVC4
 
-#endif /* __CVC4__PRINTER__PRINTER_H */
+#endif /* CVC4__PRINTER__PRINTER_H */