src/printer/printer.h

   1 /*********************                                                        */
   2 /*! \file printer.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Base of the pretty-printer interface
  13  **
  14  ** Base of the pretty-printer interface.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__PRINTER__PRINTER_H
  20 #define __CVC4__PRINTER__PRINTER_H
  21
  22 #include <map>
  23 #include <string>
  24
  25 #include "expr/node.h"
  26 #include "expr/sexpr.h"
  27 #include "options/language.h"
  28 #include "smt_util/command.h"
  29 #include "smt_util/model.h"
  30
  31 namespace CVC4 {
  32
  33 class Printer {
  34   /** Printers for each OutputLanguage */
  35   static Printer* d_printers[language::output::LANG_MAX];
  36
  37   /** Make a Printer for a given OutputLanguage */
  38   static Printer* makePrinter(OutputLanguage lang) throw();
  39
  40   // disallow copy, assignment
  41   Printer(const Printer&) CVC4_UNUSED;
  42   Printer& operator=(const Printer&) CVC4_UNUSED;
  43
  44 protected:
  45   // derived classes can construct, but no one else.
  46   Printer() throw() {}
  47   virtual ~Printer() {}
  48
  49   /** write model response to command */
  50   virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0;
  51
  52   /** write model response to command using another language printer */
  53   void toStreamUsing(OutputLanguage lang, std::ostream& out, const Model& m, const Command* c) const throw() {
  54     getPrinter(lang)->toStream(out, m, c);
  55   }
  56
  57 public:
  58   /** Get the Printer for a given OutputLanguage */
  59   static Printer* getPrinter(OutputLanguage lang) throw() {
  60     if(lang == language::output::LANG_AUTO) {
  61       // Infer the language to use for output.
  62       //
  63       // Options can be null in certain circumstances (e.g., when printing
  64       // the singleton "null" expr.  So we guard against segfault
  65       if(not Options::isCurrentNull()) {
  66         if(options::outputLanguage.wasSetByUser()) {
  67           lang = options::outputLanguage();
  68         }
  69         if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) {
  70           lang = language::toOutputLanguage(options::inputLanguage());
  71         }
  72       }
  73       if(lang == language::output::LANG_AUTO) {
  74         lang = language::output::LANG_CVC4; // default
  75       }
  76     }
  77     if(d_printers[lang] == NULL) {
  78       d_printers[lang] = makePrinter(lang);
  79     }
  80     return d_printers[lang];
  81   }
  82
  83   /** Write a Node out to a stream with this Printer. */
  84   virtual void toStream(std::ostream& out, TNode n,
  85                         int toDepth, bool types, size_t dag) const throw() = 0;
  86
  87   /** Write a Command out to a stream with this Printer. */
  88   virtual void toStream(std::ostream& out, const Command* c,
  89                         int toDepth, bool types, size_t dag) const throw() = 0;
  90
  91   /** Write a CommandStatus out to a stream with this Printer. */
  92   virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
  93
  94
  95
  96   /** Write a Model out to a stream with this Printer. */
  97   virtual void toStream(std::ostream& out, const Model& m) const throw();
  98
  99   /** Write an UnsatCore out to a stream with this Printer. */
 100   virtual void toStream(std::ostream& out, const UnsatCore& core) const throw();
 101
 102   /** Write an UnsatCore out to a stream with this Printer. */
 103   virtual void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
 104
 105 };/* class Printer */
 106
 107 }/* CVC4 namespace */
 108
 109 #endif /* __CVC4__PRINTER__PRINTER_H */