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
|
/******************************************************************************
* Top contributors (to current version):
* Abdalrhman Mohamed, Andrew Reynolds, Tim King
*
* This file is part of the cvc5 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.
* ****************************************************************************
*
* The pretty-printer interface for the SMT2 output language.
*/
#include "cvc4_private.h"
#ifndef CVC5__PRINTER__SMT2_PRINTER_H
#define CVC5__PRINTER__SMT2_PRINTER_H
#include "printer/printer.h"
namespace cvc5 {
class LetBinding;
namespace printer {
namespace smt2 {
enum Variant
{
no_variant,
smt2_6_variant, // new-style 2.6 syntax, when it makes a difference, with
// support for the string standard
}; /* enum Variant */
class Smt2Printer : public cvc5::Printer
{
public:
Smt2Printer(Variant variant = no_variant) : d_variant(variant) {}
using cvc5::Printer::toStream;
void toStream(std::ostream& out,
TNode n,
int toDepth,
size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const smt::Model& m) const override;
/**
* Writes the unsat core to the stream out.
* We use the expression names that are stored in the SMT engine associated
* with the core (UnsatCore::getSmtEngine) for printing named assertions.
*/
void toStream(std::ostream& out, const UnsatCore& core) const override;
/** Print empty command */
void toStreamCmdEmpty(std::ostream& out,
const std::string& name) const override;
/** Print echo command */
void toStreamCmdEcho(std::ostream& out,
const std::string& output) const override;
/** Print assert command */
void toStreamCmdAssert(std::ostream& out, Node n) const override;
/** Print push command */
void toStreamCmdPush(std::ostream& out) const override;
/** Print pop command */
void toStreamCmdPop(std::ostream& out) const override;
/** Print declare-fun command */
void toStreamCmdDeclareFunction(std::ostream& out,
const std::string& id,
TypeNode type) const override;
/** Print declare-sort command */
void toStreamCmdDeclareType(std::ostream& out,
TypeNode type) const override;
/** Print define-sort command */
void toStreamCmdDefineType(std::ostream& out,
const std::string& id,
const std::vector<TypeNode>& params,
TypeNode t) const override;
/** Print define-fun command */
void toStreamCmdDefineFunction(std::ostream& out,
const std::string& id,
const std::vector<Node>& formals,
TypeNode range,
Node formula) const override;
/** Print define-fun-rec command */
void toStreamCmdDefineFunctionRec(
std::ostream& out,
const std::vector<Node>& funcs,
const std::vector<std::vector<Node>>& formals,
const std::vector<Node>& formulas) const override;
/** Print check-sat command */
void toStreamCmdCheckSat(std::ostream& out,
Node n = Node::null()) const override;
/** Print check-sat-assuming command */
void toStreamCmdCheckSatAssuming(
std::ostream& out, const std::vector<Node>& nodes) const override;
/** Print query command */
void toStreamCmdQuery(std::ostream& out, Node n) const override;
/** Print declare-var command */
void toStreamCmdDeclareVar(std::ostream& out,
Node var,
TypeNode type) const override;
/** Print synth-fun command */
void toStreamCmdSynthFun(std::ostream& out,
Node f,
const std::vector<Node>& vars,
bool isInv,
TypeNode sygusType = TypeNode::null()) const override;
/** Print constraint command */
void toStreamCmdConstraint(std::ostream& out, Node n) const override;
/** Print inv-constraint command */
void toStreamCmdInvConstraint(std::ostream& out,
Node inv,
Node pre,
Node trans,
Node post) const override;
/** Print check-synth command */
void toStreamCmdCheckSynth(std::ostream& out) const override;
/** Print simplify command */
void toStreamCmdSimplify(std::ostream& out, Node nodes) const override;
/** Print get-value command */
void toStreamCmdGetValue(std::ostream& out,
const std::vector<Node>& n) const override;
/** Print get-assignment command */
void toStreamCmdGetAssignment(std::ostream& out) const override;
/** Print get-model command */
void toStreamCmdGetModel(std::ostream& out) const override;
/** Print get-proof command */
void toStreamCmdGetProof(std::ostream& out) const override;
/** Print get-abduct command */
void toStreamCmdGetAbduct(std::ostream& out,
const std::string& name,
Node conj,
TypeNode sygusType) const override;
/** Print get-unsat-assumptions command */
void toStreamCmdGetUnsatAssumptions(std::ostream& out) const override;
/** Print get-unsat-core command */
void toStreamCmdGetUnsatCore(std::ostream& out) const override;
/** Print get-assertions command */
void toStreamCmdGetAssertions(std::ostream& out) const override;
/** Print set-info :status command */
void toStreamCmdSetBenchmarkStatus(std::ostream& out,
Result::Sat status) const override;
/** Print set-logic command */
void toStreamCmdSetBenchmarkLogic(std::ostream& out,
const std::string& logic) const override;
/** Print set-info command */
void toStreamCmdSetInfo(std::ostream& out,
const std::string& flag,
const std::string& value) const override;
/** Print get-info command */
void toStreamCmdGetInfo(std::ostream& out,
const std::string& flag) const override;
/** Print set-option command */
void toStreamCmdSetOption(std::ostream& out,
const std::string& flag,
const std::string& value) const override;
/** Print get-option command */
void toStreamCmdGetOption(std::ostream& out,
const std::string& flag) const override;
/** Print declare-datatype(s) command */
void toStreamCmdDatatypeDeclaration(
std::ostream& out, const std::vector<TypeNode>& datatypes) const override;
/** Print reset command */
void toStreamCmdReset(std::ostream& out) const override;
/** Print reset-assertions command */
void toStreamCmdResetAssertions(std::ostream& out) const override;
/** Print quit command */
void toStreamCmdQuit(std::ostream& out) const override;
/** Print comment command */
void toStreamCmdComment(std::ostream& out,
const std::string& comment) const override;
/** Print declare-heap command */
void toStreamCmdDeclareHeap(std::ostream& out,
TypeNode locType,
TypeNode dataType) const override;
/** Print command sequence command */
void toStreamCmdCommandSequence(
std::ostream& out, const std::vector<Command*>& sequence) const override;
/** Print declaration sequence command */
void toStreamCmdDeclarationSequence(
std::ostream& out, const std::vector<Command*>& sequence) const override;
/**
* Get the string for a kind k, which returns how the kind k is printed in
* the SMT-LIB format (with variant v).
*/
static std::string smtKindString(Kind k, Variant v = smt2_6_variant);
private:
/**
* The main printing method for nodes n.
*/
void toStream(std::ostream& out,
TNode n,
int toDepth,
LetBinding* lbind = nullptr) const;
/**
* To stream, with a forced type. This method is used in some corner cases
* to force a node n to be printed as if it had type tn. This is used e.g.
* for the body of define-fun commands and arguments of singleton terms.
*/
void toStreamCastToType(std::ostream& out,
TNode n,
int toDepth,
TypeNode tn) const;
void toStream(std::ostream& out, const DType& dt) const;
/**
* To stream model sort. This prints the appropriate output for type
* tn declared via declare-sort or declare-datatype.
*/
void toStreamModelSort(std::ostream& out,
const smt::Model& m,
TypeNode tn) const override;
/**
* To stream model term. This prints the appropriate output for term
* n declared via declare-fun.
*/
void toStreamModelTerm(std::ostream& out,
const smt::Model& m,
Node n) const override;
/**
* To stream with let binding. This prints n, possibly in the scope
* of letification generated by this method based on lbind.
*/
void toStreamWithLetify(std::ostream& out,
Node n,
int toDepth,
LetBinding* lbind) const;
Variant d_variant;
}; /* class Smt2Printer */
} // namespace smt2
} // namespace printer
} // namespace cvc5
#endif /* CVC5__PRINTER__SMT2_PRINTER_H */
|
