GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/printer/ast/ast_printer.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

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