1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Abdalrhman Mohamed, Andrew Reynolds, Morgan Deters |
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 |
|
#include "printer/printer.h" |
16 |
|
|
17 |
|
#include <string> |
18 |
|
|
19 |
|
#include "options/base_options.h" |
20 |
|
#include "options/language.h" |
21 |
|
#include "printer/ast/ast_printer.h" |
22 |
|
#include "printer/cvc/cvc_printer.h" |
23 |
|
#include "printer/smt2/smt2_printer.h" |
24 |
|
#include "printer/tptp/tptp_printer.h" |
25 |
|
#include "proof/unsat_core.h" |
26 |
|
#include "smt/command.h" |
27 |
|
#include "smt/node_command.h" |
28 |
|
#include "theory/quantifiers/instantiation_list.h" |
29 |
|
|
30 |
|
using namespace std; |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
|
34 |
|
unique_ptr<Printer> |
35 |
19716 |
Printer::d_printers[static_cast<size_t>(Language::LANG_MAX)]; |
36 |
|
|
37 |
6605 |
unique_ptr<Printer> Printer::makePrinter(Language lang) |
38 |
|
{ |
39 |
6605 |
switch(lang) { |
40 |
5552 |
case Language::LANG_SMTLIB_V2_6: |
41 |
|
return unique_ptr<Printer>( |
42 |
5552 |
new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); |
43 |
|
|
44 |
41 |
case Language::LANG_TPTP: |
45 |
41 |
return unique_ptr<Printer>(new printer::tptp::TptpPrinter()); |
46 |
|
|
47 |
807 |
case Language::LANG_CVC: |
48 |
807 |
return unique_ptr<Printer>(new printer::cvc::CvcPrinter()); |
49 |
|
|
50 |
201 |
case Language::LANG_SYGUS_V2: |
51 |
|
// sygus version 2.0 does not have discrepancies with smt2, hence we use |
52 |
|
// a normal smt2 variant here. |
53 |
|
return unique_ptr<Printer>( |
54 |
201 |
new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); |
55 |
|
|
56 |
4 |
case Language::LANG_AST: |
57 |
4 |
return unique_ptr<Printer>(new printer::ast::AstPrinter()); |
58 |
|
|
59 |
|
default: Unhandled() << lang; |
60 |
|
} |
61 |
|
} |
62 |
|
|
63 |
29 |
void Printer::toStream(std::ostream& out, const smt::Model& m) const |
64 |
|
{ |
65 |
|
// print the declared sorts |
66 |
29 |
const std::vector<TypeNode>& dsorts = m.getDeclaredSorts(); |
67 |
35 |
for (const TypeNode& tn : dsorts) |
68 |
|
{ |
69 |
6 |
toStreamModelSort(out, tn, m.getDomainElements(tn)); |
70 |
|
} |
71 |
|
// print the declared terms |
72 |
29 |
const std::vector<Node>& dterms = m.getDeclaredTerms(); |
73 |
63 |
for (const Node& n : dterms) |
74 |
|
{ |
75 |
34 |
toStreamModelTerm(out, n, m.getValue(n)); |
76 |
|
} |
77 |
29 |
} |
78 |
|
|
79 |
|
void Printer::toStreamUsing(Language lang, |
80 |
|
std::ostream& out, |
81 |
|
const smt::Model& m) const |
82 |
|
{ |
83 |
|
getPrinter(lang)->toStream(out, m); |
84 |
|
} |
85 |
|
|
86 |
|
void Printer::toStream(std::ostream& out, const UnsatCore& core) const |
87 |
|
{ |
88 |
|
for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { |
89 |
|
toStreamCmdAssert(out, *i); |
90 |
|
out << std::endl; |
91 |
|
} |
92 |
|
}/* Printer::toStream(UnsatCore) */ |
93 |
|
|
94 |
15 |
void Printer::toStream(std::ostream& out, const InstantiationList& is) const |
95 |
|
{ |
96 |
15 |
out << "(instantiations " << is.d_quant << std::endl; |
97 |
30 |
for (const InstantiationVec& i : is.d_inst) |
98 |
|
{ |
99 |
15 |
out << " "; |
100 |
15 |
if (i.d_id != theory::InferenceId::UNKNOWN) |
101 |
|
{ |
102 |
|
out << "(! "; |
103 |
|
} |
104 |
15 |
out << "( "; |
105 |
30 |
for (const Node& n : i.d_vec) |
106 |
|
{ |
107 |
15 |
out << n << " "; |
108 |
|
} |
109 |
15 |
out << ")"; |
110 |
15 |
if (i.d_id != theory::InferenceId::UNKNOWN) |
111 |
|
{ |
112 |
|
out << " :source " << i.d_id; |
113 |
|
if (!i.d_pfArg.isNull()) |
114 |
|
{ |
115 |
|
out << " " << i.d_pfArg; |
116 |
|
} |
117 |
|
out << ")"; |
118 |
|
} |
119 |
15 |
out << std::endl; |
120 |
|
} |
121 |
15 |
out << ")" << std::endl; |
122 |
15 |
} |
123 |
|
|
124 |
9 |
void Printer::toStream(std::ostream& out, const SkolemList& sks) const |
125 |
|
{ |
126 |
9 |
out << "(skolem " << sks.d_quant << std::endl; |
127 |
9 |
out << " ( "; |
128 |
18 |
for (const Node& n : sks.d_sks) |
129 |
|
{ |
130 |
9 |
out << n << " "; |
131 |
|
} |
132 |
9 |
out << ")" << std::endl; |
133 |
9 |
out << ")" << std::endl; |
134 |
9 |
} |
135 |
|
|
136 |
370908 |
Printer* Printer::getPrinter(Language lang) |
137 |
|
{ |
138 |
370908 |
if (lang == Language::LANG_AUTO) |
139 |
|
{ |
140 |
|
// Infer the language to use for output. |
141 |
|
// |
142 |
|
// Options can be null in certain circumstances (e.g., when printing |
143 |
|
// the singleton "null" expr. So we guard against segfault |
144 |
2397 |
if (not Options::isCurrentNull()) |
145 |
|
{ |
146 |
2387 |
if (Options::current().base.outputLanguageWasSetByUser) |
147 |
|
{ |
148 |
15 |
lang = options::outputLanguage(); |
149 |
|
} |
150 |
2387 |
if (lang == Language::LANG_AUTO |
151 |
2387 |
&& Options::current().base.inputLanguageWasSetByUser) |
152 |
|
{ |
153 |
19 |
lang = options::inputLanguage(); |
154 |
|
} |
155 |
|
} |
156 |
2397 |
if (lang == Language::LANG_AUTO) |
157 |
|
{ |
158 |
2363 |
lang = Language::LANG_SMTLIB_V2_6; // default |
159 |
|
} |
160 |
|
} |
161 |
370908 |
if (d_printers[static_cast<size_t>(lang)] == nullptr) |
162 |
|
{ |
163 |
6605 |
d_printers[static_cast<size_t>(lang)] = makePrinter(lang); |
164 |
|
} |
165 |
370908 |
return d_printers[static_cast<size_t>(lang)].get(); |
166 |
|
} |
167 |
|
|
168 |
|
void Printer::printUnknownCommand(std::ostream& out, |
169 |
|
const std::string& name) const |
170 |
|
{ |
171 |
|
out << "ERROR: don't know how to print " << name << " command" << std::endl; |
172 |
|
} |
173 |
|
|
174 |
|
void Printer::toStreamCmdEmpty(std::ostream& out, const std::string& name) const |
175 |
|
{ |
176 |
|
printUnknownCommand(out, "empty"); |
177 |
|
} |
178 |
|
|
179 |
|
void Printer::toStreamCmdEcho(std::ostream& out, |
180 |
|
const std::string& output) const |
181 |
|
{ |
182 |
|
printUnknownCommand(out, "echo"); |
183 |
|
} |
184 |
|
|
185 |
|
void Printer::toStreamCmdAssert(std::ostream& out, Node n) const |
186 |
|
{ |
187 |
|
printUnknownCommand(out, "assert"); |
188 |
|
} |
189 |
|
|
190 |
|
void Printer::toStreamCmdPush(std::ostream& out) const |
191 |
|
{ |
192 |
|
printUnknownCommand(out, "push"); |
193 |
|
} |
194 |
|
|
195 |
|
void Printer::toStreamCmdPop(std::ostream& out) const |
196 |
|
{ |
197 |
|
printUnknownCommand(out, "pop"); |
198 |
|
} |
199 |
|
|
200 |
|
void Printer::toStreamCmdDeclareFunction(std::ostream& out, |
201 |
|
const std::string& id, |
202 |
|
TypeNode type) const |
203 |
|
{ |
204 |
|
printUnknownCommand(out, "declare-fun"); |
205 |
|
} |
206 |
|
|
207 |
5 |
void Printer::toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const |
208 |
|
{ |
209 |
10 |
std::stringstream vs; |
210 |
5 |
vs << v; |
211 |
5 |
toStreamCmdDeclareFunction(out, vs.str(), v.getType()); |
212 |
5 |
} |
213 |
|
|
214 |
|
void Printer::toStreamCmdDeclarePool(std::ostream& out, |
215 |
|
const std::string& id, |
216 |
|
TypeNode type, |
217 |
|
const std::vector<Node>& initValue) const |
218 |
|
{ |
219 |
|
printUnknownCommand(out, "declare-pool"); |
220 |
|
} |
221 |
|
|
222 |
|
void Printer::toStreamCmdDeclareType(std::ostream& out, |
223 |
|
TypeNode type) const |
224 |
|
{ |
225 |
|
printUnknownCommand(out, "declare-sort"); |
226 |
|
} |
227 |
|
|
228 |
|
void Printer::toStreamCmdDefineType(std::ostream& out, |
229 |
|
const std::string& id, |
230 |
|
const std::vector<TypeNode>& params, |
231 |
|
TypeNode t) const |
232 |
|
{ |
233 |
|
printUnknownCommand(out, "define-sort"); |
234 |
|
} |
235 |
|
|
236 |
|
void Printer::toStreamCmdDefineFunction(std::ostream& out, |
237 |
|
const std::string& id, |
238 |
|
const std::vector<Node>& formals, |
239 |
|
TypeNode range, |
240 |
|
Node formula) const |
241 |
|
{ |
242 |
|
printUnknownCommand(out, "define-fun"); |
243 |
|
} |
244 |
|
|
245 |
|
void Printer::toStreamCmdDefineFunction(std::ostream& out, |
246 |
|
Node v, |
247 |
|
Node lambda) const |
248 |
|
{ |
249 |
|
std::stringstream vs; |
250 |
|
vs << v; |
251 |
|
std::vector<Node> formals; |
252 |
|
Node body = lambda; |
253 |
|
TypeNode rangeType = v.getType(); |
254 |
|
if (body.getKind() == kind::LAMBDA) |
255 |
|
{ |
256 |
|
formals.insert(formals.end(), lambda[0].begin(), lambda[0].end()); |
257 |
|
body = lambda[1]; |
258 |
|
Assert(rangeType.isFunction()); |
259 |
|
rangeType = rangeType.getRangeType(); |
260 |
|
} |
261 |
|
toStreamCmdDefineFunction(out, vs.str(), formals, rangeType, body); |
262 |
|
} |
263 |
|
|
264 |
|
void Printer::toStreamCmdDefineFunctionRec( |
265 |
|
std::ostream& out, |
266 |
|
const std::vector<Node>& funcs, |
267 |
|
const std::vector<std::vector<Node>>& formals, |
268 |
|
const std::vector<Node>& formulas) const |
269 |
|
{ |
270 |
|
printUnknownCommand(out, "define-fun-rec"); |
271 |
|
} |
272 |
|
|
273 |
|
void Printer::toStreamCmdDefineFunctionRec( |
274 |
|
std::ostream& out, |
275 |
|
const std::vector<Node>& funcs, |
276 |
|
const std::vector<Node>& lambdas) const |
277 |
|
{ |
278 |
|
std::vector<std::vector<Node>> formals; |
279 |
|
std::vector<Node> formulas; |
280 |
|
for (const Node& l : lambdas) |
281 |
|
{ |
282 |
|
std::vector<Node> formalsVec; |
283 |
|
Node formula; |
284 |
|
if (l.getKind() == kind::LAMBDA) |
285 |
|
{ |
286 |
|
formalsVec.insert(formalsVec.end(), l[0].begin(), l[0].end()); |
287 |
|
formula = l[1]; |
288 |
|
} |
289 |
|
else |
290 |
|
{ |
291 |
|
formula = l; |
292 |
|
} |
293 |
|
formals.emplace_back(formalsVec); |
294 |
|
formulas.emplace_back(formula); |
295 |
|
} |
296 |
|
toStreamCmdDefineFunctionRec(out, funcs, formals, formulas); |
297 |
|
} |
298 |
|
|
299 |
|
void Printer::toStreamCmdSetUserAttribute(std::ostream& out, |
300 |
|
const std::string& attr, |
301 |
|
Node n) const |
302 |
|
{ |
303 |
|
printUnknownCommand(out, "set-user-attribute"); |
304 |
|
} |
305 |
|
|
306 |
|
void Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const |
307 |
|
{ |
308 |
|
printUnknownCommand(out, "check-sat"); |
309 |
|
} |
310 |
|
|
311 |
|
void Printer::toStreamCmdCheckSatAssuming(std::ostream& out, |
312 |
|
const std::vector<Node>& nodes) const |
313 |
|
{ |
314 |
|
printUnknownCommand(out, "check-sat-assuming"); |
315 |
|
} |
316 |
|
|
317 |
|
void Printer::toStreamCmdQuery(std::ostream& out, Node n) const |
318 |
|
{ |
319 |
|
printUnknownCommand(out, "query"); |
320 |
|
} |
321 |
|
|
322 |
|
void Printer::toStreamCmdDeclareVar(std::ostream& out, |
323 |
|
Node var, |
324 |
|
TypeNode type) const |
325 |
|
{ |
326 |
|
printUnknownCommand(out, "declare-var"); |
327 |
|
} |
328 |
|
|
329 |
|
void Printer::toStreamCmdSynthFun(std::ostream& out, |
330 |
|
Node f, |
331 |
|
const std::vector<Node>& vars, |
332 |
|
bool isInv, |
333 |
|
TypeNode sygusType) const |
334 |
|
{ |
335 |
|
printUnknownCommand(out, isInv ? "synth-inv" : "synth-fun"); |
336 |
|
} |
337 |
|
|
338 |
|
void Printer::toStreamCmdConstraint(std::ostream& out, Node n) const |
339 |
|
{ |
340 |
|
printUnknownCommand(out, "constraint"); |
341 |
|
} |
342 |
|
|
343 |
|
void Printer::toStreamCmdAssume(std::ostream& out, Node n) const |
344 |
|
{ |
345 |
|
printUnknownCommand(out, "assume"); |
346 |
|
} |
347 |
|
|
348 |
|
void Printer::toStreamCmdInvConstraint( |
349 |
|
std::ostream& out, Node inv, Node pre, Node trans, Node post) const |
350 |
|
{ |
351 |
|
printUnknownCommand(out, "inv-constraint"); |
352 |
|
} |
353 |
|
|
354 |
|
void Printer::toStreamCmdCheckSynth(std::ostream& out) const |
355 |
|
{ |
356 |
|
printUnknownCommand(out, "check-synth"); |
357 |
|
} |
358 |
|
|
359 |
|
void Printer::toStreamCmdSimplify(std::ostream& out, Node n) const |
360 |
|
{ |
361 |
|
printUnknownCommand(out, "simplify"); |
362 |
|
} |
363 |
|
|
364 |
|
void Printer::toStreamCmdGetValue(std::ostream& out, |
365 |
|
const std::vector<Node>& nodes) const |
366 |
|
{ |
367 |
|
printUnknownCommand(out, "get-value"); |
368 |
|
} |
369 |
|
|
370 |
|
void Printer::toStreamCmdGetAssignment(std::ostream& out) const |
371 |
|
{ |
372 |
|
printUnknownCommand(out, "get-assignment"); |
373 |
|
} |
374 |
|
|
375 |
|
void Printer::toStreamCmdGetModel(std::ostream& out) const |
376 |
|
{ |
377 |
|
printUnknownCommand(out, "ge-model"); |
378 |
|
} |
379 |
|
|
380 |
|
void Printer::toStreamCmdBlockModel(std::ostream& out) const |
381 |
|
{ |
382 |
|
printUnknownCommand(out, "block-model"); |
383 |
|
} |
384 |
|
|
385 |
|
void Printer::toStreamCmdBlockModelValues(std::ostream& out, |
386 |
|
const std::vector<Node>& nodes) const |
387 |
|
{ |
388 |
|
printUnknownCommand(out, "block-model-values"); |
389 |
|
} |
390 |
|
|
391 |
|
void Printer::toStreamCmdGetProof(std::ostream& out) const |
392 |
|
{ |
393 |
|
printUnknownCommand(out, "get-proof"); |
394 |
|
} |
395 |
|
|
396 |
|
void Printer::toStreamCmdGetInstantiations(std::ostream& out) const |
397 |
|
{ |
398 |
|
printUnknownCommand(out, "get-instantiations"); |
399 |
|
} |
400 |
|
|
401 |
|
void Printer::toStreamCmdGetInterpol(std::ostream& out, |
402 |
|
const std::string& name, |
403 |
|
Node conj, |
404 |
|
TypeNode sygusType) const |
405 |
|
{ |
406 |
|
printUnknownCommand(out, "get-interpol"); |
407 |
|
} |
408 |
|
|
409 |
|
void Printer::toStreamCmdGetAbduct(std::ostream& out, |
410 |
|
const std::string& name, |
411 |
|
Node conj, |
412 |
|
TypeNode sygusType) const |
413 |
|
{ |
414 |
|
printUnknownCommand(out, "get-abduct"); |
415 |
|
} |
416 |
|
|
417 |
|
void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out, |
418 |
|
Node n) const |
419 |
|
{ |
420 |
|
printUnknownCommand(out, "get-quantifier-elimination"); |
421 |
|
} |
422 |
|
|
423 |
|
void Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const |
424 |
|
{ |
425 |
|
printUnknownCommand(out, "get-unsat-assumption"); |
426 |
|
} |
427 |
|
|
428 |
|
void Printer::toStreamCmdGetUnsatCore(std::ostream& out) const |
429 |
|
{ |
430 |
|
printUnknownCommand(out, "get-unsat-core"); |
431 |
|
} |
432 |
|
|
433 |
|
void Printer::toStreamCmdGetDifficulty(std::ostream& out) const |
434 |
|
{ |
435 |
|
printUnknownCommand(out, "get-difficulty"); |
436 |
|
} |
437 |
|
|
438 |
|
void Printer::toStreamCmdGetAssertions(std::ostream& out) const |
439 |
|
{ |
440 |
|
printUnknownCommand(out, "get-assertions"); |
441 |
|
} |
442 |
|
|
443 |
|
void Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out, |
444 |
|
Result::Sat status) const |
445 |
|
{ |
446 |
|
printUnknownCommand(out, "set-info"); |
447 |
|
} |
448 |
|
|
449 |
|
void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out, |
450 |
|
const std::string& logic) const |
451 |
|
{ |
452 |
|
printUnknownCommand(out, "set-logic"); |
453 |
|
} |
454 |
|
|
455 |
|
void Printer::toStreamCmdSetInfo(std::ostream& out, |
456 |
|
const std::string& flag, |
457 |
|
const std::string& value) const |
458 |
|
{ |
459 |
|
printUnknownCommand(out, "set-info"); |
460 |
|
} |
461 |
|
|
462 |
|
void Printer::toStreamCmdGetInfo(std::ostream& out, |
463 |
|
const std::string& flag) const |
464 |
|
{ |
465 |
|
printUnknownCommand(out, "get-info"); |
466 |
|
} |
467 |
|
|
468 |
|
void Printer::toStreamCmdSetOption(std::ostream& out, |
469 |
|
const std::string& flag, |
470 |
|
const std::string& value) const |
471 |
|
{ |
472 |
|
printUnknownCommand(out, "set-option"); |
473 |
|
} |
474 |
|
|
475 |
|
void Printer::toStreamCmdGetOption(std::ostream& out, |
476 |
|
const std::string& flag) const |
477 |
|
{ |
478 |
|
printUnknownCommand(out, "get-option"); |
479 |
|
} |
480 |
|
|
481 |
|
void Printer::toStreamCmdSetExpressionName(std::ostream& out, |
482 |
|
Node n, |
483 |
|
const std::string& name) const |
484 |
|
{ |
485 |
|
printUnknownCommand(out, "set-expression-name"); |
486 |
|
} |
487 |
|
|
488 |
|
void Printer::toStreamCmdDatatypeDeclaration( |
489 |
|
std::ostream& out, const std::vector<TypeNode>& datatypes) const |
490 |
|
{ |
491 |
|
printUnknownCommand( |
492 |
|
out, datatypes.size() == 1 ? "declare-datatype" : "declare-datatypes"); |
493 |
|
} |
494 |
|
|
495 |
|
void Printer::toStreamCmdReset(std::ostream& out) const |
496 |
|
{ |
497 |
|
printUnknownCommand(out, "reset"); |
498 |
|
} |
499 |
|
|
500 |
|
void Printer::toStreamCmdResetAssertions(std::ostream& out) const |
501 |
|
{ |
502 |
|
printUnknownCommand(out, "reset-assertions"); |
503 |
|
} |
504 |
|
|
505 |
|
void Printer::toStreamCmdQuit(std::ostream& out) const |
506 |
|
{ |
507 |
|
printUnknownCommand(out, "quit"); |
508 |
|
} |
509 |
|
|
510 |
|
void Printer::toStreamCmdComment(std::ostream& out, |
511 |
|
const std::string& comment) const |
512 |
|
{ |
513 |
|
printUnknownCommand(out, "comment"); |
514 |
|
} |
515 |
|
|
516 |
|
void Printer::toStreamCmdDeclareHeap(std::ostream& out, |
517 |
|
TypeNode locType, |
518 |
|
TypeNode dataType) const |
519 |
|
{ |
520 |
|
printUnknownCommand(out, "declare-heap"); |
521 |
|
} |
522 |
|
|
523 |
|
void Printer::toStreamCmdCommandSequence( |
524 |
|
std::ostream& out, const std::vector<Command*>& sequence) const |
525 |
|
{ |
526 |
|
printUnknownCommand(out, "sequence"); |
527 |
|
} |
528 |
|
|
529 |
|
void Printer::toStreamCmdDeclarationSequence( |
530 |
|
std::ostream& out, const std::vector<Command*>& sequence) const |
531 |
|
{ |
532 |
|
printUnknownCommand(out, "sequence"); |
533 |
|
} |
534 |
|
|
535 |
29574 |
} // namespace cvc5 |