diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-18 16:53:18 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-18 16:53:23 -0400 |
| commit | aa16fb32ac7a66e327f32ea4c794a3ccf832c587 (patch) | |
| tree | cdb11834a67cfa393311028d06addaef265590b2 /src/printer | |
| parent | 066191d91d9f42f34a412162203be818e202aeba (diff) | |
Support for bv2nat/int2bv in parser and BV rewriter.
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 7b25c6fd9..756e521a6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -304,6 +304,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BITVECTOR_SLE: out << "bvsle "; break; case kind::BITVECTOR_SGT: out << "bvsgt "; break; case kind::BITVECTOR_SGE: out << "bvsge "; break; + case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break; case kind::BITVECTOR_EXTRACT: case kind::BITVECTOR_REPEAT: @@ -311,6 +312,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BITVECTOR_SIGN_EXTEND: case kind::BITVECTOR_ROTATE_LEFT: case kind::BITVECTOR_ROTATE_RIGHT: + case kind::INT_TO_BITVECTOR: printBvParameterizedOp(out, n); out << ' '; stillNeedToPrintParams = false; @@ -535,6 +537,10 @@ static void printBvParameterizedOp(std::ostream& out, TNode n) throw() { out << "rotate_right " << n.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount; break; + case kind::INT_TO_BITVECTOR: + out << "int2bv " + << n.getOperator().getConst<IntToBitVector>().size; + break; default: out << n.getKind(); } |