-
Notifications
You must be signed in to change notification settings - Fork 19
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
38 changed files
with
988 additions
and
307 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,88 @@ | ||
| #include "FastInteger.h" | ||
|
|
||
| namespace opensmt { | ||
| FastInteger::FastInteger(const char* str, const int base) : FastRational(str, base) { | ||
| assert(isIntegerValue()); | ||
| } | ||
|
|
||
| FastInteger gcd(FastInteger const & a, FastInteger const & b) | ||
| { | ||
| assert(a.isIntegerValue() and b.isIntegerValue()); | ||
| if (a.wordPartValid() && b.wordPartValid()) { | ||
| // Refers to FastRational.h:gcd | ||
| return FastInteger(gcd(a.num, b.num)); | ||
| } | ||
| else { | ||
| a.ensure_mpq_valid(); | ||
| b.ensure_mpq_valid(); | ||
| mpz_gcd(FastInteger::mpz(), mpq_numref(a.mpq), mpq_numref(b.mpq)); | ||
| return FastInteger(FastInteger::mpz()); | ||
| } | ||
| } | ||
|
|
||
| FastInteger lcm(FastInteger const & a, FastInteger const & b) | ||
| { | ||
| assert(a.isIntegerValue() and b.isIntegerValue()); | ||
| if (a.wordPartValid() && b.wordPartValid()) { | ||
| // Refers to FastRational.h:lcm | ||
| return lcm(a.num, b.num); | ||
| } | ||
| else { | ||
| a.ensure_mpq_valid(); | ||
| b.ensure_mpq_valid(); | ||
| mpz_lcm(FastInteger::mpz(), mpq_numref(a.mpq), mpq_numref(b.mpq)); | ||
| return FastInteger(FastInteger::mpz()); | ||
| } | ||
| } | ||
|
|
||
| // The quotient of n and d using the fast rationals. | ||
| // Divide n by d, forming a quotient q. | ||
| // Rounds q down towards -infinity, and q will satisfy n = q*d + r for some 0 <= abs(r) <= abs(d) | ||
| FastInteger fastint_fdiv_q(FastInteger const & n, FastInteger const & d) { | ||
| assert(n.isIntegerValue() && d.isIntegerValue()); | ||
| if (n.wordPartValid() && d.wordPartValid()) { | ||
| word num = n.num; | ||
| word den = d.num; | ||
| word quo; | ||
| if (num == INT_MIN) // The abs is guaranteed to overflow. Otherwise this is always fine | ||
| goto overflow; | ||
| // After this -INT_MIN+1 <= numerator <= INT_MAX, and therefore the result always fits into a word. | ||
| quo = num / den; | ||
| if (num % den != 0 && ((num < 0 && den >=0) || (den < 0 && num >= 0))) // The result should be negative | ||
| quo--; // INT_MAX-1 >= quo >= -INT_MIN | ||
|
|
||
| return quo; | ||
| } | ||
| overflow: | ||
| n.ensure_mpq_valid(); | ||
| d.ensure_mpq_valid(); | ||
| mpz_fdiv_q(FastInteger::mpz(), mpq_numref(n.mpq), mpq_numref(d.mpq)); | ||
| return FastInteger(FastInteger::mpz()); | ||
| } | ||
|
|
||
| //void mpz_divexact (mpz_ptr, mpz_srcptr, mpz_srcptr); | ||
| FastInteger divexact(FastInteger const & n, FastInteger const & d) { | ||
| assert(d != 0); | ||
| assert(n.isIntegerValue() && d.isIntegerValue()); | ||
| if (n.wordPartValid() && d.wordPartValid()) { | ||
| word num = n.num; | ||
| word den = d.num; | ||
| word quo; | ||
| if (den != 0){ | ||
| quo = num / den; | ||
| return quo; | ||
| } | ||
| else { | ||
| // Division by zero | ||
| assert(false); | ||
| return FastInteger(0); | ||
| } | ||
| } else { | ||
| assert(n.mpqPartValid() || d.mpqPartValid()); | ||
| n.ensure_mpq_valid(); | ||
| d.ensure_mpq_valid(); | ||
| mpz_divexact(FastInteger::mpz(), mpq_numref(n.mpq), mpq_numref(d.mpq)); | ||
| return FastInteger(FastInteger::mpz()); | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,116 @@ | ||
| // | ||
| // Created by Tomas Kolarik in 08/2024. | ||
| // | ||
|
|
||
| #ifndef OPENSMT_FAST_INTEGER_H | ||
| #define OPENSMT_FAST_INTEGER_H | ||
|
|
||
| #include "FastRational.h" | ||
|
|
||
| #include <concepts> | ||
|
|
||
| namespace opensmt { | ||
| // TODO: inefficient, rational representation & uses mpq instead of mpz | ||
| class FastInteger : public FastRational { | ||
| public: | ||
| using FastRational::FastRational; | ||
| explicit FastInteger(FastRational rat) : FastRational(std::move(rat)) { assert(isIntegerValue()); } | ||
| explicit FastInteger(char const *, int const base = 10); | ||
| FastInteger & operator=(FastRational const & other) { | ||
| assert(this != &other); | ||
| assert(other.isIntegerValue()); | ||
| FastRational::operator=(other); | ||
| return *this; | ||
| } | ||
| FastInteger & operator=(FastRational && other) { | ||
| assert(other.isIntegerValue()); | ||
| FastRational::operator=(std::move(other)); | ||
| return *this; | ||
| } | ||
| FastInteger & operator=(std::integral auto i) { return operator=(FastInteger(i)); } | ||
|
|
||
| FastInteger ceil() const noexcept { return *this; } | ||
| FastInteger floor() const noexcept { return *this; } | ||
|
|
||
| FastInteger operator-() const { return static_cast<FastInteger &&>(FastRational::operator-()); } | ||
| FastInteger operator+(FastInteger const & b) const { | ||
| return static_cast<FastInteger &&>(FastRational::operator+(b)); | ||
| } | ||
| FastInteger operator-(FastInteger const & b) const { | ||
| return static_cast<FastInteger &&>(FastRational::operator-(b)); | ||
| } | ||
| FastInteger operator*(FastInteger const & b) const { | ||
| return static_cast<FastInteger &&>(FastRational::operator*(b)); | ||
| } | ||
| FastInteger & operator+=(FastInteger const & b) { | ||
| FastRational::operator+=(b); | ||
| return *this; | ||
| } | ||
| FastInteger & operator-=(FastInteger const & b) { | ||
| FastRational::operator-=(b); | ||
| return *this; | ||
| } | ||
| FastInteger & operator*=(FastInteger const & b) { | ||
| FastRational::operator*=(b); | ||
| return *this; | ||
| } | ||
| FastInteger & operator+=(std::integral auto i) { return operator+=(FastInteger(i)); } | ||
| FastInteger & operator-=(std::integral auto i) { return operator-=(FastInteger(i)); } | ||
| FastInteger & operator*=(std::integral auto i) { return operator*=(FastInteger(i)); } | ||
| FastRational & operator+=(FastRational const &) = delete; | ||
| FastRational & operator-=(FastRational const &) = delete; | ||
| FastRational & operator*=(FastRational const &) = delete; | ||
|
|
||
| FastRational operator/(FastInteger const & b) const { return FastRational::operator/(b); } | ||
| void operator/=(FastInteger const &) = delete; | ||
| FastRational & operator/=(FastRational const &) = delete; | ||
|
|
||
| // The return value will have the sign of d | ||
| FastInteger operator%(FastInteger const & d) const { | ||
| assert(isIntegerValue() && d.isIntegerValue()); | ||
| if (wordPartValid() && d.wordPartValid()) { | ||
| uword w = absVal(num % d.num); // Largest value is absVal(INT_MAX % INT_MIN) = INT_MAX | ||
| return (word)(d.num > 0 ? w : -w); // No overflow since 0 <= w <= INT_MAX | ||
| } | ||
| FastRational r = operator/(d); | ||
| auto i = FastInteger(r.floor()); | ||
| return operator-(i * d); | ||
| } | ||
| FastInteger & operator%=(FastInteger const & d) { | ||
| //+ it would be more efficient the other way around | ||
| return operator=(operator%(d)); | ||
| } | ||
|
|
||
| private: | ||
| FastInteger(std::integral auto, std::integral auto) = delete; | ||
|
|
||
| using FastRational::get_d; | ||
| using FastRational::get_den; | ||
| using FastRational::get_num; | ||
| //- using FastRational::tryGetNumDen; | ||
|
|
||
| friend FastInteger gcd(FastInteger const &, FastInteger const &); | ||
| friend FastInteger lcm(FastInteger const &, FastInteger const &); | ||
| friend FastInteger fastint_fdiv_q(FastInteger const &, FastInteger const &); | ||
| friend FastInteger divexact(FastInteger const &, FastInteger const &); | ||
| }; | ||
|
|
||
| static_assert(!std::integral<FastInteger>); | ||
|
|
||
| // The result could not fit into integer -> FastInteger | ||
| template<std::integral integer> | ||
| FastInteger lcm(integer a, integer b) { | ||
| if (a == 0) return 0; | ||
| if (b == 0) return 0; | ||
| FastRational rat = (b > a) ? FastRational(b / gcd(a, b)) * a : FastRational(a / gcd(a, b)) * b; | ||
| assert(rat.isIntegerValue()); | ||
| return static_cast<FastInteger&&>(rat); | ||
| } | ||
|
|
||
| FastInteger gcd(FastInteger const &, FastInteger const &); | ||
| FastInteger lcm(FastInteger const &, FastInteger const &); | ||
| FastInteger fastint_fdiv_q(FastInteger const & n, FastInteger const & d); | ||
| FastInteger divexact(FastInteger const & n, FastInteger const & d); | ||
| } // namespace opensmt | ||
|
|
||
| #endif // OPENSMT_FAST_INTEGER_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.