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 smt::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 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                                              Result::Sat 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 smt::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 smt::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 */