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