diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-25 12:18:51 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-25 19:18:51 +0000 |
| commit | 99a74de90a064133a8e3d03ee9334d59be34ba1d (patch) | |
| tree | 3d18d56a020b1dbd2b7dfed0b763524324285c24 /src/printer | |
| parent | 8a3876f74f377817345af405aebfceebc7896059 (diff) | |
FP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206)
This pushes all symfpu specific parts from FloatingPoint into
FloatingPointLiteral. FloatingPoint is now generic. An additional
FloatingPointLiteral implementation using MPFR will be made configurable
similiarly to how we handle Integers with either GMP or CLN backend.
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 32 |
1 files changed, 20 insertions, 12 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e1a4058e8..3e99267cc 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -344,51 +344,59 @@ void Smt2Printer::toStream(std::ostream& out, case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: out << "(_ to_fp " << n.getConst<FloatingPointToFPIEEEBitVector>() - .d_fp_size.exponentWidth() + .getSize() + .exponentWidth() << ' ' << n.getConst<FloatingPointToFPIEEEBitVector>() - .d_fp_size.significandWidth() + .getSize() + .significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: out << "(_ to_fp " << n.getConst<FloatingPointToFPFloatingPoint>() - .d_fp_size.exponentWidth() + .getSize() + .exponentWidth() << ' ' << n.getConst<FloatingPointToFPFloatingPoint>() - .d_fp_size.significandWidth() + .getSize() + .significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_REAL_OP: out << "(_ to_fp " - << n.getConst<FloatingPointToFPReal>().d_fp_size.exponentWidth() + << n.getConst<FloatingPointToFPReal>().getSize().exponentWidth() << ' ' - << n.getConst<FloatingPointToFPReal>().d_fp_size.significandWidth() + << n.getConst<FloatingPointToFPReal>().getSize().significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: out << "(_ to_fp " << n.getConst<FloatingPointToFPSignedBitVector>() - .d_fp_size.exponentWidth() + .getSize() + .exponentWidth() << ' ' << n.getConst<FloatingPointToFPSignedBitVector>() - .d_fp_size.significandWidth() + .getSize() + .significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: out << "(_ to_fp_unsigned " << n.getConst<FloatingPointToFPUnsignedBitVector>() - .d_fp_size.exponentWidth() + .getSize() + .exponentWidth() << ' ' << n.getConst<FloatingPointToFPUnsignedBitVector>() - .d_fp_size.significandWidth() + .getSize() + .significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: out << "(_ to_fp " - << n.getConst<FloatingPointToFPGeneric>().d_fp_size.exponentWidth() + << n.getConst<FloatingPointToFPGeneric>().getSize().exponentWidth() << ' ' - << n.getConst<FloatingPointToFPGeneric>().d_fp_size.significandWidth() + << n.getConst<FloatingPointToFPGeneric>().getSize().significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_UBV_OP: |