diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/didyoumean.cpp | 6 | ||||
-rw-r--r-- | src/util/hash.h | 5 | ||||
-rw-r--r-- | src/util/integer_cln_imp.cpp | 57 | ||||
-rw-r--r-- | src/util/integer_cln_imp.h | 12 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.cpp | 97 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 16 | ||||
-rw-r--r-- | src/util/string.cpp | 15 | ||||
-rw-r--r-- | src/util/string.h | 11 |
8 files changed, 175 insertions, 44 deletions
diff --git a/src/util/didyoumean.cpp b/src/util/didyoumean.cpp index 0f95722fd..f4dbbbd36 100644 --- a/src/util/didyoumean.cpp +++ b/src/util/didyoumean.cpp @@ -37,7 +37,7 @@ uint64_t editDistance(const std::string& a, const std::string& b) { constexpr uint64_t swapCost = 0; constexpr uint64_t substituteCost = 2; constexpr uint64_t addCost = 1; - constexpr uint64_t deleteCost = 3; + constexpr uint64_t deleteCost = 2; constexpr uint64_t switchCaseCost = 0; uint64_t len1 = a.size(); @@ -104,7 +104,7 @@ std::vector<std::string> DidYouMean::getMatch(const std::string& input) } /** Magic numbers */ - constexpr uint64_t similarityThreshold = 7; + constexpr uint64_t similarityThreshold = 10; constexpr uint64_t numMatchesThreshold = 10; std::vector<std::pair<uint64_t,std::string>> scores; @@ -127,7 +127,7 @@ std::vector<std::string> DidYouMean::getMatch(const std::string& input) // from here on, matches are not similar enough if (score.first > similarityThreshold) break; // from here on, matches are way worse than the best one - if (score.first > min_score + 2) break; + if (score.first > min_score + 4) break; // we already have enough matches if (ret.size() >= numMatchesThreshold) break; ret.push_back(score.second); diff --git a/src/util/hash.h b/src/util/hash.h index db280984b..ef8bf4a2a 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -43,12 +43,15 @@ namespace cvc5 { namespace fnv1a { +constexpr uint64_t offsetBasis = 14695981039346656037U; + /** * FNV-1a hash algorithm for 64-bit numbers. * * More details here: http://www.isthe.com/chongo/tech/comp/fnv/index.html */ -inline uint64_t fnv1a_64(uint64_t v, uint64_t hash = 14695981039346656037U) { +inline uint64_t fnv1a_64(uint64_t v, uint64_t hash = offsetBasis) +{ hash ^= v; // Compute (hash * 1099511628211) return hash + (hash << 1) + (hash << 4) + (hash << 5) + (hash << 7) + diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index e09708ae5..149e02edc 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -483,16 +483,6 @@ unsigned int Integer::getUnsignedInt() const return cln::cl_I_to_uint(d_value); } -bool Integer::fitsSignedLong() const -{ - return d_value <= s_signedLongMax && d_value >= s_signedLongMin; -} - -bool Integer::fitsUnsignedLong() const -{ - return sgn() >= 0 && d_value <= s_unsignedLongMax; -} - long Integer::getLong() const { // ensure there isn't overflow @@ -517,6 +507,53 @@ unsigned long Integer::getUnsignedLong() const return cln::cl_I_to_ulong(d_value); } +int64_t Integer::getSigned64() const +{ + if constexpr (sizeof(int64_t) == sizeof(signed long int)) + { + return getLong(); + } + else + { + if (std::numeric_limits<long>::min() <= d_value + && d_value <= std::numeric_limits<long>::max()) + { + return getLong(); + } + // ensure there isn't overflow + CheckArgument(d_value <= std::numeric_limits<int64_t>::max(), + this, + "Overflow detected in Integer::getSigned64()"); + CheckArgument(d_value >= std::numeric_limits<int64_t>::min(), + this, + "Overflow detected in Integer::getSigned64()"); + return std::stoll(toString()); + } +} +uint64_t Integer::getUnsigned64() const +{ + if constexpr (sizeof(uint64_t) == sizeof(unsigned long int)) + { + return getUnsignedLong(); + } + else + { + if (std::numeric_limits<unsigned long>::min() <= d_value + && d_value <= std::numeric_limits<unsigned long>::max()) + { + return getUnsignedLong(); + } + // ensure there isn't overflow + CheckArgument(d_value <= std::numeric_limits<uint64_t>::max(), + this, + "Overflow detected in Integer::getSigned64()"); + CheckArgument(d_value >= std::numeric_limits<uint64_t>::min(), + this, + "Overflow detected in Integer::getSigned64()"); + return std::stoull(toString()); + } +} + size_t Integer::hash() const { return equal_hashcode(d_value); } bool Integer::testBit(unsigned n) const { return cln::logbitp(n, d_value); } diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 2120a4d5d..333d8f502 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -274,18 +274,18 @@ class CVC5_EXPORT Integer /** Return the unsigned int representation of this Integer. */ unsigned int getUnsignedInt() const; - /** Return true if this Integer fits into a signed long. */ - bool fitsSignedLong() const; - - /** Return true if this Integer fits into an unsigned long. */ - bool fitsUnsignedLong() const; - /** Return the signed long representation of this Integer. */ long getLong() const; /** Return the unsigned long representation of this Integer. */ unsigned long getUnsignedLong() const; + /** Return the int64_t representation of this Integer. */ + int64_t getSigned64() const; + + /** Return the uint64_t representation of this Integer. */ + uint64_t getUnsigned64() const; + /** * Computes the hash of the node from the first word of the * numerator, the denominator. diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index f33a90408..8d9f7d050 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -14,6 +14,7 @@ */ #include <cmath> +#include <limits> #include <sstream> #include <string> @@ -38,6 +39,33 @@ Integer::Integer(const std::string& s, unsigned base) : d_value(s, base) {} +#ifdef CVC5_NEED_INT64_T_OVERLOADS +Integer::Integer(int64_t z) +{ + if (std::numeric_limits<signed long int>::min() <= z + && z <= std::numeric_limits<signed long int>::max()) + { + d_value = static_cast<signed long int>(z); + } + else + { + d_value = std::to_string(z); + } +} +Integer::Integer(uint64_t z) +{ + if (std::numeric_limits<unsigned long int>::min() <= z + && z <= std::numeric_limits<unsigned long int>::max()) + { + d_value = static_cast<unsigned long int>(z); + } + else + { + d_value = std::to_string(z); + } +} +#endif /* CVC5_NEED_INT64_T_OVERLOADS */ + Integer& Integer::operator=(const Integer& x) { if (this == &x) return *this; @@ -402,28 +430,73 @@ unsigned int Integer::getUnsignedInt() const return (unsigned int)d_value.get_ui(); } -bool Integer::fitsSignedLong() const { return d_value.fits_slong_p(); } - -bool Integer::fitsUnsignedLong() const { return d_value.fits_ulong_p(); } - long Integer::getLong() const { - long si = d_value.get_si(); - // ensure there wasn't overflow - CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, + // ensure there it fits + CheckArgument(mpz_fits_slong_p(d_value.get_mpz_t()) != 0, this, "Overflow detected in Integer::getLong()."); - return si; + return d_value.get_si(); } unsigned long Integer::getUnsignedLong() const { - unsigned long ui = d_value.get_ui(); - // ensure there wasn't overflow - CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, + // ensure that it fits + CheckArgument(mpz_fits_ulong_p(d_value.get_mpz_t()) != 0, this, "Overflow detected in Integer::getUnsignedLong()."); - return ui; + return d_value.get_ui(); +} + +int64_t Integer::getSigned64() const +{ + if constexpr (sizeof(int64_t) == sizeof(signed long int)) + { + return getLong(); + } + else + { + if (mpz_fits_slong_p(d_value.get_mpz_t()) != 0) + { + return getLong(); + } + try + { + return std::stoll(toString()); + } + catch (const std::exception& e) + { + CheckArgument( + false, this, "Overflow detected in Integer::getSigned64()."); + } + } + return 0; +} +uint64_t Integer::getUnsigned64() const +{ + if constexpr (sizeof(uint64_t) == sizeof(unsigned long int)) + { + return getUnsignedLong(); + } + else + { + if (mpz_fits_ulong_p(d_value.get_mpz_t()) != 0) + { + return getUnsignedLong(); + } + try + { + CheckArgument( + sgn() >= 0, this, "Overflow detected in Integer::getUnsigned64()."); + return std::stoull(toString()); + } + catch (const std::exception& e) + { + CheckArgument( + false, this, "Overflow detected in Integer::getUnsigned64()."); + } + } + return 0; } size_t Integer::hash() const { return gmpz_hash(d_value.get_mpz_t()); } diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index ff2ea9815..397455f87 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -59,8 +59,8 @@ class CVC5_EXPORT Integer Integer(unsigned long int z) : d_value(z) {} #ifdef CVC5_NEED_INT64_T_OVERLOADS - Integer(int64_t z) : d_value(static_cast<long>(z)) {} - Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {} + Integer(int64_t z); + Integer(uint64_t z); #endif /* CVC5_NEED_INT64_T_OVERLOADS */ /** Destructor. */ @@ -257,18 +257,18 @@ class CVC5_EXPORT Integer /** Return the unsigned int representation of this Integer. */ unsigned int getUnsignedInt() const; - /** Return true if this Integer fits into a signed long. */ - bool fitsSignedLong() const; - - /** Return true if this Integer fits into an unsigned long. */ - bool fitsUnsignedLong() const; - /** Return the signed long representation of this Integer. */ long getLong() const; /** Return the unsigned long representation of this Integer. */ unsigned long getUnsignedLong() const; + /** Return the int64_t representation of this Integer. */ + int64_t getSigned64() const; + + /** Return the uint64_t representation of this Integer. */ + uint64_t getUnsigned64() const; + /** * Computes the hash of the node from the first word of the * numerator, the denominator. diff --git a/src/util/string.cpp b/src/util/string.cpp index 50b0a7199..2235ac5ee 100644 --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -23,6 +23,7 @@ #include "base/check.h" #include "base/exception.h" +#include "util/hash.h" using namespace std; @@ -519,6 +520,20 @@ Rational String::toNumber() const return Rational(toString()); } +namespace strings { + +size_t StringHashFunction::operator()(const ::cvc5::String& s) const +{ + uint64_t ret = fnv1a::offsetBasis; + for (unsigned c : s.d_str) + { + ret = fnv1a::fnv1a_64(c, ret); + } + return static_cast<size_t>(ret); +} + +} // namespace strings + std::ostream &operator<<(std::ostream &os, const String &s) { return os << "\"" << s.toString() << "\""; } diff --git a/src/util/string.h b/src/util/string.h index 3f6384082..017c60fb8 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -26,6 +26,10 @@ namespace cvc5 { +namespace strings { +struct StringHashFunction; +} + /** The cvc5 string class * * This data structure is the domain of values for the string type. It can also @@ -33,6 +37,8 @@ namespace cvc5 { */ class String { + friend strings::StringHashFunction; + public: /** * This is the cardinality of the alphabet that is representable by this @@ -267,10 +273,7 @@ namespace strings { struct StringHashFunction { - size_t operator()(const ::cvc5::String& s) const - { - return std::hash<std::string>()(s.toString()); - } + size_t operator()(const ::cvc5::String& s) const; }; /* struct StringHashFunction */ } // namespace strings |