diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-10-20 12:14:59 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-20 19:14:59 +0000 |
| commit | 68fc65dfb303d75eab953523744103ba2b65ac8e (patch) | |
| tree | 62ef6226a6ebab50b2739d90d9238ffd84850daf /src/api/cpp/cvc5.cpp | |
| parent | 5f97877e517f024f6d44d3201f5214853d04cc26 (diff) | |
api: Rename get(BV|FP)*Size functions for consistency. (#7428)
Diffstat (limited to 'src/api/cpp/cvc5.cpp')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 778f700c0..f6a1eed17 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1682,7 +1682,7 @@ size_t Sort::getSortConstructorArity() const /* Bit-vector sort ----------------------------------------------------- */ -uint32_t Sort::getBVSize() const +uint32_t Sort::getBitVectorSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -1695,7 +1695,7 @@ uint32_t Sort::getBVSize() const /* Floating-point sort ------------------------------------------------- */ -uint32_t Sort::getFPExponentSize() const +uint32_t Sort::getFloatingPointExponentSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -1706,7 +1706,7 @@ uint32_t Sort::getFPExponentSize() const CVC5_API_TRY_CATCH_END; } -uint32_t Sort::getFPSignificandSize() const +uint32_t Sort::getFloatingPointSignificandSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -6030,10 +6030,11 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0"; uint32_t bw = exp + sig; - CVC5_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val) + CVC5_API_ARG_CHECK_EXPECTED(bw == val.d_node->getType().getBitVectorSize(), + val) << "a bit-vector constant with bit-width '" << bw << "'"; CVC5_API_ARG_CHECK_EXPECTED( - val.getSort().isBitVector() && val.d_node->isConst(), val) + val.d_node->getType().isBitVector() && val.d_node->isConst(), val) << "bit-vector constant"; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( |