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.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index e69c9a1de8e1402b8fc52efba09dd714184d0a8d..7db0e41db4fac6b173bade3c9140e7f311e65ee6 100644 (file)
--- 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>(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>(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>(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>(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>(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>(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>(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 5d14e76a1f505cc525f672fd8e155fb1ea8bc21e..7e91b3b99e405ef2d6992947c1fb27858686f0ba 100644 (file)
--- 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 d10813f580bd76f69c2974b816d3cf9514d04b88..9837d6b00db986a8bcadd3d2310e694e2a727319 100644 (file)
--- 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&);