diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-11-17 16:45:39 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-17 16:45:39 -0800 |
| commit | 4bdba195950858dc1b2b9afa80d216dc58c66b68 (patch) | |
| tree | 7f8a2082fc3739d8d8f04e67cb893abd3ed7c0cc /src/api | |
| parent | 7ffc3650a44859a51384eebbecb51bf199495102 (diff) | |
FloatingPoint: Clean up and document header, format. (#5453)
This cleans up the src/util/floatingpoint.h.in header to conform to the
code style guidelines of CVC4. This further attempts to fully document
the header. The main changes (except for added documentation) are
renames of member variables, getting rid of the redundant functions
FloatingPointSize::exponent() and FloatingPointSize::significand(),
and a more explicit naming of CVC4 wrapper types vs symFPU trait
types. Else, it's mainly reordering and formatting.
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 24902b888..a7cc8e17f 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1433,10 +1433,10 @@ uint32_t Op::getIndices() const case INT_TO_BITVECTOR: i = d_node->getConst<IntToBitVector>().d_size; break; case IAND: i = d_node->getConst<IntAnd>().d_size; break; case FLOATINGPOINT_TO_UBV: - i = d_node->getConst<FloatingPointToUBV>().bvs.d_size; + i = d_node->getConst<FloatingPointToUBV>().d_bv_size.d_size; break; case FLOATINGPOINT_TO_SBV: - i = d_node->getConst<FloatingPointToSBV>().bvs.d_size; + i = d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size; break; case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break; case REGEXP_REPEAT: @@ -1469,36 +1469,42 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const { CVC4::FloatingPointToFPIEEEBitVector ext = d_node->getConst<FloatingPointToFPIEEEBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) { CVC4::FloatingPointToFPFloatingPoint ext = d_node->getConst<FloatingPointToFPFloatingPoint>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_REAL) { CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) { CVC4::FloatingPointToFPSignedBitVector ext = d_node->getConst<FloatingPointToFPSignedBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) { CVC4::FloatingPointToFPUnsignedBitVector ext = d_node->getConst<FloatingPointToFPUnsignedBitVector>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_GENERIC) { CVC4::FloatingPointToFPGeneric ext = d_node->getConst<FloatingPointToFPGeneric>(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == REGEXP_LOOP) { |