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/api | |
| 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/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index dce190460..f33095a4b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1920,42 +1920,42 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const { CVC4::FloatingPointToFPIEEEBitVector ext = d_node->getConst<FloatingPointToFPIEEEBitVector>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) { CVC4::FloatingPointToFPFloatingPoint ext = d_node->getConst<FloatingPointToFPFloatingPoint>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_REAL) { CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) { CVC4::FloatingPointToFPSignedBitVector ext = d_node->getConst<FloatingPointToFPSignedBitVector>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) { CVC4::FloatingPointToFPUnsignedBitVector ext = d_node->getConst<FloatingPointToFPUnsignedBitVector>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_GENERIC) { CVC4::FloatingPointToFPGeneric ext = d_node->getConst<FloatingPointToFPGeneric>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == REGEXP_LOOP) { |