From 1c859fd0f43fa2081bdb247423e81d9174a5f474 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 11 Aug 2020 12:58:28 -0700 Subject: 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.h | 90 +------------------------------------------------------ 1 file changed, 1 insertion(+), 89 deletions(-) (limited to 'src/api/cvc4cpp.h') 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 -- cgit v1.2.3