src/printer/printer.h

   1 /*********************                                                        */
   2 /*! \file printer.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Abdalrhman Mohamed, 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/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                                       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-fun-rec command */
 105   virtual void toStreamCmdDefineFunctionRec(
 106       std::ostream& out,
 107       const std::vector<Node>& funcs,
 108       const std::vector<std::vector<Node>>& formals,
 109       const std::vector<Node>& formulas) const;
 110
 111   /** Print set-user-attribute command */
 112   void toStreamCmdSetUserAttribute(std::ostream& out,
 113                                    const std::string& attr,
 114                                    Node n) const;
 115
 116   /** Print check-sat command */
 117   virtual void toStreamCmdCheckSat(std::ostream& out,
 118                                    Node n = Node::null()) const;
 119
 120   /** Print check-sat-assuming command */
 121   virtual void toStreamCmdCheckSatAssuming(
 122       std::ostream& out, const std::vector<Node>& nodes) const;
 123
 124   /** Print query command */
 125   virtual void toStreamCmdQuery(std::ostream& out, Node n) const;
 126
 127   /** Print declare-var command */
 128   virtual void toStreamCmdDeclareVar(std::ostream& out,
 129                                      Node var,
 130                                      TypeNode type) const;
 131
 132   /** Print synth-fun command */
 133   virtual void toStreamCmdSynthFun(std::ostream& out,
 134                                    Node f,
 135                                    const std::vector<Node>& vars,
 136                                    bool isInv,
 137                                    TypeNode sygusType = TypeNode::null()) const;
 138
 139   /** Print constraint command */
 140   virtual void toStreamCmdConstraint(std::ostream& out, Node n) const;
 141
 142   /** Print inv-constraint command */
 143   virtual void toStreamCmdInvConstraint(
 144       std::ostream& out, Node inv, Node pre, Node trans, Node post) const;
 145
 146   /** Print check-synth command */
 147   virtual void toStreamCmdCheckSynth(std::ostream& out) const;
 148
 149   /** Print simplify command */
 150   virtual void toStreamCmdSimplify(std::ostream& out, Node n) const;
 151
 152   /** Print get-value command */
 153   virtual void toStreamCmdGetValue(std::ostream& out,
 154                                    const std::vector<Node>& nodes) const;
 155
 156   /** Print get-assignment command */
 157   virtual void toStreamCmdGetAssignment(std::ostream& out) const;
 158
 159   /** Print get-model command */
 160   virtual void toStreamCmdGetModel(std::ostream& out) const;
 161
 162   /** Print block-model command */
 163   void toStreamCmdBlockModel(std::ostream& out) const;
 164
 165   /** Print block-model-values command */
 166   void toStreamCmdBlockModelValues(std::ostream& out,
 167                                    const std::vector<Node>& nodes) const;
 168
 169   /** Print get-proof command */
 170   virtual void toStreamCmdGetProof(std::ostream& out) const;
 171
 172   /** Print get-instantiations command */
 173   void toStreamCmdGetInstantiations(std::ostream& out) const;
 174
 175   /** Print get-synth-solution command */
 176   void toStreamCmdGetSynthSolution(std::ostream& out) const;
 177
 178   /** Print get-interpol command */
 179   void toStreamCmdGetInterpol(std::ostream& out,
 180                               const std::string& name,
 181                               Node conj,
 182                               TypeNode sygusType) const;
 183
 184   /** Print get-abduct command */
 185   virtual void toStreamCmdGetAbduct(std::ostream& out,
 186                                     const std::string& name,
 187                                     Node conj,
 188                                     TypeNode sygusType) const;
 189
 190   /** Print get-quantifier-elimination command */
 191   void toStreamCmdGetQuantifierElimination(std::ostream& out, Node n) const;
 192
 193   /** Print get-unsat-assumptions command */
 194   virtual void toStreamCmdGetUnsatAssumptions(std::ostream& out) const;
 195
 196   /** Print get-unsat-core command */
 197   virtual void toStreamCmdGetUnsatCore(std::ostream& out) const;
 198
 199   /** Print get-assertions command */
 200   virtual void toStreamCmdGetAssertions(std::ostream& out) const;
 201
 202   /** Print set-info :status command */
 203   virtual void toStreamCmdSetBenchmarkStatus(std::ostream& out,
 204                                              Result::Sat status) const;
 205
 206   /** Print set-logic command */
 207   virtual void toStreamCmdSetBenchmarkLogic(std::ostream& out,
 208                                             const std::string& logic) const;
 209
 210   /** Print set-info command */
 211   virtual void toStreamCmdSetInfo(std::ostream& out,
 212                                   const std::string& flag,
 213                                   SExpr sexpr) const;
 214
 215   /** Print get-info command */
 216   virtual void toStreamCmdGetInfo(std::ostream& out,
 217                                   const std::string& flag) const;
 218
 219   /** Print set-option command */
 220   virtual void toStreamCmdSetOption(std::ostream& out,
 221                                     const std::string& flag,
 222                                     SExpr sexpr) const;
 223
 224   /** Print get-option command */
 225   virtual void toStreamCmdGetOption(std::ostream& out,
 226                                     const std::string& flag) const;
 227
 228   /** Print set-expression-name command */
 229   void toStreamCmdSetExpressionName(std::ostream& out,
 230                                     Node n,
 231                                     const std::string& name) const;
 232
 233   /** Print declare-datatype(s) command */
 234   virtual void toStreamCmdDatatypeDeclaration(
 235       std::ostream& out, const std::vector<TypeNode>& datatypes) const;
 236
 237   /** Print reset command */
 238   virtual void toStreamCmdReset(std::ostream& out) const;
 239
 240   /** Print reset-assertions command */
 241   virtual void toStreamCmdResetAssertions(std::ostream& out) const;
 242
 243   /** Print quit command */
 244   virtual void toStreamCmdQuit(std::ostream& out) const;
 245
 246   /** Print comment command */
 247   virtual void toStreamCmdComment(std::ostream& out,
 248                                   const std::string& comment) const;
 249   /** Declare heap command */
 250   virtual void toStreamCmdDeclareHeap(std::ostream& out,
 251                                       TypeNode locType,
 252                                       TypeNode dataType) const;
 253
 254   /** Print command sequence command */
 255   virtual void toStreamCmdCommandSequence(
 256       std::ostream& out, const std::vector<Command*>& sequence) const;
 257
 258   /** Print declaration sequence command */
 259   virtual void toStreamCmdDeclarationSequence(
 260       std::ostream& out, const std::vector<Command*>& sequence) const;
 261
 262  protected:
 263   /** Derived classes can construct, but no one else. */
 264   Printer() {}
 265
 266   /**
 267    * To stream model sort. This prints the appropriate output for type
 268    * tn declared via declare-sort or declare-datatype.
 269    */
 270   virtual void toStreamModelSort(std::ostream& out,
 271                                  const smt::Model& m,
 272                                  TypeNode tn) const = 0;
 273
 274   /**
 275    * To stream model term. This prints the appropriate output for term
 276    * n declared via declare-fun.
 277    */
 278   virtual void toStreamModelTerm(std::ostream& out,
 279                                  const smt::Model& m,
 280                                  Node n) const = 0;
 281
 282   /** write model response to command using another language printer */
 283   void toStreamUsing(OutputLanguage lang,
 284                      std::ostream& out,
 285                      const smt::Model& m) const;
 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 */