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