src/printer/cvc/cvc_printer.h

   1 /*********************                                                        */
   2 /*! \file cvc_printer.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Abdalrhman Mohamed, Andrew Reynolds, Tim King
   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 The pretty-printer interface for the CVC output language
  13  **
  14  ** The pretty-printer interface for the CVC output language.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__PRINTER__CVC_PRINTER_H
  20 #define CVC4__PRINTER__CVC_PRINTER_H
  21
  22 #include <iostream>
  23
  24 #include "printer/printer.h"
  25
  26 namespace CVC4 {
  27
  28 class LetBinding;
  29
  30 namespace printer {
  31 namespace cvc {
  32
  33 class CvcPrinter : public CVC4::Printer
  34 {
  35  public:
  36   using CVC4::Printer::toStream;
  37   CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) {}
  38   void toStream(std::ostream& out,
  39                 TNode n,
  40                 int toDepth,
  41                 size_t dag) const override;
  42   void toStream(std::ostream& out, const CommandStatus* s) const override;
  43   void toStream(std::ostream& out, const smt::Model& m) const override;
  44
  45   /** Print empty command */
  46   void toStreamCmdEmpty(std::ostream& out,
  47                         const std::string& name) const override;
  48
  49   /** Print echo command */
  50   void toStreamCmdEcho(std::ostream& out,
  51                        const std::string& output) const override;
  52
  53   /** Print assert command */
  54   void toStreamCmdAssert(std::ostream& out, Node n) const override;
  55
  56   /** Print push command */
  57   void toStreamCmdPush(std::ostream& out) const override;
  58
  59   /** Print pop command */
  60   void toStreamCmdPop(std::ostream& out) const override;
  61
  62   /** Print declare-fun command */
  63   void toStreamCmdDeclareFunction(std::ostream& out,
  64                                   const std::string& id,
  65                                   TypeNode type) const override;
  66
  67   /** Print declare-sort command */
  68   void toStreamCmdDeclareType(std::ostream& out,
  69                               TypeNode type) const override;
  70
  71   /** Print define-sort command */
  72   void toStreamCmdDefineType(std::ostream& out,
  73                              const std::string& id,
  74                              const std::vector<TypeNode>& params,
  75                              TypeNode t) const override;
  76
  77   /** Print define-fun command */
  78   void toStreamCmdDefineFunction(std::ostream& out,
  79                                  const std::string& id,
  80                                  const std::vector<Node>& formals,
  81                                  TypeNode range,
  82                                  Node formula) const override;
  83
  84   /** Print check-sat command */
  85   void toStreamCmdCheckSat(std::ostream& out,
  86                            Node n = Node::null()) const override;
  87
  88   /** Print check-sat-assuming command */
  89   void toStreamCmdCheckSatAssuming(
  90       std::ostream& out, const std::vector<Node>& nodes) const override;
  91
  92   /** Print query command */
  93   void toStreamCmdQuery(std::ostream& out, Node n) const override;
  94
  95   /** Print simplify command */
  96   void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
  97
  98   /** Print get-value command */
  99   void toStreamCmdGetValue(std::ostream& out,
 100                            const std::vector<Node>& n) const override;
 101
 102   /** Print get-assignment command */
 103   void toStreamCmdGetAssignment(std::ostream& out) const override;
 104
 105   /** Print get-model command */
 106   void toStreamCmdGetModel(std::ostream& out) const override;
 107
 108   /** Print get-proof command */
 109   void toStreamCmdGetProof(std::ostream& out) const override;
 110
 111   /** Print get-unsat-core command */
 112   void toStreamCmdGetUnsatCore(std::ostream& out) const override;
 113
 114   /** Print get-assertions command */
 115   void toStreamCmdGetAssertions(std::ostream& out) const override;
 116
 117   /** Print set-info :status command */
 118   void toStreamCmdSetBenchmarkStatus(std::ostream& out,
 119                                      Result::Sat status) const override;
 120
 121   /** Print set-logic command */
 122   void toStreamCmdSetBenchmarkLogic(std::ostream& out,
 123                                     const std::string& logic) const override;
 124
 125   /** Print set-info command */
 126   void toStreamCmdSetInfo(std::ostream& out,
 127                           const std::string& flag,
 128                           SExpr sexpr) const override;
 129
 130   /** Print get-info command */
 131   void toStreamCmdGetInfo(std::ostream& out,
 132                           const std::string& flag) const override;
 133
 134   /** Print set-option command */
 135   void toStreamCmdSetOption(std::ostream& out,
 136                             const std::string& flag,
 137                             SExpr sexpr) const override;
 138
 139   /** Print get-option command */
 140   void toStreamCmdGetOption(std::ostream& out,
 141                             const std::string& flag) const override;
 142
 143   /** Print declare-datatype(s) command */
 144   void toStreamCmdDatatypeDeclaration(
 145       std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
 146
 147   /** Print reset command */
 148   void toStreamCmdReset(std::ostream& out) const override;
 149
 150   /** Print reset-assertions command */
 151   void toStreamCmdResetAssertions(std::ostream& out) const override;
 152
 153   /** Print quit command */
 154   void toStreamCmdQuit(std::ostream& out) const override;
 155
 156   /** Print comment command */
 157   void toStreamCmdComment(std::ostream& out,
 158                           const std::string& comment) const override;
 159
 160   /** Print command sequence command */
 161   void toStreamCmdCommandSequence(
 162       std::ostream& out, const std::vector<Command*>& sequence) const override;
 163
 164   /** Print declaration sequence command */
 165   void toStreamCmdDeclarationSequence(
 166       std::ostream& out, const std::vector<Command*>& sequence) const override;
 167
 168  private:
 169   /**
 170    * The main method for printing Nodes.
 171    */
 172   void toStreamNode(std::ostream& out,
 173                     TNode n,
 174                     int toDepth,
 175                     bool bracket,
 176                     LetBinding* lbind) const;
 177   /**
 178    * To stream model sort. This prints the appropriate output for type
 179    * tn declared via declare-sort or declare-datatype.
 180    */
 181   void toStreamModelSort(std::ostream& out,
 182                          const smt::Model& m,
 183                          TypeNode tn) const override;
 184
 185   /**
 186    * To stream model term. This prints the appropriate output for term
 187    * n declared via declare-fun.
 188    */
 189   void toStreamModelTerm(std::ostream& out,
 190                          const smt::Model& m,
 191                          Node n) const override;
 192   /**
 193    * To stream with let binding. This prints n, possibly in the scope
 194    * of letification generated by this method based on lbind.
 195    */
 196   void toStreamNodeWithLetify(std::ostream& out,
 197                               Node n,
 198                               int toDepth,
 199                               bool bracket,
 200                               LetBinding* lbind) const;
 201
 202   bool d_cvc3Mode;
 203 }; /* class CvcPrinter */
 204
 205 }  // namespace cvc
 206 }  // namespace printer
 207 }  // namespace CVC4
 208
 209 #endif /* CVC4__PRINTER__CVC_PRINTER_H */