1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
5 * This file is part of the cvc5 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.
11 * ****************************************************************************
13 * The pretty-printer interface for the SMT2 output language.
16 #include "printer/smt2/smt2_printer.h"
24 #include "api/cpp/cvc5.h"
25 #include "expr/array_store_all.h"
26 #include "expr/ascription_type.h"
27 #include "expr/datatype_index.h"
28 #include "expr/dtype.h"
29 #include "expr/dtype_cons.h"
30 #include "expr/emptybag.h"
31 #include "expr/emptyset.h"
32 #include "expr/node_manager_attributes.h"
33 #include "expr/node_visitor.h"
34 #include "expr/sequence.h"
35 #include "expr/uninterpreted_constant.h"
36 #include "options/bv_options.h"
37 #include "options/language.h"
38 #include "options/printer_options.h"
39 #include "options/smt_options.h"
40 #include "printer/let_binding.h"
41 #include "proof/unsat_core.h"
42 #include "smt/command.h"
43 #include "smt/node_command.h"
44 #include "smt/smt_engine.h"
45 #include "smt_util/boolean_simplification.h"
46 #include "theory/arrays/theory_arrays_rewriter.h"
47 #include "theory/datatypes/sygus_datatype_utils.h"
48 #include "theory/datatypes/tuple_project_op.h"
49 #include "theory/quantifiers/quantifiers_attributes.h"
50 #include "theory/theory_model.h"
51 #include "util/bitvector.h"
52 #include "util/divisible.h"
53 #include "util/floatingpoint.h"
54 #include "util/iand.h"
55 #include "util/indexed_root_predicate.h"
56 #include "util/regexp.h"
57 #include "util/smt2_quote_string.h"
58 #include "util/string.h"
66 static void toStreamRational(std::ostream
& out
,
71 bool neg
= r
.sgn() < 0;
72 // Print the rational, possibly as decimal.
73 // Notice that we print (/ (- 5) 3) instead of (- (/ 5 3)),
74 // the former is compliant with real values in the smt lib standard.
99 Rational abs_r
= (-r
);
100 out
<< "(- " << abs_r
.getNumerator();
101 out
<< ") " << abs_r
.getDenominator();
105 out
<< r
.getNumerator();
106 out
<< ' ' << r
.getDenominator();
112 void Smt2Printer::toStream(std::ostream
& out
,
118 LetBinding
lbind(dag
+ 1);
119 toStreamWithLetify(out
, n
, toDepth
, &lbind
);
121 toStream(out
, n
, toDepth
);
125 void Smt2Printer::toStreamWithLetify(std::ostream
& out
,
128 LetBinding
* lbind
) const
130 if (lbind
== nullptr)
132 toStream(out
, n
, toDepth
);
135 std::stringstream cparen
;
136 std::vector
<Node
> letList
;
137 lbind
->letify(n
, letList
);
138 if (!letList
.empty())
140 std::map
<Node
, uint32_t>::const_iterator it
;
141 for (size_t i
= 0, nlets
= letList
.size(); i
< nlets
; i
++)
143 Node nl
= letList
[i
];
145 uint32_t id
= lbind
->getId(nl
);
146 out
<< "_let_" << id
<< " ";
147 Node nlc
= lbind
->convert(nl
, "_let_", false);
148 toStream(out
, nlc
, toDepth
, lbind
);
153 Node nc
= lbind
->convert(n
, "_let_");
154 // print the body, passing the lbind object
155 toStream(out
, nc
, toDepth
, lbind
);
160 void Smt2Printer::toStream(std::ostream
& out
,
163 LetBinding
* lbind
) const
166 if(n
.getKind() == kind::NULL_EXPR
) {
171 NodeManager
* nm
= NodeManager::currentNM();
173 if(n
.getMetaKind() == kind::metakind::CONSTANT
) {
174 switch(n
.getKind()) {
175 case kind::TYPE_CONSTANT
:
176 switch(n
.getConst
<TypeConstant
>()) {
177 case BOOLEAN_TYPE
: out
<< "Bool"; break;
178 case REAL_TYPE
: out
<< "Real"; break;
179 case INTEGER_TYPE
: out
<< "Int"; break;
180 case STRING_TYPE
: out
<< "String"; break;
181 case REGEXP_TYPE
: out
<< "RegLan"; break;
182 case ROUNDINGMODE_TYPE
: out
<< "RoundingMode"; break;
184 // fall back on whatever operator<< does on underlying type; we
185 // might luck out and be SMT-LIB v2 compliant
186 kind::metakind::NodeValueConstPrinter::toStream(out
, n
);
189 case kind::BITVECTOR_TYPE
:
190 out
<< "(_ BitVec " << n
.getConst
<BitVectorSize
>().d_size
<< ")";
192 case kind::FLOATINGPOINT_TYPE
:
193 out
<< "(_ FloatingPoint "
194 << n
.getConst
<FloatingPointSize
>().exponentWidth() << " "
195 << n
.getConst
<FloatingPointSize
>().significandWidth() << ")";
197 case kind::CONST_BITVECTOR
:
199 const BitVector
& bv
= n
.getConst
<BitVector
>();
200 if (options::bvPrintConstsAsIndexedSymbols())
202 out
<< "(_ bv" << bv
.getValue() << " " << bv
.getSize() << ")";
206 out
<< "#b" << bv
.toString();
210 case kind::CONST_FLOATINGPOINT
:
212 out
<< n
.getConst
<FloatingPoint
>().toString(
213 options::bvPrintConstsAsIndexedSymbols());
216 case kind::CONST_ROUNDINGMODE
:
217 switch (n
.getConst
<RoundingMode
>()) {
218 case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
:
219 out
<< "roundNearestTiesToEven";
221 case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
:
222 out
<< "roundNearestTiesToAway";
224 case RoundingMode::ROUND_TOWARD_POSITIVE
:
225 out
<< "roundTowardPositive";
227 case RoundingMode::ROUND_TOWARD_NEGATIVE
:
228 out
<< "roundTowardNegative";
230 case RoundingMode::ROUND_TOWARD_ZERO
: out
<< "roundTowardZero"; break;
232 Unreachable() << "Invalid value of rounding mode constant ("
233 << n
.getConst
<RoundingMode
>() << ")";
236 case kind::CONST_BOOLEAN
:
237 // the default would print "1" or "0" for bool, that's not correct
239 out
<< (n
.getConst
<bool>() ? "true" : "false");
242 out
<< smtKindString(n
.getConst
<Kind
>(), d_variant
);
244 case kind::CONST_RATIONAL
: {
245 const Rational
& r
= n
.getConst
<Rational
>();
246 toStreamRational(out
, r
, false, d_variant
);
250 case kind::CONST_STRING
: {
251 std::string s
= n
.getConst
<String
>().toString();
253 for(size_t i
= 0; i
< s
.size(); ++i
) {
264 case kind::CONST_SEQUENCE
:
266 const Sequence
& sn
= n
.getConst
<Sequence
>();
267 const std::vector
<Node
>& snvec
= sn
.getVec();
270 out
<< "(as seq.empty ";
271 toStreamType(out
, n
.getType());
274 else if (snvec
.size() > 1)
277 for (const Node
& snvc
: snvec
)
279 out
<< " (seq.unit " << snvc
<< ")";
285 out
<< "(seq.unit " << snvec
[0] << ")";
290 case kind::STORE_ALL
: {
291 ArrayStoreAll asa
= n
.getConst
<ArrayStoreAll
>();
292 out
<< "((as const ";
293 toStreamType(out
, asa
.getType());
294 out
<< ") " << asa
.getValue() << ")";
298 case kind::DATATYPE_TYPE
:
300 const DType
& dt
= (NodeManager::currentNM()->getDTypeForIndex(
301 n
.getConst
<DatatypeIndexConstant
>().getIndex()));
304 unsigned int nargs
= dt
[0].getNumArgs();
312 for (unsigned int i
= 0; i
< nargs
; i
++)
315 toStreamType(out
, dt
[0][i
].getRangeType());
322 out
<< cvc5::quoteSymbol(dt
.getName());
327 case kind::UNINTERPRETED_CONSTANT
: {
328 const UninterpretedConstant
& uc
= n
.getConst
<UninterpretedConstant
>();
329 std::stringstream ss
;
330 ss
<< "(as @" << uc
<< " " << n
.getType() << ")";
336 out
<< "(as emptyset ";
337 toStreamType(out
, n
.getConst
<EmptySet
>().getType());
342 out
<< "(as emptybag ";
343 toStreamType(out
, n
.getConst
<EmptyBag
>().getType());
346 case kind::BITVECTOR_EXTRACT_OP
:
348 BitVectorExtract p
= n
.getConst
<BitVectorExtract
>();
349 out
<< "(_ extract " << p
.d_high
<< ' ' << p
.d_low
<< ")";
352 case kind::BITVECTOR_REPEAT_OP
:
353 out
<< "(_ repeat " << n
.getConst
<BitVectorRepeat
>().d_repeatAmount
356 case kind::BITVECTOR_ZERO_EXTEND_OP
:
357 out
<< "(_ zero_extend "
358 << n
.getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
<< ")";
360 case kind::BITVECTOR_SIGN_EXTEND_OP
:
361 out
<< "(_ sign_extend "
362 << n
.getConst
<BitVectorSignExtend
>().d_signExtendAmount
<< ")";
364 case kind::BITVECTOR_ROTATE_LEFT_OP
:
365 out
<< "(_ rotate_left "
366 << n
.getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
<< ")";
368 case kind::BITVECTOR_ROTATE_RIGHT_OP
:
369 out
<< "(_ rotate_right "
370 << n
.getConst
<BitVectorRotateRight
>().d_rotateRightAmount
<< ")";
372 case kind::INT_TO_BITVECTOR_OP
:
373 out
<< "(_ int2bv " << n
.getConst
<IntToBitVector
>().d_size
<< ")";
375 case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP
:
377 << n
.getConst
<FloatingPointToFPIEEEBitVector
>()
381 << n
.getConst
<FloatingPointToFPIEEEBitVector
>()
386 case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP
:
388 << n
.getConst
<FloatingPointToFPFloatingPoint
>()
392 << n
.getConst
<FloatingPointToFPFloatingPoint
>()
397 case kind::FLOATINGPOINT_TO_FP_REAL_OP
:
399 << n
.getConst
<FloatingPointToFPReal
>().getSize().exponentWidth()
401 << n
.getConst
<FloatingPointToFPReal
>().getSize().significandWidth()
404 case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP
:
406 << n
.getConst
<FloatingPointToFPSignedBitVector
>()
410 << n
.getConst
<FloatingPointToFPSignedBitVector
>()
415 case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP
:
416 out
<< "(_ to_fp_unsigned "
417 << n
.getConst
<FloatingPointToFPUnsignedBitVector
>()
421 << n
.getConst
<FloatingPointToFPUnsignedBitVector
>()
426 case kind::FLOATINGPOINT_TO_FP_GENERIC_OP
:
428 << n
.getConst
<FloatingPointToFPGeneric
>().getSize().exponentWidth()
430 << n
.getConst
<FloatingPointToFPGeneric
>().getSize().significandWidth()
433 case kind::FLOATINGPOINT_TO_UBV_OP
:
434 out
<< "(_ fp.to_ubv "
435 << n
.getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
<< ")";
437 case kind::FLOATINGPOINT_TO_SBV_OP
:
438 out
<< "(_ fp.to_sbv "
439 << n
.getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
<< ")";
441 case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP
:
442 out
<< "(_ fp.to_ubv_total "
443 << n
.getConst
<FloatingPointToUBVTotal
>().d_bv_size
.d_size
<< ")";
445 case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP
:
446 out
<< "(_ fp.to_sbv_total "
447 << n
.getConst
<FloatingPointToSBVTotal
>().d_bv_size
.d_size
<< ")";
449 case kind::REGEXP_REPEAT_OP
:
450 out
<< "(_ re.^ " << n
.getConst
<RegExpRepeat
>().d_repeatAmount
<< ")";
452 case kind::REGEXP_LOOP_OP
:
453 out
<< "(_ re.loop " << n
.getConst
<RegExpLoop
>().d_loopMinOcc
<< " "
454 << n
.getConst
<RegExpLoop
>().d_loopMaxOcc
<< ")";
457 // fall back on whatever operator<< does on underlying type; we
458 // might luck out and be SMT-LIB v2 compliant
459 kind::metakind::NodeValueConstPrinter::toStream(out
, n
);
465 if(n
.getKind() == kind::SORT_TYPE
) {
467 if(n
.getNumChildren() != 0) {
470 if(n
.getAttribute(expr::VarNameAttr(), name
)) {
471 out
<< cvc5::quoteSymbol(name
);
473 if(n
.getNumChildren() != 0) {
474 for(unsigned i
= 0; i
< n
.getNumChildren(); ++i
) {
476 toStream(out
, n
[i
], toDepth
);
483 // determine if we are printing out a type ascription, store the argument of
484 // the type ascription into type_asc_arg.
485 Kind k
= n
.getKind();
488 if (k
== kind::APPLY_TYPE_ASCRIPTION
)
490 force_nt
= n
.getOperator().getConst
<AscriptionType
>().getType();
493 else if (k
== kind::CAST_TO_REAL
)
495 force_nt
= nm
->realType();
498 if (!type_asc_arg
.isNull())
500 if (force_nt
.isReal())
502 // we prefer using (/ x 1) instead of (to_real x) here.
503 // the reason is that (/ x 1) is SMT-LIB compliant when x is a constant
504 // or the logic is non-linear, whereas (to_real x) is compliant when
505 // the logic is mixed int/real. The former occurs more frequently.
506 bool is_int
= force_nt
.isInteger();
507 // If constant rational, print as special case
508 if (type_asc_arg
.getKind() == kind::CONST_RATIONAL
)
510 const Rational
& r
= type_asc_arg
.getConst
<Rational
>();
511 toStreamRational(out
, r
, !is_int
, d_variant
);
516 << smtKindString(is_int
? kind::TO_INTEGER
: kind::DIVISION
,
519 toStream(out
, type_asc_arg
, toDepth
, lbind
);
529 // use type ascription
531 toStream(out
, type_asc_arg
, toDepth
< 0 ? toDepth
: toDepth
- 1, lbind
);
532 out
<< " " << force_nt
<< ")";
541 if (n
.getAttribute(expr::VarNameAttr(), s
))
543 out
<< cvc5::quoteSymbol(s
);
547 if (n
.getKind() == kind::VARIABLE
)
553 out
<< n
.getKind() << '_';
560 bool stillNeedToPrintParams
= true;
561 bool forceBinary
= false; // force N-ary to binary when outputing children
563 if (n
.getNumChildren() != 0 && k
!= kind::CONSTRUCTOR_TYPE
)
569 case kind::FUNCTION_TYPE
:
574 toStream(out
, nc
, toDepth
);
578 case kind::SEXPR
: break;
581 case kind::APPLY_UF
: break;
584 if (!options::flattenHOChains())
588 // collapse "@" chains, i.e.
590 // ((a b) c) --> (a b c)
592 // (((a b) ((c d) e)) f) --> (a b (c d e) f)
595 std::vector
<Node
> args
;
596 while (head
.getKind() == kind::HO_APPLY
)
598 args
.insert(args
.begin(), head
[1]);
601 toStream(out
, head
, toDepth
, lbind
);
602 for (unsigned i
= 0, size
= args
.size(); i
< size
; ++i
)
605 toStream(out
, args
[i
], toDepth
, lbind
);
612 out
<< smtKindString(k
, d_variant
) << " ";
613 toStream(out
, n
[0], toDepth
, lbind
);
615 for (size_t i
= 1, nchild
= n
.getNumChildren(); i
< nchild
; i
++)
621 toStream(out
, n
[i
], toDepth
, lbind
);
625 case kind::MATCH_BIND_CASE
:
627 toStream(out
, n
[1], toDepth
, lbind
);
629 toStream(out
, n
[2], toDepth
, lbind
);
632 case kind::MATCH_CASE
:
638 out
<< "(_ iand " << n
.getOperator().getConst
<IntAnd
>().d_size
<< ") ";
639 stillNeedToPrintParams
= false;
642 case kind::DIVISIBLE
:
643 out
<< "(_ divisible " << n
.getOperator().getConst
<Divisible
>().k
<< ")";
644 stillNeedToPrintParams
= false;
646 case kind::INDEXED_ROOT_PREDICATE_OP
:
648 const IndexedRootPredicate
& irp
= n
.getConst
<IndexedRootPredicate
>();
649 out
<< "(_ root_predicate " << irp
.d_index
<< ")";
654 case kind::REGEXP_REPEAT
:
655 case kind::REGEXP_LOOP
:
657 out
<< n
.getOperator() << ' ';
658 stillNeedToPrintParams
= false;
662 case kind::CARDINALITY_CONSTRAINT
: out
<< "fmf.card "; break;
663 case kind::CARDINALITY_VALUE
: out
<< "fmf.card.val "; break;
666 case kind::BITVECTOR_CONCAT
:
667 case kind::BITVECTOR_AND
:
668 case kind::BITVECTOR_OR
:
669 case kind::BITVECTOR_XOR
:
670 case kind::BITVECTOR_MULT
:
671 case kind::BITVECTOR_ADD
:
673 out
<< smtKindString(k
, d_variant
) << " ";
678 case kind::BITVECTOR_EXTRACT
:
679 case kind::BITVECTOR_REPEAT
:
680 case kind::BITVECTOR_ZERO_EXTEND
:
681 case kind::BITVECTOR_SIGN_EXTEND
:
682 case kind::BITVECTOR_ROTATE_LEFT
:
683 case kind::BITVECTOR_ROTATE_RIGHT
:
684 case kind::INT_TO_BITVECTOR
:
685 toStream(out
, n
.getOperator(), toDepth
, nullptr);
687 stillNeedToPrintParams
= false;
691 case kind::SINGLETON
:
693 out
<< smtKindString(k
, d_variant
) << " ";
694 TypeNode elemType
= n
.getType().getSetElementType();
696 out
, n
[0], toDepth
< 0 ? toDepth
: toDepth
- 1, elemType
);
701 case kind::UNIVERSE_SET
:out
<< "(as univset " << n
.getType() << ")";break;
706 // print (bag (mkBag_op Real) 1 3) as (bag 1.0 3)
707 out
<< smtKindString(k
, d_variant
) << " ";
708 TypeNode elemType
= n
.getType().getBagElementType();
710 out
, n
[0], toDepth
< 0 ? toDepth
: toDepth
- 1, elemType
);
711 out
<< " " << n
[1] << ")";
716 case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
717 case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
718 case kind::FLOATINGPOINT_TO_FP_REAL
:
719 case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
720 case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
721 case kind::FLOATINGPOINT_TO_FP_GENERIC
:
722 case kind::FLOATINGPOINT_TO_UBV
:
723 case kind::FLOATINGPOINT_TO_SBV
:
724 out
<< n
.getOperator() << ' ';
725 stillNeedToPrintParams
= false;
728 case kind::APPLY_CONSTRUCTOR
:
730 const DType
& dt
= DType::datatypeOf(n
.getOperator());
733 stillNeedToPrintParams
= false;
734 out
<< "mkTuple" << ( dt
[0].getNumArgs()==0 ? "" : " ");
738 case kind::TUPLE_PROJECT
:
740 TupleProjectOp op
= n
.getOperator().getConst
<TupleProjectOp
>();
741 if (op
.getIndices().empty())
743 // e.g. (tuple_project tuple)
744 out
<< "project " << n
[0] << ")";
748 // e.g. ((_ tuple_project 2 4 4) tuple)
749 out
<< "(_ tuple_project" << op
<< ") " << n
[0] << ")";
753 case kind::CONSTRUCTOR_TYPE
:
755 out
<< n
[n
.getNumChildren()-1];
759 case kind::APPLY_SELECTOR
:
761 Node op
= n
.getOperator();
762 const DType
& dt
= DType::datatypeOf(op
);
765 stillNeedToPrintParams
= false;
766 out
<< "(_ tupSel " << DType::indexOf(op
) << ") ";
770 case kind::APPLY_TESTER
:
772 stillNeedToPrintParams
= false;
773 Node op
= n
.getOperator();
774 size_t cindex
= DType::indexOf(op
);
775 const DType
& dt
= DType::datatypeOf(op
);
778 out
, dt
[cindex
].getConstructor(), toDepth
< 0 ? toDepth
: toDepth
- 1);
782 case kind::APPLY_UPDATER
:
784 Node op
= n
.getOperator();
785 size_t index
= DType::indexOf(op
);
786 const DType
& dt
= DType::datatypeOf(op
);
787 size_t cindex
= DType::cindexOf(op
);
790 dt
[cindex
][index
].getSelector(),
791 toDepth
< 0 ? toDepth
: toDepth
- 1);
795 case kind::APPLY_SELECTOR_TOTAL
:
796 case kind::PARAMETRIC_DATATYPE
: break;
800 out
<< "(as sep.nil " << n
.getType() << ")";
809 out
<< smtKindString(k
, d_variant
) << " ";
810 // do not letify the bound variable list
811 toStream(out
, n
[0], toDepth
, nullptr);
813 std::stringstream annot
;
814 if (n
.getNumChildren() == 3)
817 for (const Node
& nc
: n
[2])
819 if (nc
.getKind() == kind::INST_PATTERN
)
822 annot
<< ":pattern ";
823 toStream(annot
, nc
, toDepth
, nullptr);
826 else if (nc
.getKind() == kind::INST_NO_PATTERN
)
829 annot
<< ":no-pattern ";
830 toStream(annot
, nc
, toDepth
, nullptr);
835 // Use a fresh let binder, since using existing let symbols may violate
836 // scoping issues for let-bound variables, see explanation in let_binding.h.
837 size_t dag
= lbind
== nullptr ? 0 : lbind
->getThreshold()-1;
838 toStream(out
, n
[1], toDepth
- 1, dag
);
839 out
<< annot
.str() << ")";
843 case kind::BOUND_VAR_LIST
:
845 // the left parenthesis is already printed (before the switch)
846 for (TNode::iterator i
= n
.begin(), iend
= n
.end(); i
!= iend
;)
849 toStream(out
, *i
, toDepth
< 0 ? toDepth
: toDepth
- 1);
851 out
<< (*i
).getType();
861 case kind::INST_PATTERN
:
862 case kind::INST_NO_PATTERN
:
863 case kind::INST_PATTERN_LIST
: break;
865 // by default, print the kind using the smtKindString utility
866 out
<< smtKindString(k
, d_variant
) << " ";
869 if( n
.getMetaKind() == kind::metakind::PARAMETERIZED
&&
870 stillNeedToPrintParams
) {
873 out
, n
.getOperator(), toDepth
< 0 ? toDepth
: toDepth
- 1, lbind
);
877 if(n
.getNumChildren() > 0) {
883 for(size_t i
= 0, c
= 1; i
< n
.getNumChildren(); ) {
885 toStream(out
, n
[i
], toDepth
< 0 ? toDepth
: toDepth
- c
, lbind
);
889 if(++i
< n
.getNumChildren()) {
890 if(forceBinary
&& i
< n
.getNumChildren() - 1) {
891 // not going to work properly for parameterized kinds!
892 Assert(n
.getMetaKind() != kind::metakind::PARAMETERIZED
);
893 out
<< " (" << smtKindString(n
.getKind(), d_variant
) << ' ';
901 if (n
.getNumChildren() != 0)
903 out
<< parens
.str() << ')';
907 void Smt2Printer::toStreamCastToType(std::ostream
& out
,
913 if (n
.getType().isInteger() && !tn
.isInteger())
916 // probably due to subtyping integers and reals, cast it
917 nasc
= NodeManager::currentNM()->mkNode(kind::CAST_TO_REAL
, n
);
923 toStream(out
, nasc
, toDepth
);
926 std::string
Smt2Printer::smtKindString(Kind k
, Variant v
)
930 case kind::EQUAL
: return "=";
931 case kind::DISTINCT
: return "distinct";
932 case kind::SEXPR
: break;
935 case kind::NOT
: return "not";
936 case kind::AND
: return "and";
937 case kind::IMPLIES
: return "=>";
938 case kind::OR
: return "or";
939 case kind::XOR
: return "xor";
940 case kind::ITE
: return "ite";
943 case kind::APPLY_UF
: break;
945 case kind::LAMBDA
: return "lambda";
946 case kind::MATCH
: return "match";
947 case kind::WITNESS
: return "witness";
950 case kind::PLUS
: return "+";
952 case kind::NONLINEAR_MULT
: return "*";
953 case kind::IAND
: return "iand";
954 case kind::POW2
: return "POW2";
955 case kind::EXPONENTIAL
: return "exp";
956 case kind::SINE
: return "sin";
957 case kind::COSINE
: return "cos";
958 case kind::TANGENT
: return "tan";
959 case kind::COSECANT
: return "csc";
960 case kind::SECANT
: return "sec";
961 case kind::COTANGENT
: return "cot";
962 case kind::ARCSINE
: return "arcsin";
963 case kind::ARCCOSINE
: return "arccos";
964 case kind::ARCTANGENT
: return "arctan";
965 case kind::ARCCOSECANT
: return "arccsc";
966 case kind::ARCSECANT
: return "arcsec";
967 case kind::ARCCOTANGENT
: return "arccot";
968 case kind::PI
: return "real.pi";
969 case kind::SQRT
: return "sqrt";
970 case kind::MINUS
: return "-";
971 case kind::UMINUS
: return "-";
972 case kind::LT
: return "<";
973 case kind::LEQ
: return "<=";
974 case kind::GT
: return ">";
975 case kind::GEQ
: return ">=";
977 case kind::DIVISION_TOTAL
: return "/";
978 case kind::INTS_DIVISION_TOTAL
:
979 case kind::INTS_DIVISION
: return "div";
980 case kind::INTS_MODULUS_TOTAL
:
981 case kind::INTS_MODULUS
: return "mod";
982 case kind::ABS
: return "abs";
983 case kind::IS_INTEGER
: return "is_int";
984 case kind::TO_INTEGER
: return "to_int";
985 case kind::TO_REAL
: return "to_real";
986 case kind::POW
: return "^";
989 case kind::SELECT
: return "select";
990 case kind::STORE
: return "store";
991 case kind::ARRAY_TYPE
: return "Array";
992 case kind::PARTIAL_SELECT_0
: return "partial_select_0";
993 case kind::PARTIAL_SELECT_1
: return "partial_select_1";
998 case kind::BITVECTOR_CONCAT
: return "concat";
999 case kind::BITVECTOR_AND
: return "bvand";
1000 case kind::BITVECTOR_OR
: return "bvor";
1001 case kind::BITVECTOR_XOR
: return "bvxor";
1002 case kind::BITVECTOR_NOT
: return "bvnot";
1003 case kind::BITVECTOR_NAND
: return "bvnand";
1004 case kind::BITVECTOR_NOR
: return "bvnor";
1005 case kind::BITVECTOR_XNOR
: return "bvxnor";
1006 case kind::BITVECTOR_COMP
: return "bvcomp";
1007 case kind::BITVECTOR_MULT
: return "bvmul";
1008 case kind::BITVECTOR_ADD
: return "bvadd";
1009 case kind::BITVECTOR_SUB
: return "bvsub";
1010 case kind::BITVECTOR_NEG
: return "bvneg";
1011 case kind::BITVECTOR_UDIV
: return "bvudiv";
1012 case kind::BITVECTOR_UREM
: return "bvurem";
1013 case kind::BITVECTOR_SDIV
: return "bvsdiv";
1014 case kind::BITVECTOR_SREM
: return "bvsrem";
1015 case kind::BITVECTOR_SMOD
: return "bvsmod";
1016 case kind::BITVECTOR_SHL
: return "bvshl";
1017 case kind::BITVECTOR_LSHR
: return "bvlshr";
1018 case kind::BITVECTOR_ASHR
: return "bvashr";
1019 case kind::BITVECTOR_ULT
: return "bvult";
1020 case kind::BITVECTOR_ULE
: return "bvule";
1021 case kind::BITVECTOR_UGT
: return "bvugt";
1022 case kind::BITVECTOR_UGE
: return "bvuge";
1023 case kind::BITVECTOR_SLT
: return "bvslt";
1024 case kind::BITVECTOR_SLE
: return "bvsle";
1025 case kind::BITVECTOR_SGT
: return "bvsgt";
1026 case kind::BITVECTOR_SGE
: return "bvsge";
1027 case kind::BITVECTOR_TO_NAT
: return "bv2nat";
1028 case kind::BITVECTOR_REDOR
: return "bvredor";
1029 case kind::BITVECTOR_REDAND
: return "bvredand";
1031 case kind::BITVECTOR_EXTRACT
: return "extract";
1032 case kind::BITVECTOR_REPEAT
: return "repeat";
1033 case kind::BITVECTOR_ZERO_EXTEND
: return "zero_extend";
1034 case kind::BITVECTOR_SIGN_EXTEND
: return "sign_extend";
1035 case kind::BITVECTOR_ROTATE_LEFT
: return "rotate_left";
1036 case kind::BITVECTOR_ROTATE_RIGHT
: return "rotate_right";
1037 case kind::INT_TO_BITVECTOR
: return "int2bv";
1038 case kind::BITVECTOR_BB_TERM
: return "bbT";
1041 case kind::APPLY_TESTER
: return "is";
1042 case kind::APPLY_UPDATER
: return "update";
1045 case kind::UNION
: return "union";
1046 case kind::INTERSECTION
: return "intersection";
1047 case kind::SETMINUS
: return "setminus";
1048 case kind::SUBSET
: return "subset";
1049 case kind::MEMBER
: return "member";
1050 case kind::SET_TYPE
: return "Set";
1051 case kind::SINGLETON
: return "singleton";
1052 case kind::INSERT
: return "insert";
1053 case kind::COMPLEMENT
: return "complement";
1054 case kind::CARD
: return "card";
1055 case kind::COMPREHENSION
: return "comprehension";
1056 case kind::CHOOSE
: return "choose";
1057 case kind::IS_SINGLETON
: return "is_singleton";
1058 case kind::JOIN
: return "join";
1059 case kind::PRODUCT
: return "product";
1060 case kind::TRANSPOSE
: return "transpose";
1061 case kind::TCLOSURE
: return "tclosure";
1062 case kind::IDEN
: return "iden";
1063 case kind::JOIN_IMAGE
: return "join_image";
1066 case kind::BAG_TYPE
: return "Bag";
1067 case kind::UNION_MAX
: return "union_max";
1068 case kind::UNION_DISJOINT
: return "union_disjoint";
1069 case kind::INTERSECTION_MIN
: return "intersection_min";
1070 case kind::DIFFERENCE_SUBTRACT
: return "difference_subtract";
1071 case kind::DIFFERENCE_REMOVE
: return "difference_remove";
1072 case kind::SUBBAG
: return "subbag";
1073 case kind::BAG_COUNT
: return "bag.count";
1074 case kind::DUPLICATE_REMOVAL
: return "duplicate_removal";
1075 case kind::MK_BAG
: return "bag";
1076 case kind::BAG_CARD
: return "bag.card";
1077 case kind::BAG_CHOOSE
: return "bag.choose";
1078 case kind::BAG_IS_SINGLETON
: return "bag.is_singleton";
1079 case kind::BAG_FROM_SET
: return "bag.from_set";
1080 case kind::BAG_TO_SET
: return "bag.to_set";
1083 case kind::FLOATINGPOINT_FP
: return "fp";
1084 case kind::FLOATINGPOINT_EQ
: return "fp.eq";
1085 case kind::FLOATINGPOINT_ABS
: return "fp.abs";
1086 case kind::FLOATINGPOINT_NEG
: return "fp.neg";
1087 case kind::FLOATINGPOINT_ADD
: return "fp.add";
1088 case kind::FLOATINGPOINT_SUB
: return "fp.sub";
1089 case kind::FLOATINGPOINT_MULT
: return "fp.mul";
1090 case kind::FLOATINGPOINT_DIV
: return "fp.div";
1091 case kind::FLOATINGPOINT_FMA
: return "fp.fma";
1092 case kind::FLOATINGPOINT_SQRT
: return "fp.sqrt";
1093 case kind::FLOATINGPOINT_REM
: return "fp.rem";
1094 case kind::FLOATINGPOINT_RTI
: return "fp.roundToIntegral";
1095 case kind::FLOATINGPOINT_MIN
: return "fp.min";
1096 case kind::FLOATINGPOINT_MAX
: return "fp.max";
1097 case kind::FLOATINGPOINT_MIN_TOTAL
: return "fp.min_total";
1098 case kind::FLOATINGPOINT_MAX_TOTAL
: return "fp.max_total";
1100 case kind::FLOATINGPOINT_LEQ
: return "fp.leq";
1101 case kind::FLOATINGPOINT_LT
: return "fp.lt";
1102 case kind::FLOATINGPOINT_GEQ
: return "fp.geq";
1103 case kind::FLOATINGPOINT_GT
: return "fp.gt";
1105 case kind::FLOATINGPOINT_ISN
: return "fp.isNormal";
1106 case kind::FLOATINGPOINT_ISSN
: return "fp.isSubnormal";
1107 case kind::FLOATINGPOINT_ISZ
: return "fp.isZero";
1108 case kind::FLOATINGPOINT_ISINF
: return "fp.isInfinite";
1109 case kind::FLOATINGPOINT_ISNAN
: return "fp.isNaN";
1110 case kind::FLOATINGPOINT_ISNEG
: return "fp.isNegative";
1111 case kind::FLOATINGPOINT_ISPOS
: return "fp.isPositive";
1113 case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
: return "to_fp";
1114 case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
: return "to_fp";
1115 case kind::FLOATINGPOINT_TO_FP_REAL
: return "to_fp";
1116 case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
: return "to_fp";
1117 case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
: return "to_fp_unsigned";
1118 case kind::FLOATINGPOINT_TO_FP_GENERIC
: return "to_fp_unsigned";
1119 case kind::FLOATINGPOINT_TO_UBV
: return "fp.to_ubv";
1120 case kind::FLOATINGPOINT_TO_UBV_TOTAL
: return "fp.to_ubv_total";
1121 case kind::FLOATINGPOINT_TO_SBV
: return "fp.to_sbv";
1122 case kind::FLOATINGPOINT_TO_SBV_TOTAL
: return "fp.to_sbv_total";
1123 case kind::FLOATINGPOINT_TO_REAL
: return "fp.to_real";
1124 case kind::FLOATINGPOINT_TO_REAL_TOTAL
: return "fp.to_real_total";
1126 case kind::FLOATINGPOINT_COMPONENT_NAN
: return "NAN";
1127 case kind::FLOATINGPOINT_COMPONENT_INF
: return "INF";
1128 case kind::FLOATINGPOINT_COMPONENT_ZERO
: return "ZERO";
1129 case kind::FLOATINGPOINT_COMPONENT_SIGN
: return "SIGN";
1130 case kind::FLOATINGPOINT_COMPONENT_EXPONENT
: return "EXPONENT";
1131 case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND
: return "SIGNIFICAND";
1132 case kind::ROUNDINGMODE_BITBLAST
:
1133 return "RMBITBLAST";
1136 case kind::STRING_CONCAT
: return "str.++";
1137 case kind::STRING_LENGTH
: return "str.len";
1138 case kind::STRING_SUBSTR
: return "str.substr" ;
1139 case kind::STRING_UPDATE
: return "str.update";
1140 case kind::STRING_CONTAINS
: return "str.contains";
1141 case kind::STRING_CHARAT
: return "str.at" ;
1142 case kind::STRING_INDEXOF
: return "str.indexof";
1143 case kind::STRING_INDEXOF_RE
: return "str.indexof_re";
1144 case kind::STRING_REPLACE
: return "str.replace";
1145 case kind::STRING_REPLACE_ALL
: return "str.replace_all";
1146 case kind::STRING_REPLACE_RE
: return "str.replace_re";
1147 case kind::STRING_REPLACE_RE_ALL
: return "str.replace_re_all";
1148 case kind::STRING_TOLOWER
: return "str.tolower";
1149 case kind::STRING_TOUPPER
: return "str.toupper";
1150 case kind::STRING_REV
: return "str.rev";
1151 case kind::STRING_PREFIX
: return "str.prefixof" ;
1152 case kind::STRING_SUFFIX
: return "str.suffixof" ;
1153 case kind::STRING_LEQ
: return "str.<=";
1154 case kind::STRING_LT
: return "str.<";
1155 case kind::STRING_FROM_CODE
: return "str.from_code";
1156 case kind::STRING_TO_CODE
: return "str.to_code";
1157 case kind::STRING_ITOS
: return "str.from_int";
1158 case kind::STRING_STOI
: return "str.to_int";
1159 case kind::STRING_IN_REGEXP
: return "str.in_re";
1160 case kind::STRING_TO_REGEXP
: return "str.to_re";
1161 case kind::REGEXP_EMPTY
: return "re.none";
1162 case kind::REGEXP_SIGMA
: return "re.allchar";
1163 case kind::REGEXP_CONCAT
: return "re.++";
1164 case kind::REGEXP_UNION
: return "re.union";
1165 case kind::REGEXP_INTER
: return "re.inter";
1166 case kind::REGEXP_STAR
: return "re.*";
1167 case kind::REGEXP_PLUS
: return "re.+";
1168 case kind::REGEXP_OPT
: return "re.opt";
1169 case kind::REGEXP_RANGE
: return "re.range";
1170 case kind::REGEXP_REPEAT
: return "re.^";
1171 case kind::REGEXP_LOOP
: return "re.loop";
1172 case kind::REGEXP_COMPLEMENT
: return "re.comp";
1173 case kind::REGEXP_DIFF
: return "re.diff";
1174 case kind::SEQUENCE_TYPE
: return "Seq";
1175 case kind::SEQ_UNIT
: return "seq.unit";
1176 case kind::SEQ_NTH
: return "seq.nth";
1179 case kind::SEP_STAR
: return "sep";
1180 case kind::SEP_PTO
: return "pto";
1181 case kind::SEP_WAND
: return "wand";
1182 case kind::SEP_EMP
: return "emp";
1185 case kind::FORALL
: return "forall";
1186 case kind::EXISTS
: return "exists";
1189 ; /* fall through */
1192 // fall back on however the kind prints itself; this probably
1193 // won't be SMT-LIB v2 compliant, but it will be clear from the
1194 // output that support for the kind needs to be added here.
1195 // no SMT way to print these
1196 return kind::kindToString(k
);
1199 void Smt2Printer::toStreamType(std::ostream
& out
, TypeNode tn
) const
1201 // we currently must call TypeNode::toStream here.
1202 tn
.toStream(out
, language::output::LANG_SMTLIB_V2_6
);
1206 static bool tryToStream(std::ostream
& out
, const Command
* c
);
1208 static bool tryToStream(std::ostream
& out
, const Command
* c
, Variant v
);
1210 static std::string
quoteSymbol(TNode n
) {
1211 std::stringstream ss
;
1213 return cvc5::quoteSymbol(ss
.str());
1217 static bool tryToStream(std::ostream
& out
, const CommandStatus
* s
, Variant v
);
1219 void Smt2Printer::toStream(std::ostream
& out
, const CommandStatus
* s
) const
1221 if (tryToStream
<CommandSuccess
>(out
, s
, d_variant
) ||
1222 tryToStream
<CommandFailure
>(out
, s
, d_variant
) ||
1223 tryToStream
<CommandRecoverableFailure
>(out
, s
, d_variant
) ||
1224 tryToStream
<CommandUnsupported
>(out
, s
, d_variant
) ||
1225 tryToStream
<CommandInterrupted
>(out
, s
, d_variant
)) {
1229 out
<< "ERROR: don't know how to print a CommandStatus of class: "
1230 << typeid(*s
).name() << endl
;
1232 }/* Smt2Printer::toStream(CommandStatus*) */
1234 void Smt2Printer::toStream(std::ostream
& out
, const UnsatCore
& core
) const
1236 out
<< "(" << std::endl
;
1237 if (core
.useNames())
1240 const std::vector
<std::string
>& cnames
= core
.getCoreNames();
1241 for (const std::string
& cn
: cnames
)
1243 out
<< cvc5::quoteSymbol(cn
) << std::endl
;
1248 // otherwise, use the formulas
1249 for (UnsatCore::const_iterator i
= core
.begin(); i
!= core
.end(); ++i
)
1255 }/* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
1257 void Smt2Printer::toStream(std::ostream
& out
, const smt::Model
& m
) const
1259 const theory::TheoryModel
* tm
= m
.getTheoryModel();
1260 //print the model comments
1261 std::stringstream c
;
1264 while( std::getline( c
, ln
) ){
1265 out
<< "; " << ln
<< std::endl
;
1269 // don't need to print approximations since they are built into choice
1270 // functions in the values of variables.
1271 this->Printer::toStream(out
, m
);
1273 //print the heap model, if it exists
1275 if (tm
->getHeapModel(h
, neq
))
1277 // description of the heap+what nil is equal to fully describes model
1278 out
<< "(heap" << endl
;
1281 out
<< ")" << std::endl
;
1285 void Smt2Printer::toStreamModelSort(std::ostream
& out
,
1286 const smt::Model
& m
,
1291 out
<< "ERROR: don't know how to print non uninterpreted sort in model: "
1295 const theory::TheoryModel
* tm
= m
.getTheoryModel();
1296 std::vector
<Node
> elements
= tm
->getDomainElements(tn
);
1297 // print the cardinality
1298 out
<< "; cardinality of " << tn
<< " is " << elements
.size() << endl
;
1299 if (options::modelUninterpPrint()
1300 == options::ModelUninterpPrintMode::DeclSortAndFun
)
1302 toStreamCmdDeclareType(out
, tn
);
1304 // print the representatives
1305 for (const Node
& trn
: elements
)
1309 if (options::modelUninterpPrint()
1310 == options::ModelUninterpPrintMode::DeclSortAndFun
1311 || options::modelUninterpPrint()
1312 == options::ModelUninterpPrintMode::DeclFun
)
1314 out
<< "(declare-fun " << quoteSymbol(trn
) << " () " << tn
<< ")"
1320 out
<< "; rep: " << trn
<< endl
;
1325 void Smt2Printer::toStreamModelTerm(std::ostream
& out
,
1326 const smt::Model
& m
,
1329 const theory::TheoryModel
* tm
= m
.getTheoryModel();
1330 // We get the value from the theory model directly, which notice
1331 // does not have to go through the standard SmtEngine::getValue interface.
1332 Node val
= tm
->getValue(n
);
1333 if (val
.getKind() == kind::LAMBDA
)
1335 TypeNode rangeType
= n
.getType().getRangeType();
1336 out
<< "(define-fun " << n
<< " " << val
[0] << " " << rangeType
<< " ";
1337 // call toStream and force its type to be proper
1338 toStreamCastToType(out
, val
[1], -1, rangeType
);
1343 out
<< "(define-fun " << n
<< " () " << n
.getType() << " ";
1344 // call toStream and force its type to be proper
1345 toStreamCastToType(out
, val
, -1, n
.getType());
1350 void Smt2Printer::toStreamCmdAssert(std::ostream
& out
, Node n
) const
1352 out
<< "(assert " << n
<< ')' << std::endl
;
1355 void Smt2Printer::toStreamCmdPush(std::ostream
& out
) const
1357 out
<< "(push 1)" << std::endl
;
1360 void Smt2Printer::toStreamCmdPop(std::ostream
& out
) const
1362 out
<< "(pop 1)" << std::endl
;
1365 void Smt2Printer::toStreamCmdCheckSat(std::ostream
& out
, Node n
) const
1369 toStreamCmdPush(out
);
1371 toStreamCmdAssert(out
, n
);
1373 toStreamCmdCheckSat(out
);
1375 toStreamCmdPop(out
);
1379 out
<< "(check-sat)";
1384 void Smt2Printer::toStreamCmdCheckSatAssuming(
1385 std::ostream
& out
, const std::vector
<Node
>& nodes
) const
1387 out
<< "(check-sat-assuming ( ";
1388 copy(nodes
.begin(), nodes
.end(), ostream_iterator
<Node
>(out
, " "));
1389 out
<< "))" << std::endl
;
1392 void Smt2Printer::toStreamCmdQuery(std::ostream
& out
, Node n
) const
1396 toStreamCmdCheckSatAssuming(out
, {n
});
1400 toStreamCmdCheckSat(out
);
1404 void Smt2Printer::toStreamCmdReset(std::ostream
& out
) const
1406 out
<< "(reset)" << std::endl
;
1409 void Smt2Printer::toStreamCmdResetAssertions(std::ostream
& out
) const
1411 out
<< "(reset-assertions)" << std::endl
;
1414 void Smt2Printer::toStreamCmdQuit(std::ostream
& out
) const
1416 out
<< "(exit)" << std::endl
;
1419 void Smt2Printer::toStreamCmdCommandSequence(
1420 std::ostream
& out
, const std::vector
<Command
*>& sequence
) const
1422 for (Command
* i
: sequence
)
1428 void Smt2Printer::toStreamCmdDeclarationSequence(
1429 std::ostream
& out
, const std::vector
<Command
*>& sequence
) const
1431 toStreamCmdCommandSequence(out
, sequence
);
1434 void Smt2Printer::toStreamCmdDeclareFunction(std::ostream
& out
,
1435 const std::string
& id
,
1436 TypeNode type
) const
1438 out
<< "(declare-fun " << cvc5::quoteSymbol(id
) << " (";
1439 if (type
.isFunction())
1441 const vector
<TypeNode
> argTypes
= type
.getArgTypes();
1442 if (argTypes
.size() > 0)
1444 copy(argTypes
.begin(),
1446 ostream_iterator
<TypeNode
>(out
, " "));
1447 out
<< argTypes
.back();
1449 type
= type
.getRangeType();
1452 out
<< ") " << type
<< ')' << std::endl
;
1455 void Smt2Printer::toStreamCmdDefineFunction(std::ostream
& out
,
1456 const std::string
& id
,
1457 const std::vector
<Node
>& formals
,
1461 out
<< "(define-fun " << id
<< " (";
1462 if (!formals
.empty())
1464 vector
<Node
>::const_iterator i
= formals
.cbegin();
1467 out
<< "(" << (*i
) << " " << (*i
).getType() << ")";
1469 if (i
!= formals
.cend())
1479 out
<< ") " << range
<< ' ' << formula
<< ')' << std::endl
;
1482 void Smt2Printer::toStreamCmdDefineFunctionRec(
1484 const std::vector
<Node
>& funcs
,
1485 const std::vector
<std::vector
<Node
>>& formals
,
1486 const std::vector
<Node
>& formulas
) const
1488 out
<< "(define-fun";
1489 if (funcs
.size() > 1)
1494 if (funcs
.size() > 1)
1498 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
1500 if (funcs
.size() > 1)
1508 out
<< funcs
[i
] << " (";
1509 // print its type signature
1510 vector
<Node
>::const_iterator itf
= formals
[i
].cbegin();
1511 while (itf
!= formals
[i
].cend())
1513 out
<< "(" << (*itf
) << " " << (*itf
).getType() << ")";
1515 if (itf
!= formals
[i
].cend())
1520 TypeNode type
= funcs
[i
].getType();
1521 if (type
.isFunction())
1523 type
= type
.getRangeType();
1525 out
<< ") " << type
;
1526 if (funcs
.size() > 1)
1531 if (funcs
.size() > 1)
1539 for (unsigned i
= 0, size
= formulas
.size(); i
< size
; i
++)
1547 if (funcs
.size() > 1)
1551 out
<< ")" << std::endl
;
1554 void Smt2Printer::toStreamCmdDeclareType(std::ostream
& out
,
1555 TypeNode type
) const
1557 Assert(type
.isSort() || type
.isSortConstructor());
1558 std::stringstream id
;
1560 size_t arity
= type
.isSortConstructor() ? type
.getSortConstructorArity() : 0;
1561 out
<< "(declare-sort " << cvc5::quoteSymbol(id
.str()) << " " << arity
<< ")"
1565 void Smt2Printer::toStreamCmdDefineType(std::ostream
& out
,
1566 const std::string
& id
,
1567 const std::vector
<TypeNode
>& params
,
1570 out
<< "(define-sort " << cvc5::quoteSymbol(id
) << " (";
1571 if (params
.size() > 0)
1574 params
.begin(), params
.end() - 1, ostream_iterator
<TypeNode
>(out
, " "));
1575 out
<< params
.back();
1577 out
<< ") " << t
<< ")" << std::endl
;
1580 void Smt2Printer::toStreamCmdSimplify(std::ostream
& out
, Node n
) const
1582 out
<< "(simplify " << n
<< ')' << std::endl
;
1585 void Smt2Printer::toStreamCmdGetValue(std::ostream
& out
,
1586 const std::vector
<Node
>& nodes
) const
1588 out
<< "(get-value ( ";
1589 copy(nodes
.begin(), nodes
.end(), ostream_iterator
<Node
>(out
, " "));
1590 out
<< "))" << std::endl
;
1593 void Smt2Printer::toStreamCmdGetModel(std::ostream
& out
) const
1595 out
<< "(get-model)" << std::endl
;
1598 void Smt2Printer::toStreamCmdGetAssignment(std::ostream
& out
) const
1600 out
<< "(get-assignment)" << std::endl
;
1603 void Smt2Printer::toStreamCmdGetAssertions(std::ostream
& out
) const
1605 out
<< "(get-assertions)" << std::endl
;
1608 void Smt2Printer::toStreamCmdGetProof(std::ostream
& out
) const
1610 out
<< "(get-proof)" << std::endl
;
1613 void Smt2Printer::toStreamCmdGetUnsatAssumptions(std::ostream
& out
) const
1615 out
<< "(get-unsat-assumptions)" << std::endl
;
1618 void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream
& out
) const
1620 out
<< "(get-unsat-core)" << std::endl
;
1623 void Smt2Printer::toStreamCmdSetBenchmarkStatus(std::ostream
& out
,
1624 Result::Sat status
) const
1626 out
<< "(set-info :status " << status
<< ')' << std::endl
;
1629 void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream
& out
,
1630 const std::string
& logic
) const
1632 out
<< "(set-logic " << logic
<< ')' << std::endl
;
1635 void Smt2Printer::toStreamCmdSetInfo(std::ostream
& out
,
1636 const std::string
& flag
,
1637 const std::string
& value
) const
1639 out
<< "(set-info :" << flag
<< ' ' << value
<< ')' << std::endl
;
1642 void Smt2Printer::toStreamCmdGetInfo(std::ostream
& out
,
1643 const std::string
& flag
) const
1645 out
<< "(get-info :" << flag
<< ')' << std::endl
;
1648 void Smt2Printer::toStreamCmdSetOption(std::ostream
& out
,
1649 const std::string
& flag
,
1650 const std::string
& value
) const
1652 out
<< "(set-option :" << flag
<< ' ' << value
<< ')' << std::endl
;
1655 void Smt2Printer::toStreamCmdGetOption(std::ostream
& out
,
1656 const std::string
& flag
) const
1658 out
<< "(get-option :" << flag
<< ')' << std::endl
;
1661 void Smt2Printer::toStream(std::ostream
& out
, const DType
& dt
) const
1663 for (size_t i
= 0, ncons
= dt
.getNumConstructors(); i
< ncons
; i
++)
1665 const DTypeConstructor
& cons
= dt
[i
];
1670 out
<< "(" << cvc5::quoteSymbol(cons
.getName());
1671 for (size_t j
= 0, nargs
= cons
.getNumArgs(); j
< nargs
; j
++)
1673 const DTypeSelector
& arg
= cons
[j
];
1674 out
<< " (" << arg
.getSelector() << " " << arg
.getRangeType() << ")";
1680 void Smt2Printer::toStreamCmdDatatypeDeclaration(
1681 std::ostream
& out
, const std::vector
<TypeNode
>& datatypes
) const
1683 Assert(!datatypes
.empty());
1684 Assert(datatypes
[0].isDatatype());
1685 const DType
& d0
= datatypes
[0].getDType();
1688 // not necessary to print tuples
1689 Assert(datatypes
.size() == 1);
1693 if (d0
.isCodatatype())
1699 for (const TypeNode
& t
: datatypes
)
1701 Assert(t
.isDatatype());
1702 const DType
& d
= t
.getDType();
1703 out
<< "(" << cvc5::quoteSymbol(d
.getName());
1704 out
<< " " << d
.getNumParameters() << ")";
1707 for (const TypeNode
& t
: datatypes
)
1709 Assert(t
.isDatatype());
1710 const DType
& d
= t
.getDType();
1711 if (d
.isParametric())
1714 for (unsigned p
= 0, nparam
= d
.getNumParameters(); p
< nparam
; p
++)
1716 out
<< (p
> 0 ? " " : "") << d
.getParameter(p
);
1723 if (d
.isParametric())
1729 out
<< ")" << std::endl
;
1732 void Smt2Printer::toStreamCmdComment(std::ostream
& out
,
1733 const std::string
& comment
) const
1735 std::string s
= comment
;
1737 while ((pos
= s
.find_first_of('"', pos
)) != string::npos
)
1739 s
.replace(pos
, 1, "\"\"");
1742 out
<< "(set-info :notes \"" << s
<< "\")" << std::endl
;
1745 void Smt2Printer::toStreamCmdDeclareHeap(std::ostream
& out
,
1747 TypeNode dataType
) const
1749 out
<< "(declare-heap (" << locType
<< " " << dataType
<< "))" << std::endl
;
1752 void Smt2Printer::toStreamCmdEmpty(std::ostream
& out
,
1753 const std::string
& name
) const
1758 void Smt2Printer::toStreamCmdEcho(std::ostream
& out
,
1759 const std::string
& output
) const
1761 std::string s
= output
;
1762 // escape all double-quotes
1764 while ((pos
= s
.find('"', pos
)) != string::npos
)
1766 s
.replace(pos
, 1, "\"\"");
1769 out
<< "(echo \"" << s
<< "\")" << std::endl
;
1773 --------------------------------------------------------------------------
1774 Handling SyGuS commands
1775 --------------------------------------------------------------------------
1778 static void toStreamSygusGrammar(std::ostream
& out
, const TypeNode
& t
)
1780 if (!t
.isNull() && t
.isDatatype() && t
.getDType().isSygus())
1782 std::stringstream types_predecl
, types_list
;
1783 std::set
<TypeNode
> grammarTypes
;
1784 std::list
<TypeNode
> typesToPrint
;
1785 grammarTypes
.insert(t
);
1786 typesToPrint
.push_back(t
);
1787 NodeManager
* nm
= NodeManager::currentNM();
1788 // for each datatype in grammar
1791 // constructors in order
1794 TypeNode curr
= typesToPrint
.front();
1795 typesToPrint
.pop_front();
1796 Assert(curr
.isDatatype() && curr
.getDType().isSygus());
1797 const DType
& dt
= curr
.getDType();
1798 types_list
<< '(' << dt
.getName() << ' ' << dt
.getSygusType() << " (";
1799 types_predecl
<< '(' << dt
.getName() << ' ' << dt
.getSygusType() << ") ";
1800 if (dt
.getSygusAllowConst())
1802 types_list
<< "(Constant " << dt
.getSygusType() << ") ";
1804 for (size_t i
= 0, ncons
= dt
.getNumConstructors(); i
< ncons
; i
++)
1806 const DTypeConstructor
& cons
= dt
[i
];
1807 // make a sygus term
1808 std::vector
<Node
> cchildren
;
1809 cchildren
.push_back(cons
.getConstructor());
1810 for (size_t j
= 0, nargs
= cons
.getNumArgs(); j
< nargs
; j
++)
1812 TypeNode argType
= cons
[j
].getRangeType();
1813 std::stringstream ss
;
1815 Node bv
= nm
->mkBoundVar(ss
.str(), argType
);
1816 cchildren
.push_back(bv
);
1817 // if fresh type, store it for later processing
1818 if (grammarTypes
.insert(argType
).second
)
1820 typesToPrint
.push_back(argType
);
1823 Node consToPrint
= nm
->mkNode(kind::APPLY_CONSTRUCTOR
, cchildren
);
1824 // now, print it using the conversion to builtin with external
1825 types_list
<< theory::datatypes::utils::sygusToBuiltin(consToPrint
,
1829 types_list
<< "))\n";
1830 } while (!typesToPrint
.empty());
1832 out
<< "\n(" << types_predecl
.str() << ")\n(" << types_list
.str() << ')';
1836 void Smt2Printer::toStreamCmdSynthFun(std::ostream
& out
,
1838 const std::vector
<Node
>& vars
,
1840 TypeNode sygusType
) const
1842 std::stringstream sym
;
1844 out
<< '(' << (isInv
? "synth-inv " : "synth-fun ")
1845 << cvc5::quoteSymbol(sym
.str()) << ' ';
1849 // print variable list
1850 std::vector
<Node
>::const_iterator i
= vars
.cbegin(), i_end
= vars
.cend();
1851 out
<< '(' << *i
<< ' ' << i
->getType() << ')';
1855 out
<< " (" << *i
<< ' ' << i
->getType() << ')';
1860 // if not invariant-to-synthesize, print return type
1863 TypeNode ftn
= f
.getType();
1864 TypeNode range
= ftn
.isFunction() ? ftn
.getRangeType() : ftn
;
1865 out
<< ' ' << range
;
1868 // print grammar, if any
1869 if (!sygusType
.isNull())
1871 toStreamSygusGrammar(out
, sygusType
);
1873 out
<< ')' << std::endl
;
1876 void Smt2Printer::toStreamCmdDeclareVar(std::ostream
& out
,
1878 TypeNode type
) const
1880 out
<< "(declare-var " << var
<< ' ' << type
<< ')' << std::endl
;
1883 void Smt2Printer::toStreamCmdConstraint(std::ostream
& out
, Node n
) const
1885 out
<< "(constraint " << n
<< ')' << std::endl
;
1888 void Smt2Printer::toStreamCmdInvConstraint(
1889 std::ostream
& out
, Node inv
, Node pre
, Node trans
, Node post
) const
1891 out
<< "(inv-constraint " << inv
<< ' ' << pre
<< ' ' << trans
<< ' ' << post
1892 << ')' << std::endl
;
1895 void Smt2Printer::toStreamCmdCheckSynth(std::ostream
& out
) const
1897 out
<< "(check-synth)" << std::endl
;
1900 void Smt2Printer::toStreamCmdGetAbduct(std::ostream
& out
,
1901 const std::string
& name
,
1903 TypeNode sygusType
) const
1905 out
<< "(get-abduct ";
1909 // print grammar, if any
1910 if (!sygusType
.isNull())
1912 toStreamSygusGrammar(out
, sygusType
);
1914 out
<< ')' << std::endl
;
1918 --------------------------------------------------------------------------
1919 End of Handling SyGuS commands
1920 --------------------------------------------------------------------------
1924 static bool tryToStream(std::ostream
& out
, const Command
* c
)
1926 if(typeid(*c
) == typeid(T
)) {
1927 toStream(out
, dynamic_cast<const T
*>(c
));
1934 static bool tryToStream(std::ostream
& out
, const Command
* c
, Variant v
)
1936 if(typeid(*c
) == typeid(T
)) {
1937 toStream(out
, dynamic_cast<const T
*>(c
), v
);
1943 static void toStream(std::ostream
& out
, const CommandSuccess
* s
, Variant v
)
1945 if(Command::printsuccess::getPrintSuccess(out
)) {
1946 out
<< "success" << endl
;
1950 static void toStream(std::ostream
& out
, const CommandInterrupted
* s
, Variant v
)
1952 out
<< "interrupted" << endl
;
1955 static void toStream(std::ostream
& out
, const CommandUnsupported
* s
, Variant v
)
1957 #ifdef CVC5_COMPETITION_MODE
1958 // if in competition mode, lie and say we're ok
1959 // (we have nothing to lose by saying success, and everything to lose
1960 // if we say "unsupported")
1961 out
<< "success" << endl
;
1962 #else /* CVC5_COMPETITION_MODE */
1963 out
<< "unsupported" << endl
;
1964 #endif /* CVC5_COMPETITION_MODE */
1967 static void errorToStream(std::ostream
& out
, std::string message
, Variant v
) {
1968 // escape all double-quotes
1970 while((pos
= message
.find('"', pos
)) != string::npos
) {
1971 message
.replace(pos
, 1, "\"\"");
1974 out
<< "(error \"" << message
<< "\")" << endl
;
1977 static void toStream(std::ostream
& out
, const CommandFailure
* s
, Variant v
) {
1978 errorToStream(out
, s
->getMessage(), v
);
1981 static void toStream(std::ostream
& out
, const CommandRecoverableFailure
* s
,
1983 errorToStream(out
, s
->getMessage(), v
);
1987 static bool tryToStream(std::ostream
& out
, const CommandStatus
* s
, Variant v
)
1989 if(typeid(*s
) == typeid(T
)) {
1990 toStream(out
, dynamic_cast<const T
*>(s
), v
);
1997 } // namespace printer