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