src/printer/printer.h

   1 /*********************                                                        */
   2 /*! \file printer.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Andrew Reynolds, Aina Niemetz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 NodeCommand;
  34
  35 class Printer
  36 {
  37  public:
  38   /**
  39    * Since the printers are managed as unique_ptr, we need public acces to
  40    * the virtual destructor.
  41    */
  42   virtual ~Printer() {}
  43
  44   /** Get the Printer for a given OutputLanguage */
  45   static Printer* getPrinter(OutputLanguage lang);
  46
  47   /** Write a Node out to a stream with this Printer. */
  48   virtual void toStream(std::ostream& out,
  49                         TNode n,
  50                         int toDepth,
  51                         bool types,
  52                         size_t dag) const = 0;
  53
  54   /** Write a CommandStatus out to a stream with this Printer. */
  55   virtual void toStream(std::ostream& out, const CommandStatus* s) const = 0;
  56
  57   /** Write a Model out to a stream with this Printer. */
  58   virtual void toStream(std::ostream& out, const Model& m) const;
  59
  60   /** Write an UnsatCore out to a stream with this Printer. */
  61   virtual void toStream(std::ostream& out, const UnsatCore& core) const;
  62
  63   /** Print empty command */
  64   virtual void toStreamCmdEmpty(std::ostream& out,
  65                                 const std::string& name) const;
  66
  67   /** Print echo command */
  68   virtual void toStreamCmdEcho(std::ostream& out,
  69                                const std::string& output) const;
  70
  71   /** Print assert command */
  72   virtual void toStreamCmdAssert(std::ostream& out, Node n) const;
  73
  74   /** Print push command */
  75   virtual void toStreamCmdPush(std::ostream& out) const;
  76
  77   /** Print pop command */
  78   virtual void toStreamCmdPop(std::ostream& out) const;
  79
  80   /** Print declare-fun command */
  81   virtual void toStreamCmdDeclareFunction(std::ostream& out,
  82                                           const std::string& id,
  83                                           TypeNode type) const;
  84
  85   /** Print declare-sort command */
  86   virtual void toStreamCmdDeclareType(std::ostream& out,
  87                                       const std::string& id,
  88                                       size_t arity,
  89                                       TypeNode type) const;
  90
  91   /** Print define-sort command */
  92   virtual void toStreamCmdDefineType(std::ostream& out,
  93                                      const std::string& id,
  94                                      const std::vector<TypeNode>& params,
  95                                      TypeNode t) const;
  96
  97   /** Print define-fun command */
  98   virtual void toStreamCmdDefineFunction(std::ostream& out,
  99                                          const std::string& id,
 100                                          const std::vector<Node>& formals,
 101                                          TypeNode range,
 102                                          Node formula) const;
 103
 104   /** Print define-named-fun command */
 105   virtual void toStreamCmdDefineNamedFunction(std::ostream& out,
 106                                               const std::string& id,
 107                                               const std::vector<Node>& formals,
 108                                               TypeNode range,
 109                                               Node formula) const;
 110
 111   /** Print define-fun-rec command */
 112   virtual void toStreamCmdDefineFunctionRec(
 113       std::ostream& out,
 114       const std::vector<Node>& funcs,
 115       const std::vector<std::vector<Node>>& formals,
 116       const std::vector<Node>& formulas) const;
 117
 118   /** Print set-user-attribute command */
 119   void toStreamCmdSetUserAttribute(std::ostream& out,
 120                                    const std::string& attr,
 121                                    Node n) const;
 122
 123   /** Print check-sat command */
 124   virtual void toStreamCmdCheckSat(std::ostream& out,
 125                                    Node n = Node::null()) const;
 126
 127   /** Print check-sat-assuming command */
 128   virtual void toStreamCmdCheckSatAssuming(
 129       std::ostream& out, const std::vector<Node>& nodes) const;
 130
 131   /** Print query command */
 132   virtual void toStreamCmdQuery(std::ostream& out, Node n) const;
 133
 134   /** Print declare-var command */
 135   virtual void toStreamCmdDeclareVar(std::ostream& out,
 136                                      Node var,
 137                                      TypeNode type) const;
 138
 139   /** Print synth-fun command */
 140   virtual void toStreamCmdSynthFun(std::ostream& out,
 141                                    const std::string& sym,
 142                                    const std::vector<Node>& vars,
 143                                    TypeNode range,
 144                                    bool isInv,
 145                                    TypeNode sygusType) const;
 146
 147   /** Print constraint command */
 148   virtual void toStreamCmdConstraint(std::ostream& out, Node n) const;
 149
 150   /** Print inv-constraint command */
 151   virtual void toStreamCmdInvConstraint(
 152       std::ostream& out, Node inv, Node pre, Node trans, Node post) const;
 153
 154   /** Print check-synth command */
 155   virtual void toStreamCmdCheckSynth(std::ostream& out) const;
 156
 157   /** Print simplify command */
 158   virtual void toStreamCmdSimplify(std::ostream& out, Node n) const;
 159
 160   /** Print expand-definitions command */
 161   void toStreamCmdExpandDefinitions(std::ostream& out, Node n) const;
 162
 163   /** Print get-value command */
 164   virtual void toStreamCmdGetValue(std::ostream& out,
 165                                    const std::vector<Node>& nodes) const;
 166
 167   /** Print get-assignment command */
 168   virtual void toStreamCmdGetAssignment(std::ostream& out) const;
 169
 170   /** Print get-model command */
 171   virtual void toStreamCmdGetModel(std::ostream& out) const;
 172
 173   /** Print block-model command */
 174   void toStreamCmdBlockModel(std::ostream& out) const;
 175
 176   /** Print block-model-values command */
 177   void toStreamCmdBlockModelValues(std::ostream& out,
 178                                    const std::vector<Node>& nodes) const;
 179
 180   /** Print get-proof command */
 181   virtual void toStreamCmdGetProof(std::ostream& out) const;
 182
 183   /** Print get-instantiations command */
 184   void toStreamCmdGetInstantiations(std::ostream& out) const;
 185
 186   /** Print get-synth-solution command */
 187   void toStreamCmdGetSynthSolution(std::ostream& out) const;
 188
 189   /** Print get-interpol command */
 190   void toStreamCmdGetInterpol(std::ostream& out,
 191                               const std::string& name,
 192                               Node conj,
 193                               TypeNode sygusType) const;
 194
 195   /** Print get-abduct command */
 196   virtual void toStreamCmdGetAbduct(std::ostream& out,
 197                                     const std::string& name,
 198                                     Node conj,
 199                                     TypeNode sygusType) const;
 200
 201   /** Print get-quantifier-elimination command */
 202   void toStreamCmdGetQuantifierElimination(std::ostream& out, Node n) const;
 203
 204   /** Print get-unsat-assumptions command */
 205   virtual void toStreamCmdGetUnsatAssumptions(std::ostream& out) const;
 206
 207   /** Print get-unsat-core command */
 208   virtual void toStreamCmdGetUnsatCore(std::ostream& out) const;
 209
 210   /** Print get-assertions command */
 211   virtual void toStreamCmdGetAssertions(std::ostream& out) const;
 212
 213   /** Print set-info :status command */
 214   virtual void toStreamCmdSetBenchmarkStatus(std::ostream& out,
 215                                              BenchmarkStatus status) const;
 216
 217   /** Print set-logic command */
 218   virtual void toStreamCmdSetBenchmarkLogic(std::ostream& out,
 219                                             const std::string& logic) const;
 220
 221   /** Print set-info command */
 222   virtual void toStreamCmdSetInfo(std::ostream& out,
 223                                   const std::string& flag,
 224                                   SExpr sexpr) const;
 225
 226   /** Print get-info command */
 227   virtual void toStreamCmdGetInfo(std::ostream& out,
 228                                   const std::string& flag) const;
 229
 230   /** Print set-option command */
 231   virtual void toStreamCmdSetOption(std::ostream& out,
 232                                     const std::string& flag,
 233                                     SExpr sexpr) const;
 234
 235   /** Print get-option command */
 236   virtual void toStreamCmdGetOption(std::ostream& out,
 237                                     const std::string& flag) const;
 238
 239   /** Print set-expression-name command */
 240   void toStreamCmdSetExpressionName(std::ostream& out,
 241                                     Node n,
 242                                     const std::string& name) const;
 243
 244   /** Print declare-datatype(s) command */
 245   virtual void toStreamCmdDatatypeDeclaration(
 246       std::ostream& out, const std::vector<TypeNode>& datatypes) const;
 247
 248   /** Print reset command */
 249   virtual void toStreamCmdReset(std::ostream& out) const;
 250
 251   /** Print reset-assertions command */
 252   virtual void toStreamCmdResetAssertions(std::ostream& out) const;
 253
 254   /** Print quit command */
 255   virtual void toStreamCmdQuit(std::ostream& out) const;
 256
 257   /** Print comment command */
 258   virtual void toStreamCmdComment(std::ostream& out,
 259                                   const std::string& comment) const;
 260
 261   /** Print command sequence command */
 262   virtual void toStreamCmdCommandSequence(
 263       std::ostream& out, const std::vector<Command*>& sequence) const;
 264
 265   /** Print declaration sequence command */
 266   virtual void toStreamCmdDeclarationSequence(
 267       std::ostream& out, const std::vector<Command*>& sequence) const;
 268
 269  protected:
 270   /** Derived classes can construct, but no one else. */
 271   Printer() {}
 272
 273   /** write model response to command */
 274   virtual void toStream(std::ostream& out,
 275                         const Model& m,
 276                         const NodeCommand* c) const = 0;
 277
 278   /** write model response to command using another language printer */
 279   void toStreamUsing(OutputLanguage lang,
 280                      std::ostream& out,
 281                      const Model& m,
 282                      const NodeCommand* c) const
 283   {
 284     getPrinter(lang)->toStream(out, m, c);
 285   }
 286
 287   /**
 288    * Write an error to `out` stating that command `name` is not supported by
 289    * this printer.
 290    */
 291   void printUnknownCommand(std::ostream& out, const std::string& name) const;
 292
 293  private:
 294   /** Disallow copy, assignment  */
 295   Printer(const Printer&) = delete;
 296   Printer& operator=(const Printer&) = delete;
 297
 298   /** Make a Printer for a given OutputLanguage */
 299   static std::unique_ptr<Printer> makePrinter(OutputLanguage lang);
 300
 301   /** Printers for each OutputLanguage */
 302   static std::unique_ptr<Printer> d_printers[language::output::LANG_MAX];
 303
 304 }; /* class Printer */
 305
 306 }  // namespace CVC4
 307
 308 #endif /* CVC4__PRINTER__PRINTER_H */