diff options
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 65117c9db..afbd7ee58 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -25,9 +25,11 @@ #include <vector> #include "expr/dtype.h" -#include "expr/expr.h" // for ExprSetDepth etc.. +#include "expr/expr.h" // for ExprSetDepth etc.. +#include "expr/expr_sequence.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "expr/node_visitor.h" +#include "expr/sequence.h" #include "options/language.h" // for LANG_AST #include "options/smt_options.h" #include "printer/dagification_visitor.h" @@ -165,6 +167,30 @@ void CvcPrinter::toStream( out << '"' << n.getConst<String>().toString() << '"'; break; } + case kind::CONST_SEQUENCE: + { + const Sequence& sn = n.getConst<ExprSequence>().getSequence(); + const std::vector<Node>& snvec = sn.getVec(); + if (snvec.size() > 1) + { + out << "CONCAT("; + } + bool first = true; + for (const Node& snvc : snvec) + { + if (!first) + { + out << ", "; + } + out << "SEQ_UNIT(" << snvc << ")"; + first = false; + } + if (snvec.size() > 1) + { + out << ")"; + } + break; + } case kind::TYPE_CONSTANT: switch(TypeConstant tc = n.getConst<TypeConstant>()) { case REAL_TYPE: |