diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-13 02:49:35 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-13 02:49:35 +0000 |
commit | 9b4696559cd2c74afb825d793614eb4cd6ee817e (patch) | |
tree | a83bd5b4aac7fe1aa8160f9de7721e85a218b3ef /src/printer | |
parent | 134c6dc95199bc57013d07e0992f89254f49038b (diff) |
Fixes lots of problems in bv rewrite rules and adds lots of assertions
to catch any that I may have missed
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 50 |
1 files changed, 40 insertions, 10 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 76c4f0abc..e4a25e008 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -483,18 +483,33 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << "@"; opType = INFIX; break; - case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_PLUS: { //This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB - out << "BVPLUS("; Assert(n.getType().isBitVector()); + unsigned numc = n.getNumChildren()-2; + unsigned child = 0; + while (child < numc) { + out << "BVPLUS("; + out << BitVectorType(n.getType().toType()).getSize(); + out << ','; + toStream(out, n[child], depth, types, false); + out << ','; + ++child; + } + out << "BVPLUS("; out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[0], depth, types, false); - out << ','; - toStream(out, n[1], depth, types, false); + toStream(out, n[child], depth, types, false); + out << ','; + toStream(out, n[child+1], depth, types, false); + while (child > 0) { + out << ')'; + --child; + } out << ')'; return; break; + } case kind::BITVECTOR_SUB: out << "BVSUB("; Assert(n.getType().isBitVector()); @@ -506,17 +521,32 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << ')'; return; break; - case kind::BITVECTOR_MULT: - out << "BVMULT("; + case kind::BITVECTOR_MULT: { Assert(n.getType().isBitVector()); + unsigned numc = n.getNumChildren()-2; + unsigned child = 0; + while (child < numc) { + out << "BVMULT("; + out << BitVectorType(n.getType().toType()).getSize(); + out << ','; + toStream(out, n[child], depth, types, false); + out << ','; + ++child; + } + out << "BVMULT("; out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[0], depth, types, false); - out << ','; - toStream(out, n[1], depth, types, false); + toStream(out, n[child], depth, types, false); + out << ','; + toStream(out, n[child+1], depth, types, false); + while (child > 0) { + out << ')'; + --child; + } out << ')'; return; break; + } case kind::BITVECTOR_EXTRACT: op << n.getOperator().getConst<BitVectorExtract>(); opType = POSTFIX; |