GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/printer/printer.cpp Lines: 52 215 24.2 %
Date: 2021-03-22 Branches: 57 305 18.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file printer.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Abdalrhman Mohamed, Andrew Reynolds, Morgan Deters
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 Base of the pretty-printer interface
13
 **
14
 ** Base of the pretty-printer interface.
15
 **/
16
#include "printer/printer.h"
17
18
#include <string>
19
20
#include "options/base_options.h"
21
#include "options/language.h"
22
#include "printer/ast/ast_printer.h"
23
#include "printer/cvc/cvc_printer.h"
24
#include "printer/smt2/smt2_printer.h"
25
#include "printer/tptp/tptp_printer.h"
26
#include "proof/unsat_core.h"
27
#include "smt/command.h"
28
#include "smt/node_command.h"
29
#include "theory/quantifiers/instantiation_list.h"
30
31
using namespace std;
32
33
namespace CVC4 {
34
35
17784
unique_ptr<Printer> Printer::d_printers[language::output::LANG_MAX];
36
37
5881
unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
38
{
39
  using namespace CVC4::language::output;
40
41
5881
  switch(lang) {
42
4911
  case LANG_SMTLIB_V2_6:
43
    return unique_ptr<Printer>(
44
4911
        new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant));
45
46
42
  case LANG_TPTP:
47
42
    return unique_ptr<Printer>(new printer::tptp::TptpPrinter());
48
49
560
  case LANG_CVC4:
50
560
    return unique_ptr<Printer>(new printer::cvc::CvcPrinter());
51
52
365
  case LANG_SYGUS_V2:
53
    // sygus version 2.0 does not have discrepancies with smt2, hence we use
54
    // a normal smt2 variant here.
55
    return unique_ptr<Printer>(
56
365
        new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant));
57
58
3
  case LANG_AST:
59
3
    return unique_ptr<Printer>(new printer::ast::AstPrinter());
60
61
  case LANG_CVC3:
62
    return unique_ptr<Printer>(
63
        new printer::cvc::CvcPrinter(/* cvc3-mode = */ true));
64
65
  default: Unhandled() << lang;
66
  }
67
}
68
69
25
void Printer::toStream(std::ostream& out, const smt::Model& m) const
70
{
71
  // print the declared sorts
72
25
  const std::vector<TypeNode>& dsorts = m.getDeclaredSorts();
73
29
  for (const TypeNode& tn : dsorts)
74
  {
75
4
    toStreamModelSort(out, m, tn);
76
  }
77
78
  // print the declared terms
79
25
  const std::vector<Node>& dterms = m.getDeclaredTerms();
80
55
  for (const Node& n : dterms)
81
  {
82
    // take into account model core, independently of the format
83
30
    if (!m.isModelCoreSymbol(n))
84
    {
85
      continue;
86
    }
87
30
    toStreamModelTerm(out, m, n);
88
  }
89
90
25
}/* Printer::toStream(Model) */
91
92
void Printer::toStreamUsing(OutputLanguage lang,
93
                            std::ostream& out,
94
                            const smt::Model& m) const
95
{
96
  getPrinter(lang)->toStream(out, m);
97
}
98
99
void Printer::toStream(std::ostream& out, const UnsatCore& core) const
100
{
101
  for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
102
    toStreamCmdAssert(out, *i);
103
    out << std::endl;
104
  }
105
}/* Printer::toStream(UnsatCore) */
106
107
7
void Printer::toStream(std::ostream& out, const InstantiationList& is) const
108
{
109
7
  out << "(instantiations " << is.d_quant << std::endl;
110
14
  for (const std::vector<Node>& i : is.d_inst)
111
  {
112
7
    out << "  ( ";
113
14
    for (const Node& n : i)
114
    {
115
7
      out << n << " ";
116
    }
117
7
    out << ")" << std::endl;
118
  }
119
7
  out << ")" << std::endl;
120
7
}
121
122
7
void Printer::toStream(std::ostream& out, const SkolemList& sks) const
123
{
124
7
  out << "(skolem " << sks.d_quant << std::endl;
125
7
  out << "  ( ";
126
14
  for (const Node& n : sks.d_sks)
127
  {
128
7
    out << n << " ";
129
  }
130
7
  out << ")" << std::endl;
131
7
  out << ")" << std::endl;
132
7
}
133
134
933619
Printer* Printer::getPrinter(OutputLanguage lang)
135
{
136
933619
  if(lang == language::output::LANG_AUTO) {
137
  // Infer the language to use for output.
138
  //
139
  // Options can be null in certain circumstances (e.g., when printing
140
  // the singleton "null" expr.  So we guard against segfault
141
2270
  if(not Options::isCurrentNull()) {
142
635724
    if(options::outputLanguage.wasSetByUser()) {
143
4
      lang = options::outputLanguage();
144
    }
145
947321
    if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) {
146
16
      lang = language::toOutputLanguage(options::inputLanguage());
147
     }
148
   }
149
2270
   if (lang == language::output::LANG_AUTO)
150
   {
151
2250
     lang = language::output::LANG_SMTLIB_V2_6;  // default
152
   }
153
  }
154
933619
  if(d_printers[lang] == NULL) {
155
5881
    d_printers[lang] = makePrinter(lang);
156
  }
157
933619
  return d_printers[lang].get();
158
}
159
160
void Printer::printUnknownCommand(std::ostream& out,
161
                                  const std::string& name) const
162
{
163
  out << "ERROR: don't know how to print " << name << " command" << std::endl;
164
}
165
166
void Printer::toStreamCmdEmpty(std::ostream& out, const std::string& name) const
167
{
168
  printUnknownCommand(out, "empty");
169
}
170
171
void Printer::toStreamCmdEcho(std::ostream& out,
172
                              const std::string& output) const
173
{
174
  printUnknownCommand(out, "echo");
175
}
176
177
void Printer::toStreamCmdAssert(std::ostream& out, Node n) const
178
{
179
  printUnknownCommand(out, "assert");
180
}
181
182
void Printer::toStreamCmdPush(std::ostream& out) const
183
{
184
  printUnknownCommand(out, "push");
185
}
186
187
void Printer::toStreamCmdPop(std::ostream& out) const
188
{
189
  printUnknownCommand(out, "pop");
190
}
191
192
void Printer::toStreamCmdDeclareFunction(std::ostream& out,
193
                                         const std::string& id,
194
                                         TypeNode type) const
195
{
196
  printUnknownCommand(out, "declare-fun");
197
}
198
199
void Printer::toStreamCmdDeclareType(std::ostream& out,
200
                                     TypeNode type) const
201
{
202
  printUnknownCommand(out, "declare-sort");
203
}
204
205
void Printer::toStreamCmdDefineType(std::ostream& out,
206
                                    const std::string& id,
207
                                    const std::vector<TypeNode>& params,
208
                                    TypeNode t) const
209
{
210
  printUnknownCommand(out, "define-sort");
211
}
212
213
void Printer::toStreamCmdDefineFunction(std::ostream& out,
214
                                        const std::string& id,
215
                                        const std::vector<Node>& formals,
216
                                        TypeNode range,
217
                                        Node formula) const
218
{
219
  printUnknownCommand(out, "define-fun");
220
}
221
222
void Printer::toStreamCmdDefineFunctionRec(
223
    std::ostream& out,
224
    const std::vector<Node>& funcs,
225
    const std::vector<std::vector<Node>>& formals,
226
    const std::vector<Node>& formulas) const
227
{
228
  printUnknownCommand(out, "define-fun-rec");
229
}
230
231
void Printer::toStreamCmdSetUserAttribute(std::ostream& out,
232
                                          const std::string& attr,
233
                                          Node n) const
234
{
235
  printUnknownCommand(out, "set-user-attribute");
236
}
237
238
void Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
239
{
240
  printUnknownCommand(out, "check-sat");
241
}
242
243
void Printer::toStreamCmdCheckSatAssuming(std::ostream& out,
244
                                          const std::vector<Node>& nodes) const
245
{
246
  printUnknownCommand(out, "check-sat-assuming");
247
}
248
249
void Printer::toStreamCmdQuery(std::ostream& out, Node n) const
250
{
251
  printUnknownCommand(out, "query");
252
}
253
254
void Printer::toStreamCmdDeclareVar(std::ostream& out,
255
                                    Node var,
256
                                    TypeNode type) const
257
{
258
  printUnknownCommand(out, "declare-var");
259
}
260
261
void Printer::toStreamCmdSynthFun(std::ostream& out,
262
                                  Node f,
263
                                  const std::vector<Node>& vars,
264
                                  bool isInv,
265
                                  TypeNode sygusType) const
266
{
267
  printUnknownCommand(out, isInv ? "synth-inv" : "synth-fun");
268
}
269
270
void Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
271
{
272
  printUnknownCommand(out, "constraint");
273
}
274
275
void Printer::toStreamCmdInvConstraint(
276
    std::ostream& out, Node inv, Node pre, Node trans, Node post) const
277
{
278
  printUnknownCommand(out, "inv-constraint");
279
}
280
281
void Printer::toStreamCmdCheckSynth(std::ostream& out) const
282
{
283
  printUnknownCommand(out, "check-synth");
284
}
285
286
void Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
287
{
288
  printUnknownCommand(out, "simplify");
289
}
290
291
void Printer::toStreamCmdGetValue(std::ostream& out,
292
                                  const std::vector<Node>& nodes) const
293
{
294
  printUnknownCommand(out, "get-value");
295
}
296
297
void Printer::toStreamCmdGetAssignment(std::ostream& out) const
298
{
299
  printUnknownCommand(out, "get-assignment");
300
}
301
302
void Printer::toStreamCmdGetModel(std::ostream& out) const
303
{
304
  printUnknownCommand(out, "ge-model");
305
}
306
307
void Printer::toStreamCmdBlockModel(std::ostream& out) const
308
{
309
  printUnknownCommand(out, "block-model");
310
}
311
312
void Printer::toStreamCmdBlockModelValues(std::ostream& out,
313
                                          const std::vector<Node>& nodes) const
314
{
315
  printUnknownCommand(out, "block-model-values");
316
}
317
318
void Printer::toStreamCmdGetProof(std::ostream& out) const
319
{
320
  printUnknownCommand(out, "get-proof");
321
}
322
323
void Printer::toStreamCmdGetInstantiations(std::ostream& out) const
324
{
325
  printUnknownCommand(out, "get-instantiations");
326
}
327
328
void Printer::toStreamCmdGetSynthSolution(std::ostream& out) const
329
{
330
  printUnknownCommand(out, "get-synth-solution");
331
}
332
333
void Printer::toStreamCmdGetInterpol(std::ostream& out,
334
                                     const std::string& name,
335
                                     Node conj,
336
                                     TypeNode sygusType) const
337
{
338
  printUnknownCommand(out, "get-interpol");
339
}
340
341
void Printer::toStreamCmdGetAbduct(std::ostream& out,
342
                                   const std::string& name,
343
                                   Node conj,
344
                                   TypeNode sygusType) const
345
{
346
  printUnknownCommand(out, "get-abduct");
347
}
348
349
void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
350
                                                  Node n) const
351
{
352
  printUnknownCommand(out, "get-quantifier-elimination");
353
}
354
355
void Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
356
{
357
  printUnknownCommand(out, "get-unsat-assumption");
358
}
359
360
void Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
361
{
362
  printUnknownCommand(out, "get-unsat-core");
363
}
364
365
void Printer::toStreamCmdGetAssertions(std::ostream& out) const
366
{
367
  printUnknownCommand(out, "get-assertions");
368
}
369
370
void Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
371
                                            Result::Sat status) const
372
{
373
  printUnknownCommand(out, "set-info");
374
}
375
376
void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
377
                                           const std::string& logic) const
378
{
379
  printUnknownCommand(out, "set-logic");
380
}
381
382
void Printer::toStreamCmdSetInfo(std::ostream& out,
383
                                 const std::string& flag,
384
                                 const std::string& value) const
385
{
386
  printUnknownCommand(out, "set-info");
387
}
388
389
void Printer::toStreamCmdGetInfo(std::ostream& out,
390
                                 const std::string& flag) const
391
{
392
  printUnknownCommand(out, "get-info");
393
}
394
395
void Printer::toStreamCmdSetOption(std::ostream& out,
396
                                   const std::string& flag,
397
                                   const std::string& value) const
398
{
399
  printUnknownCommand(out, "set-option");
400
}
401
402
void Printer::toStreamCmdGetOption(std::ostream& out,
403
                                   const std::string& flag) const
404
{
405
  printUnknownCommand(out, "get-option");
406
}
407
408
void Printer::toStreamCmdSetExpressionName(std::ostream& out,
409
                                           Node n,
410
                                           const std::string& name) const
411
{
412
  printUnknownCommand(out, "set-expression-name");
413
}
414
415
void Printer::toStreamCmdDatatypeDeclaration(
416
    std::ostream& out, const std::vector<TypeNode>& datatypes) const
417
{
418
  printUnknownCommand(
419
      out, datatypes.size() == 1 ? "declare-datatype" : "declare-datatypes");
420
}
421
422
void Printer::toStreamCmdReset(std::ostream& out) const
423
{
424
  printUnknownCommand(out, "reset");
425
}
426
427
void Printer::toStreamCmdResetAssertions(std::ostream& out) const
428
{
429
  printUnknownCommand(out, "reset-assertions");
430
}
431
432
void Printer::toStreamCmdQuit(std::ostream& out) const
433
{
434
  printUnknownCommand(out, "quit");
435
}
436
437
void Printer::toStreamCmdComment(std::ostream& out,
438
                                 const std::string& comment) const
439
{
440
  printUnknownCommand(out, "comment");
441
}
442
443
void Printer::toStreamCmdDeclareHeap(std::ostream& out,
444
                                     TypeNode locType,
445
                                     TypeNode dataType) const
446
{
447
  printUnknownCommand(out, "declare-heap");
448
}
449
450
void Printer::toStreamCmdCommandSequence(
451
    std::ostream& out, const std::vector<Command*>& sequence) const
452
{
453
  printUnknownCommand(out, "sequence");
454
}
455
456
void Printer::toStreamCmdDeclarationSequence(
457
    std::ostream& out, const std::vector<Command*>& sequence) const
458
{
459
  printUnknownCommand(out, "sequence");
460
}
461
462
1605201
}/* CVC4 namespace */