src/printer/printer.h

   1 /*********************                                                        */
   2 /*! \file printer.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing 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 "options/language.h"
  27 #include "smt/command.h"
  28 #include "smt/model.h"
  29 #include "util/sexpr.h"
  30
  31 namespace CVC4 {
  32
  33 class Printer
  34 {
  35  public:
  36   /**
  37    * Since the printers are managed as unique_ptr, we need public acces to
  38    * the virtual destructor.
  39    */
  40   virtual ~Printer() {}
  41
  42   /** Get the Printer for a given OutputLanguage */
  43   static Printer* getPrinter(OutputLanguage lang);
  44
  45   /** Write a Node out to a stream with this Printer. */
  46   virtual void toStream(std::ostream& out,
  47                         TNode n,
  48                         int toDepth,
  49                         bool types,
  50                         size_t dag) const = 0;
  51
  52   /** Write a Command out to a stream with this Printer. */
  53   virtual void toStream(std::ostream& out,
  54                         const Command* c,
  55                         int toDepth,
  56                         bool types,
  57                         size_t dag) const = 0;
  58
  59   /** Write a CommandStatus out to a stream with this Printer. */
  60   virtual void toStream(std::ostream& out, const CommandStatus* s) const = 0;
  61
  62   /** Write a Model out to a stream with this Printer. */
  63   virtual void toStream(std::ostream& out, const Model& m) const;
  64
  65   /** Write an UnsatCore out to a stream with this Printer. */
  66   virtual void toStream(std::ostream& out, const UnsatCore& core) const;
  67
  68   /**
  69    * Write the term that sygus datatype term n
  70    * encodes to a stream with this Printer.
  71    * For example, consider the datatype term
  72    *   (C_plus (C_minus C_x C_0) C_y)
  73    * where C_plus, C_minus, C_x, C_0, C_y are constructors
  74    * whose sygus operators are PLUS, MINUS, x, 0, y.
  75    * In this case, this method is equivalent to printing
  76    * the integer term:
  77    *   (PLUS (MINUS x 0) y)
  78    * This method may make calls to sygus printing callback
  79    * methods stored in sygus datatype constructors.
  80    */
  81   virtual void toStreamSygus(std::ostream& out, TNode n) const;
  82
  83  protected:
  84   /** Derived classes can construct, but no one else. */
  85   Printer() {}
  86
  87   /** write model response to command */
  88   virtual void toStream(std::ostream& out,
  89                         const Model& m,
  90                         const Command* c) const = 0;
  91
  92   /** write model response to command using another language printer */
  93   void toStreamUsing(OutputLanguage lang,
  94                      std::ostream& out,
  95                      const Model& m,
  96                      const Command* c) const
  97   {
  98     getPrinter(lang)->toStream(out, m, c);
  99   }
 100
 101  private:
 102   /** Disallow copy, assignment  */
 103   Printer(const Printer&) CVC4_UNDEFINED;
 104   Printer& operator=(const Printer&) CVC4_UNDEFINED;
 105
 106   /** Make a Printer for a given OutputLanguage */
 107   static std::unique_ptr<Printer> makePrinter(OutputLanguage lang);
 108
 109   /** Printers for each OutputLanguage */
 110   static std::unique_ptr<Printer> d_printers[language::output::LANG_MAX];
 111
 112 }; /* class Printer */
 113
 114 }  // namespace CVC4
 115
 116 #endif /* __CVC4__PRINTER__PRINTER_H */