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 : : thread_local unique_ptr<Printer>
37 : : Printer::d_printers[static_cast<size_t>(Language::LANG_MAX)];
38 : :
39 : 19847 : unique_ptr<Printer> Printer::makePrinter(Language lang)
40 : : {
41 [ + + ][ + - ]: 19847 : switch(lang) {
42 : 18942 : case Language::LANG_SMTLIB_V2_6:
43 : 18942 : return unique_ptr<Printer>(new printer::smt2::Smt2Printer);
44 : :
45 : 904 : 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 : 904 : 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 : 210 : void Printer::toStream(std::ostream& out, const smt::Model& m) const
75 : : {
76 : : // print the declared sorts
77 : 210 : const std::vector<TypeNode>& dsorts = m.getDeclaredSorts();
78 [ + + ]: 381 : for (const TypeNode& tn : dsorts)
79 : : {
80 : 171 : toStreamModelSort(out, tn, m.getDomainElements(tn));
81 : : }
82 : : // print the declared terms
83 : 210 : const std::vector<Node>& dterms = m.getDeclaredTerms();
84 [ + + ]: 599 : for (const Node& n : dterms)
85 : : {
86 : 389 : toStreamModelTerm(out, n, m.getValue(n));
87 : : }
88 : 210 : }
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 : 75 : void Printer::toStream(std::ostream& out, const InstantiationList& is) const
99 : : {
100 : 75 : out << "(instantiations " << is.d_quant << std::endl;
101 [ + + ]: 150 : for (const InstantiationVec& i : is.d_inst)
102 : : {
103 : 75 : out << " ";
104 [ - + ]: 75 : if (i.d_id != theory::InferenceId::UNKNOWN)
105 : : {
106 : 0 : out << "(! ";
107 : : }
108 : 75 : out << "( ";
109 [ + + ]: 150 : for (const Node& n : i.d_vec)
110 : : {
111 : 75 : out << n << " ";
112 : : }
113 : 75 : out << ")";
114 [ - + ]: 75 : 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 : 75 : out << std::endl;
124 : : }
125 : 75 : out << ")" << std::endl;
126 : 75 : }
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 : 19414800 : Printer* Printer::getPrinter(std::ostream& out)
141 : : {
142 : 19414800 : Language lang = options::ioutils::getOutputLanguage(out);
143 : 19414800 : return getPrinter(lang);
144 : : }
145 : :
146 : 19414800 : Printer* Printer::getPrinter(Language lang)
147 : : {
148 [ + + ]: 19414800 : if (lang == Language::LANG_AUTO)
149 : : {
150 : 11271 : lang = Language::LANG_SMTLIB_V2_6; // default
151 : : }
152 [ + + ]: 19414800 : if (d_printers[static_cast<size_t>(lang)] == nullptr)
153 : : {
154 : 19847 : d_printers[static_cast<size_t>(lang)] = makePrinter(lang);
155 : : }
156 : 19414800 : return d_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 : : const std::string& message) const
189 : : {
190 : 0 : printUnknownCommandStatus(out, "failure");
191 : 0 : }
192 : :
193 : 0 : void Printer::toStreamCmdRecoverableFailure(std::ostream& out,
194 : : const std::string& message) const
195 : : {
196 : 0 : printUnknownCommandStatus(out, "recoverable-failure");
197 : 0 : }
198 : :
199 : 0 : void Printer::toStreamCmdEmpty(std::ostream& out, const std::string& name) const
200 : : {
201 : 0 : printUnknownCommand(out, "empty");
202 : 0 : }
203 : :
204 : 0 : void Printer::toStreamCmdEcho(std::ostream& out,
205 : : const std::string& output) const
206 : : {
207 : 0 : printUnknownCommand(out, "echo");
208 : 0 : }
209 : :
210 : 0 : void Printer::toStreamCmdAssert(std::ostream& out, Node n) const
211 : : {
212 : 0 : printUnknownCommand(out, "assert");
213 : 0 : }
214 : :
215 : 0 : void Printer::toStreamCmdPush(std::ostream& out, uint32_t nscopes) const
216 : : {
217 : 0 : printUnknownCommand(out, "push");
218 : 0 : }
219 : :
220 : 0 : void Printer::toStreamCmdPop(std::ostream& out, uint32_t nscopes) const
221 : : {
222 : 0 : printUnknownCommand(out, "pop");
223 : 0 : }
224 : :
225 : 0 : void Printer::toStreamCmdDeclareFunction(std::ostream& out,
226 : : const std::string& id,
227 : : const std::vector<TypeNode>& argTypes,
228 : : TypeNode type) const
229 : : {
230 : 0 : printUnknownCommand(out, "declare-fun");
231 : 0 : }
232 : :
233 : 16593 : void Printer::toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const
234 : : {
235 : : // Must print the variable on the output stream (instead of just getting the
236 : : // name of v), since this method may be called on variables that do not have
237 : : // assigned names.
238 : 33186 : std::stringstream ss;
239 : 16593 : toStream(ss, v);
240 : 33186 : TypeNode vt = v.getType();
241 : 16593 : std::vector<TypeNode> argTypes;
242 [ + + ]: 16593 : if (vt.isFunction())
243 : : {
244 : 3885 : argTypes = vt.getArgTypes();
245 : 3885 : vt = vt.getRangeType();
246 : : }
247 : 16593 : toStreamCmdDeclareFunction(out, ss.str(), argTypes, vt);
248 : 16593 : }
249 : :
250 : 0 : void Printer::toStreamCmdDeclarePool(std::ostream& out,
251 : : const std::string& id,
252 : : TypeNode type,
253 : : const std::vector<Node>& initValue) const
254 : : {
255 : 0 : printUnknownCommand(out, "declare-pool");
256 : 0 : }
257 : :
258 : 0 : void Printer::toStreamCmdDeclareOracleFun(std::ostream& out,
259 : : const std::string& id,
260 : : const std::vector<TypeNode>& argTypes,
261 : : TypeNode type,
262 : : const std::string& binName) const
263 : : {
264 : 0 : printUnknownCommand(out, "declare-oracle-fun");
265 : 0 : }
266 : :
267 : 0 : void Printer::toStreamCmdDeclareType(std::ostream& out,
268 : : const std::string& id,
269 : : size_t arity) const
270 : : {
271 : 0 : printUnknownCommand(out, "declare-sort");
272 : 0 : }
273 : :
274 : 1220 : void Printer::toStreamCmdDeclareType(std::ostream& out, TypeNode type) const
275 : : {
276 [ + + ][ - + ]: 1220 : Assert(type.isUninterpretedSort() || type.isUninterpretedSortConstructor());
[ - + ][ - - ]
277 : 1220 : size_t arity = type.isUninterpretedSortConstructor()
278 [ + + ]: 1220 : ? type.getUninterpretedSortConstructorArity()
279 : 1220 : : 0;
280 : 1220 : toStreamCmdDeclareType(out, type.getName(), arity);
281 : 1220 : }
282 : :
283 : 0 : void Printer::toStreamCmdDefineType(std::ostream& out,
284 : : const std::string& id,
285 : : const std::vector<TypeNode>& params,
286 : : TypeNode t) const
287 : : {
288 : 0 : printUnknownCommand(out, "define-sort");
289 : 0 : }
290 : :
291 : 0 : void Printer::toStreamCmdDefineFunction(std::ostream& out,
292 : : const std::string& id,
293 : : const std::vector<Node>& formals,
294 : : TypeNode range,
295 : : Node formula) const
296 : : {
297 : 0 : printUnknownCommand(out, "define-fun");
298 : 0 : }
299 : :
300 : 506 : void Printer::toStreamCmdDefineFunction(std::ostream& out,
301 : : Node v,
302 : : Node lambda) const
303 : : {
304 : 1012 : std::stringstream vs;
305 : 506 : vs << v;
306 : 1012 : std::vector<Node> formals;
307 : 1012 : TypeNode rangeType = v.getType();
308 : : // could be a function constant
309 : 1012 : Node lam = theory::uf::FunctionConst::toLambda(lambda);
310 : 506 : Node body = lambda;
311 [ + + ]: 506 : if (!lam.isNull())
312 : : {
313 [ - + ][ - + ]: 2 : Assert(lam.getKind() == Kind::LAMBDA);
[ - - ]
314 : 2 : formals.insert(formals.end(), lam[0].begin(), lam[0].end());
315 : 2 : body = lam[1];
316 [ - + ][ - + ]: 2 : Assert(rangeType.isFunction());
[ - - ]
317 : 2 : rangeType = rangeType.getRangeType();
318 : : }
319 : 506 : toStreamCmdDefineFunction(out, vs.str(), formals, rangeType, body);
320 : 506 : }
321 : :
322 : 0 : void Printer::toStreamCmdDefineFunctionRec(
323 : : std::ostream& out,
324 : : const std::vector<Node>& funcs,
325 : : const std::vector<std::vector<Node>>& formals,
326 : : const std::vector<Node>& formulas) const
327 : : {
328 : 0 : printUnknownCommand(out, "define-fun-rec");
329 : 0 : }
330 : :
331 : 0 : void Printer::toStreamCmdDefineFunctionRec(
332 : : std::ostream& out,
333 : : const std::vector<Node>& funcs,
334 : : const std::vector<Node>& lambdas) const
335 : : {
336 : 0 : std::vector<std::vector<Node>> formals;
337 : 0 : std::vector<Node> formulas;
338 [ - - ]: 0 : for (const Node& l : lambdas)
339 : : {
340 : 0 : std::vector<Node> formalsVec;
341 : 0 : Node formula;
342 [ - - ]: 0 : if (l.getKind() == Kind::LAMBDA)
343 : : {
344 : 0 : formalsVec.insert(formalsVec.end(), l[0].begin(), l[0].end());
345 : 0 : formula = l[1];
346 : : }
347 : : else
348 : : {
349 : 0 : formula = l;
350 : : }
351 : 0 : formals.emplace_back(formalsVec);
352 : 0 : formulas.emplace_back(formula);
353 : : }
354 : 0 : toStreamCmdDefineFunctionRec(out, funcs, formals, formulas);
355 : 0 : }
356 : :
357 : 0 : void Printer::toStreamCmdSetUserAttribute(std::ostream& out,
358 : : const std::string& attr,
359 : : Node n) const
360 : : {
361 : 0 : printUnknownCommand(out, "set-user-attribute");
362 : 0 : }
363 : :
364 : 0 : void Printer::toStreamCmdCheckSat(std::ostream& out) const
365 : : {
366 : 0 : printUnknownCommand(out, "check-sat");
367 : 0 : }
368 : :
369 : 0 : void Printer::toStreamCmdCheckSatAssuming(std::ostream& out,
370 : : const std::vector<Node>& nodes) const
371 : : {
372 : 0 : printUnknownCommand(out, "check-sat-assuming");
373 : 0 : }
374 : :
375 : 0 : void Printer::toStreamCmdQuery(std::ostream& out, Node n) const
376 : : {
377 : 0 : printUnknownCommand(out, "query");
378 : 0 : }
379 : :
380 : 0 : void Printer::toStreamCmdDeclareVar(std::ostream& out,
381 : : const std::string& id,
382 : : TypeNode type) const
383 : : {
384 : 0 : printUnknownCommand(out, "declare-var");
385 : 0 : }
386 : :
387 : 0 : void Printer::toStreamCmdSynthFun(std::ostream& out,
388 : : const std::string& id,
389 : : const std::vector<Node>& vars,
390 : : TypeNode rangeType,
391 : : TypeNode sygusType) const
392 : : {
393 : 0 : printUnknownCommand(out, "synth-fun");
394 : 0 : }
395 : :
396 : 0 : void Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
397 : : {
398 : 0 : printUnknownCommand(out, "constraint");
399 : 0 : }
400 : :
401 : 0 : void Printer::toStreamCmdAssume(std::ostream& out, Node n) const
402 : : {
403 : 0 : printUnknownCommand(out, "assume");
404 : 0 : }
405 : :
406 : 0 : void Printer::toStreamCmdInvConstraint(
407 : : std::ostream& out, Node inv, Node pre, Node trans, Node post) const
408 : : {
409 : 0 : printUnknownCommand(out, "inv-constraint");
410 : 0 : }
411 : :
412 : 0 : void Printer::toStreamCmdCheckSynth(std::ostream& out) const
413 : : {
414 : 0 : printUnknownCommand(out, "check-synth");
415 : 0 : }
416 : 0 : void Printer::toStreamCmdCheckSynthNext(std::ostream& out) const
417 : : {
418 : 0 : printUnknownCommand(out, "check-synth-next");
419 : 0 : }
420 : :
421 : 0 : void Printer::toStreamCmdFindSynth(std::ostream& out,
422 : : modes::FindSynthTarget fst,
423 : : TypeNode sygusType) const
424 : : {
425 : 0 : printUnknownCommand(out, "find-synth");
426 : 0 : }
427 : :
428 : 0 : void Printer::toStreamCmdFindSynthNext(std::ostream& out) const
429 : : {
430 : 0 : printUnknownCommand(out, "find-synth-next");
431 : 0 : }
432 : :
433 : 0 : void Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
434 : : {
435 : 0 : printUnknownCommand(out, "simplify");
436 : 0 : }
437 : :
438 : 0 : void Printer::toStreamCmdGetValue(std::ostream& out,
439 : : const std::vector<Node>& nodes) const
440 : : {
441 : 0 : printUnknownCommand(out, "get-value");
442 : 0 : }
443 : :
444 : 0 : void Printer::toStreamCmdGetAssignment(std::ostream& out) const
445 : : {
446 : 0 : printUnknownCommand(out, "get-assignment");
447 : 0 : }
448 : :
449 : 0 : void Printer::toStreamCmdGetModel(std::ostream& out) const
450 : : {
451 : 0 : printUnknownCommand(out, "ge-model");
452 : 0 : }
453 : :
454 : 0 : void Printer::toStreamCmdBlockModel(std::ostream& out,
455 : : modes::BlockModelsMode mode) const
456 : : {
457 : 0 : printUnknownCommand(out, "block-model");
458 : 0 : }
459 : :
460 : 0 : void Printer::toStreamCmdBlockModelValues(std::ostream& out,
461 : : const std::vector<Node>& nodes) const
462 : : {
463 : 0 : printUnknownCommand(out, "block-model-values");
464 : 0 : }
465 : :
466 : 0 : void Printer::toStreamCmdGetProof(std::ostream& out,
467 : : modes::ProofComponent c) const
468 : : {
469 : 0 : printUnknownCommand(out, "get-proof");
470 : 0 : }
471 : :
472 : 0 : void Printer::toStreamCmdGetInstantiations(std::ostream& out) const
473 : : {
474 : 0 : printUnknownCommand(out, "get-instantiations");
475 : 0 : }
476 : :
477 : 0 : void Printer::toStreamCmdGetInterpol(std::ostream& out,
478 : : const std::string& name,
479 : : Node conj,
480 : : TypeNode sygusType) const
481 : : {
482 : 0 : printUnknownCommand(out, "get-interpolant");
483 : 0 : }
484 : :
485 : 0 : void Printer::toStreamCmdGetInterpolNext(std::ostream& out) const
486 : : {
487 : 0 : printUnknownCommand(out, "get-interpolant-next");
488 : 0 : }
489 : :
490 : 0 : void Printer::toStreamCmdGetAbduct(std::ostream& out,
491 : : const std::string& name,
492 : : Node conj,
493 : : TypeNode sygusType) const
494 : : {
495 : 0 : printUnknownCommand(out, "get-abduct");
496 : 0 : }
497 : :
498 : 0 : void Printer::toStreamCmdGetAbductNext(std::ostream& out) const
499 : : {
500 : 0 : printUnknownCommand(out, "get-abduct-next");
501 : 0 : }
502 : :
503 : 0 : void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
504 : : Node n,
505 : : bool doFull) const
506 : : {
507 : 0 : printUnknownCommand(out, "get-quantifier-elimination");
508 : 0 : }
509 : :
510 : 0 : void Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
511 : : {
512 : 0 : printUnknownCommand(out, "get-unsat-assumption");
513 : 0 : }
514 : :
515 : 0 : void Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
516 : : {
517 : 0 : printUnknownCommand(out, "get-unsat-core");
518 : 0 : }
519 : :
520 : 0 : void Printer::toStreamCmdGetDifficulty(std::ostream& out) const
521 : : {
522 : 0 : printUnknownCommand(out, "get-difficulty");
523 : 0 : }
524 : :
525 : 0 : void Printer::toStreamCmdGetTimeoutCore(std::ostream& out) const
526 : : {
527 : 0 : printUnknownCommand(out, "get-timeout-core");
528 : 0 : }
529 : :
530 : 0 : void Printer::toStreamCmdGetTimeoutCoreAssuming(
531 : : std::ostream& out, const std::vector<Node>& assumptions) const
532 : : {
533 : 0 : printUnknownCommand(out, "get-timeout-core-assuming");
534 : 0 : }
535 : :
536 : 0 : void Printer::toStreamCmdGetLearnedLiterals(std::ostream& out,
537 : : modes::LearnedLitType t) const
538 : : {
539 : 0 : printUnknownCommand(out, "get-learned-literals");
540 : 0 : }
541 : :
542 : 0 : void Printer::toStreamCmdGetAssertions(std::ostream& out) const
543 : : {
544 : 0 : printUnknownCommand(out, "get-assertions");
545 : 0 : }
546 : :
547 : 0 : void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
548 : : const std::string& logic) const
549 : : {
550 : 0 : printUnknownCommand(out, "set-logic");
551 : 0 : }
552 : :
553 : 0 : void Printer::toStreamCmdSetInfo(std::ostream& out,
554 : : const std::string& flag,
555 : : const std::string& value) const
556 : : {
557 : 0 : printUnknownCommand(out, "set-info");
558 : 0 : }
559 : :
560 : 0 : void Printer::toStreamCmdGetInfo(std::ostream& out,
561 : : const std::string& flag) const
562 : : {
563 : 0 : printUnknownCommand(out, "get-info");
564 : 0 : }
565 : :
566 : 0 : void Printer::toStreamCmdSetOption(std::ostream& out,
567 : : const std::string& flag,
568 : : const std::string& value) const
569 : : {
570 : 0 : printUnknownCommand(out, "set-option");
571 : 0 : }
572 : :
573 : 0 : void Printer::toStreamCmdGetOption(std::ostream& out,
574 : : const std::string& flag) const
575 : : {
576 : 0 : printUnknownCommand(out, "get-option");
577 : 0 : }
578 : :
579 : 0 : void Printer::toStreamCmdSetExpressionName(std::ostream& out,
580 : : Node n,
581 : : const std::string& name) const
582 : : {
583 : 0 : printUnknownCommand(out, "set-expression-name");
584 : 0 : }
585 : :
586 : 0 : void Printer::toStreamCmdDatatypeDeclaration(
587 : : std::ostream& out, const std::vector<TypeNode>& datatypes) const
588 : : {
589 [ - - ]: 0 : printUnknownCommand(
590 : 0 : out, datatypes.size() == 1 ? "declare-datatype" : "declare-datatypes");
591 : 0 : }
592 : :
593 : 0 : void Printer::toStreamCmdReset(std::ostream& out) const
594 : : {
595 : 0 : printUnknownCommand(out, "reset");
596 : 0 : }
597 : :
598 : 0 : void Printer::toStreamCmdResetAssertions(std::ostream& out) const
599 : : {
600 : 0 : printUnknownCommand(out, "reset-assertions");
601 : 0 : }
602 : :
603 : 0 : void Printer::toStreamCmdQuit(std::ostream& out) const
604 : : {
605 : 0 : printUnknownCommand(out, "quit");
606 : 0 : }
607 : :
608 : 0 : void Printer::toStreamCmdDeclareHeap(std::ostream& out,
609 : : TypeNode locType,
610 : : TypeNode dataType) const
611 : : {
612 : 0 : printUnknownCommand(out, "declare-heap");
613 : 0 : }
614 : :
615 : : } // namespace cvc5::internal
|
