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

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