GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/printer/cvc/cvc_printer.cpp Lines: 360 1035 34.8 %
Date: 2021-03-23 Branches: 473 2152 22.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cvc_printer.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
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 CVC output language
13
 **
14
 ** The pretty-printer interface for the CVC output language.
15
 **/
16
17
#include "printer/cvc/cvc_printer.h"
18
19
#include <algorithm>
20
#include <iostream>
21
#include <iterator>
22
#include <stack>
23
#include <string>
24
#include <typeinfo>
25
#include <vector>
26
27
#include "expr/dtype.h"
28
#include "expr/dtype_cons.h"
29
#include "expr/dtype_selector.h"
30
#include "expr/node_manager_attributes.h"  // for VarNameAttr
31
#include "expr/node_visitor.h"
32
#include "expr/sequence.h"
33
#include "options/language.h"  // for LANG_AST
34
#include "options/smt_options.h"
35
#include "printer/let_binding.h"
36
#include "smt/command.h"
37
#include "smt/node_command.h"
38
#include "smt/smt_engine.h"
39
#include "theory/arrays/theory_arrays_rewriter.h"
40
#include "theory/substitutions.h"
41
#include "theory/theory_model.h"
42
43
using namespace std;
44
45
namespace CVC4 {
46
namespace printer {
47
namespace cvc {
48
49
28645
void CvcPrinter::toStream(std::ostream& out,
50
                          TNode n,
51
                          int toDepth,
52
                          size_t dag) const
53
{
54
28645
  if(dag != 0) {
55
1640
    LetBinding lbind(dag + 1);
56
820
    toStreamNodeWithLetify(out, n, toDepth, false, &lbind);
57
  } else {
58
27825
    toStreamNode(out, n, toDepth, false, nullptr);
59
  }
60
28645
}
61
62
26280
void toStreamRational(std::ostream& out, Node n, bool forceRational)
63
{
64
26280
  Assert(n.getKind() == kind::CONST_RATIONAL);
65
26280
  const Rational& rat = n.getConst<Rational>();
66
26280
  if (rat.isIntegral() && !forceRational)
67
  {
68
26280
    out << rat.getNumerator();
69
  }
70
  else
71
  {
72
    out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
73
  }
74
26280
}
75
76
30908
void CvcPrinter::toStreamNode(std::ostream& out,
77
                              TNode n,
78
                              int depth,
79
                              bool bracket,
80
                              LetBinding* lbind) const
81
{
82
30908
  if (depth == 0) {
83
    out << "(...)";
84
  } else {
85
30908
    --depth;
86
  }
87
88
  // null
89
30908
  if(n.getKind() == kind::NULL_EXPR) {
90
    out << "null";
91
29982
    return;
92
  }
93
94
  // variables
95
30908
  if(n.isVar()) {
96
3600
    string s;
97
1800
    if(n.getAttribute(expr::VarNameAttr(), s)) {
98
1798
      out << s;
99
    } else {
100
2
      if(n.getKind() == kind::VARIABLE) {
101
        out << "var_";
102
      } else {
103
2
        out << n.getKind() << '_';
104
      }
105
2
      out << n.getId();
106
    }
107
1800
    return;
108
  }
109
29108
  if(n.isNullaryOp()) {
110
    if( n.getKind() == kind::UNIVERSE_SET ){
111
      out << "UNIVERSE :: " << n.getType();
112
    }else{
113
      //unknown printer
114
      out << n.getKind();
115
    }
116
    return;
117
  }
118
119
  // constants
120
29108
  if(n.getMetaKind() == kind::metakind::CONSTANT) {
121
27785
    switch(n.getKind()) {
122
504
    case kind::BITVECTOR_TYPE:
123
504
      out << "BITVECTOR(" << n.getConst<BitVectorSize>().d_size << ")";
124
504
      break;
125
12
    case kind::CONST_BITVECTOR: {
126
12
      const BitVector& bv = n.getConst<BitVector>();
127
12
      const Integer& x = bv.getValue();
128
12
      out << "0bin";
129
12
      unsigned size = bv.getSize();
130
60
      while (size-- > 0)
131
      {
132
24
        out << (x.testBit(size) ? '1' : '0');
133
      }
134
12
      break;
135
    }
136
11
    case kind::CONST_BOOLEAN:
137
      // the default would print "1" or "0" for bool, that's not correct
138
      // for our purposes
139
11
      out << (n.getConst<bool>() ? "TRUE" : "FALSE");
140
11
      break;
141
26280
    case kind::CONST_RATIONAL: {
142
26280
      toStreamRational(out, n, false);
143
26280
      break;
144
    }
145
25
    case kind::CONST_STRING:
146
    {
147
25
      out << '"' << n.getConst<String>().toString() << '"';
148
25
      break;
149
    }
150
    case kind::CONST_SEQUENCE:
151
    {
152
      const Sequence& sn = n.getConst<Sequence>();
153
      const std::vector<Node>& snvec = sn.getVec();
154
      if (snvec.size() > 1)
155
      {
156
        out << "CONCAT(";
157
      }
158
      bool first = true;
159
      for (const Node& snvc : snvec)
160
      {
161
        if (!first)
162
        {
163
          out << ", ";
164
        }
165
        out << "SEQ_UNIT(" << snvc << ")";
166
        first = false;
167
      }
168
      if (snvec.size() > 1)
169
      {
170
        out << ")";
171
      }
172
      break;
173
    }
174
729
    case kind::TYPE_CONSTANT:
175
729
      switch(TypeConstant tc = n.getConst<TypeConstant>()) {
176
34
      case REAL_TYPE:
177
34
        out << "REAL";
178
34
        break;
179
681
      case INTEGER_TYPE:
180
681
        out << "INT";
181
681
        break;
182
12
      case BOOLEAN_TYPE:
183
12
        out << "BOOLEAN";
184
12
        break;
185
2
      case STRING_TYPE:
186
2
        out << "STRING";
187
2
        break;
188
      default:
189
        out << tc;
190
        break;
191
      }
192
729
      break;
193
194
224
    case kind::DATATYPE_TYPE: {
195
      const DType& dt = NodeManager::currentNM()->getDTypeForIndex(
196
224
          n.getConst<DatatypeIndexConstant>().getIndex());
197
224
      if( dt.isTuple() ){
198
21
        out << '[';
199
54
        for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
200
33
          if (i > 0) {
201
15
            out << ", ";
202
          }
203
66
          TypeNode t = dt[0][i].getRangeType();
204
33
          out << t;
205
        }
206
21
        out << ']';
207
      }
208
203
      else if (dt.isRecord())
209
      {
210
47
        out << "[# ";
211
187
        for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
212
140
          if (i > 0) {
213
95
            out << ", ";
214
          }
215
280
          TypeNode t = dt[0][i].getRangeType();
216
140
          out << dt[0][i].getSelector() << ":" << t;
217
        }
218
47
        out << " #]";
219
      }else{
220
156
        out << dt.getName();
221
      }
222
    }
223
224
      break;
224
225
    case kind::EMPTYSET:
226
      out << "{} :: " << n.getConst<EmptySet>().getType();
227
      break;
228
229
    case kind::STORE_ALL: {
230
      const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
231
      out << "ARRAY(" << asa.getType().getArrayIndexType() << " OF "
232
          << asa.getType().getArrayConstituentType()
233
          << ") : " << asa.getValue();
234
      break;
235
    }
236
237
    default:
238
      // Fall back to whatever operator<< does on underlying type; we
239
      // might luck out and print something reasonable.
240
      kind::metakind::NodeValueConstPrinter::toStream(out, n);
241
    }
242
243
27785
    return;
244
  }
245
246
  enum OpType {
247
    PREFIX,
248
    INFIX,
249
    POSTFIX
250
  } opType;
251
252
  //The default operation type is PREFIX
253
1323
  opType = PREFIX;
254
255
2249
  stringstream op;       // operation (such as '+')
256
257
1323
  switch(n.getKind()) {
258
259
    // BUILTIN
260
69
    case kind::EQUAL:
261
69
      if( n[0].getType().isBoolean() ){
262
28
        op << "<=>";
263
      }else{
264
41
        op << '=';
265
      }
266
69
      opType = INFIX;
267
69
      break;
268
    case kind::ITE:
269
      out << "IF ";
270
      toStreamNode(out, n[0], depth, true, lbind);
271
      out << " THEN ";
272
      toStreamNode(out, n[1], depth, true, lbind);
273
      out << " ELSE ";
274
      toStreamNode(out, n[2], depth, true, lbind);
275
      out << " ENDIF";
276
      return;
277
      break;
278
    case kind::SEXPR_TYPE:
279
      out << '[';
280
      for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
281
        if (i > 0) {
282
          out << ", ";
283
        }
284
        toStreamNode(out, n[i], depth, false, lbind);
285
      }
286
      out << ']';
287
      return;
288
      break;
289
193
    case kind::SEXPR:
290
      // no-op
291
193
      break;
292
2
    case kind::LAMBDA:
293
2
      out << "(LAMBDA";
294
2
      toStreamNode(out, n[0], depth, true, lbind);
295
2
      out << ": ";
296
2
      toStreamNodeWithLetify(out, n[1], depth, true, lbind);
297
2
      out << ")";
298
2
      return;
299
      break;
300
    case kind::WITNESS:
301
      out << "(WITNESS";
302
      toStreamNode(out, n[0], depth, true, lbind);
303
      out << " : ";
304
      toStreamNodeWithLetify(out, n[1], depth, true, lbind);
305
      out << ')';
306
      return;
307
    case kind::DISTINCT:
308
      // distinct not supported directly, blast it away with the rewriter
309
      toStreamNode(out, theory::Rewriter::rewrite(n), depth, true, lbind);
310
      return;
311
188
    case kind::SORT_TYPE:
312
    {
313
188
      string name;
314
188
      if(n.getAttribute(expr::VarNameAttr(), name)) {
315
188
        out << name;
316
188
        return;
317
      }
318
    }
319
    break;
320
321
    // BOOL
322
40
    case kind::AND:
323
40
      op << "AND";
324
40
      opType = INFIX;
325
40
      break;
326
58
    case kind::OR:
327
58
      op << "OR";
328
58
      opType = INFIX;
329
58
      break;
330
84
    case kind::NOT:
331
84
      op << "NOT";
332
84
      opType = PREFIX;
333
84
      break;
334
    case kind::XOR:
335
      op << "XOR";
336
      opType = INFIX;
337
      break;
338
    case kind::IMPLIES:
339
      op << "=>";
340
      opType = INFIX;
341
      break;
342
343
    // UF
344
118
    case kind::APPLY_UF:
345
118
      toStreamNode(op, n.getOperator(), depth, false, lbind);
346
118
      break;
347
    case kind::CARDINALITY_CONSTRAINT:
348
    case kind::COMBINED_CARDINALITY_CONSTRAINT:
349
      out << "CARDINALITY_CONSTRAINT";
350
      break;
351
352
    case kind::FUNCTION_TYPE:
353
      if (n.getNumChildren() > 1) {
354
        if (n.getNumChildren() > 2) {
355
          out << '(';
356
        }
357
        for (unsigned i = 1; i < n.getNumChildren(); ++i) {
358
          if (i > 1) {
359
            out << ", ";
360
          }
361
          toStreamNode(out, n[i - 1], depth, false, lbind);
362
        }
363
        if (n.getNumChildren() > 2) {
364
          out << ')';
365
        }
366
      }
367
      out << " -> ";
368
      toStreamNode(out, n[n.getNumChildren() - 1], depth, false, lbind);
369
      return;
370
      break;
371
372
    // DATATYPES
373
    case kind::PARAMETRIC_DATATYPE: {
374
      const DType& dt = NodeManager::currentNM()->getDTypeForIndex(
375
          n[0].getConst<DatatypeIndexConstant>().getIndex());
376
      out << dt.getName() << '[';
377
      for (unsigned i = 1; i < n.getNumChildren(); ++i)
378
      {
379
        if (i > 1)
380
        {
381
          out << ',';
382
        }
383
        out << n[i];
384
      }
385
        out << ']';
386
      }
387
      return;
388
      break;
389
    case kind::APPLY_TYPE_ASCRIPTION: {
390
      toStreamNode(out, n[0], depth, false, lbind);
391
      out << "::";
392
      TypeNode t = n.getOperator().getConst<AscriptionType>().getType();
393
      out << (t.isFunctionLike() ? t.getRangeType() : t);
394
      }
395
      return;
396
      break;
397
333
    case kind::APPLY_CONSTRUCTOR: {
398
635
        TypeNode t = n.getType();
399
333
        if( t.isTuple() ){
400
302
          if( n.getNumChildren()==1 ){
401
47
            out << "TUPLE";
402
          }
403
        }
404
31
        else if (t.isRecord())
405
        {
406
1
          const DType& dt = t.getDType();
407
1
          const DTypeConstructor& recCons = dt[0];
408
1
          out << "(# ";
409
3
          for (size_t i = 0, nargs = recCons.getNumArgs(); i < nargs; i++)
410
          {
411
2
            if (i != 0)
412
            {
413
1
              out << ", ";
414
            }
415
2
            out << recCons[i].getName() << " := ";
416
2
            toStreamNode(out, n[i], depth, false, lbind);
417
          }
418
1
          out << " #)";
419
1
          return;
420
        }
421
        else
422
        {
423
30
          toStreamNode(op, n.getOperator(), depth, false, lbind);
424
30
          if (n.getNumChildren() == 0)
425
          {
426
            // for datatype constants d, we print "d" and not "d()"
427
30
            out << op.str();
428
30
            return;
429
          }
430
302
        }
431
      }
432
302
      break;
433
66
    case kind::APPLY_SELECTOR:
434
    case kind::APPLY_SELECTOR_TOTAL: {
435
68
        TypeNode t = n[0].getType();
436
68
        Node opn = n.getOperator();
437
66
        if (!t.isDatatype())
438
        {
439
          toStreamNode(op, opn, depth, false, lbind);
440
        }
441
66
        else if (t.isTuple() || t.isRecord())
442
        {
443
64
          toStreamNode(out, n[0], depth, true, lbind);
444
64
          out << '.';
445
64
          const DType& dt = t.getDType();
446
64
          if (t.isTuple())
447
          {
448
            int sindex;
449
60
            if (n.getKind() == kind::APPLY_SELECTOR)
450
            {
451
1
              sindex = DType::indexOf(opn);
452
            }
453
            else
454
            {
455
59
              sindex = dt[0].getSelectorIndexInternal(opn);
456
            }
457
60
            Assert(sindex >= 0);
458
60
            out << sindex;
459
          }
460
          else
461
          {
462
4
            toStreamNode(out, opn, depth, false, lbind);
463
          }
464
64
          return;
465
        }else{
466
2
          toStreamNode(op, opn, depth, false, lbind);
467
2
        }
468
      }
469
2
      break;
470
    case kind::APPLY_TESTER: {
471
      Assert(!n.getType().isTuple() && !n.getType().isRecord());
472
      op << "is_";
473
      unsigned cindex = DType::indexOf(n.getOperator());
474
      const DType& dt = DType::datatypeOf(n.getOperator());
475
      toStreamNode(op, dt[cindex].getConstructor(), depth, false, lbind);
476
    }
477
      break;
478
    case kind::CONSTRUCTOR_TYPE:
479
    case kind::SELECTOR_TYPE:
480
      if(n.getNumChildren() > 1) {
481
        if(n.getNumChildren() > 2) {
482
          out << '(';
483
        }
484
        for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) {
485
          if(i > 0) {
486
            out << ", ";
487
          }
488
          toStreamNode(out, n[i], depth, false, lbind);
489
        }
490
        if(n.getNumChildren() > 2) {
491
          out << ')';
492
        }
493
        out << " -> ";
494
      }
495
      toStreamNode(out, n[n.getNumChildren() - 1], depth, false, lbind);
496
      return;
497
    case kind::TESTER_TYPE:
498
      toStreamNode(out, n[0], depth, false, lbind);
499
      out << " -> BOOLEAN";
500
      return;
501
      break;
502
    case kind::TUPLE_UPDATE:
503
      toStreamNode(out, n[0], depth, true, lbind);
504
      out << " WITH ." << n.getOperator().getConst<TupleUpdate>().getIndex() << " := ";
505
      toStreamNode(out, n[1], depth, true, lbind);
506
      return;
507
      break;
508
    case kind::RECORD_UPDATE:
509
      toStreamNode(out, n[0], depth, true, lbind);
510
      out << " WITH ." << n.getOperator().getConst<RecordUpdate>().getField() << " := ";
511
      toStreamNode(out, n[1], depth, true, lbind);
512
      return;
513
      break;
514
515
    // ARRAYS
516
25
    case kind::ARRAY_TYPE:
517
25
      out << "ARRAY ";
518
25
      toStreamNode(out, n[0], depth, false, lbind);
519
25
      out << " OF ";
520
25
      toStreamNode(out, n[1], depth, false, lbind);
521
25
      return;
522
      break;
523
22
    case kind::SELECT:
524
22
      toStreamNode(out, n[0], depth, true, lbind);
525
22
      out << '[';
526
22
      toStreamNode(out, n[1], depth, false, lbind);
527
22
      out << ']';
528
22
      return;
529
      break;
530
    case kind::STORE: {
531
      stack<TNode> stk;
532
      stk.push(n);
533
      while(stk.top()[0].getKind() == kind::STORE) {
534
        stk.push(stk.top()[0]);
535
      }
536
      if (bracket) {
537
        out << '(';
538
      }
539
      TNode x = stk.top();
540
      toStreamNode(out, x[0], depth, false, lbind);
541
      out << " WITH [";
542
      toStreamNode(out, x[1], depth, false, lbind);
543
      out << "] := ";
544
      toStreamNode(out, x[2], depth, false, lbind);
545
      stk.pop();
546
      while(!stk.empty()) {
547
        x = stk.top();
548
        out << ", [";
549
        toStreamNode(out, x[1], depth, false, lbind);
550
        out << "] := ";
551
        toStreamNode(out, x[2], depth, false, lbind);
552
        stk.pop();
553
      }
554
      if (bracket) {
555
        out << ')';
556
      }
557
      return;
558
      break;
559
    }
560
561
    // ARITHMETIC
562
14
    case kind::PLUS:
563
14
      op << '+';
564
14
      opType = INFIX;
565
14
      break;
566
11
    case kind::MULT:
567
    case kind::NONLINEAR_MULT:
568
11
      op << '*';
569
11
      opType = INFIX;
570
11
      break;
571
    case kind::MINUS:
572
      op << '-';
573
      opType = INFIX;
574
      break;
575
    case kind::UMINUS:
576
      op << '-';
577
      opType = PREFIX;
578
      break;
579
1
    case kind::DIVISION:
580
    case kind::DIVISION_TOTAL:
581
1
      op << '/';
582
1
      opType = INFIX;
583
1
      break;
584
    case kind::INTS_DIVISION:
585
    case kind::INTS_DIVISION_TOTAL:
586
      op << "DIV";
587
      opType = INFIX;
588
      break;
589
    case kind::INTS_MODULUS:
590
    case kind::INTS_MODULUS_TOTAL:
591
      op << "MOD";
592
      opType = INFIX;
593
      break;
594
16
    case kind::LT:
595
16
      op << '<';
596
16
      opType = INFIX;
597
16
      break;
598
    case kind::LEQ:
599
      op << "<=";
600
      opType = INFIX;
601
      break;
602
    case kind::GT:
603
      op << '>';
604
      opType = INFIX;
605
      break;
606
8
    case kind::GEQ:
607
8
      op << ">=";
608
8
      opType = INFIX;
609
8
      break;
610
2
    case kind::POW:
611
2
      op << '^';
612
2
      opType = INFIX;
613
2
      break;
614
    case kind::ABS:
615
      op << "ABS";
616
      opType = PREFIX;
617
      break;
618
    case kind::IS_INTEGER:
619
      op << "IS_INTEGER";
620
      opType = PREFIX;
621
      break;
622
    case kind::TO_INTEGER:
623
      op << "FLOOR";
624
      opType = PREFIX;
625
      break;
626
    case kind::TO_REAL:
627
    case kind::CAST_TO_REAL:
628
    {
629
      if (n[0].getKind() == kind::CONST_RATIONAL)
630
      {
631
        // print the constant as a rational
632
        toStreamRational(out, n[0], true);
633
      }
634
      else
635
      {
636
        // ignore, there is no to-real in CVC language
637
        toStreamNode(out, n[0], depth, false, lbind);
638
      }
639
      return;
640
    }
641
    case kind::DIVISIBLE:
642
      out << "DIVISIBLE(";
643
      toStreamNode(out, n[0], depth, false, lbind);
644
      out << ", " << n.getOperator().getConst<Divisible>().k << ")";
645
      return;
646
647
    // BITVECTORS
648
    case kind::BITVECTOR_XOR:
649
      op << "BVXOR";
650
      break;
651
    case kind::BITVECTOR_NAND:
652
      op << "BVNAND";
653
      break;
654
    case kind::BITVECTOR_NOR:
655
      op << "BVNOR";
656
      break;
657
    case kind::BITVECTOR_XNOR:
658
      op << "BVXNOR";
659
      break;
660
    case kind::BITVECTOR_COMP:
661
      op << "BVCOMP";
662
      break;
663
    case kind::BITVECTOR_UDIV:
664
      op << "BVUDIV";
665
      break;
666
    case kind::BITVECTOR_UREM:
667
      op << "BVUREM";
668
      break;
669
    case kind::BITVECTOR_SDIV:
670
      op << "BVSDIV";
671
      break;
672
    case kind::BITVECTOR_SREM:
673
      op << "BVSREM";
674
      break;
675
    case kind::BITVECTOR_SMOD:
676
      op << "BVSMOD";
677
      break;
678
    case kind::BITVECTOR_SHL:
679
      op << "BVSHL";
680
      break;
681
    case kind::BITVECTOR_LSHR:
682
      op << "BVLSHR";
683
      break;
684
    case kind::BITVECTOR_ASHR:
685
      op << "BVASHR";
686
      break;
687
    case kind::BITVECTOR_ULT:
688
      op << "BVLT";
689
      break;
690
    case kind::BITVECTOR_ULE:
691
      op << "BVLE";
692
      break;
693
    case kind::BITVECTOR_UGT:
694
      op << "BVGT";
695
      break;
696
    case kind::BITVECTOR_UGE:
697
      op << "BVGE";
698
      break;
699
    case kind::BITVECTOR_SLT:
700
      op << "BVSLT";
701
      break;
702
    case kind::BITVECTOR_SLE:
703
      op << "BVSLE";
704
      break;
705
    case kind::BITVECTOR_SGT:
706
      op << "BVSGT";
707
      break;
708
    case kind::BITVECTOR_SGE:
709
      op << "BVSGE";
710
      break;
711
    case kind::BITVECTOR_NEG:
712
      op << "BVUMINUS";
713
      break;
714
4
    case kind::BITVECTOR_NOT:
715
4
      op << "~";
716
4
      break;
717
    case kind::BITVECTOR_AND:
718
      op << "&";
719
      opType = INFIX;
720
      break;
721
    case kind::BITVECTOR_OR:
722
      op << "|";
723
      opType = INFIX;
724
      break;
725
    case kind::BITVECTOR_CONCAT:
726
      op << "@";
727
      opType = INFIX;
728
      break;
729
4
    case kind::BITVECTOR_PLUS: {
730
      // This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB
731
4
      Assert(n.getType().isBitVector());
732
4
      unsigned numc = n.getNumChildren()-2;
733
4
      unsigned child = 0;
734
4
      while (child < numc) {
735
        out << "BVPLUS(";
736
        out << n.getType().getBitVectorSize();
737
        out << ',';
738
        toStreamNode(out, n[child], depth, false, lbind);
739
        out << ',';
740
        ++child;
741
      }
742
4
      out << "BVPLUS(";
743
4
      out << n.getType().getBitVectorSize();
744
4
      out << ',';
745
4
      toStreamNode(out, n[child], depth, false, lbind);
746
4
      out << ',';
747
4
      toStreamNode(out, n[child + 1], depth, false, lbind);
748
4
      while (child > 0) {
749
        out << ')';
750
        --child;
751
      }
752
4
      out << ')';
753
4
      return;
754
      break;
755
    }
756
    case kind::BITVECTOR_SUB:
757
      out << "BVSUB(";
758
      Assert(n.getType().isBitVector());
759
      out << n.getType().getBitVectorSize();
760
      out << ',';
761
      toStreamNode(out, n[0], depth, false, lbind);
762
      out << ',';
763
      toStreamNode(out, n[1], depth, false, lbind);
764
      out << ')';
765
      return;
766
      break;
767
2
    case kind::BITVECTOR_MULT: {
768
2
      Assert(n.getType().isBitVector());
769
2
      unsigned numc = n.getNumChildren()-2;
770
2
      unsigned child = 0;
771
2
      while (child < numc) {
772
        out << "BVMULT(";
773
        out << n.getType().getBitVectorSize();
774
        out << ',';
775
        toStreamNode(out, n[child], depth, false, lbind);
776
        out << ',';
777
        ++child;
778
        }
779
2
      out << "BVMULT(";
780
2
      out << n.getType().getBitVectorSize();
781
2
      out << ',';
782
2
      toStreamNode(out, n[child], depth, false, lbind);
783
2
      out << ',';
784
2
      toStreamNode(out, n[child + 1], depth, false, lbind);
785
2
      while (child > 0) {
786
        out << ')';
787
        --child;
788
      }
789
2
      out << ')';
790
2
      return;
791
      break;
792
    }
793
4
    case kind::BITVECTOR_EXTRACT:
794
4
      op << n.getOperator().getConst<BitVectorExtract>();
795
4
      opType = POSTFIX;
796
4
      break;
797
    case kind::BITVECTOR_BITOF:
798
      op << n.getOperator().getConst<BitVectorBitOf>();
799
      opType = POSTFIX;
800
      break;
801
    case kind::BITVECTOR_REPEAT:
802
      out << "BVREPEAT(";
803
      toStreamNode(out, n[0], depth, false, lbind);
804
      out << ", " << n.getOperator().getConst<BitVectorRepeat>() << ')';
805
      return;
806
      break;
807
8
    case kind::BITVECTOR_ZERO_EXTEND:
808
8
      out << "BVZEROEXTEND(";
809
8
      toStreamNode(out, n[0], depth, false, lbind);
810
8
      out << ", " << n.getOperator().getConst<BitVectorZeroExtend>() << ')';
811
8
      return;
812
      break;
813
    case kind::BITVECTOR_SIGN_EXTEND:
814
      out << "SX(";
815
      toStreamNode(out, n[0], depth, false, lbind);
816
      out << ", " << n.getType().getBitVectorSize() << ')';
817
      return;
818
      break;
819
    case kind::BITVECTOR_ROTATE_LEFT:
820
      out << "BVROTL(";
821
      toStreamNode(out, n[0], depth, false, lbind);
822
      out << ", " << n.getOperator().getConst<BitVectorRotateLeft>() << ')';
823
      return;
824
      break;
825
    case kind::BITVECTOR_ROTATE_RIGHT:
826
      out << "BVROTR(";
827
      toStreamNode(out, n[0], depth, false, lbind);
828
      out << ", " << n.getOperator().getConst<BitVectorRotateRight>() << ')';
829
      return;
830
      break;
831
832
    // SETS
833
46
    case kind::SET_TYPE:
834
46
      out << "SET OF ";
835
46
      toStreamNode(out, n[0], depth, false, lbind);
836
46
      return;
837
      break;
838
    case kind::UNION:
839
      op << '|';
840
      opType = INFIX;
841
      break;
842
    case kind::INTERSECTION:
843
      op << '&';
844
      opType = INFIX;
845
      break;
846
    case kind::SETMINUS:
847
      op << '-';
848
      opType = INFIX;
849
      break;
850
    case kind::SUBSET:
851
      op << "<=";
852
      opType = INFIX;
853
      break;
854
    case kind::MEMBER:
855
      op << "IS_IN";
856
      opType = INFIX;
857
      break;
858
    case kind::COMPLEMENT:
859
      op << "~";
860
      opType = PREFIX;
861
      break;
862
    case kind::PRODUCT:
863
      op << "PRODUCT";
864
      opType = INFIX;
865
      break;
866
    case kind::JOIN:
867
      op << "JOIN";
868
      opType = INFIX;
869
      break;
870
    case kind::TRANSPOSE:
871
      op << "TRANSPOSE";
872
      opType = PREFIX;
873
      break;
874
    case kind::TCLOSURE:
875
      op << "TCLOSURE";
876
      opType = PREFIX;
877
      break;
878
    case kind::IDEN:
879
      op << "IDEN";
880
      opType = PREFIX;
881
      break;
882
    case kind::JOIN_IMAGE:
883
      op << "JOIN_IMAGE";
884
      opType = INFIX;
885
      break;
886
3
    case kind::SINGLETON:
887
3
      out << "{";
888
3
      toStreamNode(out, n[0], depth, false, lbind);
889
3
      out << "}";
890
3
      return;
891
      break;
892
    case kind::INSERT: {
893
      if(bracket) {
894
        out << '(';
895
      }
896
      out << '{';
897
      size_t i = 0;
898
      toStreamNode(out, n[i++], depth, false, lbind);
899
      for(;i+1 < n.getNumChildren(); ++i) {
900
        out << ", ";
901
        toStreamNode(out, n[i], depth, false, lbind);
902
      }
903
      out << "} | ";
904
      toStreamNode(out, n[i], depth, true, lbind);
905
      if(bracket) {
906
        out << ')';
907
      }
908
      return;
909
      break;
910
    }
911
    case kind::CARD: {
912
      out << "CARD(";
913
      toStreamNode(out, n[0], depth, false, lbind);
914
      out << ")";
915
      return;
916
      break;
917
    }
918
919
    // Quantifiers
920
    case kind::FORALL:
921
      out << "(FORALL";
922
      toStreamNode(out, n[0], depth, true, lbind);
923
      out << " : ";
924
      toStreamNodeWithLetify(out, n[1], depth, true, lbind);
925
      out << ')';
926
      // TODO: user patterns?
927
      return;
928
    case kind::EXISTS:
929
      out << "(EXISTS";
930
      toStreamNode(out, n[0], depth, true, lbind);
931
      out << " : ";
932
      toStreamNodeWithLetify(out, n[1], depth, true, lbind);
933
      out << ')';
934
      // TODO: user patterns?
935
      return;
936
    case kind::INST_CONSTANT:
937
      out << "INST_CONSTANT";
938
      break;
939
2
    case kind::BOUND_VAR_LIST:
940
2
      out << '(';
941
4
      for(size_t i = 0; i < n.getNumChildren(); ++i) {
942
2
        if(i > 0) {
943
          out << ", ";
944
        }
945
2
        toStreamNode(out, n[i], -1, false, lbind);
946
2
        out << ":";
947
2
        n[i].getType().toStream(out, language::output::LANG_CVC4);
948
2
      }
949
2
      out << ')';
950
2
      return;
951
    case kind::INST_PATTERN:
952
      out << "INST_PATTERN";
953
      break;
954
    case kind::INST_PATTERN_LIST:
955
      out << "INST_PATTERN_LIST";
956
      break;
957
958
    // string operators
959
    case kind::STRING_CONCAT:
960
      out << "CONCAT";
961
      break;
962
    case kind::STRING_CHARAT:
963
      out << "CHARAT";
964
      break;
965
    case kind::STRING_LENGTH:
966
      out << "LENGTH";
967
      break;
968
    case kind::STRING_SUBSTR: out << "SUBSTR"; break;
969
970
    default:
971
      Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl;
972
      break;
973
  }
974
975
926
  switch (opType) {
976
703
  case PREFIX:
977
703
    out << op.str();
978
703
    if (n.getNumChildren() > 0)
979
    {
980
703
      out << '(';
981
    }
982
703
    break;
983
219
  case INFIX:
984
219
    if (bracket) {
985
103
      out << '(';
986
    }
987
219
    break;
988
4
  case POSTFIX:
989
4
    out << '(';
990
4
    break;
991
  }
992
993
2751
  for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
994
1825
    if (i > 0) {
995
899
      if (opType == INFIX) {
996
309
        out << ' ' << op.str() << ' ';
997
      } else {
998
590
        out << ", ";
999
      }
1000
    }
1001
1825
    toStreamNode(out, n[i], depth, opType == INFIX, lbind);
1002
  }
1003
1004
926
  switch (opType) {
1005
703
    case PREFIX:
1006
703
      if (n.getNumChildren() > 0)
1007
      {
1008
703
        out << ')';
1009
      }
1010
703
      break;
1011
219
    case INFIX:
1012
219
      if (bracket) {
1013
103
        out << ')';
1014
      }
1015
219
      break;
1016
4
    case POSTFIX:
1017
4
      out << ')' << op.str();
1018
4
      break;
1019
  }
1020
}
1021
1022
template <class T>
1023
static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode);
1024
1025
template <class T>
1026
static bool tryToStream(std::ostream& out,
1027
                        const CommandStatus* s,
1028
                        bool cvc3Mode);
1029
1030
11988
void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const
1031
{
1032
23976
  if (tryToStream<CommandSuccess>(out, s, d_cvc3Mode)
1033
6
      || tryToStream<CommandFailure>(out, s, d_cvc3Mode)
1034
1
      || tryToStream<CommandRecoverableFailure>(out, s, d_cvc3Mode)
1035
      || tryToStream<CommandUnsupported>(out, s, d_cvc3Mode)
1036
11988
      || tryToStream<CommandInterrupted>(out, s, d_cvc3Mode))
1037
  {
1038
11988
    return;
1039
  }
1040
1041
  out << "ERROR: don't know how to print a CommandStatus of class: "
1042
      << typeid(*s).name() << endl;
1043
1044
}/* CvcPrinter::toStream(CommandStatus*) */
1045
1046
void CvcPrinter::toStreamModelSort(std::ostream& out,
1047
                                   const smt::Model& m,
1048
                                   TypeNode tn) const
1049
{
1050
  if (!tn.isSort())
1051
  {
1052
    out << "ERROR: don't know how to print a non uninterpreted sort in model: "
1053
        << tn << std::endl;
1054
    return;
1055
  }
1056
  const theory::TheoryModel* tm = m.getTheoryModel();
1057
  const std::vector<Node>* type_reps = tm->getRepSet()->getTypeRepsOrNull(tn);
1058
47
  if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
1059
      && type_reps != nullptr)
1060
  {
1061
    out << "DATATYPE" << std::endl;
1062
    out << "  " << tn << " = ";
1063
    for (size_t i = 0; i < type_reps->size(); i++)
1064
    {
1065
      if (i > 0)
1066
      {
1067
        out << "| ";
1068
      }
1069
      out << (*type_reps)[i] << " ";
1070
    }
1071
    out << std::endl << "END;" << std::endl;
1072
  }
1073
  else if (type_reps != nullptr)
1074
  {
1075
    out << "% cardinality of " << tn << " is " << type_reps->size()
1076
        << std::endl;
1077
    toStreamCmdDeclareType(out, tn);
1078
    for (Node type_rep : *type_reps)
1079
    {
1080
      if (type_rep.isVar())
1081
      {
1082
        out << type_rep << " : " << tn << ";" << std::endl;
1083
      }
1084
      else
1085
      {
1086
        out << "% rep: " << type_rep << std::endl;
1087
      }
1088
    }
1089
  }
1090
  else
1091
  {
1092
    toStreamCmdDeclareType(out, tn);
1093
  }
1094
}
1095
1096
6
void CvcPrinter::toStreamModelTerm(std::ostream& out,
1097
                                   const smt::Model& m,
1098
                                   Node n) const
1099
{
1100
6
  const theory::TheoryModel* tm = m.getTheoryModel();
1101
12
  TypeNode tn = n.getType();
1102
6
  out << n << " : ";
1103
6
  if (tn.isFunction() || tn.isPredicate())
1104
  {
1105
2
    out << "(";
1106
4
    for (size_t i = 0; i < tn.getNumChildren() - 1; i++)
1107
    {
1108
2
      if (i > 0)
1109
      {
1110
        out << ", ";
1111
      }
1112
2
      out << tn[i];
1113
    }
1114
2
    out << ") -> " << tn.getRangeType();
1115
  }
1116
  else
1117
  {
1118
4
    out << tn;
1119
  }
1120
  // We get the value from the theory model directly, which notice
1121
  // does not have to go through the standard SmtEngine::getValue interface.
1122
12
  Node val = tm->getValue(n);
1123
12
  if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
1124
6
      && val.getKind() == kind::STORE)
1125
  {
1126
    TypeNode type_node = val[1].getType();
1127
    if (tn.isSort())
1128
    {
1129
      const std::vector<Node>* type_reps =
1130
          tm->getRepSet()->getTypeRepsOrNull(type_node);
1131
      if (type_reps != nullptr)
1132
      {
1133
        Cardinality indexCard(type_reps->size());
1134
        val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
1135
            val, indexCard);
1136
      }
1137
    }
1138
  }
1139
6
  out << " = " << val << ";" << std::endl;
1140
6
}
1141
1142
4
void CvcPrinter::toStream(std::ostream& out, const smt::Model& m) const
1143
{
1144
4
  const theory::TheoryModel* tm = m.getTheoryModel();
1145
  // print the model comments
1146
8
  std::stringstream c;
1147
4
  tm->getComments(c);
1148
8
  std::string ln;
1149
4
  while (std::getline(c, ln))
1150
  {
1151
    out << "; " << ln << std::endl;
1152
  }
1153
1154
  // print the model
1155
4
  out << "MODEL BEGIN" << std::endl;
1156
4
  this->Printer::toStream(out, m);
1157
4
  out << "MODEL END;" << std::endl;
1158
4
}
1159
1160
void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
1161
{
1162
  out << "ASSERT " << n << ';' << std::endl;
1163
}
1164
1165
void CvcPrinter::toStreamCmdPush(std::ostream& out) const
1166
{
1167
  out << "PUSH;" << std::endl;
1168
}
1169
1170
void CvcPrinter::toStreamCmdPop(std::ostream& out) const
1171
{
1172
  out << "POP;" << std::endl;
1173
}
1174
1175
void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
1176
{
1177
  if (d_cvc3Mode)
1178
  {
1179
    out << "PUSH; ";
1180
  }
1181
  if (!n.isNull())
1182
  {
1183
    out << "CHECKSAT " << n << ';';
1184
  }
1185
  else
1186
  {
1187
    out << "CHECKSAT;";
1188
  }
1189
  if (d_cvc3Mode)
1190
  {
1191
    out << " POP;";
1192
  }
1193
  out << std::endl;
1194
}
1195
1196
void CvcPrinter::toStreamCmdCheckSatAssuming(
1197
    std::ostream& out, const std::vector<Node>& nodes) const
1198
{
1199
  if (d_cvc3Mode)
1200
  {
1201
    out << "PUSH; ";
1202
  }
1203
  out << "CHECKSAT";
1204
  if (nodes.size() > 0)
1205
  {
1206
    out << ' ' << nodes[0];
1207
    for (size_t i = 1, n = nodes.size(); i < n; ++i)
1208
    {
1209
      out << " AND " << nodes[i];
1210
    }
1211
  }
1212
  out << ';';
1213
  if (d_cvc3Mode)
1214
  {
1215
    out << " POP;";
1216
  }
1217
  out << std::endl;
1218
}
1219
1220
void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
1221
{
1222
  if (d_cvc3Mode)
1223
  {
1224
    out << "PUSH; ";
1225
  }
1226
  if (!n.isNull())
1227
  {
1228
    out << "QUERY " << n << ';';
1229
  }
1230
  else
1231
  {
1232
    out << "QUERY TRUE;";
1233
  }
1234
  if (d_cvc3Mode)
1235
  {
1236
    out << " POP;";
1237
  }
1238
  out << std::endl;
1239
}
1240
1241
void CvcPrinter::toStreamCmdReset(std::ostream& out) const
1242
{
1243
  out << "RESET;" << std::endl;
1244
}
1245
1246
void CvcPrinter::toStreamCmdResetAssertions(std::ostream& out) const
1247
{
1248
  out << "RESET ASSERTIONS;" << std::endl;
1249
}
1250
1251
void CvcPrinter::toStreamCmdQuit(std::ostream& out) const
1252
{
1253
  // out << "EXIT;" << std::endl;
1254
}
1255
1256
void CvcPrinter::toStreamCmdCommandSequence(
1257
    std::ostream& out, const std::vector<Command*>& sequence) const
1258
{
1259
  for (CommandSequence::const_iterator i = sequence.cbegin();
1260
       i != sequence.cend();
1261
       ++i)
1262
  {
1263
    out << *i;
1264
  }
1265
}
1266
1267
void CvcPrinter::toStreamCmdDeclarationSequence(
1268
    std::ostream& out, const std::vector<Command*>& sequence) const
1269
{
1270
  DeclarationSequence::const_iterator i = sequence.cbegin();
1271
  for (;;)
1272
  {
1273
    DeclarationDefinitionCommand* dd =
1274
        static_cast<DeclarationDefinitionCommand*>(*i++);
1275
    Assert(dd != nullptr);
1276
    if (i != sequence.cend())
1277
    {
1278
      out << dd->getSymbol() << ", ";
1279
    }
1280
    else
1281
    {
1282
      out << *dd;
1283
      break;
1284
    }
1285
  }
1286
  out << std::endl;
1287
}
1288
1289
void CvcPrinter::toStreamCmdDeclareFunction(std::ostream& out,
1290
                                            const std::string& id,
1291
                                            TypeNode type) const
1292
{
1293
  out << id << " : " << type << ';' << std::endl;
1294
}
1295
1296
void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out,
1297
                                           const std::string& id,
1298
                                           const std::vector<Node>& formals,
1299
                                           TypeNode range,
1300
                                           Node formula) const
1301
{
1302
  std::vector<TypeNode> sorts;
1303
  sorts.reserve(formals.size() + 1);
1304
  for (const Node& n : formals)
1305
  {
1306
    sorts.push_back(n.getType());
1307
  }
1308
  sorts.push_back(range);
1309
1310
  out << id << " : " << NodeManager::currentNM()->mkFunctionType(sorts)
1311
      << " = ";
1312
  if (formals.size() > 0)
1313
  {
1314
    out << "LAMBDA(";
1315
    vector<Node>::const_iterator i = formals.cbegin();
1316
    while (i != formals.end())
1317
    {
1318
      out << (*i) << ":" << (*i).getType();
1319
      if (++i != formals.end())
1320
      {
1321
        out << ", ";
1322
      }
1323
    }
1324
    out << "): ";
1325
  }
1326
  out << formula << ';' << std::endl;
1327
}
1328
1329
void CvcPrinter::toStreamCmdDeclareType(std::ostream& out,
1330
                                        TypeNode type) const
1331
{
1332
  size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0;
1333
  if (arity > 0)
1334
  {
1335
    out << "ERROR: Don't know how to print parameterized type declaration "
1336
           "in CVC language."
1337
        << std::endl;
1338
  }
1339
  else
1340
  {
1341
    out << type << " : TYPE;" << std::endl;
1342
  }
1343
}
1344
1345
void CvcPrinter::toStreamCmdDefineType(std::ostream& out,
1346
                                       const std::string& id,
1347
                                       const std::vector<TypeNode>& params,
1348
                                       TypeNode t) const
1349
{
1350
  if (params.size() > 0)
1351
  {
1352
    out << "ERROR: Don't know how to print parameterized type definition "
1353
           "in CVC language:"
1354
        << std::endl;
1355
  }
1356
  else
1357
  {
1358
    out << id << " : TYPE = " << t << ';' << std::endl;
1359
  }
1360
}
1361
1362
void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
1363
{
1364
  out << "TRANSFORM " << n << ';' << std::endl;
1365
}
1366
1367
void CvcPrinter::toStreamCmdGetValue(std::ostream& out,
1368
                                     const std::vector<Node>& nodes) const
1369
{
1370
  Assert(!nodes.empty());
1371
  out << "GET_VALUE ";
1372
  copy(nodes.begin(),
1373
       nodes.end() - 1,
1374
       ostream_iterator<Node>(out, ";\nGET_VALUE "));
1375
  out << nodes.back() << ';' << std::endl;
1376
}
1377
1378
void CvcPrinter::toStreamCmdGetModel(std::ostream& out) const
1379
{
1380
  out << "COUNTERMODEL;" << std::endl;
1381
}
1382
1383
void CvcPrinter::toStreamCmdGetAssignment(std::ostream& out) const
1384
{
1385
  out << "% (get-assignment)" << std::endl;
1386
}
1387
1388
void CvcPrinter::toStreamCmdGetAssertions(std::ostream& out) const
1389
{
1390
  out << "WHERE;" << std::endl;
1391
}
1392
1393
void CvcPrinter::toStreamCmdGetProof(std::ostream& out) const
1394
{
1395
  out << "DUMP_PROOF;" << std::endl;
1396
}
1397
1398
void CvcPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
1399
{
1400
  out << "DUMP_UNSAT_CORE;" << std::endl;
1401
}
1402
1403
void CvcPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
1404
                                               Result::Sat status) const
1405
{
1406
  out << "% (set-info :status " << status << ')' << std::endl;
1407
}
1408
1409
void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
1410
                                              const std::string& logic) const
1411
{
1412
  out << "OPTION \"logic\" \"" << logic << "\";" << std::endl;
1413
}
1414
1415
void CvcPrinter::toStreamCmdSetInfo(std::ostream& out,
1416
                                    const std::string& flag,
1417
                                    const std::string& value) const
1418
{
1419
  out << "% (set-info " << flag << ' ' << value << ')' << std::endl;
1420
}
1421
1422
void CvcPrinter::toStreamCmdGetInfo(std::ostream& out,
1423
                                    const std::string& flag) const
1424
{
1425
  out << "% (get-info " << flag << ')' << std::endl;
1426
}
1427
1428
void CvcPrinter::toStreamCmdSetOption(std::ostream& out,
1429
                                      const std::string& flag,
1430
                                      const std::string& value) const
1431
{
1432
  out << "OPTION \"" << flag << "\" " << value << ';' << std::endl;
1433
}
1434
1435
void CvcPrinter::toStreamCmdGetOption(std::ostream& out,
1436
                                      const std::string& flag) const
1437
{
1438
  out << "% (get-option " << flag << ')' << std::endl;
1439
}
1440
1441
void CvcPrinter::toStreamCmdDatatypeDeclaration(
1442
    std::ostream& out, const std::vector<TypeNode>& datatypes) const
1443
{
1444
  Assert(!datatypes.empty() && datatypes[0].isDatatype());
1445
  const DType& dt0 = datatypes[0].getDType();
1446
  // do not print tuple/datatype internal declarations
1447
  if (datatypes.size() != 1 || (!dt0.isTuple() && !dt0.isRecord()))
1448
  {
1449
    out << "DATATYPE" << endl;
1450
    bool firstDatatype = true;
1451
    for (const TypeNode& t : datatypes)
1452
    {
1453
      if (!firstDatatype)
1454
      {
1455
        out << ',' << endl;
1456
      }
1457
      const DType& dt = t.getDType();
1458
      out << "  " << dt.getName();
1459
      if (dt.isParametric())
1460
      {
1461
        out << '[';
1462
        for (size_t j = 0; j < dt.getNumParameters(); ++j)
1463
        {
1464
          if (j > 0)
1465
          {
1466
            out << ',';
1467
          }
1468
          out << dt.getParameter(j);
1469
        }
1470
        out << ']';
1471
      }
1472
      out << " = ";
1473
      for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
1474
      {
1475
        const DTypeConstructor& cons = dt[j];
1476
        if (j != 0)
1477
        {
1478
          out << " | ";
1479
        }
1480
        out << cons.getName();
1481
        if (cons.getNumArgs() > 0)
1482
        {
1483
          out << '(';
1484
          for (size_t k = 0, nargs = cons.getNumArgs(); k < nargs; k++)
1485
          {
1486
            if (k != 0)
1487
            {
1488
              out << ", ";
1489
            }
1490
            const DTypeSelector& selector = cons[k];
1491
            TypeNode tr = selector.getRangeType();
1492
            if (tr.isDatatype())
1493
            {
1494
              const DType& sdt = tr.getDType();
1495
              out << selector.getName() << ": " << sdt.getName();
1496
            }
1497
            else
1498
            {
1499
              out << selector.getName() << ": " << tr;
1500
            }
1501
          }
1502
          out << ')';
1503
        }
1504
      }
1505
      firstDatatype = false;
1506
    }
1507
    out << endl << "END;" << std::endl;
1508
  }
1509
}
1510
1511
void CvcPrinter::toStreamCmdComment(std::ostream& out,
1512
                                    const std::string& comment) const
1513
{
1514
  out << "% " << comment << std::endl;
1515
}
1516
1517
void CvcPrinter::toStreamCmdEmpty(std::ostream& out,
1518
                                  const std::string& name) const
1519
{
1520
  out << std::endl;
1521
}
1522
1523
void CvcPrinter::toStreamCmdEcho(std::ostream& out,
1524
                                 const std::string& output) const
1525
{
1526
  out << "ECHO \"" << output << "\";" << std::endl;
1527
}
1528
1529
template <class T>
1530
static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode)
1531
{
1532
  if(typeid(*c) == typeid(T)) {
1533
    toStream(out, dynamic_cast<const T*>(c), cvc3Mode);
1534
    return true;
1535
  }
1536
  return false;
1537
}
1538
1539
11982
static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode)
1540
{
1541
11982
  if(Command::printsuccess::getPrintSuccess(out)) {
1542
    out << "OK" << endl;
1543
  }
1544
11982
}
1545
1546
static void toStream(std::ostream& out,
1547
                     const CommandUnsupported* s,
1548
                     bool cvc3Mode)
1549
{
1550
  out << "UNSUPPORTED" << endl;
1551
}
1552
1553
static void toStream(std::ostream& out,
1554
                     const CommandInterrupted* s,
1555
                     bool cvc3Mode)
1556
{
1557
  out << "INTERRUPTED" << endl;
1558
}
1559
1560
5
static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode)
1561
{
1562
5
  out << s->getMessage() << endl;
1563
5
}
1564
1565
1
static void toStream(std::ostream& out,
1566
                     const CommandRecoverableFailure* s,
1567
                     bool cvc3Mode)
1568
{
1569
1
  out << s->getMessage() << endl;
1570
1
}
1571
1572
template <class T>
1573
11995
static bool tryToStream(std::ostream& out,
1574
                        const CommandStatus* s,
1575
                        bool cvc3Mode)
1576
{
1577
11995
  if(typeid(*s) == typeid(T)) {
1578
11988
    toStream(out, dynamic_cast<const T*>(s), cvc3Mode);
1579
11988
    return true;
1580
  }
1581
7
  return false;
1582
}
1583
1584
822
void CvcPrinter::toStreamNodeWithLetify(std::ostream& out,
1585
                                        Node n,
1586
                                        int toDepth,
1587
                                        bool bracket,
1588
                                        LetBinding* lbind) const
1589
{
1590
822
  if (lbind == nullptr)
1591
  {
1592
2
    toStreamNode(out, n, toDepth, bracket, nullptr);
1593
2
    return;
1594
  }
1595
1640
  std::vector<Node> letList;
1596
820
  lbind->letify(n, letList);
1597
820
  if (!letList.empty())
1598
  {
1599
11
    std::map<Node, uint32_t>::const_iterator it;
1600
11
    out << "LET ";
1601
11
    bool first = true;
1602
60
    for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
1603
    {
1604
49
      if (!first)
1605
      {
1606
38
        out << ", ";
1607
      }
1608
      else
1609
      {
1610
11
        first = false;
1611
      }
1612
98
      Node nl = letList[i];
1613
49
      uint32_t id = lbind->getId(nl);
1614
49
      out << "_let_" << id << " = ";
1615
98
      Node nlc = lbind->convert(nl, "_let_", false);
1616
49
      toStreamNode(out, nlc, toDepth, true, lbind);
1617
    }
1618
11
    out << " IN ";
1619
  }
1620
1640
  Node nc = lbind->convert(n, "_let_");
1621
  // print the body, passing the lbind object
1622
820
  toStreamNode(out, nc, toDepth, bracket, lbind);
1623
820
  lbind->popScope();
1624
}
1625
1626
}/* CVC4::printer::cvc namespace */
1627
}/* CVC4::printer namespace */
1628
26732
}/* CVC4 namespace */