src/printer/printer.h

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