1 /********************* */
2 /*! \file smt2_printer.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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
12 ** \brief The pretty-printer interface for the SMT2 output language
14 ** The pretty-printer interface for the SMT2 output language.
17 #include "printer/smt2/smt2_printer.h"
24 #include "expr/node_manager_attributes.h"
25 #include "options/language.h"
26 #include "options/smt_options.h"
27 #include "printer/dagification_visitor.h"
28 #include "smt/smt_engine.h"
29 #include "smt_util/boolean_simplification.h"
30 #include "smt_util/node_visitor.h"
31 #include "theory/arrays/theory_arrays_rewriter.h"
32 #include "theory/quantifiers/quantifiers_attributes.h"
33 #include "theory/substitutions.h"
34 #include "theory/theory_model.h"
35 #include "util/smt2_quote_string.h"
43 static OutputLanguage
variantToLanguage(Variant v
);
45 static string
smtKindString(Kind k
, Variant v
);
47 /** returns whether the variant is smt-lib 2.6 or greater */
48 bool isVariant_2_6(Variant v
)
50 return v
== smt2_6_variant
|| v
== smt2_6_1_variant
;
53 static void printBvParameterizedOp(std::ostream
& out
, TNode n
);
54 static void printFpParameterizedOp(std::ostream
& out
, TNode n
);
56 static void toStreamRational(std::ostream
& out
,
60 void Smt2Printer::toStream(
61 std::ostream
& out
, TNode n
, int toDepth
, bool types
, size_t dag
) const
64 DagificationVisitor
dv(dag
);
65 NodeVisitor
<DagificationVisitor
> visitor
;
67 const theory::SubstitutionMap
& lets
= dv
.getLets();
69 theory::SubstitutionMap::const_iterator i
= lets
.begin();
70 theory::SubstitutionMap::const_iterator i_end
= lets
.end();
71 for(; i
!= i_end
; ++ i
) {
73 toStream(out
, (*i
).second
, toDepth
, types
, TypeNode::null());
75 toStream(out
, (*i
).first
, toDepth
, types
, TypeNode::null());
79 Node body
= dv
.getDagifiedBody();
80 toStream(out
, body
, toDepth
, types
, TypeNode::null());
82 theory::SubstitutionMap::const_iterator i
= lets
.begin();
83 theory::SubstitutionMap::const_iterator i_end
= lets
.end();
84 for(; i
!= i_end
; ++ i
) {
89 toStream(out
, n
, toDepth
, types
, TypeNode::null());
93 static std::string
maybeQuoteSymbol(const std::string
& s
) {
94 // this is the set of SMT-LIBv2 permitted characters in "simple" (non-quoted) symbols
95 if(s
.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") != string::npos
) {
98 ss
<< '|' << s
<< '|';
104 static bool stringifyRegexp(Node n
, stringstream
& ss
) {
105 if(n
.getKind() == kind::STRING_TO_REGEXP
) {
106 ss
<< n
[0].getConst
<String
>().toString(true);
107 } else if(n
.getKind() == kind::REGEXP_CONCAT
) {
108 for(unsigned i
= 0; i
< n
.getNumChildren(); ++i
) {
109 if(!stringifyRegexp(n
[i
], ss
)) {
119 // force_nt is the type that n must have
120 void Smt2Printer::toStream(std::ostream
& out
,
124 TypeNode force_nt
) const
127 if(n
.getKind() == kind::NULL_EXPR
) {
133 if(n
.getMetaKind() == kind::metakind::CONSTANT
) {
134 switch(n
.getKind()) {
135 case kind::TYPE_CONSTANT
:
136 switch(n
.getConst
<TypeConstant
>()) {
137 case BOOLEAN_TYPE
: out
<< "Bool"; break;
138 case REAL_TYPE
: out
<< "Real"; break;
139 case INTEGER_TYPE
: out
<< "Int"; break;
140 case STRING_TYPE
: out
<< "String"; break;
141 case ROUNDINGMODE_TYPE
: out
<< "RoundingMode"; break;
143 // fall back on whatever operator<< does on underlying type; we
144 // might luck out and be SMT-LIB v2 compliant
145 kind::metakind::NodeValueConstPrinter::toStream(out
, n
);
148 case kind::BITVECTOR_TYPE
:
149 if(d_variant
== sygus_variant
){
150 out
<< "(BitVec " << n
.getConst
<BitVectorSize
>().size
<< ")";
152 out
<< "(_ BitVec " << n
.getConst
<BitVectorSize
>().size
<< ")";
155 case kind::FLOATINGPOINT_TYPE
:
156 out
<< "(_ FloatingPoint "
157 << n
.getConst
<FloatingPointSize
>().exponent() << " "
158 << n
.getConst
<FloatingPointSize
>().significand()
161 case kind::CONST_BITVECTOR
: {
162 const BitVector
& bv
= n
.getConst
<BitVector
>();
163 const Integer
& x
= bv
.getValue();
164 unsigned n
= bv
.getSize();
165 if(d_variant
== sygus_variant
){
166 out
<< "#b" << bv
.toString();
169 out
<< "bv" << x
<<" " << n
;
176 // out << (x.testBit(n) ? '1' : '0');
180 case kind::CONST_FLOATINGPOINT
:
181 out
<< n
.getConst
<FloatingPoint
>();
183 case kind::CONST_ROUNDINGMODE
:
184 switch (n
.getConst
<RoundingMode
>()) {
185 case roundNearestTiesToEven
: out
<< "roundNearestTiesToEven"; break;
186 case roundNearestTiesToAway
: out
<< "roundNearestTiesToAway"; break;
187 case roundTowardPositive
: out
<< "roundTowardPositive"; break;
188 case roundTowardNegative
: out
<< "roundTowardNegative"; break;
189 case roundTowardZero
: out
<< "roundTowardZero"; break;
191 Unreachable("Invalid value of rounding mode constant (%d)",n
.getConst
<RoundingMode
>());
194 case kind::CONST_BOOLEAN
:
195 // the default would print "1" or "0" for bool, that's not correct
197 out
<< (n
.getConst
<bool>() ? "true" : "false");
200 out
<< smtKindString(n
.getConst
<Kind
>(), d_variant
);
203 out
<< smtKindString(n
.getConst
<Chain
>().getOperator(), d_variant
);
205 case kind::CONST_RATIONAL
: {
206 const Rational
& r
= n
.getConst
<Rational
>();
207 if(d_variant
== sygus_variant
){
211 toStreamRational(out
, r
, !force_nt
.isNull() && !force_nt
.isInteger());
214 toStreamRational(out
, r
, !force_nt
.isNull() && !force_nt
.isInteger());
216 // Rational r = n.getConst<Rational>();
218 // if(r.isIntegral()) {
219 // out << "(- " << -r << ')';
221 // out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
224 // if(r.isIntegral()) {
227 // out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';
233 case kind::CONST_STRING
: {
234 //const std::vector<unsigned int>& s = n.getConst<String>().getVec();
235 std::string s
= n
.getConst
<String
>().toString(true);
237 for(size_t i
= 0; i
< s
.size(); ++i
) {
238 //char c = String::convertUnsignedIntToChar(s[i]);
241 if(d_variant
== smt2_0_variant
) {
254 case kind::STORE_ALL
: {
255 ArrayStoreAll asa
= n
.getConst
<ArrayStoreAll
>();
256 out
<< "((as const " << asa
.getType() << ") " << asa
.getExpr() << ")";
260 case kind::DATATYPE_TYPE
:
262 const Datatype
& dt
= (NodeManager::currentNM()->getDatatypeForIndex(
263 n
.getConst
<DatatypeIndexConstant
>().getIndex()));
266 unsigned int n
= dt
[0].getNumArgs();
274 for (unsigned int i
= 0; i
< n
; i
++)
276 out
<< " " << dt
[0][i
].getRangeType();
283 out
<< maybeQuoteSymbol(dt
.getName());
288 case kind::UNINTERPRETED_CONSTANT
: {
289 const UninterpretedConstant
& uc
= n
.getConst
<UninterpretedConstant
>();
295 out
<< "(as emptyset " << n
.getConst
<EmptySet
>().getType() << ")";
299 // fall back on whatever operator<< does on underlying type; we
300 // might luck out and be SMT-LIB v2 compliant
301 kind::metakind::NodeValueConstPrinter::toStream(out
, n
);
307 if(n
.getKind() == kind::SORT_TYPE
) {
309 if(n
.getNumChildren() != 0) {
312 if(n
.getAttribute(expr::VarNameAttr(), name
)) {
313 out
<< maybeQuoteSymbol(name
);
315 if(n
.getNumChildren() != 0) {
316 for(unsigned i
= 0; i
< n
.getNumChildren(); ++i
) {
318 toStream(out
, n
[i
], toDepth
, types
, TypeNode::null());
325 if (!force_nt
.isNull())
327 if (n
.getType() != force_nt
)
329 if (force_nt
.isReal())
331 out
<< "(" << smtKindString(force_nt
.isInteger() ? kind::TO_INTEGER
335 toStream(out
, n
, toDepth
, types
, TypeNode::null());
340 Node nn
= NodeManager::currentNM()->mkNode(
341 kind::APPLY_TYPE_ASCRIPTION
,
342 NodeManager::currentNM()->mkConst(
343 AscriptionType(force_nt
.toType())),
345 toStream(out
, nn
, toDepth
, types
, TypeNode::null());
355 if (n
.getAttribute(expr::VarNameAttr(), s
))
357 out
<< maybeQuoteSymbol(s
);
361 if (n
.getKind() == kind::VARIABLE
)
367 out
<< n
.getKind() << '_';
373 // print the whole type, but not *its* type
375 n
.getType().toStream(out
, language::output::LANG_SMTLIB_V2_5
);
381 bool stillNeedToPrintParams
= true;
382 bool forceBinary
= false; // force N-ary to binary when outputing children
383 bool parametricTypeChildren
= false; // parametric operators that are (op t1 ... tn) where t1...tn must have same type
384 bool typeChildren
= false; // operators (op t1...tn) where at least one of t1...tn may require a type cast e.g. Int -> Real
386 if(n
.getNumChildren() != 0 &&
387 n
.getKind() != kind::INST_PATTERN_LIST
&&
388 n
.getKind() != kind::APPLY_TYPE_ASCRIPTION
) {
391 switch(Kind k
= n
.getKind()) {
393 case kind::APPLY
: break;
396 out
<< smtKindString(k
, d_variant
) << " ";
397 parametricTypeChildren
= true;
399 case kind::CHAIN
: break;
400 case kind::FUNCTION_TYPE
:
405 toStream(out
, nc
, toDepth
, types
, TypeNode::null());
409 case kind::SEXPR
: break;
418 out
<< smtKindString(k
, d_variant
) << " ";
422 case kind::APPLY_UF
: typeChildren
= true; break;
424 case kind::HO_APPLY
: break;
426 out
<< smtKindString(k
, d_variant
) << " ";
432 case kind::NONLINEAR_MULT
:
433 case kind::EXPONENTIAL
:
439 case kind::COTANGENT
:
441 case kind::ARCCOSINE
:
442 case kind::ARCTANGENT
:
443 case kind::ARCCOSECANT
:
444 case kind::ARCSECANT
:
445 case kind::ARCCOTANGENT
:
454 case kind::DIVISION_TOTAL
:
455 case kind::INTS_DIVISION
:
456 case kind::INTS_DIVISION_TOTAL
:
457 case kind::INTS_MODULUS
:
458 case kind::INTS_MODULUS_TOTAL
:
460 case kind::IS_INTEGER
:
461 case kind::TO_INTEGER
:
464 parametricTypeChildren
= true;
465 out
<< smtKindString(k
, d_variant
) << " ";
468 case kind::DIVISIBLE
:
469 out
<< "(_ divisible " << n
.getOperator().getConst
<Divisible
>().k
<< ")";
470 stillNeedToPrintParams
= false;
475 case kind::STORE
: typeChildren
= true;
476 case kind::PARTIAL_SELECT_0
:
477 case kind::PARTIAL_SELECT_1
:
478 case kind::ARRAY_TYPE
:
479 out
<< smtKindString(k
, d_variant
) << " ";
483 case kind::STRING_CONCAT
:
484 if(d_variant
== z3str_variant
) {
486 for(unsigned i
= 0; i
< n
.getNumChildren(); ++i
) {
487 toStream(out
, n
[i
], -1, types
, TypeNode::null());
488 if(i
+ 1 < n
.getNumChildren()) {
491 if(i
+ 2 < n
.getNumChildren()) {
495 for(unsigned i
= 0; i
< n
.getNumChildren() - 1; ++i
) {
502 case kind::STRING_IN_REGEXP
: {
504 if(d_variant
== z3str_variant
&& stringifyRegexp(n
[1], ss
)) {
506 toStream(out
, n
[0], -1, types
, TypeNode::null());
508 Node str
= NodeManager::currentNM()->mkConst(String(ss
.str()));
509 toStream(out
, str
, -1, types
, TypeNode::null());
513 out
<< smtKindString(k
, d_variant
) << " ";
516 case kind::STRING_LENGTH
:
517 case kind::STRING_SUBSTR
:
518 case kind::STRING_CHARAT
:
519 case kind::STRING_STRCTN
:
520 case kind::STRING_STRIDOF
:
521 case kind::STRING_STRREPL
:
522 case kind::STRING_PREFIX
:
523 case kind::STRING_SUFFIX
:
524 case kind::STRING_LEQ
:
525 case kind::STRING_LT
:
526 case kind::STRING_ITOS
:
527 case kind::STRING_STOI
:
528 case kind::STRING_CODE
:
529 case kind::STRING_TO_REGEXP
:
530 case kind::REGEXP_CONCAT
:
531 case kind::REGEXP_UNION
:
532 case kind::REGEXP_INTER
:
533 case kind::REGEXP_STAR
:
534 case kind::REGEXP_PLUS
:
535 case kind::REGEXP_OPT
:
536 case kind::REGEXP_RANGE
:
537 case kind::REGEXP_LOOP
:
538 case kind::REGEXP_EMPTY
:
539 case kind::REGEXP_SIGMA
: out
<< smtKindString(k
, d_variant
) << " "; break;
541 case kind::CARDINALITY_CONSTRAINT
: out
<< "fmf.card "; break;
542 case kind::CARDINALITY_VALUE
: out
<< "fmf.card.val "; break;
545 case kind::BITVECTOR_CONCAT
: out
<< "concat "; forceBinary
= true; break;
546 case kind::BITVECTOR_AND
: out
<< "bvand "; forceBinary
= true; break;
547 case kind::BITVECTOR_OR
: out
<< "bvor "; forceBinary
= true; break;
548 case kind::BITVECTOR_XOR
: out
<< "bvxor "; forceBinary
= true; break;
549 case kind::BITVECTOR_NOT
: out
<< "bvnot "; break;
550 case kind::BITVECTOR_NAND
: out
<< "bvnand "; break;
551 case kind::BITVECTOR_NOR
: out
<< "bvnor "; break;
552 case kind::BITVECTOR_XNOR
: out
<< "bvxnor "; break;
553 case kind::BITVECTOR_COMP
: out
<< "bvcomp "; break;
554 case kind::BITVECTOR_MULT
: out
<< "bvmul "; forceBinary
= true; break;
555 case kind::BITVECTOR_PLUS
: out
<< "bvadd "; forceBinary
= true; break;
556 case kind::BITVECTOR_SUB
: out
<< "bvsub "; break;
557 case kind::BITVECTOR_NEG
: out
<< "bvneg "; break;
558 case kind::BITVECTOR_UDIV
: out
<< "bvudiv "; break;
559 case kind::BITVECTOR_UDIV_TOTAL
: out
<< "bvudiv_total "; break;
560 case kind::BITVECTOR_UREM
: out
<< "bvurem "; break;
561 case kind::BITVECTOR_UREM_TOTAL
: out
<< "bvurem_total "; break;
562 case kind::BITVECTOR_SDIV
: out
<< "bvsdiv "; break;
563 case kind::BITVECTOR_SREM
: out
<< "bvsrem "; break;
564 case kind::BITVECTOR_SMOD
: out
<< "bvsmod "; break;
565 case kind::BITVECTOR_SHL
: out
<< "bvshl "; break;
566 case kind::BITVECTOR_LSHR
: out
<< "bvlshr "; break;
567 case kind::BITVECTOR_ASHR
: out
<< "bvashr "; break;
568 case kind::BITVECTOR_ULT
: out
<< "bvult "; break;
569 case kind::BITVECTOR_ULE
: out
<< "bvule "; break;
570 case kind::BITVECTOR_UGT
: out
<< "bvugt "; break;
571 case kind::BITVECTOR_UGE
: out
<< "bvuge "; break;
572 case kind::BITVECTOR_SLT
: out
<< "bvslt "; break;
573 case kind::BITVECTOR_SLE
: out
<< "bvsle "; break;
574 case kind::BITVECTOR_SGT
: out
<< "bvsgt "; break;
575 case kind::BITVECTOR_SGE
: out
<< "bvsge "; break;
576 case kind::BITVECTOR_TO_NAT
: out
<< "bv2nat "; break;
577 case kind::BITVECTOR_REDOR
: out
<< "bvredor "; break;
578 case kind::BITVECTOR_REDAND
: out
<< "bvredand "; break;
580 case kind::BITVECTOR_EXTRACT
:
581 case kind::BITVECTOR_REPEAT
:
582 case kind::BITVECTOR_ZERO_EXTEND
:
583 case kind::BITVECTOR_SIGN_EXTEND
:
584 case kind::BITVECTOR_ROTATE_LEFT
:
585 case kind::BITVECTOR_ROTATE_RIGHT
:
586 case kind::INT_TO_BITVECTOR
:
587 printBvParameterizedOp(out
, n
);
589 stillNeedToPrintParams
= false;
594 case kind::INTERSECTION
:
600 case kind::TRANSPOSE
:
602 parametricTypeChildren
= true;
603 out
<< smtKindString(k
, d_variant
) << " ";
605 case kind::MEMBER
: typeChildren
= true;
607 case kind::SINGLETON
:
608 case kind::COMPLEMENT
: out
<< smtKindString(k
, d_variant
) << " "; break;
609 case kind::UNIVERSE_SET
:out
<< "(as univset " << n
.getType() << ")";break;
612 case kind::FLOATINGPOINT_FP
:
613 case kind::FLOATINGPOINT_EQ
:
614 case kind::FLOATINGPOINT_ABS
:
615 case kind::FLOATINGPOINT_NEG
:
616 case kind::FLOATINGPOINT_PLUS
:
617 case kind::FLOATINGPOINT_SUB
:
618 case kind::FLOATINGPOINT_MULT
:
619 case kind::FLOATINGPOINT_DIV
:
620 case kind::FLOATINGPOINT_FMA
:
621 case kind::FLOATINGPOINT_SQRT
:
622 case kind::FLOATINGPOINT_REM
:
623 case kind::FLOATINGPOINT_RTI
:
624 case kind::FLOATINGPOINT_MIN
:
625 case kind::FLOATINGPOINT_MAX
:
626 case kind::FLOATINGPOINT_LEQ
:
627 case kind::FLOATINGPOINT_LT
:
628 case kind::FLOATINGPOINT_GEQ
:
629 case kind::FLOATINGPOINT_GT
:
630 case kind::FLOATINGPOINT_ISN
:
631 case kind::FLOATINGPOINT_ISSN
:
632 case kind::FLOATINGPOINT_ISZ
:
633 case kind::FLOATINGPOINT_ISINF
:
634 case kind::FLOATINGPOINT_ISNAN
:
635 case kind::FLOATINGPOINT_ISNEG
:
636 case kind::FLOATINGPOINT_ISPOS
:
637 case kind::FLOATINGPOINT_TO_REAL
:
638 out
<< smtKindString(k
, d_variant
) << ' ';
641 case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
642 case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
643 case kind::FLOATINGPOINT_TO_FP_REAL
:
644 case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
645 case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
646 case kind::FLOATINGPOINT_TO_FP_GENERIC
:
647 case kind::FLOATINGPOINT_TO_UBV
:
648 case kind::FLOATINGPOINT_TO_SBV
:
649 printFpParameterizedOp(out
, n
);
651 stillNeedToPrintParams
= false;
655 case kind::APPLY_TYPE_ASCRIPTION
: {
656 TypeNode t
= TypeNode::fromType(n
.getOperator().getConst
<AscriptionType
>().getType());
657 if(t
.getKind() == kind::TYPE_CONSTANT
&&
658 t
.getConst
<TypeConstant
>() == REAL_TYPE
&&
659 n
[0].getType().isInteger()) {
660 // Special case, in model output integer constants that should be
661 // Real-sorted are wrapped in a type ascription. Handle that here.
663 // Note: This is Tim making a guess about Morgan's Code.
664 Assert(n
[0].getKind() == kind::CONST_RATIONAL
);
665 toStreamRational(out
, n
[0].getConst
<Rational
>(), true);
667 //toStream(out, n[0], -1, false);
673 toStream(out
, n
[0], toDepth
< 0 ? toDepth
: toDepth
- 1, types
, TypeNode::null());
674 out
<< ' ' << (t
.isFunctionLike() ? t
.getRangeType() : t
) << ')';
679 case kind::APPLY_CONSTRUCTOR
:
682 const Datatype
& dt
= Datatype::datatypeOf(n
.getOperator().toExpr());
685 stillNeedToPrintParams
= false;
686 out
<< "mkTuple" << ( dt
[0].getNumArgs()==0 ? "" : " ");
690 case kind::APPLY_TESTER
:
691 case kind::APPLY_SELECTOR
:
692 case kind::APPLY_SELECTOR_TOTAL
:
693 case kind::PARAMETRIC_DATATYPE
: break;
699 case kind::SEP_WAND
: out
<< smtKindString(k
, d_variant
) << " "; break;
702 out
<< "(as sep.nil " << n
.getType() << ")";
708 if (k
== kind::FORALL
)
716 for (unsigned i
= 0; i
< 2; i
++)
719 if (i
== 0 && n
.getNumChildren() == 3)
724 if (n
.getNumChildren() == 3)
732 case kind::BOUND_VAR_LIST
:
733 // the left parenthesis is already printed (before the switch)
734 for (TNode::iterator i
= n
.begin(), iend
= n
.end(); i
!= iend
;)
737 toStream(out
, *i
, toDepth
< 0 ? toDepth
: toDepth
- 1, types
, 0);
739 out
<< (*i
).getType();
740 // The following code do stange things
741 // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
742 // false, language::output::LANG_SMTLIB_V2_5);
751 case kind::INST_PATTERN
: break;
752 case kind::INST_PATTERN_LIST
:
753 for (unsigned i
= 0; i
< n
.getNumChildren(); i
++)
755 if (n
[i
].getKind() == kind::INST_ATTRIBUTE
)
757 if (n
[i
][0].getAttribute(theory::FunDefAttribute()))
764 out
<< ":pattern " << n
[i
];
771 // fall back on however the kind prints itself; this probably
772 // won't be SMT-LIB v2 compliant, but it will be clear from the
773 // output that support for the kind needs to be added here.
774 out
<< n
.getKind() << ' ';
776 if( n
.getMetaKind() == kind::metakind::PARAMETERIZED
&&
777 stillNeedToPrintParams
) {
779 if( d_variant
==sygus_variant
&& n
.getKind()==kind::APPLY_CONSTRUCTOR
){
780 std::stringstream ss
;
781 toStream(ss
, n
.getOperator(), toDepth
< 0 ? toDepth
: toDepth
- 1, types
, TypeNode::null());
782 std::string tmp
= ss
.str();
784 if((pos
= tmp
.find("__Enum__", pos
)) != std::string::npos
){
785 tmp
.replace(pos
, 8, "::");
788 }else if( n
.getKind()==kind::APPLY_TESTER
){
789 unsigned cindex
= Datatype::indexOf(n
.getOperator().toExpr());
790 const Datatype
& dt
= Datatype::datatypeOf(n
.getOperator().toExpr());
791 if (isVariant_2_6(d_variant
))
794 toStream(out
, Node::fromExpr(dt
[cindex
].getConstructor()), toDepth
< 0 ? toDepth
: toDepth
- 1, types
, TypeNode::null());
798 toStream(out
, Node::fromExpr(dt
[cindex
].getConstructor()), toDepth
< 0 ? toDepth
: toDepth
- 1, types
, TypeNode::null());
801 toStream(out
, n
.getOperator(), toDepth
< 0 ? toDepth
: toDepth
- 1, types
, TypeNode::null());
806 if(n
.getNumChildren() > 0) {
812 // calculate the child type casts
813 std::map
< unsigned, TypeNode
> force_child_type
;
814 if( parametricTypeChildren
){
815 if( n
.getNumChildren()>1 ){
816 TypeNode force_ct
= n
[0].getType();
817 bool do_force
= false;
818 for(size_t i
= 1; i
< n
.getNumChildren(); ++i
) {
819 TypeNode ct
= n
[i
].getType();
821 force_ct
= TypeNode::leastCommonTypeNode( force_ct
, ct
);
826 for(size_t i
= 0; i
< n
.getNumChildren(); ++i
) {
827 force_child_type
[i
] = force_ct
;
831 // operators that may require type casting
832 }else if( typeChildren
){
833 if(n
.getKind()==kind::SELECT
){
834 TypeNode indexType
= TypeNode::leastCommonTypeNode( n
[0].getType().getArrayIndexType(), n
[1].getType() );
835 TypeNode elemType
= n
[0].getType().getArrayConstituentType();
836 force_child_type
[0] = NodeManager::currentNM()->mkArrayType( indexType
, elemType
);
837 force_child_type
[1] = indexType
;
838 }else if(n
.getKind()==kind::STORE
){
839 TypeNode indexType
= TypeNode::leastCommonTypeNode( n
[0].getType().getArrayIndexType(), n
[1].getType() );
840 TypeNode elemType
= TypeNode::leastCommonTypeNode( n
[0].getType().getArrayConstituentType(), n
[2].getType() );
841 force_child_type
[0] = NodeManager::currentNM()->mkArrayType( indexType
, elemType
);
842 force_child_type
[1] = indexType
;
843 force_child_type
[2] = elemType
;
844 }else if(n
.getKind()==kind::MEMBER
){
845 TypeNode elemType
= TypeNode::leastCommonTypeNode( n
[0].getType(), n
[1].getType().getSetElementType() );
846 force_child_type
[0] = elemType
;
847 force_child_type
[1] = NodeManager::currentNM()->mkSetType( elemType
);
849 // APPLY_UF, APPLY_CONSTRUCTOR, etc.
850 Assert( n
.hasOperator() );
851 TypeNode opt
= n
.getOperator().getType();
852 Assert( opt
.getNumChildren() == n
.getNumChildren() + 1 );
853 for(size_t i
= 0; i
< n
.getNumChildren(); ++i
) {
854 force_child_type
[i
] = opt
[i
];
859 for(size_t i
= 0, c
= 1; i
< n
.getNumChildren(); ) {
862 std::map
< unsigned, TypeNode
>::iterator itfc
= force_child_type
.find( i
);
863 if( itfc
!=force_child_type
.end() ){
864 toStream(out
, cn
, toDepth
< 0 ? toDepth
: toDepth
- c
, types
, itfc
->second
);
866 toStream(out
, cn
, toDepth
< 0 ? toDepth
: toDepth
- c
, types
, TypeNode::null());
871 if(++i
< n
.getNumChildren()) {
872 if(forceBinary
&& i
< n
.getNumChildren() - 1) {
873 // not going to work properly for parameterized kinds!
874 Assert(n
.getMetaKind() != kind::metakind::PARAMETERIZED
);
875 out
<< " (" << smtKindString(n
.getKind(), d_variant
) << ' ';
883 if(n
.getNumChildren() != 0) {
884 out
<< parens
.str() << ')';
886 }/* Smt2Printer::toStream(TNode) */
888 static string
smtKindString(Kind k
, Variant v
)
892 case kind::APPLY
: break;
893 case kind::EQUAL
: return "=";
894 case kind::DISTINCT
: return "distinct";
895 case kind::CHAIN
: break;
896 case kind::SEXPR
: break;
899 case kind::NOT
: return "not";
900 case kind::AND
: return "and";
901 case kind::IMPLIES
: return "=>";
902 case kind::OR
: return "or";
903 case kind::XOR
: return "xor";
904 case kind::ITE
: return "ite";
907 case kind::APPLY_UF
: break;
913 case kind::PLUS
: return "+";
915 case kind::NONLINEAR_MULT
: return "*";
916 case kind::EXPONENTIAL
: return "exp";
917 case kind::SINE
: return "sin";
918 case kind::COSINE
: return "cos";
919 case kind::TANGENT
: return "tan";
920 case kind::COSECANT
: return "csc";
921 case kind::SECANT
: return "sec";
922 case kind::COTANGENT
: return "cot";
923 case kind::ARCSINE
: return "arcsin";
924 case kind::ARCCOSINE
: return "arccos";
925 case kind::ARCTANGENT
: return "arctan";
926 case kind::ARCCOSECANT
: return "arccsc";
927 case kind::ARCSECANT
: return "arcsec";
928 case kind::ARCCOTANGENT
: return "arccot";
929 case kind::SQRT
: return "sqrt";
930 case kind::MINUS
: return "-";
931 case kind::UMINUS
: return "-";
932 case kind::LT
: return "<";
933 case kind::LEQ
: return "<=";
934 case kind::GT
: return ">";
935 case kind::GEQ
: return ">=";
937 case kind::DIVISION_TOTAL
: return "/";
938 case kind::INTS_DIVISION_TOTAL
:
939 case kind::INTS_DIVISION
: return "div";
940 case kind::INTS_MODULUS_TOTAL
:
941 case kind::INTS_MODULUS
: return "mod";
942 case kind::ABS
: return "abs";
943 case kind::IS_INTEGER
: return "is_int";
944 case kind::TO_INTEGER
: return "to_int";
945 case kind::TO_REAL
: return "to_real";
946 case kind::POW
: return "^";
949 case kind::SELECT
: return "select";
950 case kind::STORE
: return "store";
951 case kind::ARRAY_TYPE
: return "Array";
952 case kind::PARTIAL_SELECT_0
: return "partial_select_0";
953 case kind::PARTIAL_SELECT_1
: return "partial_select_1";
956 case kind::BITVECTOR_CONCAT
: return "concat";
957 case kind::BITVECTOR_AND
: return "bvand";
958 case kind::BITVECTOR_OR
: return "bvor";
959 case kind::BITVECTOR_XOR
: return "bvxor";
960 case kind::BITVECTOR_NOT
: return "bvnot";
961 case kind::BITVECTOR_NAND
: return "bvnand";
962 case kind::BITVECTOR_NOR
: return "bvnor";
963 case kind::BITVECTOR_XNOR
: return "bvxnor";
964 case kind::BITVECTOR_COMP
: return "bvcomp";
965 case kind::BITVECTOR_MULT
: return "bvmul";
966 case kind::BITVECTOR_PLUS
: return "bvadd";
967 case kind::BITVECTOR_SUB
: return "bvsub";
968 case kind::BITVECTOR_NEG
: return "bvneg";
969 case kind::BITVECTOR_UDIV_TOTAL
:
970 case kind::BITVECTOR_UDIV
: return "bvudiv";
971 case kind::BITVECTOR_UREM
: return "bvurem";
972 case kind::BITVECTOR_SDIV
: return "bvsdiv";
973 case kind::BITVECTOR_SREM
: return "bvsrem";
974 case kind::BITVECTOR_SMOD
: return "bvsmod";
975 case kind::BITVECTOR_SHL
: return "bvshl";
976 case kind::BITVECTOR_LSHR
: return "bvlshr";
977 case kind::BITVECTOR_ASHR
: return "bvashr";
978 case kind::BITVECTOR_ULT
: return "bvult";
979 case kind::BITVECTOR_ULE
: return "bvule";
980 case kind::BITVECTOR_UGT
: return "bvugt";
981 case kind::BITVECTOR_UGE
: return "bvuge";
982 case kind::BITVECTOR_SLT
: return "bvslt";
983 case kind::BITVECTOR_SLE
: return "bvsle";
984 case kind::BITVECTOR_SGT
: return "bvsgt";
985 case kind::BITVECTOR_SGE
: return "bvsge";
986 case kind::BITVECTOR_REDOR
: return "bvredor";
987 case kind::BITVECTOR_REDAND
: return "bvredand";
989 case kind::BITVECTOR_EXTRACT
: return "extract";
990 case kind::BITVECTOR_REPEAT
: return "repeat";
991 case kind::BITVECTOR_ZERO_EXTEND
: return "zero_extend";
992 case kind::BITVECTOR_SIGN_EXTEND
: return "sign_extend";
993 case kind::BITVECTOR_ROTATE_LEFT
: return "rotate_left";
994 case kind::BITVECTOR_ROTATE_RIGHT
: return "rotate_right";
996 case kind::UNION
: return "union";
997 case kind::INTERSECTION
: return "intersection";
998 case kind::SETMINUS
: return "setminus";
999 case kind::SUBSET
: return "subset";
1000 case kind::MEMBER
: return "member";
1001 case kind::SET_TYPE
: return "Set";
1002 case kind::SINGLETON
: return "singleton";
1003 case kind::INSERT
: return "insert";
1004 case kind::COMPLEMENT
: return "complement";
1005 case kind::CARD
: return "card";
1006 case kind::JOIN
: return "join";
1007 case kind::PRODUCT
: return "product";
1008 case kind::TRANSPOSE
: return "transpose";
1009 case kind::TCLOSURE
:
1013 case kind::FLOATINGPOINT_FP
: return "fp";
1014 case kind::FLOATINGPOINT_EQ
: return "fp.eq";
1015 case kind::FLOATINGPOINT_ABS
: return "fp.abs";
1016 case kind::FLOATINGPOINT_NEG
: return "fp.neg";
1017 case kind::FLOATINGPOINT_PLUS
: return "fp.add";
1018 case kind::FLOATINGPOINT_SUB
: return "fp.sub";
1019 case kind::FLOATINGPOINT_MULT
: return "fp.mul";
1020 case kind::FLOATINGPOINT_DIV
: return "fp.div";
1021 case kind::FLOATINGPOINT_FMA
: return "fp.fma";
1022 case kind::FLOATINGPOINT_SQRT
: return "fp.sqrt";
1023 case kind::FLOATINGPOINT_REM
: return "fp.rem";
1024 case kind::FLOATINGPOINT_RTI
: return "fp.roundToIntegral";
1025 case kind::FLOATINGPOINT_MIN
: return "fp.min";
1026 case kind::FLOATINGPOINT_MAX
: return "fp.max";
1027 case kind::FLOATINGPOINT_MIN_TOTAL
: return "fp.min_total";
1028 case kind::FLOATINGPOINT_MAX_TOTAL
: return "fp.max_total";
1030 case kind::FLOATINGPOINT_LEQ
: return "fp.leq";
1031 case kind::FLOATINGPOINT_LT
: return "fp.lt";
1032 case kind::FLOATINGPOINT_GEQ
: return "fp.geq";
1033 case kind::FLOATINGPOINT_GT
: return "fp.gt";
1035 case kind::FLOATINGPOINT_ISN
: return "fp.isNormal";
1036 case kind::FLOATINGPOINT_ISSN
: return "fp.isSubnormal";
1037 case kind::FLOATINGPOINT_ISZ
: return "fp.isZero";
1038 case kind::FLOATINGPOINT_ISINF
: return "fp.isInfinite";
1039 case kind::FLOATINGPOINT_ISNAN
: return "fp.isNaN";
1040 case kind::FLOATINGPOINT_ISNEG
: return "fp.isNegative";
1041 case kind::FLOATINGPOINT_ISPOS
: return "fp.isPositive";
1043 case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
: return "to_fp";
1044 case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
: return "to_fp";
1045 case kind::FLOATINGPOINT_TO_FP_REAL
: return "to_fp";
1046 case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
: return "to_fp";
1047 case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
: return "to_fp_unsigned";
1048 case kind::FLOATINGPOINT_TO_FP_GENERIC
: return "to_fp_unsigned";
1049 case kind::FLOATINGPOINT_TO_UBV
: return "fp.to_ubv";
1050 case kind::FLOATINGPOINT_TO_UBV_TOTAL
: return "fp.to_ubv_total";
1051 case kind::FLOATINGPOINT_TO_SBV
: return "fp.to_sbv";
1052 case kind::FLOATINGPOINT_TO_SBV_TOTAL
: return "fp.to_sbv_total";
1053 case kind::FLOATINGPOINT_TO_REAL
: return "fp.to_real";
1054 case kind::FLOATINGPOINT_TO_REAL_TOTAL
: return "fp.to_real_total";
1057 case kind::STRING_CONCAT
: return "str.++";
1058 case kind::STRING_LENGTH
: return v
== z3str_variant
? "Length" : "str.len";
1059 case kind::STRING_SUBSTR
: return "str.substr" ;
1060 case kind::STRING_STRCTN
: return "str.contains" ;
1061 case kind::STRING_CHARAT
: return "str.at" ;
1062 case kind::STRING_STRIDOF
: return "str.indexof" ;
1063 case kind::STRING_STRREPL
: return "str.replace" ;
1064 case kind::STRING_PREFIX
: return "str.prefixof" ;
1065 case kind::STRING_SUFFIX
: return "str.suffixof" ;
1066 case kind::STRING_LEQ
: return "str.<=";
1067 case kind::STRING_LT
: return "str.<";
1068 case kind::STRING_CODE
: return "str.code";
1069 case kind::STRING_ITOS
:
1070 return v
== smt2_6_1_variant
? "str.from-int" : "int.to.str";
1071 case kind::STRING_STOI
:
1072 return v
== smt2_6_1_variant
? "str.to-int" : "str.to.int";
1073 case kind::STRING_IN_REGEXP
:
1074 return v
== smt2_6_1_variant
? "str.in-re" : "str.in.re";
1075 case kind::STRING_TO_REGEXP
:
1076 return v
== smt2_6_1_variant
? "str.to-re" : "str.to.re";
1077 case kind::REGEXP_CONCAT
: return "re.++";
1078 case kind::REGEXP_UNION
: return "re.union";
1079 case kind::REGEXP_INTER
: return "re.inter";
1080 case kind::REGEXP_STAR
: return "re.*";
1081 case kind::REGEXP_PLUS
: return "re.+";
1082 case kind::REGEXP_OPT
: return "re.opt";
1083 case kind::REGEXP_RANGE
: return "re.range";
1084 case kind::REGEXP_LOOP
: return "re.loop";
1087 case kind::SEP_STAR
: return "sep";
1088 case kind::SEP_PTO
: return "pto";
1089 case kind::SEP_WAND
: return "wand";
1090 case kind::SEP_EMP
: return "emp";
1093 ; /* fall through */
1096 // no SMT way to print these
1097 return kind::kindToString(k
);
1100 static void printBvParameterizedOp(std::ostream
& out
, TNode n
)
1103 switch(n
.getKind()) {
1104 case kind::BITVECTOR_EXTRACT
: {
1105 BitVectorExtract p
= n
.getOperator().getConst
<BitVectorExtract
>();
1106 out
<< "extract " << p
.high
<< ' ' << p
.low
;
1109 case kind::BITVECTOR_REPEAT
:
1111 << n
.getOperator().getConst
<BitVectorRepeat
>().repeatAmount
;
1113 case kind::BITVECTOR_ZERO_EXTEND
:
1114 out
<< "zero_extend "
1115 << n
.getOperator().getConst
<BitVectorZeroExtend
>().zeroExtendAmount
;
1117 case kind::BITVECTOR_SIGN_EXTEND
:
1118 out
<< "sign_extend "
1119 << n
.getOperator().getConst
<BitVectorSignExtend
>().signExtendAmount
;
1121 case kind::BITVECTOR_ROTATE_LEFT
:
1122 out
<< "rotate_left "
1123 << n
.getOperator().getConst
<BitVectorRotateLeft
>().rotateLeftAmount
;
1125 case kind::BITVECTOR_ROTATE_RIGHT
:
1126 out
<< "rotate_right "
1127 << n
.getOperator().getConst
<BitVectorRotateRight
>().rotateRightAmount
;
1129 case kind::INT_TO_BITVECTOR
:
1131 << n
.getOperator().getConst
<IntToBitVector
>().size
;
1139 static void printFpParameterizedOp(std::ostream
& out
, TNode n
)
1142 switch(n
.getKind()) {
1143 case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
1144 //out << "to_fp_bv "
1146 << n
.getOperator().getConst
<FloatingPointToFPIEEEBitVector
>().t
.exponent() << ' '
1147 << n
.getOperator().getConst
<FloatingPointToFPIEEEBitVector
>().t
.significand();
1149 case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
1150 //out << "to_fp_fp "
1152 << n
.getOperator().getConst
<FloatingPointToFPFloatingPoint
>().t
.exponent() << ' '
1153 << n
.getOperator().getConst
<FloatingPointToFPFloatingPoint
>().t
.significand();
1155 case kind::FLOATINGPOINT_TO_FP_REAL
:
1156 //out << "to_fp_real "
1158 << n
.getOperator().getConst
<FloatingPointToFPReal
>().t
.exponent() << ' '
1159 << n
.getOperator().getConst
<FloatingPointToFPReal
>().t
.significand();
1161 case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
1162 //out << "to_fp_signed "
1164 << n
.getOperator().getConst
<FloatingPointToFPSignedBitVector
>().t
.exponent() << ' '
1165 << n
.getOperator().getConst
<FloatingPointToFPSignedBitVector
>().t
.significand();
1167 case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
1168 out
<< "to_fp_unsigned "
1169 << n
.getOperator().getConst
<FloatingPointToFPUnsignedBitVector
>().t
.exponent() << ' '
1170 << n
.getOperator().getConst
<FloatingPointToFPUnsignedBitVector
>().t
.significand();
1172 case kind::FLOATINGPOINT_TO_FP_GENERIC
:
1174 << n
.getOperator().getConst
<FloatingPointToFPGeneric
>().t
.exponent() << ' '
1175 << n
.getOperator().getConst
<FloatingPointToFPGeneric
>().t
.significand();
1177 case kind::FLOATINGPOINT_TO_UBV
:
1179 << n
.getOperator().getConst
<FloatingPointToUBV
>().bvs
.size
;
1181 case kind::FLOATINGPOINT_TO_SBV
:
1183 << n
.getOperator().getConst
<FloatingPointToSBV
>().bvs
.size
;
1185 case kind::FLOATINGPOINT_TO_UBV_TOTAL
:
1186 out
<< "fp.to_ubv_total "
1187 << n
.getOperator().getConst
<FloatingPointToUBVTotal
>().bvs
.size
;
1189 case kind::FLOATINGPOINT_TO_SBV_TOTAL
:
1190 out
<< "fp.to_sbv_total "
1191 << n
.getOperator().getConst
<FloatingPointToSBVTotal
>().bvs
.size
;
1200 static bool tryToStream(std::ostream
& out
, const Command
* c
);
1202 static bool tryToStream(std::ostream
& out
, const Command
* c
, Variant v
);
1204 void Smt2Printer::toStream(std::ostream
& out
,
1210 expr::ExprSetDepth::Scope
sdScope(out
, toDepth
);
1211 expr::ExprPrintTypes::Scope
ptScope(out
, types
);
1212 expr::ExprDag::Scope
dagScope(out
, dag
);
1214 if (tryToStream
<AssertCommand
>(out
, c
) || tryToStream
<PushCommand
>(out
, c
)
1215 || tryToStream
<PopCommand
>(out
, c
)
1216 || tryToStream
<CheckSatCommand
>(out
, c
)
1217 || tryToStream
<CheckSatAssumingCommand
>(out
, c
)
1218 || tryToStream
<QueryCommand
>(out
, c
, d_variant
)
1219 || tryToStream
<ResetCommand
>(out
, c
)
1220 || tryToStream
<ResetAssertionsCommand
>(out
, c
)
1221 || tryToStream
<QuitCommand
>(out
, c
)
1222 || tryToStream
<DeclarationSequence
>(out
, c
)
1223 || tryToStream
<CommandSequence
>(out
, c
)
1224 || tryToStream
<DeclareFunctionCommand
>(out
, c
)
1225 || tryToStream
<DeclareTypeCommand
>(out
, c
)
1226 || tryToStream
<DefineTypeCommand
>(out
, c
)
1227 || tryToStream
<DefineNamedFunctionCommand
>(out
, c
)
1228 || tryToStream
<DefineFunctionCommand
>(out
, c
)
1229 || tryToStream
<DefineFunctionRecCommand
>(out
, c
)
1230 || tryToStream
<SimplifyCommand
>(out
, c
)
1231 || tryToStream
<GetValueCommand
>(out
, c
)
1232 || tryToStream
<GetModelCommand
>(out
, c
)
1233 || tryToStream
<GetAssignmentCommand
>(out
, c
)
1234 || tryToStream
<GetAssertionsCommand
>(out
, c
)
1235 || tryToStream
<GetProofCommand
>(out
, c
)
1236 || tryToStream
<GetUnsatAssumptionsCommand
>(out
, c
)
1237 || tryToStream
<GetUnsatCoreCommand
>(out
, c
)
1238 || tryToStream
<SetBenchmarkStatusCommand
>(out
, c
, d_variant
)
1239 || tryToStream
<SetBenchmarkLogicCommand
>(out
, c
, d_variant
)
1240 || tryToStream
<SetInfoCommand
>(out
, c
, d_variant
)
1241 || tryToStream
<GetInfoCommand
>(out
, c
)
1242 || tryToStream
<SetOptionCommand
>(out
, c
)
1243 || tryToStream
<GetOptionCommand
>(out
, c
)
1244 || tryToStream
<DatatypeDeclarationCommand
>(out
, c
, d_variant
)
1245 || tryToStream
<CommentCommand
>(out
, c
, d_variant
)
1246 || tryToStream
<EmptyCommand
>(out
, c
)
1247 || tryToStream
<EchoCommand
>(out
, c
, d_variant
))
1252 out
<< "ERROR: don't know how to print a Command of class: "
1253 << typeid(*c
).name() << endl
;
1255 }/* Smt2Printer::toStream(Command*) */
1258 static std::string
quoteSymbol(TNode n
) {
1259 // #warning "check the old implementation. It seems off."
1260 std::stringstream ss
;
1261 ss
<< language::SetLanguage(language::output::LANG_SMTLIB_V2_5
);
1262 return CVC4::quoteSymbol(ss
.str());
1266 static bool tryToStream(std::ostream
& out
, const CommandStatus
* s
, Variant v
);
1268 void Smt2Printer::toStream(std::ostream
& out
, const CommandStatus
* s
) const
1270 if (tryToStream
<CommandSuccess
>(out
, s
, d_variant
) ||
1271 tryToStream
<CommandFailure
>(out
, s
, d_variant
) ||
1272 tryToStream
<CommandRecoverableFailure
>(out
, s
, d_variant
) ||
1273 tryToStream
<CommandUnsupported
>(out
, s
, d_variant
) ||
1274 tryToStream
<CommandInterrupted
>(out
, s
, d_variant
)) {
1278 out
<< "ERROR: don't know how to print a CommandStatus of class: "
1279 << typeid(*s
).name() << endl
;
1281 }/* Smt2Printer::toStream(CommandStatus*) */
1283 void Smt2Printer::toStream(std::ostream
& out
, const UnsatCore
& core
) const
1285 out
<< "(" << std::endl
;
1286 SmtEngine
* smt
= core
.getSmtEngine();
1287 Assert( smt
!=NULL
);
1288 for(UnsatCore::const_iterator i
= core
.begin(); i
!= core
.end(); ++i
) {
1290 if (smt
->getExpressionName(*i
,name
)) {
1291 // Named assertions always get printed
1292 out
<< maybeQuoteSymbol(name
) << endl
;
1293 } else if (options::dumpUnsatCoresFull()) {
1294 // Unnamed assertions only get printed if the option is set
1299 }/* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
1301 void Smt2Printer::toStream(std::ostream
& out
, const Model
& m
) const
1303 //print the model comments
1304 std::stringstream c
;
1307 while( std::getline( c
, ln
) ){
1308 out
<< "; " << ln
<< std::endl
;
1311 out
<< "(model" << endl
;
1312 this->Printer::toStream(out
, m
);
1314 //print the heap model, if it exists
1316 if( m
.getHeapModel( h
, neq
) ){
1317 // description of the heap+what nil is equal to fully describes model
1318 out
<< "(heap" << endl
;
1321 out
<< ")" << std::endl
;
1327 void DeclareTypeCommandToStream(std::ostream
& out
,
1328 const theory::TheoryModel
& model
,
1329 const DeclareTypeCommand
& command
,
1332 TypeNode tn
= TypeNode::fromType(command
.getType());
1333 const std::vector
<Node
>* type_refs
= model
.getRepSet()->getTypeRepsOrNull(tn
);
1334 if (options::modelUninterpDtEnum() && tn
.isSort() && type_refs
!= nullptr)
1336 if (isVariant_2_6(variant
))
1338 out
<< "(declare-datatypes ((" << command
.getSymbol() << " 0)) (";
1342 out
<< "(declare-datatypes () ((" << command
.getSymbol() << " ";
1344 for (Node type_ref
: *type_refs
)
1346 out
<< "(" << type_ref
<< ")";
1348 out
<< ")))" << endl
;
1350 else if (tn
.isSort() && type_refs
!= nullptr)
1352 // print the cardinality
1353 out
<< "; cardinality of " << tn
<< " is " << type_refs
->size() << endl
;
1354 out
<< command
<< endl
;
1355 // print the representatives
1356 for (Node type_ref
: *type_refs
)
1358 if (type_ref
.isVar())
1360 out
<< "(declare-fun " << quoteSymbol(type_ref
) << " () " << tn
<< ")"
1365 out
<< "; rep: " << type_ref
<< endl
;
1371 out
<< command
<< endl
;
1375 void DeclareFunctionCommandToStream(std::ostream
& out
,
1376 const theory::TheoryModel
& model
,
1377 const DeclareFunctionCommand
& command
)
1379 Node n
= Node::fromExpr(command
.getFunction());
1380 if (command
.getPrintInModelSetByUser())
1382 if (!command
.getPrintInModel())
1387 else if (n
.getKind() == kind::SKOLEM
)
1389 // don't print out internal stuff
1392 Node val
= Node::fromExpr(model
.getSmtEngine()->getValue(n
.toExpr()));
1393 if (val
.getKind() == kind::LAMBDA
)
1395 out
<< "(define-fun " << n
<< " " << val
[0] << " "
1396 << n
.getType().getRangeType() << " " << val
[1] << ")" << endl
;
1400 if (options::modelUninterpDtEnum() && val
.getKind() == kind::STORE
)
1402 TypeNode tn
= val
[1].getType();
1403 const std::vector
<Node
>* type_refs
=
1404 model
.getRepSet()->getTypeRepsOrNull(tn
);
1405 if (tn
.isSort() && type_refs
!= nullptr)
1407 Cardinality
indexCard(type_refs
->size());
1408 val
= theory::arrays::TheoryArraysRewriter::normalizeConstant(
1412 out
<< "(define-fun " << n
<< " () " << n
.getType() << " ";
1413 if (val
.getType().isInteger() && n
.getType().isReal()
1414 && !n
.getType().isInteger())
1416 // toStreamReal(out, val, true);
1417 toStreamRational(out
, val
.getConst
<Rational
>(), true);
1418 // out << val << ".0";
1430 void Smt2Printer::toStream(std::ostream
& out
,
1432 const Command
* command
) const
1434 const theory::TheoryModel
* theory_model
=
1435 dynamic_cast<const theory::TheoryModel
*>(&model
);
1436 AlwaysAssert(theory_model
!= nullptr);
1437 if (const DeclareTypeCommand
* dtc
=
1438 dynamic_cast<const DeclareTypeCommand
*>(command
))
1440 DeclareTypeCommandToStream(out
, *theory_model
, *dtc
, d_variant
);
1442 else if (const DeclareFunctionCommand
* dfc
=
1443 dynamic_cast<const DeclareFunctionCommand
*>(command
))
1445 DeclareFunctionCommandToStream(out
, *theory_model
, *dfc
);
1447 else if (const DatatypeDeclarationCommand
* datatype_declaration_command
=
1448 dynamic_cast<const DatatypeDeclarationCommand
*>(command
))
1450 toStream(out
, datatype_declaration_command
, -1, false, 1);
1458 void Smt2Printer::toStreamSygus(std::ostream
& out
, TNode n
) const
1460 if (n
.getKind() == kind::APPLY_CONSTRUCTOR
)
1462 TypeNode tn
= n
.getType();
1463 const Datatype
& dt
= static_cast<DatatypeType
>(tn
.toType()).getDatatype();
1466 int cIndex
= Datatype::indexOf(n
.getOperator().toExpr());
1467 Assert(!dt
[cIndex
].getSygusOp().isNull());
1468 SygusPrintCallback
* spc
= dt
[cIndex
].getSygusPrintCallback().get();
1469 if (spc
!= nullptr && options::sygusPrintCallbacks())
1471 spc
->toStreamSygus(this, out
, n
.toExpr());
1475 if (n
.getNumChildren() > 0)
1479 out
<< dt
[cIndex
].getSygusOp();
1480 if (n
.getNumChildren() > 0)
1485 toStreamSygus(out
, nc
);
1495 Node p
= n
.getAttribute(theory::SygusPrintProxyAttribute());
1502 // cannot convert term to analog, print original
1508 static void toStream(std::ostream
& out
, const AssertCommand
* c
)
1510 out
<< "(assert " << c
->getExpr() << ")";
1513 static void toStream(std::ostream
& out
, const PushCommand
* c
)
1518 static void toStream(std::ostream
& out
, const PopCommand
* c
)
1523 static void toStream(std::ostream
& out
, const CheckSatCommand
* c
)
1525 Expr e
= c
->getExpr();
1526 if(!e
.isNull() && !(e
.getKind() == kind::CONST_BOOLEAN
&& e
.getConst
<bool>())) {
1527 out
<< PushCommand() << endl
1528 << AssertCommand(e
) << endl
1529 << CheckSatCommand() << endl
1532 out
<< "(check-sat)";
1536 static void toStream(std::ostream
& out
, const CheckSatAssumingCommand
* c
)
1538 out
<< "(check-sat-assuming ( ";
1539 const vector
<Expr
>& terms
= c
->getTerms();
1540 copy(terms
.begin(), terms
.end(), ostream_iterator
<Expr
>(out
, " "));
1544 static void toStream(std::ostream
& out
, const QueryCommand
* c
, Variant v
)
1546 Expr e
= c
->getExpr();
1548 if (v
== smt2_0_variant
)
1550 out
<< PushCommand() << endl
1551 << AssertCommand(BooleanSimplification::negate(e
)) << endl
1552 << CheckSatCommand() << endl
1557 out
<< CheckSatAssumingCommand(e
.notExpr()) << endl
;
1560 out
<< "(check-sat)";
1564 static void toStream(std::ostream
& out
, const ResetCommand
* c
)
1569 static void toStream(std::ostream
& out
, const ResetAssertionsCommand
* c
)
1571 out
<< "(reset-assertions)";
1574 static void toStream(std::ostream
& out
, const QuitCommand
* c
)
1579 static void toStream(std::ostream
& out
, const CommandSequence
* c
)
1581 CommandSequence::const_iterator i
= c
->begin();
1585 if(++i
!= c
->end()) {
1594 static void toStream(std::ostream
& out
, const DeclareFunctionCommand
* c
)
1596 Type type
= c
->getType();
1597 out
<< "(declare-fun " << CVC4::quoteSymbol(c
->getSymbol()) << " (";
1598 if(type
.isFunction()) {
1599 FunctionType ft
= type
;
1600 const vector
<Type
> argTypes
= ft
.getArgTypes();
1601 if(argTypes
.size() > 0) {
1602 copy( argTypes
.begin(), argTypes
.end() - 1,
1603 ostream_iterator
<Type
>(out
, " ") );
1604 out
<< argTypes
.back();
1606 type
= ft
.getRangeType();
1609 out
<< ") " << type
<< ")";
1612 static void toStream(std::ostream
& out
, const DefineFunctionCommand
* c
)
1614 Expr func
= c
->getFunction();
1615 const vector
<Expr
>* formals
= &c
->getFormals();
1616 out
<< "(define-fun " << func
<< " (";
1617 Type type
= func
.getType();
1618 Expr formula
= c
->getFormula();
1619 if(type
.isFunction()) {
1621 if(formals
->empty()) {
1622 const vector
<Type
>& params
= FunctionType(type
).getArgTypes();
1623 for(vector
<Type
>::const_iterator j
= params
.begin(); j
!= params
.end(); ++j
) {
1624 f
.push_back(NodeManager::currentNM()->mkSkolem("a", TypeNode::fromType(*j
), "",
1625 NodeManager::SKOLEM_NO_NOTIFY
).toExpr());
1627 formula
= NodeManager::currentNM()->toExprManager()->mkExpr(kind::APPLY_UF
, formula
, f
);
1630 vector
<Expr
>::const_iterator i
= formals
->begin();
1632 out
<< "(" << (*i
) << " " << (*i
).getType() << ")";
1634 if(i
!= formals
->end()) {
1640 type
= FunctionType(type
).getRangeType();
1642 out
<< ") " << type
<< " " << formula
<< ")";
1645 static void toStream(std::ostream
& out
, const DefineFunctionRecCommand
* c
)
1647 const vector
<Expr
>& funcs
= c
->getFunctions();
1648 const vector
<vector
<Expr
> >& formals
= c
->getFormals();
1649 out
<< "(define-fun";
1650 if (funcs
.size() > 1)
1655 if (funcs
.size() > 1)
1659 for (unsigned i
= 0, size
= funcs
.size(); i
< size
; i
++)
1661 if (funcs
.size() > 1)
1669 out
<< funcs
[i
] << " (";
1670 // print its type signature
1671 vector
<Expr
>::const_iterator itf
= formals
[i
].begin();
1674 out
<< "(" << (*itf
) << " " << (*itf
).getType() << ")";
1676 if (itf
!= formals
[i
].end())
1685 Type type
= funcs
[i
].getType();
1686 type
= static_cast<FunctionType
>(type
).getRangeType();
1687 out
<< ") " << type
;
1688 if (funcs
.size() > 1)
1693 if (funcs
.size() > 1)
1697 const vector
<Expr
>& formulas
= c
->getFormulas();
1698 for (unsigned i
= 0, size
= formulas
.size(); i
< size
; i
++)
1706 if (funcs
.size() > 1)
1713 static void toStreamRational(std::ostream
& out
, const Rational
& r
, bool decimal
)
1715 bool neg
= r
.sgn() < 0;
1718 // We are currently printing (- (/ 5 3))
1719 // instead of (/ (- 5) 3) which is what is in the SMT-LIB value in the theory definition.
1720 // Before switching, I'll keep to what was there and send an email.
1722 // Tim: Apologies for the ifs on one line but in this case they are cleaner.
1724 if (neg
) { out
<< "(- "; }
1726 if(r
.isIntegral()) {
1732 if (decimal
) { out
<< ".0"; }
1736 Rational abs_r
= (-r
);
1737 out
<< abs_r
.getNumerator();
1738 if(decimal
) { out
<< ".0"; }
1739 out
<< ' ' << abs_r
.getDenominator();
1740 if(decimal
) { out
<< ".0"; }
1742 out
<< r
.getNumerator();
1743 if(decimal
) { out
<< ".0"; }
1744 out
<< ' ' << r
.getDenominator();
1745 if(decimal
) { out
<< ".0"; }
1750 if (neg
) { out
<< ')';}
1753 // Rational abs_r = -r;
1754 // if(r.isIntegral()) {
1755 // out << "(- " << abs_r << ')';
1757 // out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
1760 // if(r.isIntegral()) {
1763 // out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';
1768 static void toStream(std::ostream
& out
, const DeclareTypeCommand
* c
)
1770 out
<< "(declare-sort " << c
->getSymbol() << " " << c
->getArity() << ")";
1773 static void toStream(std::ostream
& out
, const DefineTypeCommand
* c
)
1775 const vector
<Type
>& params
= c
->getParameters();
1776 out
<< "(define-sort " << c
->getSymbol() << " (";
1777 if(params
.size() > 0) {
1778 copy( params
.begin(), params
.end() - 1,
1779 ostream_iterator
<Type
>(out
, " ") );
1780 out
<< params
.back();
1782 out
<< ") " << c
->getType() << ")";
1785 static void toStream(std::ostream
& out
, const DefineNamedFunctionCommand
* c
)
1787 out
<< "DefineNamedFunction( ";
1788 toStream(out
, static_cast<const DefineFunctionCommand
*>(c
));
1791 out
<< "ERROR: don't know how to output define-named-function command" << endl
;
1794 static void toStream(std::ostream
& out
, const SimplifyCommand
* c
)
1796 out
<< "(simplify " << c
->getTerm() << ")";
1799 static void toStream(std::ostream
& out
, const GetValueCommand
* c
)
1801 out
<< "(get-value ( ";
1802 const vector
<Expr
>& terms
= c
->getTerms();
1803 copy(terms
.begin(), terms
.end(), ostream_iterator
<Expr
>(out
, " "));
1807 static void toStream(std::ostream
& out
, const GetModelCommand
* c
)
1809 out
<< "(get-model)";
1812 static void toStream(std::ostream
& out
, const GetAssignmentCommand
* c
)
1814 out
<< "(get-assignment)";
1817 static void toStream(std::ostream
& out
, const GetAssertionsCommand
* c
)
1819 out
<< "(get-assertions)";
1822 static void toStream(std::ostream
& out
, const GetProofCommand
* c
)
1824 out
<< "(get-proof)";
1827 static void toStream(std::ostream
& out
, const GetUnsatAssumptionsCommand
* c
)
1829 out
<< "(get-unsat-assumptions)";
1832 static void toStream(std::ostream
& out
, const GetUnsatCoreCommand
* c
)
1834 out
<< "(get-unsat-core)";
1837 static void toStream(std::ostream
& out
,
1838 const SetBenchmarkStatusCommand
* c
,
1841 if(v
== z3str_variant
|| v
== smt2_0_variant
) {
1842 out
<< "(set-info :status " << c
->getStatus() << ")";
1844 out
<< "(meta-info :status " << c
->getStatus() << ")";
1848 static void toStream(std::ostream
& out
,
1849 const SetBenchmarkLogicCommand
* c
,
1852 // Z3-str doesn't have string-specific logic strings(?), so comment it
1853 if(v
== z3str_variant
) {
1854 out
<< "; (set-logic " << c
->getLogic() << ")";
1856 out
<< "(set-logic " << c
->getLogic() << ")";
1860 static void toStream(std::ostream
& out
, const SetInfoCommand
* c
, Variant v
)
1862 if(v
== z3str_variant
|| v
== smt2_0_variant
) {
1863 out
<< "(set-info :" << c
->getFlag() << " ";
1865 out
<< "(meta-info :" << c
->getFlag() << " ";
1868 SExpr::toStream(out
, c
->getSExpr(), variantToLanguage(v
));
1872 static void toStream(std::ostream
& out
, const GetInfoCommand
* c
)
1874 out
<< "(get-info :" << c
->getFlag() << ")";
1877 static void toStream(std::ostream
& out
, const SetOptionCommand
* c
)
1879 out
<< "(set-option :" << c
->getFlag() << " ";
1880 SExpr::toStream(out
, c
->getSExpr(), language::output::LANG_SMTLIB_V2_5
);
1884 static void toStream(std::ostream
& out
, const GetOptionCommand
* c
)
1886 out
<< "(get-option :" << c
->getFlag() << ")";
1889 static void toStream(std::ostream
& out
, const Datatype
& d
) {
1890 for(Datatype::const_iterator ctor
= d
.begin(), ctor_end
= d
.end();
1891 ctor
!= ctor_end
; ++ctor
){
1892 if( ctor
!=d
.begin() ) out
<< " ";
1893 out
<< "(" << maybeQuoteSymbol(ctor
->getName());
1895 for(DatatypeConstructor::const_iterator arg
= ctor
->begin(), arg_end
= ctor
->end();
1896 arg
!= arg_end
; ++arg
){
1897 out
<< " (" << arg
->getSelector() << " "
1898 << static_cast<SelectorType
>(arg
->getType()).getRangeType() << ")";
1904 static void toStream(std::ostream
& out
,
1905 const DatatypeDeclarationCommand
* c
,
1908 const vector
<DatatypeType
>& datatypes
= c
->getDatatypes();
1909 Assert(!datatypes
.empty());
1910 if (datatypes
[0].getDatatype().isTuple())
1912 // not necessary to print tuples
1913 Assert(datatypes
.size() == 1);
1917 if (datatypes
[0].getDatatype().isCodatatype())
1922 if (isVariant_2_6(v
))
1925 for (vector
<DatatypeType
>::const_iterator i
= datatypes
.begin(),
1926 i_end
= datatypes
.end();
1930 const Datatype
& d
= i
->getDatatype();
1931 out
<< "(" << maybeQuoteSymbol(d
.getName());
1932 out
<< " " << d
.getNumParameters() << ")";
1935 for (vector
<DatatypeType
>::const_iterator i
= datatypes
.begin(),
1936 i_end
= datatypes
.end();
1940 const Datatype
& d
= i
->getDatatype();
1950 for (vector
<DatatypeType
>::const_iterator i
= datatypes
.begin(),
1951 i_end
= datatypes
.end();
1955 const Datatype
& d
= i
->getDatatype();
1956 out
<< "(" << maybeQuoteSymbol(d
.getName()) << " ";
1965 static void toStream(std::ostream
& out
, const CommentCommand
* c
, Variant v
)
1967 string s
= c
->getComment();
1969 while((pos
= s
.find_first_of('"', pos
)) != string::npos
) {
1970 s
.replace(pos
, 1, (v
== z3str_variant
|| v
== smt2_0_variant
) ? "\\\"" : "\"\"");
1973 out
<< "(set-info :notes \"" << s
<< "\")";
1976 static void toStream(std::ostream
& out
, const EmptyCommand
* c
) {}
1978 static void toStream(std::ostream
& out
, const EchoCommand
* c
, Variant v
)
1980 std::string s
= c
->getOutput();
1981 // escape all double-quotes
1983 while((pos
= s
.find('"', pos
)) != string::npos
) {
1984 s
.replace(pos
, 1, (v
== z3str_variant
|| v
== smt2_0_variant
) ? "\\\"" : "\"\"");
1987 out
<< "(echo \"" << s
<< "\")";
1991 static bool tryToStream(std::ostream
& out
, const Command
* c
)
1993 if(typeid(*c
) == typeid(T
)) {
1994 toStream(out
, dynamic_cast<const T
*>(c
));
2001 static bool tryToStream(std::ostream
& out
, const Command
* c
, Variant v
)
2003 if(typeid(*c
) == typeid(T
)) {
2004 toStream(out
, dynamic_cast<const T
*>(c
), v
);
2010 static void toStream(std::ostream
& out
, const CommandSuccess
* s
, Variant v
)
2012 if(Command::printsuccess::getPrintSuccess(out
)) {
2013 out
<< "success" << endl
;
2017 static void toStream(std::ostream
& out
, const CommandInterrupted
* s
, Variant v
)
2019 out
<< "interrupted" << endl
;
2022 static void toStream(std::ostream
& out
, const CommandUnsupported
* s
, Variant v
)
2024 #ifdef CVC4_COMPETITION_MODE
2025 // if in competition mode, lie and say we're ok
2026 // (we have nothing to lose by saying success, and everything to lose
2027 // if we say "unsupported")
2028 out
<< "success" << endl
;
2029 #else /* CVC4_COMPETITION_MODE */
2030 out
<< "unsupported" << endl
;
2031 #endif /* CVC4_COMPETITION_MODE */
2034 static void errorToStream(std::ostream
& out
, std::string message
, Variant v
) {
2035 // escape all double-quotes
2037 while((pos
= message
.find('"', pos
)) != string::npos
) {
2038 message
.replace(pos
, 1, (v
== z3str_variant
|| v
== smt2_0_variant
) ? "\\\"" : "\"\"");
2041 out
<< "(error \"" << message
<< "\")" << endl
;
2044 static void toStream(std::ostream
& out
, const CommandFailure
* s
, Variant v
) {
2045 errorToStream(out
, s
->getMessage(), v
);
2048 static void toStream(std::ostream
& out
, const CommandRecoverableFailure
* s
,
2050 errorToStream(out
, s
->getMessage(), v
);
2054 static bool tryToStream(std::ostream
& out
, const CommandStatus
* s
, Variant v
)
2056 if(typeid(*s
) == typeid(T
)) {
2057 toStream(out
, dynamic_cast<const T
*>(s
), v
);
2063 static OutputLanguage
variantToLanguage(Variant variant
)
2066 case smt2_0_variant
:
2067 return language::output::LANG_SMTLIB_V2_0
;
2069 return language::output::LANG_Z3STR
;
2071 return language::output::LANG_SYGUS
;
2074 return language::output::LANG_SMTLIB_V2_5
;
2078 }/* CVC4::printer::smt2 namespace */
2079 }/* CVC4::printer namespace */
2080 }/* CVC4 namespace */