1 /********************* */
2 /*! \file cvc_printer.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Dejan Jovanovic, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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 CVC output language
14 ** The pretty-printer interface for the CVC output language.
17 #include "printer/cvc/cvc_printer.h"
27 #include "expr/dtype.h"
28 #include "expr/expr.h" // for ExprSetDepth etc..
29 #include "expr/expr_sequence.h"
30 #include "expr/node_manager_attributes.h" // for VarNameAttr
31 #include "expr/node_visitor.h"
32 #include "expr/sequence.h"
33 #include "options/language.h" // for LANG_AST
34 #include "options/smt_options.h"
35 #include "printer/dagification_visitor.h"
36 #include "smt/command.h"
37 #include "smt/smt_engine.h"
38 #include "theory/arrays/theory_arrays_rewriter.h"
39 #include "theory/substitutions.h"
40 #include "theory/theory_model.h"
48 void CvcPrinter::toStream(
49 std::ostream
& out
, TNode n
, int toDepth
, bool types
, size_t dag
) const
52 DagificationVisitor
dv(dag
);
53 NodeVisitor
<DagificationVisitor
> visitor
;
55 const theory::SubstitutionMap
& lets
= dv
.getLets();
59 for(theory::SubstitutionMap::const_iterator i
= lets
.begin();
67 toStream(out
, (*i
).second
, toDepth
, types
, false);
69 toStream(out
, (*i
).first
, toDepth
, types
, false);
73 Node body
= dv
.getDagifiedBody();
74 toStream(out
, body
, toDepth
, types
, false);
76 toStream(out
, n
, toDepth
, types
, false);
80 void toStreamRational(std::ostream
& out
, Node n
, bool forceRational
)
82 Assert(n
.getKind() == kind::CONST_RATIONAL
);
83 const Rational
& rat
= n
.getConst
<Rational
>();
84 if (rat
.isIntegral() && !forceRational
)
86 out
<< rat
.getNumerator();
90 out
<< '(' << rat
.getNumerator() << '/' << rat
.getDenominator() << ')';
94 void CvcPrinter::toStream(
95 std::ostream
& out
, TNode n
, int depth
, bool types
, bool bracket
) const
104 if(n
.getKind() == kind::NULL_EXPR
) {
112 if(n
.getAttribute(expr::VarNameAttr(), s
)) {
115 if(n
.getKind() == kind::VARIABLE
) {
118 out
<< n
.getKind() << '_';
123 // print the whole type, but not *its* type
125 n
.getType().toStream(out
, language::output::LANG_CVC4
);
129 if(n
.isNullaryOp()) {
130 if( n
.getKind() == kind::UNIVERSE_SET
){
131 out
<< "UNIVERSE :: " << n
.getType();
140 if(n
.getMetaKind() == kind::metakind::CONSTANT
) {
141 switch(n
.getKind()) {
142 case kind::BITVECTOR_TYPE
:
143 out
<< "BITVECTOR(" << n
.getConst
<BitVectorSize
>().d_size
<< ")";
145 case kind::CONST_BITVECTOR
: {
146 const BitVector
& bv
= n
.getConst
<BitVector
>();
147 const Integer
& x
= bv
.getValue();
149 unsigned size
= bv
.getSize();
152 out
<< (x
.testBit(size
) ? '1' : '0');
156 case kind::CONST_BOOLEAN
:
157 // the default would print "1" or "0" for bool, that's not correct
159 out
<< (n
.getConst
<bool>() ? "TRUE" : "FALSE");
161 case kind::CONST_RATIONAL
: {
162 toStreamRational(out
, n
, false);
165 case kind::CONST_STRING
:
167 out
<< '"' << n
.getConst
<String
>().toString() << '"';
170 case kind::CONST_SEQUENCE
:
172 const Sequence
& sn
= n
.getConst
<ExprSequence
>().getSequence();
173 const std::vector
<Node
>& snvec
= sn
.getVec();
174 if (snvec
.size() > 1)
179 for (const Node
& snvc
: snvec
)
185 out
<< "SEQ_UNIT(" << snvc
<< ")";
188 if (snvec
.size() > 1)
194 case kind::TYPE_CONSTANT
:
195 switch(TypeConstant tc
= n
.getConst
<TypeConstant
>()) {
214 case kind::DATATYPE_TYPE
: {
216 NodeManager::currentNM()->toExprManager()->getDatatypeForIndex(
217 n
.getConst
<DatatypeIndexConstant
>().getIndex());
220 for (unsigned i
= 0; i
< dt
[0].getNumArgs(); ++ i
) {
224 Type t
= ((SelectorType
)dt
[0][i
].getSelector().getType()).getRangeType();
228 }else if( dt
.isRecord() ){
230 for (unsigned i
= 0; i
< dt
[0].getNumArgs(); ++ i
) {
234 Type t
= ((SelectorType
)dt
[0][i
].getSelector().getType()).getRangeType();
235 out
<< dt
[0][i
].getSelector() << ":" << t
;
245 out
<< "{} :: " << n
.getConst
<EmptySet
>().getType();
248 case kind::STORE_ALL
: {
249 const ArrayStoreAll
& asa
= n
.getConst
<ArrayStoreAll
>();
250 out
<< "ARRAY(" << asa
.getType().getIndexType() << " OF "
251 << asa
.getType().getConstituentType() << ") : " << asa
.getExpr();
256 // Fall back to whatever operator<< does on underlying type; we
257 // might luck out and print something reasonable.
258 kind::metakind::NodeValueConstPrinter::toStream(out
, n
);
270 //The default operation type is PREFIX
273 stringstream op
; // operation (such as '+')
275 switch(n
.getKind()) {
279 if( n
[0].getType().isBoolean() ){
288 toStream(out
, n
[0], depth
, types
, true);
290 toStream(out
, n
[1], depth
, types
, true);
292 toStream(out
, n
[2], depth
, types
, true);
296 case kind::SEXPR_TYPE
:
298 for (unsigned i
= 0; i
< n
.getNumChildren(); ++ i
) {
302 toStream(out
, n
[i
], depth
, types
, false);
312 toStream(out
, n
[0], depth
, types
, true);
314 toStream(out
, n
[1], depth
, types
, true);
319 // distinct not supported directly, blast it away with the rewriter
320 toStream(out
, theory::Rewriter::rewrite(n
), depth
, types
, true);
322 case kind::SORT_TYPE
:
325 if(n
.getAttribute(expr::VarNameAttr(), name
)) {
356 toStream(op
, n
.getOperator(), depth
, types
, false);
358 case kind::CARDINALITY_CONSTRAINT
:
359 case kind::COMBINED_CARDINALITY_CONSTRAINT
:
360 out
<< "CARDINALITY_CONSTRAINT";
363 case kind::FUNCTION_TYPE
:
364 if (n
.getNumChildren() > 1) {
365 if (n
.getNumChildren() > 2) {
368 for (unsigned i
= 1; i
< n
.getNumChildren(); ++i
) {
372 toStream(out
, n
[i
- 1], depth
, types
, false);
374 if (n
.getNumChildren() > 2) {
379 toStream(out
, n
[n
.getNumChildren() - 1], depth
, types
, false);
384 case kind::PARAMETRIC_DATATYPE
: {
385 const DType
& dt
= NodeManager::currentNM()->getDTypeForIndex(
386 n
[0].getConst
<DatatypeIndexConstant
>().getIndex());
387 out
<< dt
.getName() << '[';
388 for (unsigned i
= 1; i
< n
.getNumChildren(); ++i
)
400 case kind::APPLY_TYPE_ASCRIPTION
: {
401 toStream(out
, n
[0], depth
, types
, false);
403 TypeNode t
= TypeNode::fromType(n
.getOperator().getConst
<AscriptionType
>().getType());
404 out
<< (t
.isFunctionLike() ? t
.getRangeType() : t
);
408 case kind::APPLY_CONSTRUCTOR
: {
409 TypeNode t
= n
.getType();
411 if( n
.getNumChildren()==1 ){
415 else if (t
.toType().isRecord())
417 const Record
& rec
= static_cast<DatatypeType
>(t
.toType()).getRecord();
419 TNode::iterator i
= n
.begin();
421 const Record::FieldVector
& fields
= rec
.getFields();
422 for(Record::FieldVector::const_iterator j
= fields
.begin(); j
!= fields
.end(); ++i
, ++j
) {
426 out
<< (*j
).first
<< " := ";
427 toStream(out
, *i
, depth
, types
, false);
435 toStream(op
, n
.getOperator(), depth
, types
, false);
436 if (n
.getNumChildren() == 0)
438 // for datatype constants d, we print "d" and not "d()"
445 case kind::APPLY_SELECTOR
:
446 case kind::APPLY_SELECTOR_TOTAL
: {
447 TypeNode t
= n
[0].getType();
448 Node opn
= n
.getOperator();
451 toStream(op
, opn
, depth
, types
, false);
454 || DatatypeType(t
.toType()).isRecord())
456 toStream(out
, n
[0], depth
, types
, true);
458 const Datatype
& dt
= ((DatatypeType
)t
.toType()).getDatatype();
462 if (n
.getKind() == kind::APPLY_SELECTOR
)
464 sindex
= Datatype::indexOf(opn
.toExpr());
468 sindex
= dt
[0].getSelectorIndexInternal(opn
.toExpr());
475 toStream(out
, opn
, depth
, types
, false);
479 toStream(op
, opn
, depth
, types
, false);
483 case kind::APPLY_TESTER
: {
484 Assert(!n
.getType().isTuple() && !n
.getType().toType().isRecord());
486 unsigned cindex
= Datatype::indexOf(n
.getOperator().toExpr());
487 const Datatype
& dt
= Datatype::datatypeOf(n
.getOperator().toExpr());
488 toStream(op
, Node::fromExpr(dt
[cindex
].getConstructor()), depth
, types
, false);
491 case kind::CONSTRUCTOR_TYPE
:
492 case kind::SELECTOR_TYPE
:
493 if(n
.getNumChildren() > 1) {
494 if(n
.getNumChildren() > 2) {
497 for(unsigned i
= 0; i
< n
.getNumChildren() - 1; ++i
) {
501 toStream(out
, n
[i
], depth
, types
, false);
503 if(n
.getNumChildren() > 2) {
508 toStream(out
, n
[n
.getNumChildren() - 1], depth
, types
, false);
510 case kind::TESTER_TYPE
:
511 toStream(out
, n
[0], depth
, types
, false);
512 out
<< " -> BOOLEAN";
515 case kind::TUPLE_UPDATE
:
516 toStream(out
, n
[0], depth
, types
, true);
517 out
<< " WITH ." << n
.getOperator().getConst
<TupleUpdate
>().getIndex() << " := ";
518 toStream(out
, n
[1], depth
, types
, true);
521 case kind::RECORD_UPDATE
:
522 toStream(out
, n
[0], depth
, types
, true);
523 out
<< " WITH ." << n
.getOperator().getConst
<RecordUpdate
>().getField() << " := ";
524 toStream(out
, n
[1], depth
, types
, true);
529 case kind::ARRAY_TYPE
:
531 toStream(out
, n
[0], depth
, types
, false);
533 toStream(out
, n
[1], depth
, types
, false);
537 toStream(out
, n
[0], depth
, types
, true);
539 toStream(out
, n
[1], depth
, types
, false);
546 while(stk
.top()[0].getKind() == kind::STORE
) {
547 stk
.push(stk
.top()[0]);
553 toStream(out
, x
[0], depth
, types
, false);
555 toStream(out
, x
[1], depth
, types
, false);
557 toStream(out
, x
[2], depth
, types
, false);
559 while(!stk
.empty()) {
562 toStream(out
, x
[1], depth
, types
, false);
564 toStream(out
, x
[2], depth
, types
, false);
580 case kind::NONLINEAR_MULT
:
593 case kind::DIVISION_TOTAL
:
597 case kind::INTS_DIVISION
:
598 case kind::INTS_DIVISION_TOTAL
:
602 case kind::INTS_MODULUS
:
603 case kind::INTS_MODULUS_TOTAL
:
631 case kind::IS_INTEGER
:
635 case kind::TO_INTEGER
:
640 if (n
[0].getKind() == kind::CONST_RATIONAL
)
642 // print the constant as a rational
643 toStreamRational(out
, n
[0], true);
647 // ignore, there is no to-real in CVC language
648 toStream(out
, n
[0], depth
, types
, false);
651 case kind::DIVISIBLE
:
653 toStream(out
, n
[0], depth
, types
, false);
654 out
<< ", " << n
.getOperator().getConst
<Divisible
>().k
<< ")";
658 case kind::BITVECTOR_XOR
:
661 case kind::BITVECTOR_NAND
:
664 case kind::BITVECTOR_NOR
:
667 case kind::BITVECTOR_XNOR
:
670 case kind::BITVECTOR_COMP
:
673 case kind::BITVECTOR_UDIV
:
676 case kind::BITVECTOR_UDIV_TOTAL
:
677 op
<< "BVUDIV_TOTAL";
679 case kind::BITVECTOR_UREM
:
682 case kind::BITVECTOR_UREM_TOTAL
:
683 op
<< "BVUREM_TOTAL";
685 case kind::BITVECTOR_SDIV
:
688 case kind::BITVECTOR_SREM
:
691 case kind::BITVECTOR_SMOD
:
694 case kind::BITVECTOR_SHL
:
697 case kind::BITVECTOR_LSHR
:
700 case kind::BITVECTOR_ASHR
:
703 case kind::BITVECTOR_ULT
:
706 case kind::BITVECTOR_ULE
:
709 case kind::BITVECTOR_UGT
:
712 case kind::BITVECTOR_UGE
:
715 case kind::BITVECTOR_SLT
:
718 case kind::BITVECTOR_SLE
:
721 case kind::BITVECTOR_SGT
:
724 case kind::BITVECTOR_SGE
:
727 case kind::BITVECTOR_NEG
:
730 case kind::BITVECTOR_NOT
:
733 case kind::BITVECTOR_AND
:
737 case kind::BITVECTOR_OR
:
741 case kind::BITVECTOR_CONCAT
:
745 case kind::BITVECTOR_PLUS
: {
746 // This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB
747 Assert(n
.getType().isBitVector());
748 unsigned numc
= n
.getNumChildren()-2;
750 while (child
< numc
) {
752 out
<< BitVectorType(n
.getType().toType()).getSize();
754 toStream(out
, n
[child
], depth
, types
, false);
759 out
<< BitVectorType(n
.getType().toType()).getSize();
761 toStream(out
, n
[child
], depth
, types
, false);
763 toStream(out
, n
[child
+ 1], depth
, types
, false);
772 case kind::BITVECTOR_SUB
:
774 Assert(n
.getType().isBitVector());
775 out
<< BitVectorType(n
.getType().toType()).getSize();
777 toStream(out
, n
[0], depth
, types
, false);
779 toStream(out
, n
[1], depth
, types
, false);
783 case kind::BITVECTOR_MULT
: {
784 Assert(n
.getType().isBitVector());
785 unsigned numc
= n
.getNumChildren()-2;
787 while (child
< numc
) {
789 out
<< BitVectorType(n
.getType().toType()).getSize();
791 toStream(out
, n
[child
], depth
, types
, false);
796 out
<< BitVectorType(n
.getType().toType()).getSize();
798 toStream(out
, n
[child
], depth
, types
, false);
800 toStream(out
, n
[child
+ 1], depth
, types
, false);
809 case kind::BITVECTOR_EXTRACT
:
810 op
<< n
.getOperator().getConst
<BitVectorExtract
>();
813 case kind::BITVECTOR_BITOF
:
814 op
<< n
.getOperator().getConst
<BitVectorBitOf
>();
817 case kind::BITVECTOR_REPEAT
:
819 toStream(out
, n
[0], depth
, types
, false);
820 out
<< ", " << n
.getOperator().getConst
<BitVectorRepeat
>() << ')';
823 case kind::BITVECTOR_ZERO_EXTEND
:
824 out
<< "BVZEROEXTEND(";
825 toStream(out
, n
[0], depth
, types
, false);
826 out
<< ", " << n
.getOperator().getConst
<BitVectorZeroExtend
>() << ')';
829 case kind::BITVECTOR_SIGN_EXTEND
:
831 toStream(out
, n
[0], depth
, types
, false);
832 out
<< ", " << BitVectorType(n
.getType().toType()).getSize() << ')';
835 case kind::BITVECTOR_ROTATE_LEFT
:
837 toStream(out
, n
[0], depth
, types
, false);
838 out
<< ", " << n
.getOperator().getConst
<BitVectorRotateLeft
>() << ')';
841 case kind::BITVECTOR_ROTATE_RIGHT
:
843 toStream(out
, n
[0], depth
, types
, false);
844 out
<< ", " << n
.getOperator().getConst
<BitVectorRotateRight
>() << ')';
851 toStream(out
, n
[0], depth
, types
, false);
858 case kind::INTERSECTION
:
874 case kind::COMPLEMENT
:
886 case kind::TRANSPOSE
:
898 case kind::JOIN_IMAGE
:
902 case kind::SINGLETON
:
904 toStream(out
, n
[0], depth
, types
, false);
914 toStream(out
, n
[i
++], depth
, types
, false);
915 for(;i
+1 < n
.getNumChildren(); ++i
) {
917 toStream(out
, n
[i
], depth
, types
, false);
920 toStream(out
, n
[i
], depth
, types
, true);
929 toStream(out
, n
[0], depth
, types
, false);
938 toStream(out
, n
[0], depth
, types
, false);
940 toStream(out
, n
[1], depth
, types
, false);
942 // TODO: user patterns?
946 toStream(out
, n
[0], depth
, types
, false);
948 toStream(out
, n
[1], depth
, types
, false);
950 // TODO: user patterns?
952 case kind::INST_CONSTANT
:
953 out
<< "INST_CONSTANT";
955 case kind::BOUND_VAR_LIST
:
957 for(size_t i
= 0; i
< n
.getNumChildren(); ++i
) {
961 toStream(out
, n
[i
], -1, true, false); // ascribe types
965 case kind::INST_PATTERN
:
966 out
<< "INST_PATTERN";
968 case kind::INST_PATTERN_LIST
:
969 out
<< "INST_PATTERN_LIST";
973 case kind::STRING_CONCAT
:
976 case kind::STRING_CHARAT
:
979 case kind::STRING_LENGTH
:
982 case kind::STRING_SUBSTR
: out
<< "SUBSTR"; break;
985 Warning() << "Kind printing not implemented for the case of " << n
.getKind() << endl
;
992 if (n
.getNumChildren() > 0)
1007 for (unsigned i
= 0; i
< n
.getNumChildren(); ++ i
) {
1009 if (opType
== INFIX
) {
1010 out
<< ' ' << op
.str() << ' ';
1015 toStream(out
, n
[i
], depth
, types
, opType
== INFIX
);
1020 if (n
.getNumChildren() > 0)
1031 out
<< ')' << op
.str();
1035 }/* CvcPrinter::toStream(TNode) */
1038 static bool tryToStream(std::ostream
& out
, const Command
* c
, bool cvc3Mode
);
1040 void CvcPrinter::toStream(std::ostream
& out
,
1046 expr::ExprSetDepth::Scope
sdScope(out
, toDepth
);
1047 expr::ExprPrintTypes::Scope
ptScope(out
, types
);
1048 expr::ExprDag::Scope
dagScope(out
, dag
);
1050 if(tryToStream
<AssertCommand
>(out
, c
, d_cvc3Mode
) ||
1051 tryToStream
<PushCommand
>(out
, c
, d_cvc3Mode
) ||
1052 tryToStream
<PopCommand
>(out
, c
, d_cvc3Mode
) ||
1053 tryToStream
<CheckSatCommand
>(out
, c
, d_cvc3Mode
) ||
1054 tryToStream
<CheckSatAssumingCommand
>(out
, c
, d_cvc3Mode
) ||
1055 tryToStream
<QueryCommand
>(out
, c
, d_cvc3Mode
) ||
1056 tryToStream
<ResetCommand
>(out
, c
, d_cvc3Mode
) ||
1057 tryToStream
<ResetAssertionsCommand
>(out
, c
, d_cvc3Mode
) ||
1058 tryToStream
<QuitCommand
>(out
, c
, d_cvc3Mode
) ||
1059 tryToStream
<DeclarationSequence
>(out
, c
, d_cvc3Mode
) ||
1060 tryToStream
<CommandSequence
>(out
, c
, d_cvc3Mode
) ||
1061 tryToStream
<DeclareFunctionCommand
>(out
, c
, d_cvc3Mode
) ||
1062 tryToStream
<DeclareTypeCommand
>(out
, c
, d_cvc3Mode
) ||
1063 tryToStream
<DefineTypeCommand
>(out
, c
, d_cvc3Mode
) ||
1064 tryToStream
<DefineNamedFunctionCommand
>(out
, c
, d_cvc3Mode
) ||
1065 tryToStream
<DefineFunctionCommand
>(out
, c
, d_cvc3Mode
) ||
1066 tryToStream
<SimplifyCommand
>(out
, c
, d_cvc3Mode
) ||
1067 tryToStream
<GetValueCommand
>(out
, c
, d_cvc3Mode
) ||
1068 tryToStream
<GetModelCommand
>(out
, c
, d_cvc3Mode
) ||
1069 tryToStream
<GetAssignmentCommand
>(out
, c
, d_cvc3Mode
) ||
1070 tryToStream
<GetAssertionsCommand
>(out
, c
, d_cvc3Mode
) ||
1071 tryToStream
<GetProofCommand
>(out
, c
, d_cvc3Mode
) ||
1072 tryToStream
<GetUnsatCoreCommand
>(out
, c
, d_cvc3Mode
) ||
1073 tryToStream
<SetBenchmarkStatusCommand
>(out
, c
, d_cvc3Mode
) ||
1074 tryToStream
<SetBenchmarkLogicCommand
>(out
, c
, d_cvc3Mode
) ||
1075 tryToStream
<SetInfoCommand
>(out
, c
, d_cvc3Mode
) ||
1076 tryToStream
<GetInfoCommand
>(out
, c
, d_cvc3Mode
) ||
1077 tryToStream
<SetOptionCommand
>(out
, c
, d_cvc3Mode
) ||
1078 tryToStream
<GetOptionCommand
>(out
, c
, d_cvc3Mode
) ||
1079 tryToStream
<DatatypeDeclarationCommand
>(out
, c
, d_cvc3Mode
) ||
1080 tryToStream
<CommentCommand
>(out
, c
, d_cvc3Mode
) ||
1081 tryToStream
<EmptyCommand
>(out
, c
, d_cvc3Mode
) ||
1082 tryToStream
<EchoCommand
>(out
, c
, d_cvc3Mode
)) {
1086 out
<< "ERROR: don't know how to print a Command of class: "
1087 << typeid(*c
).name() << endl
;
1089 }/* CvcPrinter::toStream(Command*) */
1092 static bool tryToStream(std::ostream
& out
,
1093 const CommandStatus
* s
,
1096 void CvcPrinter::toStream(std::ostream
& out
, const CommandStatus
* s
) const
1098 if (tryToStream
<CommandSuccess
>(out
, s
, d_cvc3Mode
)
1099 || tryToStream
<CommandFailure
>(out
, s
, d_cvc3Mode
)
1100 || tryToStream
<CommandRecoverableFailure
>(out
, s
, d_cvc3Mode
)
1101 || tryToStream
<CommandUnsupported
>(out
, s
, d_cvc3Mode
)
1102 || tryToStream
<CommandInterrupted
>(out
, s
, d_cvc3Mode
))
1107 out
<< "ERROR: don't know how to print a CommandStatus of class: "
1108 << typeid(*s
).name() << endl
;
1110 }/* CvcPrinter::toStream(CommandStatus*) */
1114 void DeclareTypeCommandToStream(std::ostream
& out
,
1115 const theory::TheoryModel
& model
,
1116 const DeclareTypeCommand
& command
)
1118 TypeNode type_node
= TypeNode::fromType(command
.getType());
1119 const std::vector
<Node
>* type_reps
=
1120 model
.getRepSet()->getTypeRepsOrNull(type_node
);
1121 if (options::modelUninterpDtEnum() && type_node
.isSort()
1122 && type_reps
!= nullptr)
1124 out
<< "DATATYPE" << std::endl
;
1125 out
<< " " << command
.getSymbol() << " = ";
1126 for (size_t i
= 0; i
< type_reps
->size(); i
++)
1132 out
<< (*type_reps
)[i
] << " ";
1134 out
<< std::endl
<< "END;" << std::endl
;
1136 else if (type_node
.isSort() && type_reps
!= nullptr)
1138 out
<< "% cardinality of " << type_node
<< " is " << type_reps
->size()
1140 out
<< command
<< std::endl
;
1141 for (Node type_rep
: *type_reps
)
1143 if (type_rep
.isVar())
1145 out
<< type_rep
<< " : " << type_node
<< ";" << std::endl
;
1149 out
<< "% rep: " << type_rep
<< std::endl
;
1155 out
<< command
<< std::endl
;
1159 void DeclareFunctionCommandToStream(std::ostream
& out
,
1160 const theory::TheoryModel
& model
,
1161 const DeclareFunctionCommand
& command
)
1163 Node n
= Node::fromExpr(command
.getFunction());
1164 if (n
.getKind() == kind::SKOLEM
)
1166 // don't print out internal stuff
1169 TypeNode tn
= n
.getType();
1171 if (tn
.isFunction() || tn
.isPredicate())
1174 for (size_t i
= 0; i
< tn
.getNumChildren() - 1; i
++)
1182 out
<< ") -> " << tn
.getRangeType();
1188 Node val
= Node::fromExpr(model
.getSmtEngine()->getValue(n
.toExpr()));
1189 if (options::modelUninterpDtEnum() && val
.getKind() == kind::STORE
)
1191 TypeNode type_node
= val
[1].getType();
1194 if (const std::vector
<Node
>* type_reps
=
1195 model
.getRepSet()->getTypeRepsOrNull(type_node
))
1197 Cardinality
indexCard(type_reps
->size());
1198 val
= theory::arrays::TheoryArraysRewriter::normalizeConstant(
1203 out
<< " = " << val
<< ";" << std::endl
;
1208 void CvcPrinter::toStream(std::ostream
& out
, const Model
& m
) const
1210 // print the model comments
1211 std::stringstream c
;
1214 while (std::getline(c
, ln
))
1216 out
<< "; " << ln
<< std::endl
;
1220 out
<< "MODEL BEGIN" << std::endl
;
1221 this->Printer::toStream(out
, m
);
1222 out
<< "MODEL END;" << std::endl
;
1225 void CvcPrinter::toStream(std::ostream
& out
,
1227 const Command
* command
) const
1229 const auto* theory_model
= dynamic_cast<const theory::TheoryModel
*>(&model
);
1230 AlwaysAssert(theory_model
!= nullptr);
1231 if (const auto* declare_type_command
=
1232 dynamic_cast<const DeclareTypeCommand
*>(command
))
1234 DeclareTypeCommandToStream(out
, *theory_model
, *declare_type_command
);
1236 else if (const auto* dfc
=
1237 dynamic_cast<const DeclareFunctionCommand
*>(command
))
1239 DeclareFunctionCommandToStream(out
, *theory_model
, *dfc
);
1243 out
<< command
<< std::endl
;
1247 static void toStream(std::ostream
& out
, const AssertCommand
* c
, bool cvc3Mode
)
1249 out
<< "ASSERT " << c
->getExpr() << ";";
1252 static void toStream(std::ostream
& out
, const PushCommand
* c
, bool cvc3Mode
)
1257 static void toStream(std::ostream
& out
, const PopCommand
* c
, bool cvc3Mode
)
1262 static void toStream(std::ostream
& out
, const CheckSatCommand
* c
, bool cvc3Mode
)
1264 Expr e
= c
->getExpr();
1269 out
<< "CHECKSAT " << e
<< ";";
1278 static void toStream(std::ostream
& out
,
1279 const CheckSatAssumingCommand
* c
,
1282 const vector
<Expr
>& exprs
= c
->getTerms();
1288 if (exprs
.size() > 0)
1290 out
<< " " << exprs
[0];
1291 for (size_t i
= 1, n
= exprs
.size(); i
< n
; ++i
)
1293 out
<< " AND " << exprs
[i
];
1303 static void toStream(std::ostream
& out
, const QueryCommand
* c
, bool cvc3Mode
)
1305 Expr e
= c
->getExpr();
1310 out
<< "QUERY " << e
<< ";";
1312 out
<< "QUERY TRUE;";
1319 static void toStream(std::ostream
& out
, const ResetCommand
* c
, bool cvc3Mode
)
1324 static void toStream(std::ostream
& out
,
1325 const ResetAssertionsCommand
* c
,
1328 out
<< "RESET ASSERTIONS;";
1331 static void toStream(std::ostream
& out
, const QuitCommand
* c
, bool cvc3Mode
)
1336 static void toStream(std::ostream
& out
, const CommandSequence
* c
, bool cvc3Mode
)
1338 for(CommandSequence::const_iterator i
= c
->begin();
1345 static void toStream(std::ostream
& out
,
1346 const DeclarationSequence
* c
,
1349 DeclarationSequence::const_iterator i
= c
->begin();
1351 DeclarationDefinitionCommand
* dd
=
1352 static_cast<DeclarationDefinitionCommand
*>(*i
++);
1354 out
<< dd
->getSymbol() << ", ";
1362 static void toStream(std::ostream
& out
,
1363 const DeclareFunctionCommand
* c
,
1366 out
<< c
->getSymbol() << " : " << c
->getType() << ";";
1369 static void toStream(std::ostream
& out
,
1370 const DefineFunctionCommand
* c
,
1373 Expr func
= c
->getFunction();
1374 const vector
<Expr
>& formals
= c
->getFormals();
1375 Expr formula
= c
->getFormula();
1376 out
<< func
<< " : " << func
.getType() << " = ";
1377 if(formals
.size() > 0) {
1379 vector
<Expr
>::const_iterator i
= formals
.begin();
1380 while(i
!= formals
.end()) {
1381 out
<< (*i
) << ":" << (*i
).getType();
1382 if(++i
!= formals
.end()) {
1388 out
<< formula
<< ";";
1391 static void toStream(std::ostream
& out
,
1392 const DeclareTypeCommand
* c
,
1395 if(c
->getArity() > 0) {
1397 out
<< "ERROR: Don't know how to print parameterized type declaration "
1398 "in CVC language." << endl
;
1400 out
<< c
->getSymbol() << " : TYPE;";
1404 static void toStream(std::ostream
& out
,
1405 const DefineTypeCommand
* c
,
1408 if(c
->getParameters().size() > 0) {
1409 out
<< "ERROR: Don't know how to print parameterized type definition "
1410 "in CVC language:" << endl
<< c
->toString() << endl
;
1412 out
<< c
->getSymbol() << " : TYPE = " << c
->getType() << ";";
1416 static void toStream(std::ostream
& out
,
1417 const DefineNamedFunctionCommand
* c
,
1420 toStream(out
, static_cast<const DefineFunctionCommand
*>(c
), cvc3Mode
);
1423 static void toStream(std::ostream
& out
, const SimplifyCommand
* c
, bool cvc3Mode
)
1425 out
<< "TRANSFORM " << c
->getTerm() << ";";
1428 static void toStream(std::ostream
& out
, const GetValueCommand
* c
, bool cvc3Mode
)
1430 const vector
<Expr
>& terms
= c
->getTerms();
1431 Assert(!terms
.empty());
1432 out
<< "GET_VALUE ";
1433 copy(terms
.begin(), terms
.end() - 1, ostream_iterator
<Expr
>(out
, ";\nGET_VALUE "));
1434 out
<< terms
.back() << ";";
1437 static void toStream(std::ostream
& out
, const GetModelCommand
* c
, bool cvc3Mode
)
1439 out
<< "COUNTERMODEL;";
1442 static void toStream(std::ostream
& out
,
1443 const GetAssignmentCommand
* c
,
1446 out
<< "% (get-assignment)";
1449 static void toStream(std::ostream
& out
,
1450 const GetAssertionsCommand
* c
,
1456 static void toStream(std::ostream
& out
, const GetProofCommand
* c
, bool cvc3Mode
)
1458 out
<< "DUMP_PROOF;";
1461 static void toStream(std::ostream
& out
,
1462 const GetUnsatCoreCommand
* c
,
1465 out
<< "DUMP_UNSAT_CORE;";
1468 static void toStream(std::ostream
& out
,
1469 const SetBenchmarkStatusCommand
* c
,
1472 out
<< "% (set-info :status " << c
->getStatus() << ")";
1475 static void toStream(std::ostream
& out
,
1476 const SetBenchmarkLogicCommand
* c
,
1479 out
<< "OPTION \"logic\" \"" << c
->getLogic() << "\";";
1482 static void toStream(std::ostream
& out
, const SetInfoCommand
* c
, bool cvc3Mode
)
1484 out
<< "% (set-info " << c
->getFlag() << " ";
1485 OutputLanguage language
=
1486 cvc3Mode
? language::output::LANG_CVC3
: language::output::LANG_CVC4
;
1487 SExpr::toStream(out
, c
->getSExpr(), language
);
1491 static void toStream(std::ostream
& out
, const GetInfoCommand
* c
, bool cvc3Mode
)
1493 out
<< "% (get-info " << c
->getFlag() << ")";
1496 static void toStream(std::ostream
& out
,
1497 const SetOptionCommand
* c
,
1500 out
<< "OPTION \"" << c
->getFlag() << "\" ";
1501 SExpr::toStream(out
, c
->getSExpr(), language::output::LANG_CVC4
);
1505 static void toStream(std::ostream
& out
,
1506 const GetOptionCommand
* c
,
1509 out
<< "% (get-option " << c
->getFlag() << ")";
1512 static void toStream(std::ostream
& out
,
1513 const DatatypeDeclarationCommand
* c
,
1516 const vector
<Type
>& datatypes
= c
->getDatatypes();
1517 Assert(!datatypes
.empty() && datatypes
[0].isDatatype());
1518 const Datatype
& dt0
= DatatypeType(datatypes
[0]).getDatatype();
1519 //do not print tuple/datatype internal declarations
1520 if (datatypes
.size() != 1 || (!dt0
.isTuple() && !dt0
.isRecord()))
1522 out
<< "DATATYPE" << endl
;
1523 bool firstDatatype
= true;
1524 for (const Type
& t
: datatypes
)
1526 if(! firstDatatype
) {
1529 const Datatype
& dt
= DatatypeType(t
).getDatatype();
1530 out
<< " " << dt
.getName();
1531 if(dt
.isParametric()) {
1533 for(size_t j
= 0; j
< dt
.getNumParameters(); ++j
) {
1537 out
<< dt
.getParameter(j
);
1542 bool firstConstructor
= true;
1543 for(Datatype::const_iterator j
= dt
.begin(); j
!= dt
.end(); ++j
) {
1544 if(! firstConstructor
) {
1547 firstConstructor
= false;
1548 const DatatypeConstructor
& cons
= *j
;
1549 out
<< cons
.getName();
1550 if (cons
.getNumArgs() > 0)
1553 bool firstSelector
= true;
1554 for (DatatypeConstructor::const_iterator k
= cons
.begin();
1558 if(! firstSelector
) {
1561 firstSelector
= false;
1562 const DatatypeConstructorArg
& selector
= *k
;
1563 Type tr
= SelectorType(selector
.getType()).getRangeType();
1564 if (tr
.isDatatype())
1566 const Datatype
& sdt
= DatatypeType(tr
).getDatatype();
1567 out
<< selector
.getName() << ": " << sdt
.getName();
1571 out
<< selector
.getName() << ": " << tr
;
1577 firstDatatype
= false;
1579 out
<< endl
<< "END;";
1583 static void toStream(std::ostream
& out
, const CommentCommand
* c
, bool cvc3Mode
)
1585 out
<< "% " << c
->getComment();
1588 static void toStream(std::ostream
& out
, const EmptyCommand
* c
, bool cvc3Mode
) {}
1590 static void toStream(std::ostream
& out
, const EchoCommand
* c
, bool cvc3Mode
)
1592 out
<< "ECHO \"" << c
->getOutput() << "\";";
1596 static bool tryToStream(std::ostream
& out
, const Command
* c
, bool cvc3Mode
)
1598 if(typeid(*c
) == typeid(T
)) {
1599 toStream(out
, dynamic_cast<const T
*>(c
), cvc3Mode
);
1605 static void toStream(std::ostream
& out
, const CommandSuccess
* s
, bool cvc3Mode
)
1607 if(Command::printsuccess::getPrintSuccess(out
)) {
1608 out
<< "OK" << endl
;
1612 static void toStream(std::ostream
& out
,
1613 const CommandUnsupported
* s
,
1616 out
<< "UNSUPPORTED" << endl
;
1619 static void toStream(std::ostream
& out
,
1620 const CommandInterrupted
* s
,
1623 out
<< "INTERRUPTED" << endl
;
1626 static void toStream(std::ostream
& out
, const CommandFailure
* s
, bool cvc3Mode
)
1628 out
<< s
->getMessage() << endl
;
1631 static void toStream(std::ostream
& out
,
1632 const CommandRecoverableFailure
* s
,
1635 out
<< s
->getMessage() << endl
;
1639 static bool tryToStream(std::ostream
& out
,
1640 const CommandStatus
* s
,
1643 if(typeid(*s
) == typeid(T
)) {
1644 toStream(out
, dynamic_cast<const T
*>(s
), cvc3Mode
);
1650 }/* CVC4::printer::cvc namespace */
1651 }/* CVC4::printer namespace */
1652 }/* CVC4 namespace */