GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/printer/smt2/smt2_printer.cpp Lines: 605 1193 50.7 %
Date: 2021-03-23 Branches: 1007 3230 31.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file smt2_printer.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
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 SMT2 output language
13
 **
14
 ** The pretty-printer interface for the SMT2 output language.
15
 **/
16
17
#include "printer/smt2/smt2_printer.h"
18
19
#include <iostream>
20
#include <list>
21
#include <string>
22
#include <typeinfo>
23
#include <vector>
24
25
#include "api/cvc4cpp.h"
26
#include "expr/dtype.h"
27
#include "expr/dtype_cons.h"
28
#include "expr/node_manager_attributes.h"
29
#include "expr/node_visitor.h"
30
#include "expr/sequence.h"
31
#include "options/bv_options.h"
32
#include "options/language.h"
33
#include "options/printer_options.h"
34
#include "options/smt_options.h"
35
#include "printer/let_binding.h"
36
#include "proof/unsat_core.h"
37
#include "smt/command.h"
38
#include "smt/node_command.h"
39
#include "smt/smt_engine.h"
40
#include "smt_util/boolean_simplification.h"
41
#include "theory/arrays/theory_arrays_rewriter.h"
42
#include "theory/datatypes/sygus_datatype_utils.h"
43
#include "theory/quantifiers/quantifiers_attributes.h"
44
#include "theory/theory_model.h"
45
#include "util/smt2_quote_string.h"
46
47
using namespace std;
48
49
namespace CVC4 {
50
namespace printer {
51
namespace smt2 {
52
53
726121
static void toStreamRational(std::ostream& out,
54
                             const Rational& r,
55
                             bool decimal,
56
                             Variant v)
57
{
58
726121
  bool neg = r.sgn() < 0;
59
  // Print the rational, possibly as decimal.
60
  // Notice that we print (/ (- 5) 3) instead of (- (/ 5 3)),
61
  // the former is compliant with real values in the smt lib standard.
62
726121
  if (r.isIntegral())
63
  {
64
726001
    if (neg)
65
    {
66
74436
      out << "(- " << -r;
67
    }
68
    else
69
    {
70
651565
      out << r;
71
    }
72
726001
    if (decimal)
73
    {
74
14
      out << ".0";
75
    }
76
726001
    if (neg)
77
    {
78
74436
      out << ")";
79
    }
80
  }
81
  else
82
  {
83
120
    out << "(/ ";
84
120
    if (neg)
85
    {
86
60
      Rational abs_r = (-r);
87
30
      out << "(- " << abs_r.getNumerator();
88
30
      out << ") " << abs_r.getDenominator();
89
    }
90
    else
91
    {
92
90
      out << r.getNumerator();
93
90
      out << ' ' << r.getDenominator();
94
    }
95
120
    out << ')';
96
  }
97
726121
}
98
99
623798
void Smt2Printer::toStream(std::ostream& out,
100
                           TNode n,
101
                           int toDepth,
102
                           size_t dag) const
103
{
104
623798
  if(dag != 0) {
105
115722
    LetBinding lbind(dag + 1);
106
57875
    toStreamWithLetify(out, n, toDepth, &lbind);
107
  } else {
108
565937
    toStream(out, n, toDepth);
109
  }
110
623784
}
111
112
57861
void Smt2Printer::toStreamWithLetify(std::ostream& out,
113
                                     Node n,
114
                                     int toDepth,
115
                                     LetBinding* lbind) const
116
{
117
57861
  if (lbind == nullptr)
118
  {
119
    toStream(out, n, toDepth);
120
    return;
121
  }
122
115722
  std::stringstream cparen;
123
115722
  std::vector<Node> letList;
124
57861
  lbind->letify(n, letList);
125
57861
  if (!letList.empty())
126
  {
127
31641
    std::map<Node, uint32_t>::const_iterator it;
128
120252
    for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
129
    {
130
177222
      Node nl = letList[i];
131
88611
      out << "(let ((";
132
88611
      uint32_t id = lbind->getId(nl);
133
88611
      out << "_let_" << id << " ";
134
177222
      Node nlc = lbind->convert(nl, "_let_", false);
135
88611
      toStream(out, nlc, toDepth, lbind);
136
88611
      out << ")) ";
137
88611
      cparen << ")";
138
    }
139
  }
140
115722
  Node nc = lbind->convert(n, "_let_");
141
  // print the body, passing the lbind object
142
57847
  toStream(out, nc, toDepth, lbind);
143
57847
  out << cparen.str();
144
57847
  lbind->popScope();
145
}
146
147
2101204
void Smt2Printer::toStream(std::ostream& out,
148
                           TNode n,
149
                           int toDepth,
150
                           LetBinding* lbind) const
151
{
152
  // null
153
2101204
  if(n.getKind() == kind::NULL_EXPR) {
154
    out << "null";
155
1508874
    return;
156
  }
157
158
2101204
  NodeManager* nm = NodeManager::currentNM();
159
  // constant
160
2101204
  if(n.getMetaKind() == kind::metakind::CONSTANT) {
161
782724
    switch(n.getKind()) {
162
14380
    case kind::TYPE_CONSTANT:
163
14380
      switch(n.getConst<TypeConstant>()) {
164
2493
      case BOOLEAN_TYPE: out << "Bool"; break;
165
573
      case REAL_TYPE: out << "Real"; break;
166
10554
      case INTEGER_TYPE: out << "Int"; break;
167
692
      case STRING_TYPE: out << "String"; break;
168
6
      case REGEXP_TYPE: out << "RegLan"; break;
169
62
      case ROUNDINGMODE_TYPE: out << "RoundingMode"; break;
170
      default:
171
        // fall back on whatever operator<< does on underlying type; we
172
        // might luck out and be SMT-LIB v2 compliant
173
        kind::metakind::NodeValueConstPrinter::toStream(out, n);
174
      }
175
14380
      break;
176
4922
    case kind::BITVECTOR_TYPE:
177
4922
      out << "(_ BitVec " << n.getConst<BitVectorSize>().d_size << ")";
178
4922
      break;
179
212
    case kind::FLOATINGPOINT_TYPE:
180
212
      out << "(_ FloatingPoint "
181
212
          << n.getConst<FloatingPointSize>().exponentWidth() << " "
182
212
          << n.getConst<FloatingPointSize>().significandWidth() << ")";
183
212
      break;
184
243
    case kind::CONST_BITVECTOR:
185
    {
186
243
      const BitVector& bv = n.getConst<BitVector>();
187
490
      if (options::bvPrintConstsAsIndexedSymbols())
188
      {
189
2
        out << "(_ bv" << bv.getValue() << " " << bv.getSize() << ")";
190
      }
191
      else
192
      {
193
241
        out << "#b" << bv.toString();
194
      }
195
243
      break;
196
    }
197
    case kind::CONST_FLOATINGPOINT:
198
    {
199
      out << n.getConst<FloatingPoint>().toString(
200
          options::bvPrintConstsAsIndexedSymbols());
201
      break;
202
    }
203
    case kind::CONST_ROUNDINGMODE:
204
      switch (n.getConst<RoundingMode>()) {
205
        case ROUND_NEAREST_TIES_TO_EVEN: out << "roundNearestTiesToEven"; break;
206
        case ROUND_NEAREST_TIES_TO_AWAY: out << "roundNearestTiesToAway"; break;
207
        case ROUND_TOWARD_POSITIVE: out << "roundTowardPositive"; break;
208
        case ROUND_TOWARD_NEGATIVE: out << "roundTowardNegative"; break;
209
        case ROUND_TOWARD_ZERO: out << "roundTowardZero"; break;
210
        default:
211
          Unreachable() << "Invalid value of rounding mode constant ("
212
                        << n.getConst<RoundingMode>() << ")";
213
      }
214
      break;
215
32803
    case kind::CONST_BOOLEAN:
216
      // the default would print "1" or "0" for bool, that's not correct
217
      // for our purposes
218
32803
      out << (n.getConst<bool>() ? "true" : "false");
219
32803
      break;
220
    case kind::BUILTIN:
221
      out << smtKindString(n.getConst<Kind>(), d_variant);
222
      break;
223
726107
    case kind::CONST_RATIONAL: {
224
726107
      const Rational& r = n.getConst<Rational>();
225
726107
      toStreamRational(out, r, false, d_variant);
226
726107
      break;
227
    }
228
229
1646
    case kind::CONST_STRING: {
230
3292
      std::string s = n.getConst<String>().toString();
231
1646
      out << '"';
232
3814
      for(size_t i = 0; i < s.size(); ++i) {
233
2168
        char c = s[i];
234
2168
        if(c == '"') {
235
4
          out << "\"\"";
236
        } else {
237
2164
          out << c;
238
        }
239
      }
240
1646
      out << '"';
241
1646
      break;
242
    }
243
4
    case kind::CONST_SEQUENCE:
244
    {
245
4
      const Sequence& sn = n.getConst<Sequence>();
246
4
      const std::vector<Node>& snvec = sn.getVec();
247
4
      if (snvec.empty())
248
      {
249
4
        out << "(as seq.empty " << n.getType() << ")";
250
      }
251
4
      if (snvec.size() > 1)
252
      {
253
        out << "(seq.++ ";
254
      }
255
4
      for (const Node& snvc : snvec)
256
      {
257
        out << "(seq.unit " << snvc << ")";
258
      }
259
4
      if (snvec.size() > 1)
260
      {
261
        out << ")";
262
      }
263
4
      break;
264
    }
265
266
21
    case kind::STORE_ALL: {
267
42
      ArrayStoreAll asa = n.getConst<ArrayStoreAll>();
268
21
      out << "((as const " << asa.getType() << ") " << asa.getValue() << ")";
269
21
      break;
270
    }
271
272
2317
    case kind::DATATYPE_TYPE:
273
    {
274
      const DType& dt = (NodeManager::currentNM()->getDTypeForIndex(
275
2317
          n.getConst<DatatypeIndexConstant>().getIndex()));
276
2317
      if (dt.isTuple())
277
      {
278
6
        unsigned int nargs = dt[0].getNumArgs();
279
6
        if (nargs == 0)
280
        {
281
          out << "Tuple";
282
        }
283
        else
284
        {
285
6
          out << "(Tuple";
286
20
          for (unsigned int i = 0; i < nargs; i++)
287
          {
288
14
            out << " " << dt[0][i].getRangeType();
289
          }
290
6
          out << ")";
291
        }
292
      }
293
      else
294
      {
295
2311
        out << CVC4::quoteSymbol(dt.getName());
296
      }
297
2317
      break;
298
    }
299
300
1
    case kind::UNINTERPRETED_CONSTANT: {
301
1
      const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>();
302
2
      std::stringstream ss;
303
1
      ss << "(as @" << uc << " " << n.getType() << ")";
304
1
      out << ss.str();
305
1
      break;
306
    }
307
308
8
    case kind::EMPTYSET:
309
8
      out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
310
8
      break;
311
312
    case kind::EMPTYBAG:
313
      out << "(as emptybag " << n.getConst<EmptyBag>().getType() << ")";
314
      break;
315
8
    case kind::BITVECTOR_EXTRACT_OP:
316
    {
317
8
      BitVectorExtract p = n.getConst<BitVectorExtract>();
318
8
      out << "(_ extract " << p.d_high << ' ' << p.d_low << ")";
319
8
      break;
320
    }
321
4
    case kind::BITVECTOR_REPEAT_OP:
322
4
      out << "(_ repeat " << n.getConst<BitVectorRepeat>().d_repeatAmount
323
4
          << ")";
324
4
      break;
325
16
    case kind::BITVECTOR_ZERO_EXTEND_OP:
326
16
      out << "(_ zero_extend "
327
16
          << n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount << ")";
328
16
      break;
329
    case kind::BITVECTOR_SIGN_EXTEND_OP:
330
      out << "(_ sign_extend "
331
          << n.getConst<BitVectorSignExtend>().d_signExtendAmount << ")";
332
      break;
333
    case kind::BITVECTOR_ROTATE_LEFT_OP:
334
      out << "(_ rotate_left "
335
          << n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount << ")";
336
      break;
337
    case kind::BITVECTOR_ROTATE_RIGHT_OP:
338
      out << "(_ rotate_right "
339
          << n.getConst<BitVectorRotateRight>().d_rotateRightAmount << ")";
340
      break;
341
20
    case kind::INT_TO_BITVECTOR_OP:
342
20
      out << "(_ int2bv " << n.getConst<IntToBitVector>().d_size << ")";
343
20
      break;
344
    case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
345
      out << "(_ to_fp "
346
          << n.getConst<FloatingPointToFPIEEEBitVector>()
347
                 .d_fp_size.exponentWidth()
348
          << ' '
349
          << n.getConst<FloatingPointToFPIEEEBitVector>()
350
                 .d_fp_size.significandWidth()
351
          << ")";
352
      break;
353
    case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
354
      out << "(_ to_fp "
355
          << n.getConst<FloatingPointToFPFloatingPoint>()
356
                 .d_fp_size.exponentWidth()
357
          << ' '
358
          << n.getConst<FloatingPointToFPFloatingPoint>()
359
                 .d_fp_size.significandWidth()
360
          << ")";
361
      break;
362
    case kind::FLOATINGPOINT_TO_FP_REAL_OP:
363
      out << "(_ to_fp "
364
          << n.getConst<FloatingPointToFPReal>().d_fp_size.exponentWidth()
365
          << ' '
366
          << n.getConst<FloatingPointToFPReal>().d_fp_size.significandWidth()
367
          << ")";
368
      break;
369
    case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
370
      out << "(_ to_fp "
371
          << n.getConst<FloatingPointToFPSignedBitVector>()
372
                 .d_fp_size.exponentWidth()
373
          << ' '
374
          << n.getConst<FloatingPointToFPSignedBitVector>()
375
                 .d_fp_size.significandWidth()
376
          << ")";
377
      break;
378
    case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
379
      out << "(_ to_fp_unsigned "
380
          << n.getConst<FloatingPointToFPUnsignedBitVector>()
381
                 .d_fp_size.exponentWidth()
382
          << ' '
383
          << n.getConst<FloatingPointToFPUnsignedBitVector>()
384
                 .d_fp_size.significandWidth()
385
          << ")";
386
      break;
387
    case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
388
      out << "(_ to_fp "
389
          << n.getConst<FloatingPointToFPGeneric>().d_fp_size.exponentWidth()
390
          << ' '
391
          << n.getConst<FloatingPointToFPGeneric>().d_fp_size.significandWidth()
392
          << ")";
393
      break;
394
    case kind::FLOATINGPOINT_TO_UBV_OP:
395
      out << "(_ fp.to_ubv "
396
          << n.getConst<FloatingPointToUBV>().d_bv_size.d_size << ")";
397
      break;
398
    case kind::FLOATINGPOINT_TO_SBV_OP:
399
      out << "(_ fp.to_sbv "
400
          << n.getConst<FloatingPointToSBV>().d_bv_size.d_size << ")";
401
      break;
402
    case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
403
      out << "(_ fp.to_ubv_total "
404
          << n.getConst<FloatingPointToUBVTotal>().d_bv_size.d_size << ")";
405
      break;
406
    case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
407
      out << "(_ fp.to_sbv_total "
408
          << n.getConst<FloatingPointToSBVTotal>().d_bv_size.d_size << ")";
409
      break;
410
2
    case kind::REGEXP_REPEAT_OP:
411
2
      out << "(_ re.^ " << n.getConst<RegExpRepeat>().d_repeatAmount << ")";
412
2
      break;
413
2
    case kind::REGEXP_LOOP_OP:
414
2
      out << "(_ re.loop " << n.getConst<RegExpLoop>().d_loopMinOcc << " "
415
2
          << n.getConst<RegExpLoop>().d_loopMaxOcc << ")";
416
2
      break;
417
8
    default:
418
      // fall back on whatever operator<< does on underlying type; we
419
      // might luck out and be SMT-LIB v2 compliant
420
8
      kind::metakind::NodeValueConstPrinter::toStream(out, n);
421
    }
422
423
782724
    return;
424
  }
425
426
1318480
  if(n.getKind() == kind::SORT_TYPE) {
427
12226
    string name;
428
6113
    if(n.getNumChildren() != 0) {
429
28
      out << '(';
430
    }
431
6113
    if(n.getAttribute(expr::VarNameAttr(), name)) {
432
6113
      out << CVC4::quoteSymbol(name);
433
    }
434
6113
    if(n.getNumChildren() != 0) {
435
60
      for(unsigned i = 0; i < n.getNumChildren(); ++i) {
436
32
	      out << ' ';
437
32
              toStream(out, n[i], toDepth);
438
      }
439
28
      out << ')';
440
    }
441
6113
    return;
442
  }
443
444
  // determine if we are printing out a type ascription, store the argument of
445
  // the type ascription into type_asc_arg.
446
1312367
  Kind k = n.getKind();
447
1904697
  Node type_asc_arg;
448
1904697
  TypeNode force_nt;
449
1312367
  if (k == kind::APPLY_TYPE_ASCRIPTION)
450
  {
451
20
    force_nt = n.getOperator().getConst<AscriptionType>().getType();
452
20
    type_asc_arg = n[0];
453
  }
454
1312347
  else if (k == kind::CAST_TO_REAL)
455
  {
456
14
    force_nt = nm->realType();
457
14
    type_asc_arg = n[0];
458
  }
459
1312367
  if (!type_asc_arg.isNull())
460
  {
461
34
    if (force_nt.isReal())
462
    {
463
      // we prefer using (/ x 1) instead of (to_real x) here.
464
      // the reason is that (/ x 1) is SMT-LIB compliant when x is a constant
465
      // or the logic is non-linear, whereas (to_real x) is compliant when
466
      // the logic is mixed int/real. The former occurs more frequently.
467
14
      bool is_int = force_nt.isInteger();
468
      // If constant rational, print as special case
469
14
      if (type_asc_arg.getKind() == kind::CONST_RATIONAL)
470
      {
471
14
        const Rational& r = type_asc_arg.getConst<Rational>();
472
14
        toStreamRational(out, r, !is_int, d_variant);
473
      }
474
      else
475
      {
476
        out << "("
477
            << smtKindString(is_int ? kind::TO_INTEGER : kind::DIVISION,
478
                             d_variant)
479
            << " ";
480
        toStream(out, type_asc_arg, toDepth, lbind);
481
        if (!is_int)
482
        {
483
          out << " 1";
484
        }
485
        out << ")";
486
      }
487
    }
488
    else
489
    {
490
      // use type ascription
491
20
      out << "(as ";
492
20
      toStream(out, type_asc_arg, toDepth < 0 ? toDepth : toDepth - 1, lbind);
493
20
      out << " " << force_nt << ")";
494
    }
495
34
    return;
496
  }
497
498
  // variable
499
1312333
  if (n.isVar())
500
  {
501
1435318
    string s;
502
717659
    if (n.getAttribute(expr::VarNameAttr(), s))
503
    {
504
715571
      out << CVC4::quoteSymbol(s);
505
    }
506
    else
507
    {
508
2088
      if (n.getKind() == kind::VARIABLE)
509
      {
510
        out << "var_";
511
      }
512
      else
513
      {
514
2088
        out << n.getKind() << '_';
515
      }
516
2088
      out << n.getId();
517
    }
518
717659
    return;
519
  }
520
521
594674
  bool stillNeedToPrintParams = true;
522
594674
  bool forceBinary = false; // force N-ary to binary when outputing children
523
  // operator
524
1783087
  if (n.getNumChildren() != 0 && k != kind::INST_PATTERN_LIST
525
1188410
      && k != kind::CONSTRUCTOR_TYPE)
526
  {
527
593724
    out << '(';
528
  }
529
594674
  switch(k) {
530
    // builtin theory
531
38358
  case kind::EQUAL:
532
  case kind::DISTINCT:
533
38358
    out << smtKindString(k, d_variant) << " ";
534
38358
    break;
535
1154
  case kind::FUNCTION_TYPE:
536
1154
    out << "->";
537
4894
    for (Node nc : n)
538
    {
539
3740
      out << " ";
540
3740
      toStream(out, nc, toDepth);
541
1154
    }
542
1154
    out << ")";
543
1154
    return;
544
351586
  case kind::SEXPR: break;
545
546
    // bool theory
547
23019
  case kind::NOT:
548
  case kind::AND:
549
  case kind::IMPLIES:
550
  case kind::OR:
551
  case kind::XOR:
552
  case kind::ITE:
553
23019
    out << smtKindString(k, d_variant) << " ";
554
23019
    break;
555
556
  // uf theory
557
41418
  case kind::APPLY_UF: break;
558
  // higher-order
559
  case kind::HO_APPLY:
560
    if (!options::flattenHOChains())
561
    {
562
      break;
563
    }
564
    // collapse "@" chains, i.e.
565
    //
566
    // ((a b) c) --> (a b c)
567
    //
568
    // (((a b) ((c d) e)) f) --> (a b (c d e) f)
569
    {
570
      Node head = n;
571
      std::vector<Node> args;
572
      while (head.getKind() == kind::HO_APPLY)
573
      {
574
        args.insert(args.begin(), head[1]);
575
        head = head[0];
576
      }
577
      toStream(out, head, toDepth, lbind);
578
      for (unsigned i = 0, size = args.size(); i < size; ++i)
579
      {
580
        out << " ";
581
        toStream(out, args[i], toDepth, lbind);
582
      }
583
      out << ")";
584
    }
585
    return;
586
587
  case kind::MATCH:
588
    out << smtKindString(k, d_variant) << " ";
589
    toStream(out, n[0], toDepth, lbind);
590
    out << " (";
591
    for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++)
592
    {
593
      if (i > 1)
594
      {
595
        out << " ";
596
      }
597
      toStream(out, n[i], toDepth, lbind);
598
    }
599
    out << "))";
600
    return;
601
  case kind::MATCH_BIND_CASE:
602
    // ignore the binder
603
    toStream(out, n[1], toDepth, lbind);
604
    out << " ";
605
    toStream(out, n[2], toDepth, lbind);
606
    out << ")";
607
    return;
608
  case kind::MATCH_CASE:
609
    // do nothing
610
    break;
611
612
  // arith theory
613
123808
  case kind::PLUS:
614
  case kind::MULT:
615
  case kind::NONLINEAR_MULT:
616
  case kind::EXPONENTIAL:
617
  case kind::SINE:
618
  case kind::COSINE:
619
  case kind::TANGENT:
620
  case kind::COSECANT:
621
  case kind::SECANT:
622
  case kind::COTANGENT:
623
  case kind::ARCSINE:
624
  case kind::ARCCOSINE:
625
  case kind::ARCTANGENT:
626
  case kind::ARCCOSECANT:
627
  case kind::ARCSECANT:
628
  case kind::ARCCOTANGENT:
629
  case kind::PI:
630
  case kind::SQRT:
631
  case kind::MINUS:
632
  case kind::UMINUS:
633
  case kind::LT:
634
  case kind::LEQ:
635
  case kind::GT:
636
  case kind::GEQ:
637
  case kind::DIVISION:
638
  case kind::DIVISION_TOTAL:
639
  case kind::INTS_DIVISION:
640
  case kind::INTS_DIVISION_TOTAL:
641
  case kind::INTS_MODULUS:
642
  case kind::INTS_MODULUS_TOTAL:
643
  case kind::ABS:
644
  case kind::IS_INTEGER:
645
  case kind::TO_INTEGER:
646
  case kind::TO_REAL:
647
  case kind::POW:
648
123808
    out << smtKindString(k, d_variant) << " ";
649
123808
    break;
650
1
  case kind::IAND:
651
1
    out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") ";
652
1
    stillNeedToPrintParams = false;
653
1
    break;
654
655
  case kind::DIVISIBLE:
656
    out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
657
    stillNeedToPrintParams = false;
658
    break;
659
  case kind::INDEXED_ROOT_PREDICATE_OP:
660
  {
661
    const IndexedRootPredicate& irp = n.getConst<IndexedRootPredicate>();
662
    out << "(_ root_predicate " << irp.d_index << ")";
663
    break;
664
  }
665
666
    // arrays theory
667
472
  case kind::SELECT:
668
  case kind::STORE:
669
  case kind::PARTIAL_SELECT_0:
670
  case kind::PARTIAL_SELECT_1:
671
  case kind::ARRAY_TYPE:
672
472
  case kind::EQ_RANGE: out << smtKindString(k, d_variant) << " "; break;
673
674
  // string theory
675
333
  case kind::STRING_CONCAT:
676
333
    out << "str.++ ";
677
333
    break;
678
6
  case kind::STRING_IN_REGEXP: {
679
12
    stringstream ss;
680
6
    out << smtKindString(k, d_variant) << " ";
681
6
    break;
682
  }
683
4054
  case kind::STRING_LENGTH:
684
  case kind::STRING_SUBSTR:
685
  case kind::STRING_UPDATE:
686
  case kind::STRING_CHARAT:
687
  case kind::STRING_STRCTN:
688
  case kind::STRING_STRIDOF:
689
  case kind::STRING_STRREPL:
690
  case kind::STRING_STRREPLALL:
691
  case kind::STRING_REPLACE_RE:
692
  case kind::STRING_REPLACE_RE_ALL:
693
  case kind::STRING_TOLOWER:
694
  case kind::STRING_TOUPPER:
695
  case kind::STRING_REV:
696
  case kind::STRING_PREFIX:
697
  case kind::STRING_SUFFIX:
698
  case kind::STRING_LEQ:
699
  case kind::STRING_LT:
700
  case kind::STRING_ITOS:
701
  case kind::STRING_STOI:
702
  case kind::STRING_FROM_CODE:
703
  case kind::STRING_TO_CODE:
704
  case kind::STRING_TO_REGEXP:
705
  case kind::REGEXP_CONCAT:
706
  case kind::REGEXP_UNION:
707
  case kind::REGEXP_INTER:
708
  case kind::REGEXP_STAR:
709
  case kind::REGEXP_PLUS:
710
  case kind::REGEXP_OPT:
711
  case kind::REGEXP_RANGE:
712
  case kind::REGEXP_COMPLEMENT:
713
  case kind::REGEXP_DIFF:
714
  case kind::REGEXP_EMPTY:
715
  case kind::REGEXP_SIGMA:
716
  case kind::SEQ_UNIT:
717
  case kind::SEQ_NTH:
718
4054
  case kind::SEQUENCE_TYPE: out << smtKindString(k, d_variant) << " "; break;
719
4
  case kind::REGEXP_REPEAT:
720
  case kind::REGEXP_LOOP:
721
  {
722
4
    out << n.getOperator() << ' ';
723
4
    stillNeedToPrintParams = false;
724
4
    break;
725
  }
726
727
  case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break;
728
  case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break;
729
730
    // bv theory
731
  case kind::BITVECTOR_CONCAT: out << "concat "; forceBinary = true; break;
732
143
  case kind::BITVECTOR_AND: out << "bvand "; forceBinary = true; break;
733
139
  case kind::BITVECTOR_OR: out << "bvor "; forceBinary = true; break;
734
  case kind::BITVECTOR_XOR: out << "bvxor "; forceBinary = true; break;
735
179
  case kind::BITVECTOR_NOT: out << "bvnot "; break;
736
  case kind::BITVECTOR_NAND: out << "bvnand "; break;
737
  case kind::BITVECTOR_NOR: out << "bvnor "; break;
738
  case kind::BITVECTOR_XNOR: out << "bvxnor "; break;
739
  case kind::BITVECTOR_COMP: out << "bvcomp "; break;
740
277
  case kind::BITVECTOR_MULT: out << "bvmul "; forceBinary = true; break;
741
290
  case kind::BITVECTOR_PLUS: out << "bvadd "; forceBinary = true; break;
742
  case kind::BITVECTOR_SUB: out << "bvsub "; break;
743
149
  case kind::BITVECTOR_NEG: out << "bvneg "; break;
744
  case kind::BITVECTOR_UDIV: out << "bvudiv "; break;
745
  case kind::BITVECTOR_UREM: out << "bvurem "; break;
746
  case kind::BITVECTOR_SDIV: out << "bvsdiv "; break;
747
  case kind::BITVECTOR_SREM: out << "bvsrem "; break;
748
  case kind::BITVECTOR_SMOD: out << "bvsmod "; break;
749
463
  case kind::BITVECTOR_SHL: out << "bvshl "; break;
750
402
  case kind::BITVECTOR_LSHR: out << "bvlshr "; break;
751
  case kind::BITVECTOR_ASHR: out << "bvashr "; break;
752
2
  case kind::BITVECTOR_ULT: out << "bvult "; break;
753
  case kind::BITVECTOR_ULE: out << "bvule "; break;
754
  case kind::BITVECTOR_UGT: out << "bvugt "; break;
755
  case kind::BITVECTOR_UGE: out << "bvuge "; break;
756
  case kind::BITVECTOR_SLT: out << "bvslt "; break;
757
  case kind::BITVECTOR_SLE: out << "bvsle "; break;
758
  case kind::BITVECTOR_SGT: out << "bvsgt "; break;
759
  case kind::BITVECTOR_SGE: out << "bvsge "; break;
760
35
  case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break;
761
  case kind::BITVECTOR_REDOR: out << "bvredor "; break;
762
  case kind::BITVECTOR_REDAND: out << "bvredand "; break;
763
764
44
  case kind::BITVECTOR_EXTRACT:
765
  case kind::BITVECTOR_REPEAT:
766
  case kind::BITVECTOR_ZERO_EXTEND:
767
  case kind::BITVECTOR_SIGN_EXTEND:
768
  case kind::BITVECTOR_ROTATE_LEFT:
769
  case kind::BITVECTOR_ROTATE_RIGHT:
770
  case kind::INT_TO_BITVECTOR:
771
44
    out << n.getOperator() << ' ';
772
44
    stillNeedToPrintParams = false;
773
44
    break;
774
775
    // sets
776
2
  case kind::UNION:
777
  case kind::INTERSECTION:
778
  case kind::SETMINUS:
779
  case kind::SUBSET:
780
  case kind::CARD:
781
  case kind::JOIN:
782
  case kind::PRODUCT:
783
  case kind::TRANSPOSE:
784
  case kind::TCLOSURE:
785
2
    out << smtKindString(k, d_variant) << " ";
786
2
    break;
787
  case kind::COMPREHENSION: out << smtKindString(k, d_variant) << " "; break;
788
12
  case kind::SINGLETON:
789
  {
790
12
    out << smtKindString(k, d_variant) << " ";
791
24
    TypeNode elemType = n.getType().getSetElementType();
792
12
    toStreamCastToType(
793
        out, n[0], toDepth < 0 ? toDepth : toDepth - 1, elemType);
794
12
    out << ")";
795
12
    return;
796
  }
797
  break;
798
94
  case kind::MEMBER:
799
  case kind::INSERT:
800
  case kind::SET_TYPE:
801
  case kind::COMPLEMENT:
802
  case kind::CHOOSE:
803
94
  case kind::IS_SINGLETON: out << smtKindString(k, d_variant) << " "; break;
804
  case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break;
805
806
  // bags
807
34
  case kind::BAG_TYPE:
808
  case kind::UNION_MAX:
809
  case kind::UNION_DISJOINT:
810
  case kind::INTERSECTION_MIN:
811
  case kind::DIFFERENCE_SUBTRACT:
812
  case kind::DIFFERENCE_REMOVE:
813
  case kind::SUBBAG:
814
  case kind::BAG_COUNT:
815
  case kind::DUPLICATE_REMOVAL:
816
  case kind::BAG_CARD:
817
  case kind::BAG_CHOOSE:
818
  case kind::BAG_IS_SINGLETON:
819
  case kind::BAG_FROM_SET:
820
34
  case kind::BAG_TO_SET: out << smtKindString(k, d_variant) << " "; break;
821
4
  case kind::MK_BAG:
822
  {
823
    // print (bag (mkBag_op Real) 1 3) as (bag 1.0 3)
824
4
    out << smtKindString(k, d_variant) << " ";
825
8
    TypeNode elemType = n.getType().getBagElementType();
826
4
    toStreamCastToType(
827
        out, n[0], toDepth < 0 ? toDepth : toDepth - 1, elemType);
828
4
    out << " " << n[1] << ")";
829
4
    return;
830
  }
831
832
    // fp theory
833
74
  case kind::FLOATINGPOINT_FP:
834
  case kind::FLOATINGPOINT_EQ:
835
  case kind::FLOATINGPOINT_ABS:
836
  case kind::FLOATINGPOINT_NEG:
837
  case kind::FLOATINGPOINT_PLUS:
838
  case kind::FLOATINGPOINT_SUB:
839
  case kind::FLOATINGPOINT_MULT:
840
  case kind::FLOATINGPOINT_DIV:
841
  case kind::FLOATINGPOINT_FMA:
842
  case kind::FLOATINGPOINT_SQRT:
843
  case kind::FLOATINGPOINT_REM:
844
  case kind::FLOATINGPOINT_RTI:
845
  case kind::FLOATINGPOINT_MIN:
846
  case kind::FLOATINGPOINT_MAX:
847
  case kind::FLOATINGPOINT_LEQ:
848
  case kind::FLOATINGPOINT_LT:
849
  case kind::FLOATINGPOINT_GEQ:
850
  case kind::FLOATINGPOINT_GT:
851
  case kind::FLOATINGPOINT_ISN:
852
  case kind::FLOATINGPOINT_ISSN:
853
  case kind::FLOATINGPOINT_ISZ:
854
  case kind::FLOATINGPOINT_ISINF:
855
  case kind::FLOATINGPOINT_ISNAN:
856
  case kind::FLOATINGPOINT_ISNEG:
857
  case kind::FLOATINGPOINT_ISPOS:
858
  case kind::FLOATINGPOINT_TO_REAL:
859
  case kind::FLOATINGPOINT_COMPONENT_NAN:
860
  case kind::FLOATINGPOINT_COMPONENT_INF:
861
  case kind::FLOATINGPOINT_COMPONENT_ZERO:
862
  case kind::FLOATINGPOINT_COMPONENT_SIGN:
863
  case kind::FLOATINGPOINT_COMPONENT_EXPONENT:
864
  case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND:
865
  case kind::ROUNDINGMODE_BITBLAST:
866
74
    out << smtKindString(k, d_variant) << ' ';
867
74
    break;
868
869
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
870
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
871
  case kind::FLOATINGPOINT_TO_FP_REAL:
872
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
873
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
874
  case kind::FLOATINGPOINT_TO_FP_GENERIC:
875
  case kind::FLOATINGPOINT_TO_UBV:
876
  case kind::FLOATINGPOINT_TO_SBV:
877
    out << n.getOperator() << ' ';
878
    stillNeedToPrintParams = false;
879
    break;
880
881
5840
  case kind::APPLY_CONSTRUCTOR:
882
  {
883
5840
    const DType& dt = DType::datatypeOf(n.getOperator());
884
5840
    if (dt.isTuple())
885
    {
886
28
      stillNeedToPrintParams = false;
887
28
      out << "mkTuple" << ( dt[0].getNumArgs()==0 ? "" : " ");
888
    }
889
5840
    break;
890
  }
891
6
  case kind::TUPLE_PROJECT:
892
  {
893
12
    TupleProjectOp op = n.getOperator().getConst<TupleProjectOp>();
894
6
    if (op.getIndices().empty())
895
    {
896
      // e.g. (tuple_project tuple)
897
      out << "project " << n[0] << ")";
898
    }
899
    else
900
    {
901
      // e.g. ((_ tuple_project 2 4 4) tuple)
902
6
      out << "(_ tuple_project" << op << ") " << n[0] << ")";
903
    }
904
6
    return;
905
  }
906
12
  case kind::CONSTRUCTOR_TYPE:
907
  {
908
12
    out << n[n.getNumChildren()-1];
909
12
    return;
910
    break;
911
  }
912
675
  case kind::APPLY_TESTER:
913
  case kind::APPLY_SELECTOR:
914
  case kind::APPLY_SELECTOR_TOTAL:
915
675
  case kind::PARAMETRIC_DATATYPE: break;
916
917
  // separation logic
918
3
  case kind::SEP_EMP:
919
  case kind::SEP_PTO:
920
  case kind::SEP_STAR:
921
3
  case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break;
922
923
90
  case kind::SEP_NIL:
924
90
    out << "(as sep.nil " << n.getType() << ")";
925
90
    break;
926
927
    // quantifiers
928
32
  case kind::FORALL:
929
  case kind::EXISTS:
930
  case kind::LAMBDA:
931
  case kind::WITNESS:
932
  {
933
32
    out << smtKindString(k, d_variant) << " ";
934
    // do not letify the bound variable list
935
32
    toStream(out, n[0], toDepth, nullptr);
936
32
    out << " ";
937
32
    if (n.getNumChildren() == 3)
938
    {
939
3
      out << "(! ";
940
    }
941
    // Use a fresh let binder, since using existing let symbols may violate
942
    // scoping issues for let-bound variables, see explanation in let_binding.h.
943
32
    size_t dag = lbind == nullptr ? 0 : lbind->getThreshold()-1;
944
32
    toStream(out, n[1], toDepth - 1, dag);
945
32
    if (n.getNumChildren() == 3)
946
    {
947
3
      out << " ";
948
      // do not letify the annotation
949
3
      toStream(out, n[2], toDepth, nullptr);
950
3
      out << ")";
951
    }
952
32
    out << ")";
953
32
    return;
954
    break;
955
  }
956
1121
  case kind::BOUND_VAR_LIST:
957
  {
958
    // the left parenthesis is already printed (before the switch)
959
3573
    for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;)
960
    {
961
2452
      out << '(';
962
2452
      toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1);
963
2452
      out << ' ';
964
2452
      out << (*i).getType();
965
2452
      out << ')';
966
2452
      if (++i != iend)
967
      {
968
1331
        out << ' ';
969
      }
970
    }
971
1121
    out << ')';
972
1121
    return;
973
  }
974
  case kind::INST_PATTERN:
975
  case kind::INST_NO_PATTERN: break;
976
3
  case kind::INST_PATTERN_LIST:
977
  {
978
6
    for (const Node& nc : n)
979
    {
980
3
      if (nc.getKind() == kind::INST_PATTERN)
981
      {
982
        out << ":pattern " << nc;
983
      }
984
3
      else if (nc.getKind() == kind::INST_NO_PATTERN)
985
      {
986
        out << ":no-pattern " << nc[0];
987
      }
988
    }
989
3
    return;
990
    break;
991
  }
992
336
  default:
993
    // fall back on however the kind prints itself; this probably
994
    // won't be SMT-LIB v2 compliant, but it will be clear from the
995
    // output that support for the kind needs to be added here.
996
336
    out << n.getKind() << ' ';
997
  }
998
592330
  if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&
999
      stillNeedToPrintParams ) {
1000
47879
    if(toDepth != 0) {
1001
47879
      if (n.getKind() == kind::APPLY_TESTER)
1002
      {
1003
        unsigned cindex = DType::indexOf(n.getOperator());
1004
        const DType& dt = DType::datatypeOf(n.getOperator());
1005
        out << "(_ is ";
1006
        toStream(out,
1007
                 dt[cindex].getConstructor(),
1008
                 toDepth < 0 ? toDepth : toDepth - 1);
1009
        out << ")";
1010
      }else{
1011
95758
        toStream(
1012
95758
            out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind);
1013
      }
1014
    } else {
1015
      out << "(...)";
1016
    }
1017
47879
    if(n.getNumChildren() > 0) {
1018
47554
      out << ' ';
1019
    }
1020
  }
1021
1184660
  stringstream parens;
1022
1023
1926941
  for(size_t i = 0, c = 1; i < n.getNumChildren(); ) {
1024
1334611
    if(toDepth != 0) {
1025
1334611
      toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - c, lbind);
1026
    } else {
1027
      out << "(...)";
1028
    }
1029
1334611
    if(++i < n.getNumChildren()) {
1030
743216
      if(forceBinary && i < n.getNumChildren() - 1) {
1031
        // not going to work properly for parameterized kinds!
1032
        Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
1033
        out << " (" << smtKindString(n.getKind(), d_variant) << ' ';
1034
        parens << ')';
1035
        ++c;
1036
      } else {
1037
743216
        out << ' ';
1038
      }
1039
    }
1040
  }
1041
592330
  if (n.getNumChildren() != 0)
1042
  {
1043
591395
    out << parens.str() << ')';
1044
  }
1045
}
1046
1047
40
void Smt2Printer::toStreamCastToType(std::ostream& out,
1048
                                     TNode n,
1049
                                     int toDepth,
1050
                                     TypeNode tn) const
1051
{
1052
80
  Node nasc;
1053
40
  if (n.getType().isInteger() && !tn.isInteger())
1054
  {
1055
2
    Assert(tn.isReal());
1056
    // probably due to subtyping integers and reals, cast it
1057
2
    nasc = NodeManager::currentNM()->mkNode(kind::CAST_TO_REAL, n);
1058
  }
1059
  else
1060
  {
1061
38
    nasc = n;
1062
  }
1063
40
  toStream(out, nasc, toDepth);
1064
40
}
1065
1066
189972
std::string Smt2Printer::smtKindString(Kind k, Variant v)
1067
{
1068
189972
  switch(k) {
1069
    // builtin theory
1070
38355
  case kind::EQUAL: return "=";
1071
3
  case kind::DISTINCT: return "distinct";
1072
  case kind::SEXPR: break;
1073
1074
    // bool theory
1075
22730
  case kind::NOT: return "not";
1076
198
  case kind::AND: return "and";
1077
6
  case kind::IMPLIES: return "=>";
1078
65
  case kind::OR: return "or";
1079
20
  case kind::XOR: return "xor";
1080
  case kind::ITE: return "ite";
1081
1082
    // uf theory
1083
  case kind::APPLY_UF: break;
1084
1085
6
  case kind::LAMBDA: return "lambda";
1086
  case kind::MATCH: return "match";
1087
2
  case kind::WITNESS: return "witness";
1088
1089
  // arith theory
1090
38054
  case kind::PLUS: return "+";
1091
34649
  case kind::MULT:
1092
34649
  case kind::NONLINEAR_MULT: return "*";
1093
  case kind::IAND: return "iand";
1094
38
  case kind::EXPONENTIAL: return "exp";
1095
296
  case kind::SINE: return "sin";
1096
  case kind::COSINE: return "cos";
1097
  case kind::TANGENT: return "tan";
1098
  case kind::COSECANT: return "csc";
1099
  case kind::SECANT: return "sec";
1100
  case kind::COTANGENT: return "cot";
1101
  case kind::ARCSINE: return "arcsin";
1102
  case kind::ARCCOSINE: return "arccos";
1103
  case kind::ARCTANGENT: return "arctan";
1104
  case kind::ARCCOSECANT: return "arccsc";
1105
  case kind::ARCSECANT: return "arcsec";
1106
  case kind::ARCCOTANGENT: return "arccot";
1107
304
  case kind::PI: return "real.pi";
1108
  case kind::SQRT: return "sqrt";
1109
11
  case kind::MINUS: return "-";
1110
4
  case kind::UMINUS: return "-";
1111
18642
  case kind::LT: return "<";
1112
86
  case kind::LEQ: return "<=";
1113
2262
  case kind::GT: return ">";
1114
29453
  case kind::GEQ: return ">=";
1115
5
  case kind::DIVISION:
1116
5
  case kind::DIVISION_TOTAL: return "/";
1117
3
  case kind::INTS_DIVISION_TOTAL:
1118
3
  case kind::INTS_DIVISION: return "div";
1119
1
  case kind::INTS_MODULUS_TOTAL:
1120
1
  case kind::INTS_MODULUS: return "mod";
1121
  case kind::ABS: return "abs";
1122
  case kind::IS_INTEGER: return "is_int";
1123
  case kind::TO_INTEGER: return "to_int";
1124
  case kind::TO_REAL: return "to_real";
1125
  case kind::POW: return "^";
1126
1127
    // arrays theory
1128
226
  case kind::SELECT: return "select";
1129
  case kind::STORE: return "store";
1130
246
  case kind::ARRAY_TYPE: return "Array";
1131
  case kind::PARTIAL_SELECT_0: return "partial_select_0";
1132
  case kind::PARTIAL_SELECT_1: return "partial_select_1";
1133
  case kind::EQ_RANGE:
1134
    return "eqrange";
1135
1136
    // bv theory
1137
  case kind::BITVECTOR_CONCAT: return "concat";
1138
  case kind::BITVECTOR_AND: return "bvand";
1139
  case kind::BITVECTOR_OR: return "bvor";
1140
  case kind::BITVECTOR_XOR: return "bvxor";
1141
  case kind::BITVECTOR_NOT: return "bvnot";
1142
  case kind::BITVECTOR_NAND: return "bvnand";
1143
  case kind::BITVECTOR_NOR: return "bvnor";
1144
  case kind::BITVECTOR_XNOR: return "bvxnor";
1145
  case kind::BITVECTOR_COMP: return "bvcomp";
1146
  case kind::BITVECTOR_MULT: return "bvmul";
1147
  case kind::BITVECTOR_PLUS: return "bvadd";
1148
  case kind::BITVECTOR_SUB: return "bvsub";
1149
  case kind::BITVECTOR_NEG: return "bvneg";
1150
  case kind::BITVECTOR_UDIV: return "bvudiv";
1151
  case kind::BITVECTOR_UREM: return "bvurem";
1152
  case kind::BITVECTOR_SDIV: return "bvsdiv";
1153
  case kind::BITVECTOR_SREM: return "bvsrem";
1154
  case kind::BITVECTOR_SMOD: return "bvsmod";
1155
  case kind::BITVECTOR_SHL: return "bvshl";
1156
  case kind::BITVECTOR_LSHR: return "bvlshr";
1157
  case kind::BITVECTOR_ASHR: return "bvashr";
1158
  case kind::BITVECTOR_ULT: return "bvult";
1159
  case kind::BITVECTOR_ULE: return "bvule";
1160
  case kind::BITVECTOR_UGT: return "bvugt";
1161
  case kind::BITVECTOR_UGE: return "bvuge";
1162
  case kind::BITVECTOR_SLT: return "bvslt";
1163
  case kind::BITVECTOR_SLE: return "bvsle";
1164
  case kind::BITVECTOR_SGT: return "bvsgt";
1165
  case kind::BITVECTOR_SGE: return "bvsge";
1166
  case kind::BITVECTOR_TO_NAT: return "bv2nat";
1167
  case kind::BITVECTOR_REDOR: return "bvredor";
1168
  case kind::BITVECTOR_REDAND: return "bvredand";
1169
1170
  case kind::BITVECTOR_EXTRACT: return "extract";
1171
  case kind::BITVECTOR_REPEAT: return "repeat";
1172
  case kind::BITVECTOR_ZERO_EXTEND: return "zero_extend";
1173
  case kind::BITVECTOR_SIGN_EXTEND: return "sign_extend";
1174
  case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
1175
  case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
1176
1177
  case kind::UNION: return "union";
1178
  case kind::INTERSECTION: return "intersection";
1179
  case kind::SETMINUS: return "setminus";
1180
  case kind::SUBSET: return "subset";
1181
  case kind::MEMBER: return "member";
1182
94
  case kind::SET_TYPE: return "Set";
1183
12
  case kind::SINGLETON: return "singleton";
1184
  case kind::INSERT: return "insert";
1185
  case kind::COMPLEMENT: return "complement";
1186
2
  case kind::CARD: return "card";
1187
  case kind::COMPREHENSION: return "comprehension";
1188
  case kind::CHOOSE: return "choose";
1189
  case kind::IS_SINGLETON: return "is_singleton";
1190
  case kind::JOIN: return "join";
1191
  case kind::PRODUCT: return "product";
1192
  case kind::TRANSPOSE: return "transpose";
1193
  case kind::TCLOSURE: return "tclosure";
1194
1195
  // bag theory
1196
2
  case kind::BAG_TYPE: return "Bag";
1197
  case kind::UNION_MAX: return "union_max";
1198
  case kind::UNION_DISJOINT: return "union_disjoint";
1199
  case kind::INTERSECTION_MIN: return "intersection_min";
1200
  case kind::DIFFERENCE_SUBTRACT: return "difference_subtract";
1201
  case kind::DIFFERENCE_REMOVE: return "difference_remove";
1202
  case kind::SUBBAG: return "subbag";
1203
26
  case kind::BAG_COUNT: return "bag.count";
1204
6
  case kind::DUPLICATE_REMOVAL: return "duplicate_removal";
1205
4
  case kind::MK_BAG: return "bag";
1206
  case kind::BAG_CARD: return "bag.card";
1207
  case kind::BAG_CHOOSE: return "bag.choose";
1208
  case kind::BAG_IS_SINGLETON: return "bag.is_singleton";
1209
  case kind::BAG_FROM_SET: return "bag.from_set";
1210
  case kind::BAG_TO_SET: return "bag.to_set";
1211
1212
    // fp theory
1213
  case kind::FLOATINGPOINT_FP: return "fp";
1214
  case kind::FLOATINGPOINT_EQ: return "fp.eq";
1215
1
  case kind::FLOATINGPOINT_ABS: return "fp.abs";
1216
2
  case kind::FLOATINGPOINT_NEG: return "fp.neg";
1217
6
  case kind::FLOATINGPOINT_PLUS: return "fp.add";
1218
13
  case kind::FLOATINGPOINT_SUB: return "fp.sub";
1219
10
  case kind::FLOATINGPOINT_MULT: return "fp.mul";
1220
19
  case kind::FLOATINGPOINT_DIV: return "fp.div";
1221
  case kind::FLOATINGPOINT_FMA: return "fp.fma";
1222
2
  case kind::FLOATINGPOINT_SQRT: return "fp.sqrt";
1223
15
  case kind::FLOATINGPOINT_REM: return "fp.rem";
1224
  case kind::FLOATINGPOINT_RTI: return "fp.roundToIntegral";
1225
  case kind::FLOATINGPOINT_MIN: return "fp.min";
1226
  case kind::FLOATINGPOINT_MAX: return "fp.max";
1227
  case kind::FLOATINGPOINT_MIN_TOTAL: return "fp.min_total";
1228
  case kind::FLOATINGPOINT_MAX_TOTAL: return "fp.max_total";
1229
1230
  case kind::FLOATINGPOINT_LEQ: return "fp.leq";
1231
  case kind::FLOATINGPOINT_LT: return "fp.lt";
1232
  case kind::FLOATINGPOINT_GEQ: return "fp.geq";
1233
  case kind::FLOATINGPOINT_GT: return "fp.gt";
1234
1235
1
  case kind::FLOATINGPOINT_ISN: return "fp.isNormal";
1236
1
  case kind::FLOATINGPOINT_ISSN: return "fp.isSubnormal";
1237
1
  case kind::FLOATINGPOINT_ISZ: return "fp.isZero";
1238
  case kind::FLOATINGPOINT_ISINF: return "fp.isInfinite";
1239
1
  case kind::FLOATINGPOINT_ISNAN: return "fp.isNaN";
1240
1
  case kind::FLOATINGPOINT_ISNEG: return "fp.isNegative";
1241
1
  case kind::FLOATINGPOINT_ISPOS: return "fp.isPositive";
1242
1243
  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "to_fp";
1244
  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "to_fp";
1245
  case kind::FLOATINGPOINT_TO_FP_REAL: return "to_fp";
1246
  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "to_fp";
1247
  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "to_fp_unsigned";
1248
  case kind::FLOATINGPOINT_TO_FP_GENERIC: return "to_fp_unsigned";
1249
  case kind::FLOATINGPOINT_TO_UBV: return "fp.to_ubv";
1250
  case kind::FLOATINGPOINT_TO_UBV_TOTAL: return "fp.to_ubv_total";
1251
  case kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv";
1252
  case kind::FLOATINGPOINT_TO_SBV_TOTAL: return "fp.to_sbv_total";
1253
  case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real";
1254
  case kind::FLOATINGPOINT_TO_REAL_TOTAL: return "fp.to_real_total";
1255
1256
  case kind::FLOATINGPOINT_COMPONENT_NAN: return "NAN";
1257
  case kind::FLOATINGPOINT_COMPONENT_INF: return "INF";
1258
  case kind::FLOATINGPOINT_COMPONENT_ZERO: return "ZERO";
1259
  case kind::FLOATINGPOINT_COMPONENT_SIGN: return "SIGN";
1260
  case kind::FLOATINGPOINT_COMPONENT_EXPONENT: return "EXPONENT";
1261
  case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: return "SIGNIFICAND";
1262
  case kind::ROUNDINGMODE_BITBLAST:
1263
    return "RMBITBLAST";
1264
1265
  //string theory
1266
  case kind::STRING_CONCAT: return "str.++";
1267
1600
  case kind::STRING_LENGTH: return "str.len";
1268
410
  case kind::STRING_SUBSTR: return "str.substr" ;
1269
  case kind::STRING_UPDATE: return "str.update";
1270
136
  case kind::STRING_STRCTN: return "str.contains" ;
1271
16
  case kind::STRING_CHARAT: return "str.at" ;
1272
125
  case kind::STRING_STRIDOF: return "str.indexof" ;
1273
370
  case kind::STRING_STRREPL: return "str.replace" ;
1274
  case kind::STRING_STRREPLALL: return "str.replace_all";
1275
12
  case kind::STRING_REPLACE_RE: return "str.replace_re";
1276
12
  case kind::STRING_REPLACE_RE_ALL: return "str.replace_re_all";
1277
  case kind::STRING_TOLOWER: return "str.tolower";
1278
  case kind::STRING_TOUPPER: return "str.toupper";
1279
  case kind::STRING_REV: return "str.rev";
1280
4
  case kind::STRING_PREFIX: return "str.prefixof" ;
1281
4
  case kind::STRING_SUFFIX: return "str.suffixof" ;
1282
  case kind::STRING_LEQ: return "str.<=";
1283
  case kind::STRING_LT: return "str.<";
1284
2
  case kind::STRING_FROM_CODE: return "str.from_code";
1285
670
  case kind::STRING_TO_CODE: return "str.to_code";
1286
13
  case kind::STRING_ITOS: return "str.from_int";
1287
  case kind::STRING_STOI: return "str.to_int";
1288
6
  case kind::STRING_IN_REGEXP: return "str.in_re";
1289
196
  case kind::STRING_TO_REGEXP: return "str.to_re";
1290
  case kind::REGEXP_EMPTY: return "re.none";
1291
216
  case kind::REGEXP_SIGMA: return "re.allchar";
1292
126
  case kind::REGEXP_CONCAT: return "re.++";
1293
4
  case kind::REGEXP_UNION: return "re.union";
1294
  case kind::REGEXP_INTER: return "re.inter";
1295
114
  case kind::REGEXP_STAR: return "re.*";
1296
  case kind::REGEXP_PLUS: return "re.+";
1297
  case kind::REGEXP_OPT: return "re.opt";
1298
  case kind::REGEXP_RANGE: return "re.range";
1299
  case kind::REGEXP_REPEAT: return "re.^";
1300
  case kind::REGEXP_LOOP: return "re.loop";
1301
  case kind::REGEXP_COMPLEMENT: return "re.comp";
1302
  case kind::REGEXP_DIFF: return "re.diff";
1303
12
  case kind::SEQUENCE_TYPE: return "Seq";
1304
  case kind::SEQ_UNIT: return "seq.unit";
1305
12
  case kind::SEQ_NTH: return "seq.nth";
1306
1307
  //sep theory
1308
  case kind::SEP_STAR: return "sep";
1309
  case kind::SEP_PTO: return "pto";
1310
1
  case kind::SEP_WAND: return "wand";
1311
2
  case kind::SEP_EMP: return "emp";
1312
1313
  // quantifiers
1314
22
  case kind::FORALL: return "forall";
1315
2
  case kind::EXISTS: return "exists";
1316
1317
  default:
1318
    ; /* fall through */
1319
  }
1320
1321
  // no SMT way to print these
1322
  return kind::kindToString(k);
1323
}
1324
1325
template <class T>
1326
static bool tryToStream(std::ostream& out, const Command* c);
1327
template <class T>
1328
static bool tryToStream(std::ostream& out, const Command* c, Variant v);
1329
1330
2
static std::string quoteSymbol(TNode n) {
1331
4
  std::stringstream ss;
1332
2
  ss << n;
1333
4
  return CVC4::quoteSymbol(ss.str());
1334
}
1335
1336
template <class T>
1337
static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v);
1338
1339
256738
void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const
1340
{
1341
513526
  if (tryToStream<CommandSuccess>(out, s, d_variant) ||
1342
65
      tryToStream<CommandFailure>(out, s, d_variant) ||
1343
15
      tryToStream<CommandRecoverableFailure>(out, s, d_variant) ||
1344
256738
      tryToStream<CommandUnsupported>(out, s, d_variant) ||
1345
      tryToStream<CommandInterrupted>(out, s, d_variant)) {
1346
256738
    return;
1347
  }
1348
1349
  out << "ERROR: don't know how to print a CommandStatus of class: "
1350
      << typeid(*s).name() << endl;
1351
1352
}/* Smt2Printer::toStream(CommandStatus*) */
1353
1354
10
void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const
1355
{
1356
10
  out << "(" << std::endl;
1357
10
  if (core.useNames())
1358
  {
1359
    // use the names
1360
7
    const std::vector<std::string>& cnames = core.getCoreNames();
1361
34
    for (const std::string& cn : cnames)
1362
    {
1363
27
      out << CVC4::quoteSymbol(cn) << std::endl;
1364
    }
1365
  }
1366
  else
1367
  {
1368
    // otherwise, use the formulas
1369
6
    for (UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i)
1370
    {
1371
3
      out << *i << endl;
1372
    }
1373
  }
1374
10
  out << ")" << endl;
1375
10
}/* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
1376
1377
21
void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const
1378
{
1379
21
  const theory::TheoryModel* tm = m.getTheoryModel();
1380
  //print the model comments
1381
42
  std::stringstream c;
1382
21
  tm->getComments(c);
1383
42
  std::string ln;
1384
21
  while( std::getline( c, ln ) ){
1385
    out << "; " << ln << std::endl;
1386
  }
1387
  //print the model
1388
21
  out << "(" << endl;
1389
  // don't need to print approximations since they are built into choice
1390
  // functions in the values of variables.
1391
21
  this->Printer::toStream(out, m);
1392
21
  out << ")" << endl;
1393
  //print the heap model, if it exists
1394
42
  Node h, neq;
1395
21
  if (tm->getHeapModel(h, neq))
1396
  {
1397
    // description of the heap+what nil is equal to fully describes model
1398
    out << "(heap" << endl;
1399
    out << h << endl;
1400
    out << neq << endl;
1401
    out << ")" << std::endl;
1402
  }
1403
21
}
1404
1405
4
void Smt2Printer::toStreamModelSort(std::ostream& out,
1406
                                    const smt::Model& m,
1407
                                    TypeNode tn) const
1408
{
1409
4
  if (!tn.isSort())
1410
  {
1411
    out << "ERROR: don't know how to print non uninterpreted sort in model: "
1412
        << tn << std::endl;
1413
    return;
1414
  }
1415
4
  const theory::TheoryModel* tm = m.getTheoryModel();
1416
8
  std::vector<Node> elements = tm->getDomainElements(tn);
1417
4
  if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum)
1418
  {
1419
    out << "(declare-datatypes ((" << tn << " 0)) (";
1420
    for (const Node& type_ref : elements)
1421
    {
1422
      out << "(" << type_ref << ")";
1423
    }
1424
    out << ")))" << endl;
1425
    return;
1426
  }
1427
  // print the cardinality
1428
4
  out << "; cardinality of " << tn << " is " << elements.size() << endl;
1429
8
  if (options::modelUninterpPrint()
1430
4
      == options::ModelUninterpPrintMode::DeclSortAndFun)
1431
  {
1432
    toStreamCmdDeclareType(out, tn);
1433
  }
1434
  // print the representatives
1435
8
  for (const Node& trn : elements)
1436
  {
1437
4
    if (trn.isVar())
1438
    {
1439
8
      if (options::modelUninterpPrint()
1440
              == options::ModelUninterpPrintMode::DeclSortAndFun
1441
4
          || options::modelUninterpPrint()
1442
                 == options::ModelUninterpPrintMode::DeclFun)
1443
      {
1444
4
        out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")"
1445
2
            << endl;
1446
      }
1447
    }
1448
    else
1449
    {
1450
      out << "; rep: " << trn << endl;
1451
    }
1452
  }
1453
}
1454
1455
24
void Smt2Printer::toStreamModelTerm(std::ostream& out,
1456
                                    const smt::Model& m,
1457
                                    Node n) const
1458
{
1459
24
  const theory::TheoryModel* tm = m.getTheoryModel();
1460
  // We get the value from the theory model directly, which notice
1461
  // does not have to go through the standard SmtEngine::getValue interface.
1462
48
  Node val = tm->getValue(n);
1463
24
  if (val.getKind() == kind::LAMBDA)
1464
  {
1465
2
    TypeNode rangeType = n.getType().getRangeType();
1466
1
    out << "(define-fun " << n << " " << val[0] << " " << rangeType << " ";
1467
    // call toStream and force its type to be proper
1468
1
    toStreamCastToType(out, val[1], -1, rangeType);
1469
1
    out << ")" << endl;
1470
  }
1471
  else
1472
  {
1473
46
    if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
1474
23
        && val.getKind() == kind::STORE)
1475
    {
1476
      TypeNode tn = val[1].getType();
1477
      const std::vector<Node>* type_refs =
1478
          tm->getRepSet()->getTypeRepsOrNull(tn);
1479
      if (tn.isSort() && type_refs != nullptr)
1480
      {
1481
        Cardinality indexCard(type_refs->size());
1482
        val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
1483
            val, indexCard);
1484
      }
1485
    }
1486
23
    out << "(define-fun " << n << " () " << n.getType() << " ";
1487
    // call toStream and force its type to be proper
1488
23
    toStreamCastToType(out, val, -1, n.getType());
1489
23
    out << ")" << endl;
1490
  }
1491
24
}
1492
1493
7
void Smt2Printer::toStreamCmdAssert(std::ostream& out, Node n) const
1494
{
1495
7
  out << "(assert " << n << ')' << std::endl;
1496
7
}
1497
1498
void Smt2Printer::toStreamCmdPush(std::ostream& out) const
1499
{
1500
  out << "(push 1)" << std::endl;
1501
}
1502
1503
void Smt2Printer::toStreamCmdPop(std::ostream& out) const
1504
{
1505
  out << "(pop 1)" << std::endl;
1506
}
1507
1508
2
void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
1509
{
1510
2
  if (!n.isNull())
1511
  {
1512
    toStreamCmdPush(out);
1513
    out << std::endl;
1514
    toStreamCmdAssert(out, n);
1515
    out << std::endl;
1516
    toStreamCmdCheckSat(out);
1517
    out << std::endl;
1518
    toStreamCmdPop(out);
1519
  }
1520
  else
1521
  {
1522
2
    out << "(check-sat)";
1523
  }
1524
2
  out << std::endl;
1525
2
}
1526
1527
void Smt2Printer::toStreamCmdCheckSatAssuming(
1528
    std::ostream& out, const std::vector<Node>& nodes) const
1529
{
1530
  out << "(check-sat-assuming ( ";
1531
  copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
1532
  out << "))" << std::endl;
1533
}
1534
1535
void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const
1536
{
1537
  if (!n.isNull())
1538
  {
1539
    toStreamCmdCheckSatAssuming(out, {n});
1540
  }
1541
  else
1542
  {
1543
    toStreamCmdCheckSat(out);
1544
  }
1545
}
1546
1547
void Smt2Printer::toStreamCmdReset(std::ostream& out) const
1548
{
1549
  out << "(reset)" << std::endl;
1550
}
1551
1552
void Smt2Printer::toStreamCmdResetAssertions(std::ostream& out) const
1553
{
1554
  out << "(reset-assertions)" << std::endl;
1555
}
1556
1557
void Smt2Printer::toStreamCmdQuit(std::ostream& out) const
1558
{
1559
  out << "(exit)" << std::endl;
1560
}
1561
1562
void Smt2Printer::toStreamCmdCommandSequence(
1563
    std::ostream& out, const std::vector<Command*>& sequence) const
1564
{
1565
  for (Command* i : sequence)
1566
  {
1567
    out << *i;
1568
  }
1569
}
1570
1571
void Smt2Printer::toStreamCmdDeclarationSequence(
1572
    std::ostream& out, const std::vector<Command*>& sequence) const
1573
{
1574
  toStreamCmdCommandSequence(out, sequence);
1575
}
1576
1577
10
void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out,
1578
                                             const std::string& id,
1579
                                             TypeNode type) const
1580
{
1581
10
  out << "(declare-fun " << CVC4::quoteSymbol(id) << " (";
1582
10
  if (type.isFunction())
1583
  {
1584
    const vector<TypeNode> argTypes = type.getArgTypes();
1585
    if (argTypes.size() > 0)
1586
    {
1587
      copy(argTypes.begin(),
1588
           argTypes.end() - 1,
1589
           ostream_iterator<TypeNode>(out, " "));
1590
      out << argTypes.back();
1591
    }
1592
    type = type.getRangeType();
1593
  }
1594
1595
10
  out << ") " << type << ')' << std::endl;
1596
10
}
1597
1598
5
void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out,
1599
                                            const std::string& id,
1600
                                            const std::vector<Node>& formals,
1601
                                            TypeNode range,
1602
                                            Node formula) const
1603
{
1604
5
  out << "(define-fun " << id << " (";
1605
5
  if (!formals.empty())
1606
  {
1607
3
    vector<Node>::const_iterator i = formals.cbegin();
1608
    for (;;)
1609
    {
1610
5
      out << "(" << (*i) << " " << (*i).getType() << ")";
1611
4
      ++i;
1612
4
      if (i != formals.cend())
1613
      {
1614
1
        out << " ";
1615
      }
1616
      else
1617
      {
1618
3
        break;
1619
      }
1620
    }
1621
  }
1622
5
  out << ") " << range << ' ' << formula << ')' << std::endl;
1623
5
}
1624
1625
void Smt2Printer::toStreamCmdDefineFunctionRec(
1626
    std::ostream& out,
1627
    const std::vector<Node>& funcs,
1628
    const std::vector<std::vector<Node>>& formals,
1629
    const std::vector<Node>& formulas) const
1630
{
1631
  out << "(define-fun";
1632
  if (funcs.size() > 1)
1633
  {
1634
    out << "s";
1635
  }
1636
  out << "-rec ";
1637
  if (funcs.size() > 1)
1638
  {
1639
    out << "(";
1640
  }
1641
  for (unsigned i = 0, size = funcs.size(); i < size; i++)
1642
  {
1643
    if (funcs.size() > 1)
1644
    {
1645
      if (i > 0)
1646
      {
1647
        out << " ";
1648
      }
1649
      out << "(";
1650
    }
1651
    out << funcs[i] << " (";
1652
    // print its type signature
1653
    vector<Node>::const_iterator itf = formals[i].cbegin();
1654
    for (;;)
1655
    {
1656
      out << "(" << (*itf) << " " << (*itf).getType() << ")";
1657
      ++itf;
1658
      if (itf != formals[i].end())
1659
      {
1660
        out << " ";
1661
      }
1662
      else
1663
      {
1664
        break;
1665
      }
1666
    }
1667
    TypeNode type = funcs[i].getType();
1668
    type = type.getRangeType();
1669
    out << ") " << type;
1670
    if (funcs.size() > 1)
1671
    {
1672
      out << ")";
1673
    }
1674
  }
1675
  if (funcs.size() > 1)
1676
  {
1677
    out << ") (";
1678
  }
1679
  for (unsigned i = 0, size = formulas.size(); i < size; i++)
1680
  {
1681
    if (i > 0)
1682
    {
1683
      out << " ";
1684
    }
1685
    out << formulas[i];
1686
  }
1687
  if (funcs.size() > 1)
1688
  {
1689
    out << ")";
1690
  }
1691
  out << ")" << std::endl;
1692
}
1693
1694
void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
1695
                                         TypeNode type) const
1696
{
1697
  Assert(type.isSort() || type.isSortConstructor());
1698
  std::stringstream id;
1699
  id << type;
1700
  size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0;
1701
  out << "(declare-sort " << CVC4::quoteSymbol(id.str()) << " " << arity << ")"
1702
      << std::endl;
1703
}
1704
1705
void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
1706
                                        const std::string& id,
1707
                                        const std::vector<TypeNode>& params,
1708
                                        TypeNode t) const
1709
{
1710
  out << "(define-sort " << CVC4::quoteSymbol(id) << " (";
1711
  if (params.size() > 0)
1712
  {
1713
    copy(
1714
        params.begin(), params.end() - 1, ostream_iterator<TypeNode>(out, " "));
1715
    out << params.back();
1716
  }
1717
  out << ") " << t << ")" << std::endl;
1718
}
1719
1720
void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
1721
{
1722
  out << "(simplify " << n << ')' << std::endl;
1723
}
1724
1725
void Smt2Printer::toStreamCmdGetValue(std::ostream& out,
1726
                                      const std::vector<Node>& nodes) const
1727
{
1728
  out << "(get-value ( ";
1729
  copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
1730
  out << "))" << std::endl;
1731
}
1732
1733
void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const
1734
{
1735
  out << "(get-model)" << std::endl;
1736
}
1737
1738
void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const
1739
{
1740
  out << "(get-assignment)" << std::endl;
1741
}
1742
1743
void Smt2Printer::toStreamCmdGetAssertions(std::ostream& out) const
1744
{
1745
  out << "(get-assertions)" << std::endl;
1746
}
1747
1748
void Smt2Printer::toStreamCmdGetProof(std::ostream& out) const
1749
{
1750
  out << "(get-proof)" << std::endl;
1751
}
1752
1753
void Smt2Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
1754
{
1755
  out << "(get-unsat-assumptions)" << std::endl;
1756
}
1757
1758
void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
1759
{
1760
  out << "(get-unsat-core)" << std::endl;
1761
}
1762
1763
void Smt2Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
1764
                                                Result::Sat status) const
1765
{
1766
  out << "(set-info :status " << status << ')' << std::endl;
1767
}
1768
1769
2
void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
1770
                                               const std::string& logic) const
1771
{
1772
2
  out << "(set-logic " << logic << ')' << std::endl;
1773
2
}
1774
1775
void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
1776
                                     const std::string& flag,
1777
                                     const std::string& value) const
1778
{
1779
  out << "(set-info :" << flag << ' ' << value << ')' << std::endl;
1780
}
1781
1782
11
void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
1783
                                     const std::string& flag) const
1784
{
1785
11
  out << "(get-info :" << flag << ')' << std::endl;
1786
11
}
1787
1788
3
void Smt2Printer::toStreamCmdSetOption(std::ostream& out,
1789
                                       const std::string& flag,
1790
                                       const std::string& value) const
1791
{
1792
3
  out << "(set-option :" << flag << ' ' << value << ')' << std::endl;
1793
3
}
1794
1795
void Smt2Printer::toStreamCmdGetOption(std::ostream& out,
1796
                                       const std::string& flag) const
1797
{
1798
  out << "(get-option :" << flag << ')' << std::endl;
1799
}
1800
1801
void Smt2Printer::toStream(std::ostream& out, const DType& dt) const
1802
{
1803
  for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
1804
  {
1805
    const DTypeConstructor& cons = dt[i];
1806
    if (i != 0)
1807
    {
1808
      out << " ";
1809
    }
1810
    out << "(" << CVC4::quoteSymbol(cons.getName());
1811
    for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
1812
    {
1813
      const DTypeSelector& arg = cons[j];
1814
      out << " (" << arg.getSelector() << " " << arg.getRangeType() << ")";
1815
    }
1816
    out << ")";
1817
  }
1818
}
1819
1820
void Smt2Printer::toStreamCmdDatatypeDeclaration(
1821
    std::ostream& out, const std::vector<TypeNode>& datatypes) const
1822
{
1823
  Assert(!datatypes.empty());
1824
  Assert(datatypes[0].isDatatype());
1825
  const DType& d0 = datatypes[0].getDType();
1826
  if (d0.isTuple())
1827
  {
1828
    // not necessary to print tuples
1829
    Assert(datatypes.size() == 1);
1830
    return;
1831
  }
1832
  out << "(declare-";
1833
  if (d0.isCodatatype())
1834
  {
1835
    out << "co";
1836
  }
1837
  out << "datatypes";
1838
  out << " (";
1839
  for (const TypeNode& t : datatypes)
1840
  {
1841
    Assert(t.isDatatype());
1842
    const DType& d = t.getDType();
1843
    out << "(" << CVC4::quoteSymbol(d.getName());
1844
    out << " " << d.getNumParameters() << ")";
1845
  }
1846
  out << ") (";
1847
  for (const TypeNode& t : datatypes)
1848
  {
1849
    Assert(t.isDatatype());
1850
    const DType& d = t.getDType();
1851
    if (d.isParametric())
1852
    {
1853
      out << "(par (";
1854
      for (unsigned p = 0, nparam = d.getNumParameters(); p < nparam; p++)
1855
      {
1856
        out << (p > 0 ? " " : "") << d.getParameter(p);
1857
      }
1858
      out << ")";
1859
    }
1860
    out << "(";
1861
    toStream(out, d);
1862
    out << ")";
1863
    if (d.isParametric())
1864
    {
1865
      out << ")";
1866
    }
1867
  }
1868
  out << ")";
1869
  out << ")" << std::endl;
1870
}
1871
1872
3
void Smt2Printer::toStreamCmdComment(std::ostream& out,
1873
                                     const std::string& comment) const
1874
{
1875
6
  std::string s = comment;
1876
3
  size_t pos = 0;
1877
3
  while ((pos = s.find_first_of('"', pos)) != string::npos)
1878
  {
1879
    s.replace(pos, 1, "\"\"");
1880
    pos += 2;
1881
  }
1882
3
  out << "(set-info :notes \"" << s << "\")" << std::endl;
1883
3
}
1884
1885
void Smt2Printer::toStreamCmdDeclareHeap(std::ostream& out,
1886
                                         TypeNode locType,
1887
                                         TypeNode dataType) const
1888
{
1889
  out << "(declare-heap (" << locType << " " << dataType << "))" << std::endl;
1890
}
1891
1892
void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
1893
                                   const std::string& name) const
1894
{
1895
  out << std::endl;
1896
}
1897
1898
void Smt2Printer::toStreamCmdEcho(std::ostream& out,
1899
                                  const std::string& output) const
1900
{
1901
  std::string s = output;
1902
  // escape all double-quotes
1903
  size_t pos = 0;
1904
  while ((pos = s.find('"', pos)) != string::npos)
1905
  {
1906
    s.replace(pos, 1, "\"\"");
1907
    pos += 2;
1908
  }
1909
  out << "(echo \"" << s << "\")" << std::endl;
1910
}
1911
1912
/*
1913
   --------------------------------------------------------------------------
1914
    Handling SyGuS commands
1915
   --------------------------------------------------------------------------
1916
*/
1917
1918
1
static void toStreamSygusGrammar(std::ostream& out, const TypeNode& t)
1919
{
1920
1
  if (!t.isNull() && t.isDatatype() && t.getDType().isSygus())
1921
  {
1922
2
    std::stringstream types_predecl, types_list;
1923
2
    std::set<TypeNode> grammarTypes;
1924
2
    std::list<TypeNode> typesToPrint;
1925
1
    grammarTypes.insert(t);
1926
1
    typesToPrint.push_back(t);
1927
1
    NodeManager* nm = NodeManager::currentNM();
1928
    // for each datatype in grammar
1929
    //   name
1930
    //   sygus type
1931
    //   constructors in order
1932
    do
1933
    {
1934
2
      TypeNode curr = typesToPrint.front();
1935
1
      typesToPrint.pop_front();
1936
1
      Assert(curr.isDatatype() && curr.getDType().isSygus());
1937
1
      const DType& dt = curr.getDType();
1938
1
      types_list << '(' << dt.getName() << ' ' << dt.getSygusType() << " (";
1939
1
      types_predecl << '(' << dt.getName() << ' ' << dt.getSygusType() << ") ";
1940
1
      if (dt.getSygusAllowConst())
1941
      {
1942
        types_list << "(Constant " << dt.getSygusType() << ") ";
1943
      }
1944
2
      for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
1945
      {
1946
1
        const DTypeConstructor& cons = dt[i];
1947
        // make a sygus term
1948
2
        std::vector<Node> cchildren;
1949
1
        cchildren.push_back(cons.getConstructor());
1950
1
        for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
1951
        {
1952
          TypeNode argType = cons[j].getRangeType();
1953
          std::stringstream ss;
1954
          ss << argType;
1955
          Node bv = nm->mkBoundVar(ss.str(), argType);
1956
          cchildren.push_back(bv);
1957
          // if fresh type, store it for later processing
1958
          if (grammarTypes.insert(argType).second)
1959
          {
1960
            typesToPrint.push_back(argType);
1961
          }
1962
        }
1963
2
        Node consToPrint = nm->mkNode(kind::APPLY_CONSTRUCTOR, cchildren);
1964
        // now, print it using the conversion to builtin with external
1965
3
        types_list << theory::datatypes::utils::sygusToBuiltin(consToPrint,
1966
2
                                                               true);
1967
1
        types_list << ' ';
1968
      }
1969
1
      types_list << "))\n";
1970
1
    } while (!typesToPrint.empty());
1971
1972
1
    out << "\n(" << types_predecl.str() << ")\n(" << types_list.str() << ')';
1973
  }
1974
1
}
1975
1976
2
void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
1977
                                      Node f,
1978
                                      const std::vector<Node>& vars,
1979
                                      bool isInv,
1980
                                      TypeNode sygusType) const
1981
{
1982
4
  std::stringstream sym;
1983
2
  sym << f;
1984
  out << '(' << (isInv ? "synth-inv " : "synth-fun ")
1985
2
      << CVC4::quoteSymbol(sym.str()) << ' ';
1986
2
  out << '(';
1987
2
  if (!vars.empty())
1988
  {
1989
    // print variable list
1990
2
    std::vector<Node>::const_iterator i = vars.cbegin(), i_end = vars.cend();
1991
2
    out << '(' << *i << ' ' << i->getType() << ')';
1992
2
    ++i;
1993
2
    while (i != i_end)
1994
    {
1995
      out << " (" << *i << ' ' << i->getType() << ')';
1996
      ++i;
1997
    }
1998
  }
1999
2
  out << ')';
2000
  // if not invariant-to-synthesize, print return type
2001
2
  if (!isInv)
2002
  {
2003
2
    TypeNode ftn = f.getType();
2004
2
    TypeNode range = ftn.isFunction() ? ftn.getRangeType() : ftn;
2005
1
    out << ' ' << range;
2006
  }
2007
2
  out << '\n';
2008
  // print grammar, if any
2009
2
  if (!sygusType.isNull())
2010
  {
2011
1
    toStreamSygusGrammar(out, sygusType);
2012
  }
2013
2
  out << ')' << std::endl;
2014
2
}
2015
2016
1
void Smt2Printer::toStreamCmdDeclareVar(std::ostream& out,
2017
                                        Node var,
2018
                                        TypeNode type) const
2019
{
2020
1
  out << "(declare-var " << var << ' ' << type << ')' << std::endl;
2021
1
}
2022
2023
1
void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
2024
{
2025
1
  out << "(constraint " << n << ')' << std::endl;
2026
1
}
2027
2028
1
void Smt2Printer::toStreamCmdInvConstraint(
2029
    std::ostream& out, Node inv, Node pre, Node trans, Node post) const
2030
{
2031
2
  out << "(inv-constraint " << inv << ' ' << pre << ' ' << trans << ' ' << post
2032
1
      << ')' << std::endl;
2033
1
}
2034
2035
1
void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const
2036
{
2037
1
  out << "(check-synth)" << std::endl;
2038
1
}
2039
2040
void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
2041
                                       const std::string& name,
2042
                                       Node conj,
2043
                                       TypeNode sygusType) const
2044
{
2045
  out << "(get-abduct ";
2046
  out << name << ' ';
2047
  out << conj << ' ';
2048
2049
  // print grammar, if any
2050
  if (!sygusType.isNull())
2051
  {
2052
    toStreamSygusGrammar(out, sygusType);
2053
  }
2054
  out << ')' << std::endl;
2055
}
2056
2057
/*
2058
   --------------------------------------------------------------------------
2059
    End of Handling SyGuS commands
2060
   --------------------------------------------------------------------------
2061
*/
2062
2063
template <class T>
2064
static bool tryToStream(std::ostream& out, const Command* c)
2065
{
2066
  if(typeid(*c) == typeid(T)) {
2067
    toStream(out, dynamic_cast<const T*>(c));
2068
    return true;
2069
  }
2070
  return false;
2071
}
2072
2073
template <class T>
2074
static bool tryToStream(std::ostream& out, const Command* c, Variant v)
2075
{
2076
  if(typeid(*c) == typeid(T)) {
2077
    toStream(out, dynamic_cast<const T*>(c), v);
2078
    return true;
2079
  }
2080
  return false;
2081
}
2082
2083
256688
static void toStream(std::ostream& out, const CommandSuccess* s, Variant v)
2084
{
2085
256688
  if(Command::printsuccess::getPrintSuccess(out)) {
2086
18
    out << "success" << endl;
2087
  }
2088
256688
}
2089
2090
static void toStream(std::ostream& out, const CommandInterrupted* s, Variant v)
2091
{
2092
  out << "interrupted" << endl;
2093
}
2094
2095
static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v)
2096
{
2097
#ifdef CVC4_COMPETITION_MODE
2098
  // if in competition mode, lie and say we're ok
2099
  // (we have nothing to lose by saying success, and everything to lose
2100
  // if we say "unsupported")
2101
  out << "success" << endl;
2102
#else /* CVC4_COMPETITION_MODE */
2103
  out << "unsupported" << endl;
2104
#endif /* CVC4_COMPETITION_MODE */
2105
}
2106
2107
50
static void errorToStream(std::ostream& out, std::string message, Variant v) {
2108
  // escape all double-quotes
2109
50
  size_t pos = 0;
2110
54
  while((pos = message.find('"', pos)) != string::npos) {
2111
2
    message.replace(pos, 1, "\"\"");
2112
2
    pos += 2;
2113
  }
2114
50
  out << "(error \"" << message << "\")" << endl;
2115
50
}
2116
2117
35
static void toStream(std::ostream& out, const CommandFailure* s, Variant v) {
2118
35
  errorToStream(out, s->getMessage(), v);
2119
35
}
2120
2121
15
static void toStream(std::ostream& out, const CommandRecoverableFailure* s,
2122
                     Variant v) {
2123
15
  errorToStream(out, s->getMessage(), v);
2124
15
}
2125
2126
template <class T>
2127
256803
static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v)
2128
{
2129
256803
  if(typeid(*s) == typeid(T)) {
2130
256738
    toStream(out, dynamic_cast<const T*>(s), v);
2131
256738
    return true;
2132
  }
2133
65
  return false;
2134
}
2135
2136
}/* CVC4::printer::smt2 namespace */
2137
}/* CVC4::printer namespace */
2138
26932
}/* CVC4 namespace */