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