From 1c859fd0f43fa2081bdb247423e81d9174a5f474 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 11 Aug 2020 12:58:28 -0700 Subject: [PATCH] New C++ API: Remove redundant API functions for mkReal. (#4870) This further removes redundant API functions with a `const char*` parameter. These are redundant (and can create ambiguity) since they have `const string&` counterparts. --- src/api/cvc4cpp.cpp | 89 ++--------------------------------- src/api/cvc4cpp.h | 90 +----------------------------------- test/unit/api/solver_black.h | 2 - 3 files changed, 4 insertions(+), 177 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index e69c9a1de..7db0e41db 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3451,16 +3451,6 @@ Term Solver::mkPi() const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkReal(const char* s) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULLPTR(s); - - return mkRealFromStrHelper(std::string(s)); - - CVC4_API_SOLVER_TRY_CATCH_END; -} - Term Solver::mkReal(const std::string& s) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3468,13 +3458,6 @@ Term Solver::mkReal(const std::string& s) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkReal(int32_t val) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper(CVC4::Rational(val)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - Term Solver::mkReal(int64_t val) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3482,27 +3465,6 @@ Term Solver::mkReal(int64_t val) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkReal(uint32_t val) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper(CVC4::Rational(val)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Term Solver::mkReal(uint64_t val) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper(CVC4::Rational(val)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Term Solver::mkReal(int32_t num, int32_t den) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper(CVC4::Rational(num, den)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - Term Solver::mkReal(int64_t num, int64_t den) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3510,20 +3472,6 @@ Term Solver::mkReal(int64_t num, int64_t den) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkReal(uint32_t num, uint32_t den) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper(CVC4::Rational(num, den)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Term Solver::mkReal(uint64_t num, uint64_t den) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper(CVC4::Rational(num, den)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - Term Solver::mkRegexpEmpty() const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3575,13 +3523,6 @@ Term Solver::mkSepNil(Sort sort) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkString(const char* s, bool useEscSequences) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - return mkValHelper(CVC4::String(s, useEscSequences)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - Term Solver::mkString(const std::string& s, bool useEscSequences) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3610,14 +3551,6 @@ Term Solver::mkChar(const std::string& s) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkChar(const char* s) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULLPTR(s); - return mkCharFromStrHelper(std::string(s)); - CVC4_API_SOLVER_TRY_CATCH_END; -} - Term Solver::mkEmptySequence(Sort sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3654,16 +3587,6 @@ Term Solver::mkBitVector(uint32_t size, uint64_t val) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkBitVector(const char* s, uint32_t base) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULLPTR(s); - - return mkBVFromStrHelper(std::string(s), base); - - CVC4_API_SOLVER_TRY_CATCH_END; -} - Term Solver::mkBitVector(const std::string& s, uint32_t base) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3671,15 +3594,9 @@ Term Solver::mkBitVector(const std::string& s, uint32_t base) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkBitVector(uint32_t size, const char* s, uint32_t base) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_NOT_NULLPTR(s); - return mkBVFromStrHelper(size, s, base); - CVC4_API_SOLVER_TRY_CATCH_END; -} - -Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const +Term Solver::mkBitVector(uint32_t size, + const std::string& s, + uint32_t base) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; return mkBVFromStrHelper(size, s, base); diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 5d14e76a1..7e91b3b99 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2510,14 +2510,6 @@ class CVC4_PUBLIC Solver */ Term mkPi() const; - /** - * Create a real constant from a string. - * @param s the string representation of the constant, may represent an - * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34"). - * @return a constant of sort Real or Integer (if 's' represents an integer) - */ - Term mkReal(const char* s) const; - /** * Create a real constant from a string. * @param s the string representation of the constant, may represent an @@ -2526,13 +2518,6 @@ class CVC4_PUBLIC Solver */ Term mkReal(const std::string& s) const; - /** - * Create a real constant from an integer. - * @param val the value of the constant - * @return a constant of sort Integer - */ - Term mkReal(int32_t val) const; - /** * Create a real constant from an integer. * @param val the value of the constant @@ -2540,28 +2525,6 @@ class CVC4_PUBLIC Solver */ Term mkReal(int64_t val) const; - /** - * Create a real constant from an unsigned integer. - * @param val the value of the constant - * @return a constant of sort Integer - */ - Term mkReal(uint32_t val) const; - - /** - * Create a real constant from an unsigned integer. - * @param val the value of the constant - * @return a constant of sort Integer - */ - Term mkReal(uint64_t val) const; - - /** - * Create a real constant from a rational. - * @param num the value of the numerator - * @param den the value of the denominator - * @return a constant of sort Real or Integer (if 'num' is divisible by 'den') - */ - Term mkReal(int32_t num, int32_t den) const; - /** * Create a real constant from a rational. * @param num the value of the numerator @@ -2570,22 +2533,6 @@ class CVC4_PUBLIC Solver */ Term mkReal(int64_t num, int64_t den) const; - /** - * Create a real constant from a rational. - * @param num the value of the numerator - * @param den the value of the denominator - * @return a constant of sort Real or Integer (if 'num' is divisible by 'den') - */ - Term mkReal(uint32_t num, uint32_t den) const; - - /** - * Create a real constant from a rational. - * @param num the value of the numerator - * @param den the value of the denominator - * @return a constant of sort Real or Integer (if 'num' is divisible by 'den') - */ - Term mkReal(uint64_t num, uint64_t den) const; - /** * Create a regular expression empty term. * @return the empty term @@ -2612,15 +2559,6 @@ class CVC4_PUBLIC Solver */ Term mkSepNil(Sort sort) const; - /** - * Create a String constant. - * @param s the string this constant represents - * @param useEscSequences determines whether escape sequences in \p s should - * be converted to the corresponding character - * @return the String constant - */ - Term mkString(const char* s, bool useEscSequences = false) const; - /** * Create a String constant. * @param s the string this constant represents @@ -2651,13 +2589,6 @@ class CVC4_PUBLIC Solver */ Term mkChar(const std::string& s) const; - /** - * Create a character constant from a given string. - * @param s the string denoting the code point of the character (in base 16) - * @return the character constant - */ - Term mkChar(const char* s) const; - /** * Create an empty sequence of the given element sort. * @param sort The element sort of the sequence. @@ -2680,14 +2611,6 @@ class CVC4_PUBLIC Solver */ Term mkBitVector(uint32_t size, uint64_t val = 0) const; - /** - * Create a bit-vector constant from a given string. - * @param s the string representation of the constant - * @param base the base of the string representation (2, 10, or 16) - * @return the bit-vector constant - */ - Term mkBitVector(const char* s, uint32_t base = 2) const; - /** * Create a bit-vector constant from a given string of base 2, 10 or 16. * @@ -2703,17 +2626,6 @@ class CVC4_PUBLIC Solver */ Term mkBitVector(const std::string& s, uint32_t base = 2) const; - /** - * Create a bit-vector constant of a given bit-width from a given string of - * base 2, 10 or 16. - * - * @param size the bit-width of the constant - * @param s the string representation of the constant - * @param base the base of the string representation (2, 10, or 16) - * @return the bit-vector constant - */ - Term mkBitVector(uint32_t size, const char* s, uint32_t base) const; - /** * Create a bit-vector constant of a given bit-width from a given string of * base 2, 10 or 16. @@ -2722,7 +2634,7 @@ class CVC4_PUBLIC Solver * @param base the base of the string representation (2, 10, or 16) * @return the bit-vector constant */ - Term mkBitVector(uint32_t size, std::string& s, uint32_t base) const; + Term mkBitVector(uint32_t size, const std::string& s, uint32_t base) const; /** * Create a constant array with the provided constant value stored at every diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index d10813f58..9837d6b00 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -661,7 +661,6 @@ void SolverBlack::testMkReal() TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("12/3")); TS_ASSERT_THROWS_NOTHING(d_solver->mkReal(".2")); TS_ASSERT_THROWS_NOTHING(d_solver->mkReal("2.")); - TS_ASSERT_THROWS(d_solver->mkReal(nullptr), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkReal(""), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkReal("asdf"), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkReal("1.2/3"), CVC4ApiException&); @@ -737,7 +736,6 @@ void SolverBlack::testMkChar() { TS_ASSERT_THROWS_NOTHING(d_solver->mkChar(std::string("0123"))); TS_ASSERT_THROWS_NOTHING(d_solver->mkChar("aA")); - TS_ASSERT_THROWS(d_solver->mkChar(nullptr), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkChar(""), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkChar("0g0"), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkChar("100000"), CVC4ApiException&); -- 2.30.2