/********************* */
/*! \file printer.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** 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
**
** \brief Base of the pretty-printer interface
**
#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>
#include "expr/node.h"
-#include "expr/sexpr.h"
#include "options/language.h"
-#include "smt_util/command.h"
-#include "smt_util/model.h"
+#include "smt/command.h"
+#include "smt/model.h"
+#include "util/sexpr.h"
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_UNUSED;
- Printer& operator=(const Printer&) CVC4_UNUSED;
-
-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 */
projects / cvc5.git / blobdiff