diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-18 19:08:11 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-18 19:08:11 +0000 |
commit | d1ba1ccd5a3c55ba7a0e63b33fd921642e44752d (patch) | |
tree | f3d22cdd12076a488dff2e9176dd1f619c731902 /src/printer | |
parent | 267858307741675cb78e829270e619f57cf21a27 (diff) |
more work on CVC language
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 39 |
1 files changed, 29 insertions, 10 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index c3253d05a..97f434e9b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -144,13 +144,36 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, return; } else if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { - out << n.getOperator(); - if(n.getNumChildren() > 0) { - out << '('; - if(n.getNumChildren() > 1) { - copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ", ")); + switch(n.getKind()) { + case kind::BITVECTOR_EXTRACT: + out << n[0] << n.getOperator().getConst<BitVectorExtract>(); + break; + case kind::BITVECTOR_REPEAT: + out << "BVREPEAT(" << n[0] << "," << n.getOperator() << ')'; + break; + case kind::BITVECTOR_ZERO_EXTEND: + out << "BVZEROEXTEND(" << n[0] << "," << n.getOperator() << ')'; + break; + case kind::BITVECTOR_SIGN_EXTEND: + out << "SX(" << n[0] << "," << n.getOperator() << ')'; + break; + case kind::BITVECTOR_ROTATE_LEFT: + out << "BVROTL(" << n[0] << "," << n.getOperator() << ')'; + break; + case kind::BITVECTOR_ROTATE_RIGHT: + out << "BVROTR(" << n[0] << "," << n.getOperator() << ')'; + break; + + + default: + out << n.getOperator(); + if(n.getNumChildren() > 0) { + out << '('; + if(n.getNumChildren() > 1) { + copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ", ")); + } + out << n[n.getNumChildren() - 1] << ')'; } - out << n[n.getNumChildren() - 1] << ')'; } return; } else if(n.getMetaKind() == kind::metakind::OPERATOR) { @@ -220,10 +243,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, out << n.getOperator() << '(' << n[0] << ',' << n[1] << ')'; break; - case kind::BITVECTOR_EXTRACT: - out << n[0] << '[' << n.getOperator().getConst<BitVectorExtract>() << ']'; - break; - default: if(k == kind::NOT && n[0].getKind() == kind::EQUAL) { // collapse NOT-over-EQUAL |