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