GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/printer/ast/ast_printer.cpp Lines: 37 224 16.5 %
Date: 2021-03-23 Branches: 43 258 16.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ast_printer.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Abdalrhman Mohamed, Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief The pretty-printer interface for the AST output language
13
 **
14
 ** The pretty-printer interface for the AST output language.
15
 **/
16
#include "printer/ast/ast_printer.h"
17
18
#include <iostream>
19
#include <string>
20
#include <typeinfo>
21
#include <vector>
22
23
#include "expr/node_manager_attributes.h"  // for VarNameAttr
24
#include "expr/node_visitor.h"
25
#include "options/language.h"  // for LANG_AST
26
#include "printer/let_binding.h"
27
#include "smt/command.h"
28
#include "smt/node_command.h"
29
30
using namespace std;
31
32
namespace CVC4 {
33
namespace printer {
34
namespace ast {
35
36
26
void AstPrinter::toStream(std::ostream& out,
37
                          TNode n,
38
                          int toDepth,
39
                          size_t dag) const
40
{
41
26
  if(dag != 0) {
42
4
    LetBinding lbind(dag + 1);
43
2
    toStreamWithLetify(out, n, toDepth, &lbind);
44
  } else {
45
24
    toStream(out, n, toDepth);
46
  }
47
26
}
48
49
208
void AstPrinter::toStream(std::ostream& out,
50
                          TNode n,
51
                          int toDepth,
52
                          LetBinding* lbind) const
53
{
54
  // null
55
208
  if(n.getKind() == kind::NULL_EXPR) {
56
    out << "null";
57
    return;
58
  }
59
60
  // variable
61
208
  if(n.getMetaKind() == kind::metakind::VARIABLE) {
62
248
    string s;
63
124
    if(n.getAttribute(expr::VarNameAttr(), s)) {
64
124
      out << s;
65
    } else {
66
      out << "var_" << n.getId();
67
    }
68
124
    return;
69
  }
70
71
84
  out << '(' << n.getKind();
72
84
  if(n.getMetaKind() == kind::metakind::CONSTANT) {
73
    // constant
74
    out << ' ';
75
    kind::metakind::NodeValueConstPrinter::toStream(out, n);
76
  }
77
84
  else if (n.isClosure())
78
  {
79
    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
80
    {
81
      // body is re-letified
82
      if (i == 1)
83
      {
84
        toStreamWithLetify(out, n[i], toDepth, lbind);
85
        continue;
86
      }
87
      toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - 1, lbind);
88
    }
89
  }
90
  else
91
  {
92
    // operator
93
84
    if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
94
      out << ' ';
95
      if(toDepth != 0) {
96
        toStream(
97
            out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind);
98
      } else {
99
        out << "(...)";
100
      }
101
    }
102
290
    for(TNode::iterator i = n.begin(),
103
84
          iend = n.end();
104
290
        i != iend;
105
        ++i) {
106
206
      if(i != iend) {
107
206
        out << ' ';
108
      }
109
206
      if(toDepth != 0) {
110
182
        toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, lbind);
111
      } else {
112
24
        out << "(...)";
113
      }
114
    }
115
  }
116
84
  out << ')';
117
}/* AstPrinter::toStream(TNode) */
118
119
template <class T>
120
static bool tryToStream(std::ostream& out, const Command* c);
121
122
template <class T>
123
static bool tryToStream(std::ostream& out, const CommandStatus* s);
124
125
void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const
126
{
127
  if(tryToStream<CommandSuccess>(out, s) ||
128
     tryToStream<CommandFailure>(out, s) ||
129
     tryToStream<CommandUnsupported>(out, s) ||
130
     tryToStream<CommandInterrupted>(out, s)) {
131
    return;
132
  }
133
134
  out << "ERROR: don't know how to print a CommandStatus of class: "
135
      << typeid(*s).name() << endl;
136
137
}/* AstPrinter::toStream(CommandStatus*) */
138
139
void AstPrinter::toStream(std::ostream& out, const smt::Model& m) const
140
{
141
  out << "Model()";
142
}
143
144
void AstPrinter::toStreamModelSort(std::ostream& out,
145
                                   const smt::Model& m,
146
                                   TypeNode tn) const
147
{
148
  // shouldn't be called; only the non-Command* version above should be
149
  Unreachable();
150
}
151
152
void AstPrinter::toStreamModelTerm(std::ostream& out,
153
                                   const smt::Model& m,
154
                                   Node n) const
155
{
156
  // shouldn't be called; only the non-Command* version above should be
157
  Unreachable();
158
}
159
160
void AstPrinter::toStreamCmdEmpty(std::ostream& out,
161
                                  const std::string& name) const
162
{
163
  out << "EmptyCommand(" << name << ')' << std::endl;
164
}
165
166
void AstPrinter::toStreamCmdEcho(std::ostream& out,
167
                                 const std::string& output) const
168
{
169
  out << "EchoCommand(" << output << ')' << std::endl;
170
}
171
172
void AstPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
173
{
174
  out << "Assert(" << n << ')' << std::endl;
175
}
176
177
void AstPrinter::toStreamCmdPush(std::ostream& out) const
178
{
179
  out << "Push()" << std::endl;
180
}
181
182
void AstPrinter::toStreamCmdPop(std::ostream& out) const {
183
  out << "Pop()" << std::endl;
184
}
185
186
void AstPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
187
{
188
  if (n.isNull())
189
  {
190
    out << "CheckSat()";
191
  }
192
  else
193
  {
194
    out << "CheckSat(" << n << ')';
195
  }
196
  out << std::endl;
197
}
198
199
void AstPrinter::toStreamCmdCheckSatAssuming(
200
    std::ostream& out, const std::vector<Node>& nodes) const
201
{
202
  out << "CheckSatAssuming( << ";
203
  copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
204
  out << ">> )" << std::endl;
205
}
206
207
void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
208
{
209
  out << "Query(" << n << ')' << std::endl;
210
}
211
212
void AstPrinter::toStreamCmdReset(std::ostream& out) const
213
{
214
  out << "Reset()" << std::endl;
215
}
216
217
void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
218
{
219
  out << "ResetAssertions()" << std::endl;
220
}
221
222
void AstPrinter::toStreamCmdQuit(std::ostream& out) const
223
{
224
  out << "Quit()" << std::endl;
225
}
226
227
void AstPrinter::toStreamCmdDeclarationSequence(
228
    std::ostream& out, const std::vector<Command*>& sequence) const
229
{
230
  out << "DeclarationSequence[" << endl;
231
  for (CommandSequence::const_iterator i = sequence.cbegin();
232
       i != sequence.cend();
233
       ++i)
234
  {
235
    out << *i << endl;
236
  }
237
  out << "]" << std::endl;
238
}
239
240
void AstPrinter::toStreamCmdCommandSequence(
241
    std::ostream& out, const std::vector<Command*>& sequence) const
242
{
243
  out << "CommandSequence[" << endl;
244
  for (CommandSequence::const_iterator i = sequence.cbegin();
245
       i != sequence.cend();
246
       ++i)
247
  {
248
    out << *i << endl;
249
  }
250
  out << "]" << std::endl;
251
}
252
253
void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out,
254
                                            const std::string& id,
255
                                            TypeNode type) const
256
{
257
  out << "Declare(" << id << "," << type << ')' << std::endl;
258
}
259
260
void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
261
                                           const std::string& id,
262
                                           const std::vector<Node>& formals,
263
                                           TypeNode range,
264
                                           Node formula) const
265
{
266
  out << "DefineFunction( \"" << id << "\", [";
267
  if (formals.size() > 0)
268
  {
269
    copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
270
    out << formals.back();
271
  }
272
  out << "], << " << formula << " >> )" << std::endl;
273
}
274
275
void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
276
                                        TypeNode type) const
277
{
278
  out << "DeclareType(" << type << ')' << std::endl;
279
}
280
281
void AstPrinter::toStreamCmdDefineType(std::ostream& out,
282
                                       const std::string& id,
283
                                       const std::vector<TypeNode>& params,
284
                                       TypeNode t) const
285
{
286
  out << "DefineType(" << id << ",[";
287
  if (params.size() > 0)
288
  {
289
    copy(params.begin(),
290
         params.end() - 1,
291
         ostream_iterator<TypeNode>(out, ", "));
292
    out << params.back();
293
  }
294
  out << "]," << t << ')' << std::endl;
295
}
296
297
void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
298
{
299
  out << "Simplify( << " << n << " >> )" << std::endl;
300
}
301
302
void AstPrinter::toStreamCmdGetValue(std::ostream& out,
303
                                     const std::vector<Node>& nodes) const
304
{
305
  out << "GetValue( << ";
306
  copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
307
  out << ">> )" << std::endl;
308
}
309
310
void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
311
{
312
  out << "GetModel()" << std::endl;
313
}
314
315
void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
316
{
317
  out << "GetAssignment()" << std::endl;
318
}
319
320
void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
321
{
322
  out << "GetAssertions()" << std::endl;
323
}
324
325
void AstPrinter::toStreamCmdGetProof(std::ostream& out) const
326
{
327
  out << "GetProof()" << std::endl;
328
}
329
330
void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
331
{
332
  out << "GetUnsatCore()" << std::endl;
333
}
334
335
void AstPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
336
                                               Result::Sat status) const
337
{
338
  out << "SetBenchmarkStatus(" << status << ')' << std::endl;
339
}
340
341
void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
342
                                              const std::string& logic) const
343
{
344
  out << "SetBenchmarkLogic(" << logic << ')' << std::endl;
345
}
346
347
void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
348
                                    const std::string& flag,
349
                                    const std::string& value) const
350
{
351
  out << "SetInfo(" << flag << ", " << value << ')' << std::endl;
352
}
353
354
void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
355
                                    const std::string& flag) const
356
{
357
  out << "GetInfo(" << flag << ')' << std::endl;
358
}
359
360
void AstPrinter::toStreamCmdSetOption(std::ostream& out,
361
                                      const std::string& flag,
362
                                      const std::string& value) const
363
{
364
  out << "SetOption(" << flag << ", " << value << ')' << std::endl;
365
}
366
367
void AstPrinter::toStreamCmdGetOption(std::ostream& out,
368
                                      const std::string& flag) const
369
{
370
  out << "GetOption(" << flag << ')' << std::endl;
371
}
372
373
void AstPrinter::toStreamCmdDatatypeDeclaration(
374
    std::ostream& out, const std::vector<TypeNode>& datatypes) const
375
{
376
  out << "DatatypeDeclarationCommand([";
377
  for (const TypeNode& t : datatypes)
378
  {
379
    out << t << ";" << endl;
380
  }
381
  out << "])" << std::endl;
382
}
383
384
void AstPrinter::toStreamCmdComment(std::ostream& out,
385
                                    const std::string& comment) const
386
{
387
  out << "CommentCommand([" << comment << "])" << std::endl;
388
}
389
390
2
void AstPrinter::toStreamWithLetify(std::ostream& out,
391
                                    Node n,
392
                                    int toDepth,
393
                                    LetBinding* lbind) const
394
{
395
2
  if (lbind == nullptr)
396
  {
397
    toStream(out, n, toDepth);
398
    return;
399
  }
400
4
  std::stringstream cparen;
401
4
  std::vector<Node> letList;
402
2
  lbind->letify(n, letList);
403
2
  if (!letList.empty())
404
  {
405
    std::map<Node, uint32_t>::const_iterator it;
406
    out << "(LET ";
407
    cparen << ")";
408
    bool first = true;
409
    for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
410
    {
411
      if (!first)
412
      {
413
        out << ", ";
414
      }
415
      else
416
      {
417
        first = false;
418
      }
419
      Node nl = letList[i];
420
      uint32_t id = lbind->getId(nl);
421
      out << "_let_" << id << " := ";
422
      Node nlc = lbind->convert(nl, "_let_", false);
423
      toStream(out, nlc, toDepth, lbind);
424
    }
425
    out << " IN ";
426
  }
427
4
  Node nc = lbind->convert(n, "_let_");
428
  // print the body, passing the lbind object
429
2
  toStream(out, nc, toDepth, lbind);
430
2
  out << cparen.str();
431
2
  lbind->popScope();
432
}
433
434
template <class T>
435
static bool tryToStream(std::ostream& out, const Command* c)
436
{
437
  if(typeid(*c) == typeid(T)) {
438
    toStream(out, dynamic_cast<const T*>(c));
439
    return true;
440
  }
441
  return false;
442
}
443
444
static void toStream(std::ostream& out, const CommandSuccess* s)
445
{
446
  if(Command::printsuccess::getPrintSuccess(out)) {
447
    out << "OK" << endl;
448
  }
449
}
450
451
static void toStream(std::ostream& out, const CommandInterrupted* s)
452
{
453
  out << "INTERRUPTED" << endl;
454
}
455
456
static void toStream(std::ostream& out, const CommandUnsupported* s)
457
{
458
  out << "UNSUPPORTED" << endl;
459
}
460
461
static void toStream(std::ostream& out, const CommandFailure* s)
462
{
463
  out << s->getMessage() << endl;
464
}
465
466
template <class T>
467
static bool tryToStream(std::ostream& out, const CommandStatus* s)
468
{
469
  if(typeid(*s) == typeid(T)) {
470
    toStream(out, dynamic_cast<const T*>(s));
471
    return true;
472
  }
473
  return false;
474
}
475
476
}/* CVC4::printer::ast namespace */
477
}/* CVC4::printer namespace */
478
26685
}/* CVC4 namespace */