summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/didyoumean.cpp6
-rw-r--r--src/util/hash.h5
-rw-r--r--src/util/integer_cln_imp.cpp57
-rw-r--r--src/util/integer_cln_imp.h12
-rw-r--r--src/util/integer_gmp_imp.cpp97
-rw-r--r--src/util/integer_gmp_imp.h16
-rw-r--r--src/util/string.cpp15
-rw-r--r--src/util/string.h11
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback