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 : : * The pretty-printer interface for the AST output language.
11 : : */
12 : : #include "printer/ast/ast_printer.h"
13 : :
14 : : #include <iostream>
15 : : #include <sstream>
16 : : #include <string>
17 : : #include <typeinfo>
18 : : #include <vector>
19 : :
20 : : #include "expr/node_visitor.h"
21 : : #include "options/io_utils.h"
22 : : #include "options/language.h" // for LANG_AST
23 : : #include "printer/let_binding.h"
24 : :
25 : : using namespace std;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace printer {
29 : : namespace ast {
30 : :
31 : 13 : void AstPrinter::toStream(std::ostream& out, TNode n) const
32 : : {
33 : 13 : size_t dag = options::ioutils::getDagThresh(out);
34 : 13 : int toDepth = options::ioutils::getNodeDepth(out);
35 [ + + ]: 13 : if (dag != 0)
36 : : {
37 : 2 : LetBinding lbind("_let_", dag + 1);
38 : 1 : toStreamWithLetify(out, n, toDepth, &lbind);
39 : 1 : }
40 : : else
41 : : {
42 : 12 : toStream(out, n, toDepth);
43 : : }
44 : 13 : }
45 : :
46 : 42 : void AstPrinter::toStream(std::ostream& out, Kind k) const
47 : : {
48 : 42 : out << kind::kindToString(k);
49 : 42 : }
50 : :
51 : 104 : void AstPrinter::toStream(std::ostream& out,
52 : : TNode n,
53 : : int toDepth,
54 : : LetBinding* lbind) const
55 : : {
56 : : // null
57 [ - + ]: 104 : if (n.getKind() == Kind::NULL_EXPR)
58 : : {
59 : 0 : out << "null";
60 : 0 : return;
61 : : }
62 : :
63 : : // variable
64 [ + + ]: 104 : if (n.getMetaKind() == kind::metakind::VARIABLE)
65 : : {
66 [ + - ]: 62 : if (n.hasName())
67 : : {
68 : 62 : out << n.getName();
69 : : }
70 : : else
71 : : {
72 : 0 : out << "var_" << n.getId();
73 : : }
74 : 62 : return;
75 : : }
76 : :
77 : 42 : out << '(' << n.getKind();
78 [ - + ]: 42 : if (n.getMetaKind() == kind::metakind::CONSTANT)
79 : : {
80 : : // constant
81 : 0 : out << ' ';
82 : 0 : n.constToStream(out);
83 : : }
84 [ - + ]: 42 : else if (n.isClosure())
85 : : {
86 [ - - ]: 0 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
87 : : {
88 : 0 : out << ' ';
89 : : // body is re-letified
90 [ - - ]: 0 : if (i == 1)
91 : : {
92 : 0 : toStreamWithLetify(out, n[i], toDepth, lbind);
93 : 0 : continue;
94 : : }
95 [ - - ]: 0 : toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - 1, lbind);
96 : : }
97 : : }
98 : : else
99 : : {
100 : : // operator
101 [ - + ]: 42 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
102 : : {
103 : 0 : out << ' ';
104 [ - - ]: 0 : if (toDepth != 0)
105 : : {
106 [ - - ]: 0 : toStream(
107 : 0 : out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind);
108 : : }
109 : : else
110 : : {
111 : 0 : out << "(...)";
112 : : }
113 : : }
114 [ + + ]: 145 : for (TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i)
115 : : {
116 [ + - ]: 103 : if (i != iend)
117 : : {
118 : 103 : out << ' ';
119 : : }
120 [ + + ]: 103 : if (toDepth != 0)
121 : : {
122 [ + + ]: 91 : toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, lbind);
123 : : }
124 : : else
125 : : {
126 : 12 : out << "(...)";
127 : : }
128 : : }
129 : : }
130 : 42 : out << ')';
131 : : } /* AstPrinter::toStream(TNode) */
132 : :
133 : 0 : void AstPrinter::toStream(std::ostream& out, const smt::Model& m) const
134 : : {
135 : 0 : out << "Model(" << std::endl;
136 : 0 : this->Printer::toStream(out, m);
137 : 0 : out << ")" << std::endl;
138 : 0 : }
139 : :
140 : 0 : void AstPrinter::toStreamModelSort(std::ostream& out,
141 : : TypeNode tn,
142 : : const std::vector<Node>& elements) const
143 : : {
144 : 0 : out << "(" << tn << "(";
145 : 0 : bool firstTime = true;
146 [ - - ]: 0 : for (const Node& elem : elements)
147 : : {
148 [ - - ]: 0 : if (firstTime)
149 : : {
150 : 0 : firstTime = false;
151 : : }
152 : : else
153 : : {
154 : 0 : out << " ";
155 : : }
156 : 0 : out << elem;
157 : : }
158 : 0 : out << "))" << std::endl;
159 : 0 : }
160 : :
161 : 0 : void AstPrinter::toStreamModelTerm(std::ostream& out,
162 : : const Node& n,
163 : : const Node& value) const
164 : : {
165 : 0 : out << "(" << n << " " << value << ")" << std::endl;
166 : 0 : }
167 : :
168 : 0 : void AstPrinter::toStreamCmdSuccess(std::ostream& out) const
169 : : {
170 : 0 : out << "OK" << endl;
171 : 0 : }
172 : :
173 : 0 : void AstPrinter::toStreamCmdInterrupted(std::ostream& out) const
174 : : {
175 : 0 : out << "INTERRUPTED" << endl;
176 : 0 : }
177 : :
178 : 0 : void AstPrinter::toStreamCmdUnsupported(std::ostream& out) const
179 : : {
180 : 0 : out << "UNSUPPORTED" << endl;
181 : 0 : }
182 : :
183 : 0 : void AstPrinter::toStreamCmdFailure(std::ostream& out,
184 : : const std::string& message) const
185 : : {
186 : 0 : out << message << endl;
187 : 0 : }
188 : :
189 : 0 : void AstPrinter::toStreamCmdRecoverableFailure(std::ostream& out,
190 : : const std::string& message) const
191 : : {
192 : 0 : out << message << endl;
193 : 0 : }
194 : :
195 : 0 : void AstPrinter::toStreamCmdEmpty(std::ostream& out,
196 : : const std::string& name) const
197 : : {
198 : 0 : out << "Emptycvc5::Command(" << name << ')' << std::endl;
199 : 0 : }
200 : :
201 : 0 : void AstPrinter::toStreamCmdEcho(std::ostream& out,
202 : : const std::string& output) const
203 : : {
204 : 0 : out << "Echocvc5::Command(" << output << ')' << std::endl;
205 : 0 : }
206 : :
207 : 0 : void AstPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
208 : : {
209 : 0 : out << "Assert(" << n << ')' << std::endl;
210 : 0 : }
211 : :
212 : 0 : void AstPrinter::toStreamCmdPush(std::ostream& out, uint32_t nscopes) const
213 : : {
214 : 0 : out << "Push(" << nscopes << ")" << std::endl;
215 : 0 : }
216 : :
217 : 0 : void AstPrinter::toStreamCmdPop(std::ostream& out, uint32_t nscopes) const
218 : : {
219 : 0 : out << "Pop(" << nscopes << ")" << std::endl;
220 : 0 : }
221 : :
222 : 0 : void AstPrinter::toStreamCmdCheckSat(std::ostream& out) const
223 : : {
224 : 0 : out << "CheckSat()" << std::endl;
225 : 0 : }
226 : :
227 : 0 : void AstPrinter::toStreamCmdCheckSatAssuming(
228 : : std::ostream& out, const std::vector<Node>& nodes) const
229 : : {
230 : 0 : out << "CheckSatAssuming( << ";
231 : 0 : copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
232 : 0 : out << ">> )" << std::endl;
233 : 0 : }
234 : :
235 : 0 : void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
236 : : {
237 : 0 : out << "Query(" << n << ')' << std::endl;
238 : 0 : }
239 : :
240 : 0 : void AstPrinter::toStreamCmdReset(std::ostream& out) const
241 : : {
242 : 0 : out << "Reset()" << std::endl;
243 : 0 : }
244 : :
245 : 0 : void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
246 : : {
247 : 0 : out << "ResetAssertions()" << std::endl;
248 : 0 : }
249 : :
250 : 0 : void AstPrinter::toStreamCmdQuit(std::ostream& out) const
251 : : {
252 : 0 : out << "Quit()" << std::endl;
253 : 0 : }
254 : :
255 : 0 : void AstPrinter::toStreamCmdDeclareFunction(
256 : : std::ostream& out,
257 : : const std::string& id,
258 : : const std::vector<TypeNode>& argTypes,
259 : : TypeNode type) const
260 : : {
261 : 0 : out << "Declare(" << id << ",";
262 : 0 : copy(argTypes.begin(), argTypes.end(), ostream_iterator<TypeNode>(out, ", "));
263 : 0 : out << "," << type << ')' << std::endl;
264 : 0 : }
265 : :
266 : 0 : void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
267 : : const std::string& id,
268 : : const std::vector<Node>& formals,
269 : : CVC5_UNUSED TypeNode range,
270 : : Node formula) const
271 : : {
272 : 0 : out << "DefineFunction( \"" << id << "\", [";
273 [ - - ]: 0 : if (formals.size() > 0)
274 : : {
275 : 0 : copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
276 : 0 : out << formals.back();
277 : : }
278 : 0 : out << "], << " << formula << " >> )" << std::endl;
279 : 0 : }
280 : :
281 : 0 : void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
282 : : const std::string& id,
283 : : size_t arity) const
284 : : {
285 : 0 : out << "DeclareType(" << id << ", " << arity << ')' << std::endl;
286 : 0 : }
287 : :
288 : 0 : void AstPrinter::toStreamCmdDefineType(std::ostream& out,
289 : : const std::string& id,
290 : : const std::vector<TypeNode>& params,
291 : : TypeNode t) const
292 : : {
293 : 0 : out << "DefineType(" << id << ",[";
294 [ - - ]: 0 : if (params.size() > 0)
295 : : {
296 : 0 : copy(params.begin(),
297 : 0 : params.end() - 1,
298 : 0 : ostream_iterator<TypeNode>(out, ", "));
299 : 0 : out << params.back();
300 : : }
301 : 0 : out << "]," << t << ')' << std::endl;
302 : 0 : }
303 : :
304 : 0 : void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
305 : : {
306 : 0 : out << "Simplify( << " << n << " >> )" << std::endl;
307 : 0 : }
308 : :
309 : 0 : void AstPrinter::toStreamCmdGetValue(std::ostream& out,
310 : : const std::vector<Node>& nodes) const
311 : : {
312 : 0 : out << "GetValue( << ";
313 : 0 : copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
314 : 0 : out << ">> )" << std::endl;
315 : 0 : }
316 : :
317 : 0 : void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
318 : : {
319 : 0 : out << "GetModel()" << std::endl;
320 : 0 : }
321 : :
322 : 0 : void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
323 : : {
324 : 0 : out << "GetAssignment()" << std::endl;
325 : 0 : }
326 : :
327 : 0 : void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
328 : : {
329 : 0 : out << "GetAssertions()" << std::endl;
330 : 0 : }
331 : :
332 : 0 : void AstPrinter::toStreamCmdGetProof(std::ostream& out,
333 : : modes::ProofComponent c) const
334 : : {
335 : 0 : out << "GetProof(" << c << ")" << std::endl;
336 : 0 : }
337 : :
338 : 0 : void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
339 : : {
340 : 0 : out << "GetUnsatCore()" << std::endl;
341 : 0 : }
342 : :
343 : 0 : void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
344 : : const std::string& logic) const
345 : : {
346 : 0 : out << "SetBenchmarkLogic(" << logic << ')' << std::endl;
347 : 0 : }
348 : :
349 : 0 : void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
350 : : const std::string& flag,
351 : : const std::string& value) const
352 : : {
353 : 0 : out << "SetInfo(" << flag << ", " << value << ')' << std::endl;
354 : 0 : }
355 : :
356 : 0 : void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
357 : : const std::string& flag) const
358 : : {
359 : 0 : out << "GetInfo(" << flag << ')' << std::endl;
360 : 0 : }
361 : :
362 : 0 : void AstPrinter::toStreamCmdSetOption(std::ostream& out,
363 : : const std::string& flag,
364 : : const std::string& value) const
365 : : {
366 : 0 : out << "SetOption(" << flag << ", " << value << ')' << std::endl;
367 : 0 : }
368 : :
369 : 0 : void AstPrinter::toStreamCmdGetOption(std::ostream& out,
370 : : const std::string& flag) const
371 : : {
372 : 0 : out << "GetOption(" << flag << ')' << std::endl;
373 : 0 : }
374 : :
375 : 0 : void AstPrinter::toStreamCmdDatatypeDeclaration(
376 : : std::ostream& out, const std::vector<TypeNode>& datatypes) const
377 : : {
378 : 0 : out << "DatatypeDeclarationcvc5::Command([";
379 [ - - ]: 0 : for (const TypeNode& t : datatypes)
380 : : {
381 : 0 : out << t << ";" << endl;
382 : : }
383 : 0 : out << "])" << std::endl;
384 : 0 : }
385 : :
386 : 1 : void AstPrinter::toStreamWithLetify(std::ostream& out,
387 : : Node n,
388 : : int toDepth,
389 : : LetBinding* lbind) const
390 : : {
391 [ - + ]: 1 : if (lbind == nullptr)
392 : : {
393 : 0 : toStream(out, n, toDepth);
394 : 0 : return;
395 : : }
396 : 1 : std::stringstream cparen;
397 : 1 : std::vector<Node> letList;
398 : 1 : lbind->letify(n, letList);
399 [ - + ]: 1 : if (!letList.empty())
400 : : {
401 : 0 : std::map<Node, uint32_t>::const_iterator it;
402 : 0 : out << "(LET ";
403 : 0 : cparen << ")";
404 : 0 : bool first = true;
405 [ - - ]: 0 : for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
406 : : {
407 [ - - ]: 0 : if (!first)
408 : : {
409 : 0 : out << ", ";
410 : : }
411 : : else
412 : : {
413 : 0 : first = false;
414 : : }
415 : 0 : Node nl = letList[i];
416 : 0 : uint32_t id = lbind->getId(nl);
417 : 0 : out << "_let_" << id << " := ";
418 : 0 : Node nlc = lbind->convert(nl, false);
419 : 0 : toStream(out, nlc, toDepth, lbind);
420 : 0 : }
421 : 0 : out << " IN ";
422 : : }
423 : 1 : Node nc = lbind->convert(n);
424 : : // print the body, passing the lbind object
425 : 1 : toStream(out, nc, toDepth, lbind);
426 : 1 : out << cparen.str();
427 : 1 : lbind->popScope();
428 : 1 : }
429 : :
430 : : } // namespace ast
431 : : } // namespace printer
432 : : } // namespace cvc5::internal
|
