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 "util/language.h"
  26 #include "util/sexpr.h"
  27 #include "util/model.h"
  28 #include "expr/node.h"
  29 #include "expr/command.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
  48   /** write model response to command */
  49   virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0;
  50
  51   /** write model response to command using another language printer */
  52   void toStreamUsing(OutputLanguage lang, std::ostream& out, const Model& m, const Command* c) const throw() {
  53     getPrinter(lang)->toStream(out, m, c);
  54   }
  55
  56 public:
  57   /** Get the Printer for a given OutputLanguage */
  58   static Printer* getPrinter(OutputLanguage lang) throw() {
  59     if(lang == language::output::LANG_AUTO) {
  60       // Infer the language to use for output.
  61       //
  62       // Options can be null in certain circumstances (e.g., when printing
  63       // the singleton "null" expr.  So we guard against segfault
  64       if(&Options::current() != NULL) {
  65         if(options::outputLanguage.wasSetByUser()) {
  66           lang = options::outputLanguage();
  67         }
  68         if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) {
  69           lang = language::toOutputLanguage(options::inputLanguage());
  70         }
  71       }
  72       if(lang == language::output::LANG_AUTO) {
  73         lang = language::output::LANG_CVC4; // default
  74       }
  75     }
  76     if(d_printers[lang] == NULL) {
  77       d_printers[lang] = makePrinter(lang);
  78     }
  79     return d_printers[lang];
  80   }
  81
  82   /** Write a Node out to a stream with this Printer. */
  83   virtual void toStream(std::ostream& out, TNode n,
  84                         int toDepth, bool types, size_t dag) const throw() = 0;
  85
  86   /** Write a Command out to a stream with this Printer. */
  87   virtual void toStream(std::ostream& out, const Command* c,
  88                         int toDepth, bool types, size_t dag) const throw() = 0;
  89
  90   /** Write a CommandStatus out to a stream with this Printer. */
  91   virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
  92
  93   /** Write an SExpr out to a stream with this Printer. */
  94   virtual void toStream(std::ostream& out, const SExpr& sexpr) const throw();
  95
  96   /**
  97    * Write a Result out to a stream with this Printer.
  98    *
  99    * The default implementation writes a reasonable string in lowercase
 100    * for sat, unsat, valid, invalid, or unknown results.  This behavior
 101    * is overridable by each Printer, since sometimes an output language
 102    * has a particular preference for how results should appear.
 103    */
 104   virtual void toStream(std::ostream& out, const Result& r) const throw();
 105
 106   /** Write a Model out to a stream with this Printer. */
 107   virtual void toStream(std::ostream& out, const Model& m) const throw();
 108
 109   /** Write an UnsatCore out to a stream with this Printer. */
 110   virtual void toStream(std::ostream& out, const UnsatCore& core) const throw();
 111
 112   /** Write an UnsatCore out to a stream with this Printer. */
 113   virtual void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
 114
 115 };/* class Printer */
 116
 117 /**
 118  * IOStream manipulator to pretty-print SExprs.
 119  */
 120 class PrettySExprs {
 121   /**
 122    * The allocated index in ios_base for our setting.
 123    */
 124   static const int s_iosIndex;
 125
 126   /**
 127    * When this manipulator is used, the setting is stored here.
 128    */
 129   bool d_prettySExprs;
 130
 131 public:
 132   /**
 133    * Construct a PrettySExprs with the given setting.
 134    */
 135   PrettySExprs(bool prettySExprs) : d_prettySExprs(prettySExprs) {}
 136
 137   inline void applyPrettySExprs(std::ostream& out) {
 138     out.iword(s_iosIndex) = d_prettySExprs;
 139   }
 140
 141   static inline bool getPrettySExprs(std::ostream& out) {
 142     return out.iword(s_iosIndex);
 143   }
 144
 145   static inline void setPrettySExprs(std::ostream& out, bool prettySExprs) {
 146     out.iword(s_iosIndex) = prettySExprs;
 147   }
 148
 149   /**
 150    * Set the pretty-sexprs state on the output stream for the current
 151    * stack scope.  This makes sure the old state is reset on the
 152    * stream after normal OR exceptional exit from the scope, using the
 153    * RAII C++ idiom.
 154    */
 155   class Scope {
 156     std::ostream& d_out;
 157     bool d_oldPrettySExprs;
 158
 159   public:
 160
 161     inline Scope(std::ostream& out, bool prettySExprs) :
 162       d_out(out),
 163       d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) {
 164       PrettySExprs::setPrettySExprs(out, prettySExprs);
 165     }
 166
 167     inline ~Scope() {
 168       PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs);
 169     }
 170
 171   };/* class PrettySExprs::Scope */
 172
 173 };/* class PrettySExprs */
 174
 175 /**
 176  * Sets the default pretty-sexprs setting for an ostream.  Use like this:
 177  *
 178  *   // let out be an ostream, s an SExpr
 179  *   out << PrettySExprs(true) << s << endl;
 180  *
 181  * The setting stays permanently (until set again) with the stream.
 182  */
 183 inline std::ostream& operator<<(std::ostream& out, PrettySExprs ps) {
 184   ps.applyPrettySExprs(out);
 185   return out;
 186 }
 187
 188 }/* CVC4 namespace */
 189
 190 #endif /* __CVC4__PRINTER__PRINTER_H */
 191