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
|
/********************* */
/*! \file smt2_printer.h
** \verbatim
** Top contributors (to current version):
** Tim King, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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 The pretty-printer interface for the SMT2 output language
**
** The pretty-printer interface for the SMT2 output language.
**/
#include "cvc4_private.h"
#ifndef CVC4__PRINTER__SMT2_PRINTER_H
#define CVC4__PRINTER__SMT2_PRINTER_H
#include <iostream>
#include "printer/printer.h"
namespace CVC4 {
namespace printer {
namespace smt2 {
enum Variant
{
no_variant,
smt2_0_variant, // old-style 2.0 syntax, when it makes a difference
smt2_6_variant, // new-style 2.6 syntax, when it makes a difference, with
// support for the string standard
sygus_variant // variant for sygus
}; /* enum Variant */
class Smt2Printer : public CVC4::Printer
{
public:
Smt2Printer(Variant variant = no_variant) : d_variant(variant) {}
using CVC4::Printer::toStream;
void toStream(std::ostream& out,
TNode n,
int toDepth,
bool types,
size_t dag) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const 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,
const std::string& id,
size_t arity,
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-named-fun command */
void toStreamCmdDefineNamedFunction(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,
const std::string& sym,
const std::vector<Node>& vars,
TypeNode range,
bool isInv,
TypeNode sygusType) 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,
BenchmarkStatus 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,
SExpr sexpr) 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,
SExpr sexpr) 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 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;
private:
void toStream(
std::ostream& out, TNode n, int toDepth, bool types, TypeNode nt) const;
void toStream(std::ostream& out,
const Model& m,
const Command* c) const override;
void toStream(std::ostream& out, const SExpr& sexpr) const;
void toStream(std::ostream& out, const DType& dt) const;
Variant d_variant;
}; /* class Smt2Printer */
} // namespace smt2
} // namespace printer
} // namespace CVC4
#endif /* CVC4__PRINTER__SMT2_PRINTER_H */
|
