Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Abdalrhman Mohamed, Andrew Reynolds, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 <sstream>
18 : : #include <string>
19 : :
20 : : #include "expr/node.h"
21 : : #include "options/base_options.h"
22 : : #include "options/language.h"
23 : : #include "options/printer_options.h"
24 : : #include "printer/ast/ast_printer.h"
25 : : #include "printer/let_binding.h"
26 : : #include "printer/smt2/smt2_printer.h"
27 : : #include "proof/unsat_core.h"
28 : : #include "smt/model.h"
29 : : #include "theory/uf/function_const.h"
30 : : #include "theory/quantifiers/instantiation_list.h"
31 : :
32 : : using namespace std;
33 : :
34 : : namespace cvc5::internal {
35 : :
36 : : static thread_local unique_ptr<Printer>
37 : : global_printers[static_cast<size_t>(Language::LANG_MAX)];
38 : :
39 : 19901 : unique_ptr<Printer> Printer::makePrinter(Language lang)
40 : : {
41 [ + + ][ + - ]: 19901 : switch(lang) {
42 : 18988 : case Language::LANG_SMTLIB_V2_6:
43 : 18988 : return unique_ptr<Printer>(new printer::smt2::Smt2Printer);
44 : :
45 : 912 : case Language::LANG_SYGUS_V2:
46 : : // sygus version 2.0 does not have discrepancies with smt2, hence we use
47 : : // a normal smt2 variant here.
48 : 912 : return unique_ptr<Printer>(new printer::smt2::Smt2Printer);
49 : :
50 : 1 : case Language::LANG_AST:
51 : 1 : return unique_ptr<Printer>(new printer::ast::AstPrinter());
52 : :
53 : 0 : default: Unhandled() << lang;
54 : : }
55 : : }
56 : :
57 : 0 : void Printer::toStream(std::ostream& out,
58 : : TNode n,
59 : : const LetBinding* lbind,
60 : : bool lbindTop) const
61 : : {
62 : : // no special implementation, just convert and print with default prefix
63 [ - - ]: 0 : if (lbind != nullptr)
64 : : {
65 : 0 : Node nc = lbind->convert(n, lbindTop);
66 : 0 : toStream(out, nc);
67 : : }
68 : : else
69 : : {
70 : 0 : toStream(out, n);
71 : : }
72 : 0 : }
73 : :
74 : 239 : void Printer::toStream(std::ostream& out, const smt::Model& m) const
75 : : {
76 : : // print the declared sorts
77 : 239 : const std::vector<TypeNode>& dsorts = m.getDeclaredSorts();
78 [ + + ]: 439 : for (const TypeNode& tn : dsorts)
79 : : {
80 : 200 : toStreamModelSort(out, tn, m.getDomainElements(tn));
81 : : }
82 : : // print the declared terms
83 : 239 : const std::vector<Node>& dterms = m.getDeclaredTerms();
84 [ + + ]: 684 : for (const Node& n : dterms)
85 : : {
86 : 445 : toStreamModelTerm(out, n, m.getValue(n));
87 : : }
88 : 239 : }
89 : :
90 : 0 : void Printer::toStream(std::ostream& out, const UnsatCore& core) const
91 : : {
92 [ - - ]: 0 : for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
93 : 0 : toStreamCmdAssert(out, *i);
94 : 0 : out << std::endl;
95 : : }
96 : 0 : }/* Printer::toStream(UnsatCore) */
97 : :
98 : 79 : void Printer::toStream(std::ostream& out, const InstantiationList& is) const
99 : : {
100 : 79 : out << "(instantiations " << is.d_quant << std::endl;
101 [ + + ]: 158 : for (const InstantiationVec& i : is.d_inst)
102 : : {
103 : 79 : out << " ";
104 [ - + ]: 79 : if (i.d_id != theory::InferenceId::UNKNOWN)
105 : : {
106 : 0 : out << "(! ";
107 : : }
108 : 79 : out << "( ";
109 [ + + ]: 158 : for (const Node& n : i.d_vec)
110 : : {
111 : 79 : out << n << " ";
112 : : }
113 : 79 : out << ")";
114 [ - + ]: 79 : if (i.d_id != theory::InferenceId::UNKNOWN)
115 : : {
116 : 0 : out << " :source " << i.d_id;
117 [ - - ]: 0 : if (!i.d_pfArg.isNull())
118 : : {
119 : 0 : out << " " << i.d_pfArg;
120 : : }
121 : 0 : out << ")";
122 : : }
123 : 79 : out << std::endl;
124 : : }
125 : 79 : out << ")" << std::endl;
126 : 79 : }
127 : :
128 : 6 : void Printer::toStream(std::ostream& out, const SkolemList& sks) const
129 : : {
130 : 6 : out << "(skolem " << sks.d_quant << std::endl;
131 : 6 : out << " ( ";
132 [ + + ]: 12 : for (const Node& n : sks.d_sks)
133 : : {
134 : 6 : out << n << " ";
135 : : }
136 : 6 : out << ")" << std::endl;
137 : 6 : out << ")" << std::endl;
138 : 6 : }
139 : :
140 : 16382500 : Printer* Printer::getPrinter(std::ostream& out)
141 : : {
142 : 16382500 : Language lang = options::ioutils::getOutputLanguage(out);
143 : 16382500 : return getPrinter(lang);
144 : : }
145 : :
146 : 16382500 : Printer* Printer::getPrinter(Language lang)
147 : : {
148 [ + + ]: 16382500 : if (lang == Language::LANG_AUTO)
149 : : {
150 : 130128 : lang = Language::LANG_SMTLIB_V2_6; // default
151 : : }
152 [ + + ]: 16382500 : if (global_printers[static_cast<size_t>(lang)] == nullptr)
153 : : {
154 : 19901 : global_printers[static_cast<size_t>(lang)] = makePrinter(lang);
155 : : }
156 : 16382500 : return global_printers[static_cast<size_t>(lang)].get();
157 : : }
158 : :
159 : 0 : void Printer::printUnknownCommandStatus(std::ostream& out,
160 : : const std::string& name) const
161 : : {
162 : 0 : out << "ERROR: don't know how to print " << name << " command status"
163 : 0 : << std::endl;
164 : 0 : }
165 : :
166 : 0 : void Printer::printUnknownCommand(std::ostream& out,
167 : : const std::string& name) const
168 : : {
169 : 0 : out << "ERROR: don't know how to print " << name << " command";
170 : 0 : }
171 : :
172 : 0 : void Printer::toStreamCmdSuccess(std::ostream& out) const
173 : : {
174 : 0 : printUnknownCommandStatus(out, "success");
175 : 0 : }
176 : :
177 : 0 : void Printer::toStreamCmdInterrupted(std::ostream& out) const
178 : : {
179 : 0 : printUnknownCommandStatus(out, "interrupted");
180 : 0 : }
181 : :
182 : 0 : void Printer::toStreamCmdUnsupported(std::ostream& out) const
183 : : {
184 : 0 : printUnknownCommandStatus(out, "unsupported");
185 : 0 : }
186 : :
187 : 0 : void Printer::toStreamCmdFailure(std::ostream& out,
188 : : CVC5_UNUSED const std::string& message) const
189 : : {
190 : 0 : printUnknownCommandStatus(out, "failure");
191 : 0 : }
192 : :
193 : 0 : void Printer::toStreamCmdRecoverableFailure(
194 : : std::ostream& out, CVC5_UNUSED const std::string& message) const
195 : : {
196 : 0 : printUnknownCommandStatus(out, "recoverable-failure");
197 : 0 : }
198 : :
199 : 0 : void Printer::toStreamCmdEmpty(std::ostream& out,
200 : : CVC5_UNUSED const std::string& name) const
201 : : {
202 : 0 : printUnknownCommand(out, "empty");
203 : 0 : }
204 : :
205 : 0 : void Printer::toStreamCmdEcho(std::ostream& out,
206 : : CVC5_UNUSED const std::string& output) const
207 : : {
208 : 0 : printUnknownCommand(out, "echo");
209 : 0 : }
210 : :
211 : 0 : void Printer::toStreamCmdAssert(std::ostream& out, CVC5_UNUSED Node n) const
212 : : {
213 : 0 : printUnknownCommand(out, "assert");
214 : 0 : }
215 : :
216 : 0 : void Printer::toStreamCmdPush(std::ostream& out,
217 : : CVC5_UNUSED uint32_t nscopes) const
218 : : {
219 : 0 : printUnknownCommand(out, "push");
220 : 0 : }
221 : :
222 : 0 : void Printer::toStreamCmdPop(std::ostream& out,
223 : : CVC5_UNUSED uint32_t nscopes) const
224 : : {
225 : 0 : printUnknownCommand(out, "pop");
226 : 0 : }
227 : :
228 : 0 : void Printer::toStreamCmdDeclareFunction(
229 : : std::ostream& out,
230 : : CVC5_UNUSED const std::string& id,
231 : : CVC5_UNUSED const std::vector<TypeNode>& argTypes,
232 : : CVC5_UNUSED TypeNode type) const
233 : : {
234 : 0 : printUnknownCommand(out, "declare-fun");
235 : 0 : }
236 : :
237 : 17147 : void Printer::toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const
238 : : {
239 : : // Must print the variable on the output stream (instead of just getting the
240 : : // name of v), since this method may be called on variables that do not have
241 : : // assigned names.
242 : 34294 : std::stringstream ss;
243 : 17147 : toStream(ss, v);
244 : 34294 : TypeNode vt = v.getType();
245 : 17147 : std::vector<TypeNode> argTypes;
246 [ + + ]: 17147 : if (vt.isFunction())
247 : : {
248 : 4108 : argTypes = vt.getArgTypes();
249 : 4108 : vt = vt.getRangeType();
250 : : }
251 : 17147 : toStreamCmdDeclareFunction(out, ss.str(), argTypes, vt);
252 : 17147 : }
253 : :
254 : 0 : void Printer::toStreamCmdDeclarePool(
255 : : std::ostream& out,
256 : : CVC5_UNUSED const std::string& id,
257 : : CVC5_UNUSED TypeNode type,
258 : : CVC5_UNUSED const std::vector<Node>& initValue) const
259 : : {
260 : 0 : printUnknownCommand(out, "declare-pool");
261 : 0 : }
262 : :
263 : 0 : void Printer::toStreamCmdDeclareOracleFun(
264 : : std::ostream& out,
265 : : CVC5_UNUSED const std::string& id,
266 : : CVC5_UNUSED const std::vector<TypeNode>& argTypes,
267 : : CVC5_UNUSED TypeNode type,
268 : : CVC5_UNUSED const std::string& binName) const
269 : : {
270 : 0 : printUnknownCommand(out, "declare-oracle-fun");
271 : 0 : }
272 : :
273 : 0 : void Printer::toStreamCmdDeclareType(std::ostream& out,
274 : : CVC5_UNUSED const std::string& id,
275 : : CVC5_UNUSED size_t arity) const
276 : : {
277 : 0 : printUnknownCommand(out, "declare-sort");
278 : 0 : }
279 : :
280 : 1293 : void Printer::toStreamCmdDeclareType(std::ostream& out, TypeNode type) const
281 : : {
282 [ + + ][ - + ]: 1293 : Assert(type.isUninterpretedSort() || type.isUninterpretedSortConstructor());
[ - + ][ - - ]
283 : 1293 : size_t arity = type.isUninterpretedSortConstructor()
284 [ + + ]: 1293 : ? type.getUninterpretedSortConstructorArity()
285 : 1293 : : 0;
286 : 1293 : toStreamCmdDeclareType(out, type.getName(), arity);
287 : 1293 : }
288 : :
289 : 0 : void Printer::toStreamCmdDefineType(
290 : : std::ostream& out,
291 : : CVC5_UNUSED const std::string& id,
292 : : CVC5_UNUSED const std::vector<TypeNode>& params,
293 : : CVC5_UNUSED TypeNode t) const
294 : : {
295 : 0 : printUnknownCommand(out, "define-sort");
296 : 0 : }
297 : :
298 : 0 : void Printer::toStreamCmdDefineFunction(
299 : : std::ostream& out,
300 : : CVC5_UNUSED const std::string& id,
301 : : CVC5_UNUSED const std::vector<Node>& formals,
302 : : CVC5_UNUSED TypeNode range,
303 : : CVC5_UNUSED Node formula) const
304 : : {
305 : 0 : printUnknownCommand(out, "define-fun");
306 : 0 : }
307 : :
308 : 563 : void Printer::toStreamCmdDefineFunction(std::ostream& out,
309 : : Node v,
310 : : Node lambda) const
311 : : {
312 : 1126 : std::stringstream vs;
313 : 563 : vs << v;
314 : 1126 : std::vector<Node> formals;
315 : 1126 : TypeNode rangeType = v.getType();
316 : : // could be a function constant
317 : 1126 : Node lam = theory::uf::FunctionConst::toLambda(lambda);
318 : 563 : Node body = lambda;
319 [ + + ]: 563 : if (!lam.isNull())
320 : : {
321 [ - + ][ - + ]: 2 : Assert(lam.getKind() == Kind::LAMBDA);
[ - - ]
322 : 2 : formals.insert(formals.end(), lam[0].begin(), lam[0].end());
323 : 2 : body = lam[1];
324 [ - + ][ - + ]: 2 : Assert(rangeType.isFunction());
[ - - ]
325 : 2 : rangeType = rangeType.getRangeType();
326 : : }
327 : 563 : toStreamCmdDefineFunction(out, vs.str(), formals, rangeType, body);
328 : 563 : }
329 : :
330 : 0 : void Printer::toStreamCmdDefineFunctionRec(
331 : : std::ostream& out,
332 : : CVC5_UNUSED const std::vector<Node>& funcs,
333 : : CVC5_UNUSED const std::vector<std::vector<Node>>& formals,
334 : : CVC5_UNUSED const std::vector<Node>& formulas) const
335 : : {
336 : 0 : printUnknownCommand(out, "define-fun-rec");
337 : 0 : }
338 : :
339 : 0 : void Printer::toStreamCmdDefineFunctionRec(
340 : : std::ostream& out,
341 : : const std::vector<Node>& funcs,
342 : : const std::vector<Node>& lambdas) const
343 : : {
344 : 0 : std::vector<std::vector<Node>> formals;
345 : 0 : std::vector<Node> formulas;
346 [ - - ]: 0 : for (const Node& l : lambdas)
347 : : {
348 : 0 : std::vector<Node> formalsVec;
349 : 0 : Node formula;
350 [ - - ]: 0 : if (l.getKind() == Kind::LAMBDA)
351 : : {
352 : 0 : formalsVec.insert(formalsVec.end(), l[0].begin(), l[0].end());
353 : 0 : formula = l[1];
354 : : }
355 : : else
356 : : {
357 : 0 : formula = l;
358 : : }
359 : 0 : formals.emplace_back(formalsVec);
360 : 0 : formulas.emplace_back(formula);
361 : : }
362 : 0 : toStreamCmdDefineFunctionRec(out, funcs, formals, formulas);
363 : 0 : }
364 : :
365 : 0 : void Printer::toStreamCmdSetUserAttribute(std::ostream& out,
366 : : CVC5_UNUSED const std::string& attr,
367 : : CVC5_UNUSED Node n) const
368 : : {
369 : 0 : printUnknownCommand(out, "set-user-attribute");
370 : 0 : }
371 : :
372 : 0 : void Printer::toStreamCmdCheckSat(std::ostream& out) const
373 : : {
374 : 0 : printUnknownCommand(out, "check-sat");
375 : 0 : }
376 : :
377 : 0 : void Printer::toStreamCmdCheckSatAssuming(
378 : : std::ostream& out, CVC5_UNUSED const std::vector<Node>& nodes) const
379 : : {
380 : 0 : printUnknownCommand(out, "check-sat-assuming");
381 : 0 : }
382 : :
383 : 0 : void Printer::toStreamCmdQuery(std::ostream& out, CVC5_UNUSED Node n) const
384 : : {
385 : 0 : printUnknownCommand(out, "query");
386 : 0 : }
387 : :
388 : 0 : void Printer::toStreamCmdDeclareVar(std::ostream& out,
389 : : CVC5_UNUSED const std::string& id,
390 : : CVC5_UNUSED TypeNode type) const
391 : : {
392 : 0 : printUnknownCommand(out, "declare-var");
393 : 0 : }
394 : :
395 : 0 : void Printer::toStreamCmdSynthFun(std::ostream& out,
396 : : CVC5_UNUSED const std::string& id,
397 : : CVC5_UNUSED const std::vector<Node>& vars,
398 : : CVC5_UNUSED TypeNode rangeType,
399 : : CVC5_UNUSED TypeNode sygusType) const
400 : : {
401 : 0 : printUnknownCommand(out, "synth-fun");
402 : 0 : }
403 : :
404 : 0 : void Printer::toStreamCmdConstraint(std::ostream& out, CVC5_UNUSED Node n) const
405 : : {
406 : 0 : printUnknownCommand(out, "constraint");
407 : 0 : }
408 : :
409 : 0 : void Printer::toStreamCmdAssume(std::ostream& out, CVC5_UNUSED Node n) const
410 : : {
411 : 0 : printUnknownCommand(out, "assume");
412 : 0 : }
413 : :
414 : 0 : void Printer::toStreamCmdInvConstraint(std::ostream& out,
415 : : CVC5_UNUSED Node inv,
416 : : CVC5_UNUSED Node pre,
417 : : CVC5_UNUSED Node trans,
418 : : CVC5_UNUSED Node post) const
419 : : {
420 : 0 : printUnknownCommand(out, "inv-constraint");
421 : 0 : }
422 : :
423 : 0 : void Printer::toStreamCmdCheckSynth(std::ostream& out) const
424 : : {
425 : 0 : printUnknownCommand(out, "check-synth");
426 : 0 : }
427 : 0 : void Printer::toStreamCmdCheckSynthNext(std::ostream& out) const
428 : : {
429 : 0 : printUnknownCommand(out, "check-synth-next");
430 : 0 : }
431 : :
432 : 0 : void Printer::toStreamCmdFindSynth(std::ostream& out,
433 : : CVC5_UNUSED modes::FindSynthTarget fst,
434 : : CVC5_UNUSED TypeNode sygusType) const
435 : : {
436 : 0 : printUnknownCommand(out, "find-synth");
437 : 0 : }
438 : :
439 : 0 : void Printer::toStreamCmdFindSynthNext(std::ostream& out) const
440 : : {
441 : 0 : printUnknownCommand(out, "find-synth-next");
442 : 0 : }
443 : :
444 : 0 : void Printer::toStreamCmdSimplify(std::ostream& out, CVC5_UNUSED Node n) const
445 : : {
446 : 0 : printUnknownCommand(out, "simplify");
447 : 0 : }
448 : :
449 : 0 : void Printer::toStreamCmdGetValue(
450 : : std::ostream& out, CVC5_UNUSED const std::vector<Node>& nodes) const
451 : : {
452 : 0 : printUnknownCommand(out, "get-value");
453 : 0 : }
454 : :
455 : 0 : void Printer::toStreamCmdGetModelDomainElements(std::ostream& out,
456 : : CVC5_UNUSED TypeNode type) const
457 : : {
458 : 0 : printUnknownCommand(out, "get-model-domain-elements");
459 : 0 : }
460 : :
461 : 0 : void Printer::toStreamCmdGetAssignment(std::ostream& out) const
462 : : {
463 : 0 : printUnknownCommand(out, "get-assignment");
464 : 0 : }
465 : :
466 : 0 : void Printer::toStreamCmdGetModel(std::ostream& out) const
467 : : {
468 : 0 : printUnknownCommand(out, "ge-model");
469 : 0 : }
470 : :
471 : 0 : void Printer::toStreamCmdBlockModel(
472 : : std::ostream& out, CVC5_UNUSED modes::BlockModelsMode mode) const
473 : : {
474 : 0 : printUnknownCommand(out, "block-model");
475 : 0 : }
476 : :
477 : 0 : void Printer::toStreamCmdBlockModelValues(
478 : : std::ostream& out, CVC5_UNUSED const std::vector<Node>& nodes) const
479 : : {
480 : 0 : printUnknownCommand(out, "block-model-values");
481 : 0 : }
482 : :
483 : 0 : void Printer::toStreamCmdGetProof(std::ostream& out,
484 : : CVC5_UNUSED modes::ProofComponent c) const
485 : : {
486 : 0 : printUnknownCommand(out, "get-proof");
487 : 0 : }
488 : :
489 : 0 : void Printer::toStreamCmdGetInstantiations(std::ostream& out) const
490 : : {
491 : 0 : printUnknownCommand(out, "get-instantiations");
492 : 0 : }
493 : :
494 : 0 : void Printer::toStreamCmdGetInterpol(std::ostream& out,
495 : : CVC5_UNUSED const std::string& name,
496 : : CVC5_UNUSED Node conj,
497 : : CVC5_UNUSED TypeNode sygusType) const
498 : : {
499 : 0 : printUnknownCommand(out, "get-interpolant");
500 : 0 : }
501 : :
502 : 0 : void Printer::toStreamCmdGetInterpolNext(std::ostream& out) const
503 : : {
504 : 0 : printUnknownCommand(out, "get-interpolant-next");
505 : 0 : }
506 : :
507 : 0 : void Printer::toStreamCmdGetAbduct(std::ostream& out,
508 : : CVC5_UNUSED const std::string& name,
509 : : CVC5_UNUSED Node conj,
510 : : CVC5_UNUSED TypeNode sygusType) const
511 : : {
512 : 0 : printUnknownCommand(out, "get-abduct");
513 : 0 : }
514 : :
515 : 0 : void Printer::toStreamCmdGetAbductNext(std::ostream& out) const
516 : : {
517 : 0 : printUnknownCommand(out, "get-abduct-next");
518 : 0 : }
519 : :
520 : 0 : void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
521 : : CVC5_UNUSED Node n,
522 : : CVC5_UNUSED bool doFull) const
523 : : {
524 : 0 : printUnknownCommand(out, "get-quantifier-elimination");
525 : 0 : }
526 : :
527 : 0 : void Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
528 : : {
529 : 0 : printUnknownCommand(out, "get-unsat-assumption");
530 : 0 : }
531 : :
532 : 0 : void Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
533 : : {
534 : 0 : printUnknownCommand(out, "get-unsat-core");
535 : 0 : }
536 : :
537 : 0 : void Printer::toStreamCmdGetDifficulty(std::ostream& out) const
538 : : {
539 : 0 : printUnknownCommand(out, "get-difficulty");
540 : 0 : }
541 : :
542 : 0 : void Printer::toStreamCmdGetTimeoutCore(std::ostream& out) const
543 : : {
544 : 0 : printUnknownCommand(out, "get-timeout-core");
545 : 0 : }
546 : :
547 : 0 : void Printer::toStreamCmdGetTimeoutCoreAssuming(
548 : : std::ostream& out, CVC5_UNUSED const std::vector<Node>& assumptions) const
549 : : {
550 : 0 : printUnknownCommand(out, "get-timeout-core-assuming");
551 : 0 : }
552 : :
553 : 0 : void Printer::toStreamCmdGetLearnedLiterals(
554 : : std::ostream& out, CVC5_UNUSED modes::LearnedLitType t) const
555 : : {
556 : 0 : printUnknownCommand(out, "get-learned-literals");
557 : 0 : }
558 : :
559 : 0 : void Printer::toStreamCmdGetAssertions(std::ostream& out) const
560 : : {
561 : 0 : printUnknownCommand(out, "get-assertions");
562 : 0 : }
563 : :
564 : 0 : void Printer::toStreamCmdSetBenchmarkLogic(
565 : : std::ostream& out, CVC5_UNUSED const std::string& logic) const
566 : : {
567 : 0 : printUnknownCommand(out, "set-logic");
568 : 0 : }
569 : :
570 : 0 : void Printer::toStreamCmdSetInfo(std::ostream& out,
571 : : CVC5_UNUSED const std::string& flag,
572 : : CVC5_UNUSED const std::string& value) const
573 : : {
574 : 0 : printUnknownCommand(out, "set-info");
575 : 0 : }
576 : :
577 : 0 : void Printer::toStreamCmdGetInfo(std::ostream& out,
578 : : CVC5_UNUSED const std::string& flag) const
579 : : {
580 : 0 : printUnknownCommand(out, "get-info");
581 : 0 : }
582 : :
583 : 0 : void Printer::toStreamCmdSetOption(std::ostream& out,
584 : : CVC5_UNUSED const std::string& flag,
585 : : CVC5_UNUSED const std::string& value) const
586 : : {
587 : 0 : printUnknownCommand(out, "set-option");
588 : 0 : }
589 : :
590 : 0 : void Printer::toStreamCmdGetOption(std::ostream& out,
591 : : CVC5_UNUSED const std::string& flag) const
592 : : {
593 : 0 : printUnknownCommand(out, "get-option");
594 : 0 : }
595 : :
596 : 0 : void Printer::toStreamCmdSetExpressionName(
597 : : std::ostream& out,
598 : : CVC5_UNUSED Node n,
599 : : CVC5_UNUSED const std::string& name) const
600 : : {
601 : 0 : printUnknownCommand(out, "set-expression-name");
602 : 0 : }
603 : :
604 : 0 : void Printer::toStreamCmdDatatypeDeclaration(
605 : : std::ostream& out, const std::vector<TypeNode>& datatypes) const
606 : : {
607 [ - - ]: 0 : printUnknownCommand(
608 : 0 : out, datatypes.size() == 1 ? "declare-datatype" : "declare-datatypes");
609 : 0 : }
610 : :
611 : 0 : void Printer::toStreamCmdReset(std::ostream& out) const
612 : : {
613 : 0 : printUnknownCommand(out, "reset");
614 : 0 : }
615 : :
616 : 0 : void Printer::toStreamCmdResetAssertions(std::ostream& out) const
617 : : {
618 : 0 : printUnknownCommand(out, "reset-assertions");
619 : 0 : }
620 : :
621 : 0 : void Printer::toStreamCmdQuit(std::ostream& out) const
622 : : {
623 : 0 : printUnknownCommand(out, "quit");
624 : 0 : }
625 : :
626 : 0 : void Printer::toStreamCmdDeclareHeap(std::ostream& out,
627 : : CVC5_UNUSED TypeNode locType,
628 : : CVC5_UNUSED TypeNode dataType) const
629 : : {
630 : 0 : printUnknownCommand(out, "declare-heap");
631 : 0 : }
632 : :
633 : : } // namespace cvc5::internal
|
