diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-06-05 09:54:51 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-05 09:54:51 -0300 |
commit | 80b0795702e71d54ed7c17ba809eebde628eb516 (patch) | |
tree | d9950f742d4763b520185d4f27aa666d67509429 /src/printer | |
parent | 60746dc3ac7806475b5b6dab03123df024bf613e (diff) |
Printing FP values as binary or indexed BVs according to option (#4554)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 28 |
1 files changed, 9 insertions, 19 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 0c0c4c3a8..6670fa065 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -146,31 +146,25 @@ void Smt2Printer::toStream(std::ostream& out, << n.getConst<FloatingPointSize>().significand() << ")"; break; - case kind::CONST_BITVECTOR: { + case kind::CONST_BITVECTOR: + { const BitVector& bv = n.getConst<BitVector>(); - const Integer& x = bv.getValue(); - unsigned width = bv.getSize(); - if (d_variant == sygus_variant || options::bvPrintConstsInBinary()) + if (options::bvPrintConstsAsIndexedSymbols()) { - out << "#b" << bv.toString(); + out << "(_ bv" << bv.getValue() << " " << bv.getSize() << ")"; } else { - out << "(_ "; - out << "bv" << x << " " << width; - out << ")"; + out << "#b" << bv.toString(); } - - // //out << "#b"; - - // while(n-- > 0) { - // out << (x.testBit(n) ? '1' : '0'); - // } break; } case kind::CONST_FLOATINGPOINT: - out << n.getConst<FloatingPoint>(); + { + out << n.getConst<FloatingPoint>().toString( + options::bvPrintConstsAsIndexedSymbols()); break; + } case kind::CONST_ROUNDINGMODE: switch (n.getConst<RoundingMode>()) { case roundNearestTiesToEven : out << "roundNearestTiesToEven"; break; @@ -292,26 +286,22 @@ void Smt2Printer::toStream(std::ostream& out, out << "(_ int2bv " << n.getConst<IntToBitVector>().d_size << ")"; break; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: - // out << "to_fp_bv " out << "(_ to_fp " << n.getConst<FloatingPointToFPIEEEBitVector>().t.exponent() << ' ' << n.getConst<FloatingPointToFPIEEEBitVector>().t.significand() << ")"; break; case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: - // out << "to_fp_fp " out << "(_ to_fp " << n.getConst<FloatingPointToFPFloatingPoint>().t.exponent() << ' ' << n.getConst<FloatingPointToFPFloatingPoint>().t.significand() << ")"; break; case kind::FLOATINGPOINT_TO_FP_REAL_OP: - // out << "to_fp_real " out << "(_ to_fp " << n.getConst<FloatingPointToFPReal>().t.exponent() << ' ' << n.getConst<FloatingPointToFPReal>().t.significand() << ")"; break; case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: - // out << "to_fp_signed " out << "(_ to_fp " << n.getConst<FloatingPointToFPSignedBitVector>().t.exponent() << ' ' << n.getConst<FloatingPointToFPSignedBitVector>().t.significand() |