-
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.
Separated integers from rationals and added
FastInteger wrapper
- Loading branch information
Showing
18 changed files
with
554 additions
and
167 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,86 @@ | ||
| #include "FastInteger.h" | ||
|
|
||
| namespace opensmt { | ||
| FastInteger::FastInteger(const char* str, const int base) : FastRational(str, base) { | ||
| assert(isInteger()); | ||
| } | ||
|
|
||
| FastInteger gcd(FastInteger const & a, FastInteger const & b) | ||
| { | ||
| assert(a.isInteger() and b.isInteger()); | ||
| if (a.wordPartValid() && b.wordPartValid()) { | ||
| 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.isInteger() and b.isInteger()); | ||
| if (a.wordPartValid() && b.wordPartValid()) { | ||
| 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.isInteger() && d.isInteger()); | ||
| 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.isInteger() && d.isInteger()); | ||
| 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,125 @@ | ||
| // | ||
| // 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; | ||
| FastInteger(FastRational rat) : FastRational(std::move(rat)) { | ||
| assert(isInteger()); | ||
| } | ||
| explicit FastInteger(const char*, const int base = 10); | ||
| FastInteger & operator=(FastRational const & other) { | ||
| assert(other.isInteger()); | ||
| FastRational::operator=(other); | ||
| return *this; | ||
| } | ||
| FastInteger & operator=(FastRational && other) { | ||
| assert(other.isInteger()); | ||
| FastRational::operator=(std::move(other)); | ||
| return *this; | ||
| } | ||
| FastInteger & operator=(std::integral auto i) { | ||
| return operator=(FastInteger(i)); | ||
| } | ||
|
|
||
| FastInteger operator-() const { | ||
| return FastRational::operator-(); | ||
| } | ||
| FastInteger operator+(const FastInteger& b) const | ||
| { | ||
| return FastRational::operator+(b); | ||
| } | ||
| FastInteger operator-(const FastInteger& b) const | ||
| { | ||
| return FastRational::operator-(b); | ||
| } | ||
| FastInteger operator*(const FastInteger& b) const | ||
| { | ||
| return FastRational::operator*(b); | ||
| } | ||
| FastInteger& operator+=(const FastInteger& b) | ||
| { | ||
| FastRational::operator+=(b); | ||
| return *this; | ||
| } | ||
| FastInteger& operator-=(const FastInteger& b) | ||
| { | ||
| FastRational::operator-=(b); | ||
| return *this; | ||
| } | ||
| FastInteger& operator*=(const FastInteger& 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+=(const FastRational&) = delete; | ||
| FastRational& operator-=(const FastRational&) = delete; | ||
| FastRational& operator*=(const FastRational&) = delete; | ||
|
|
||
| FastRational operator/(const FastInteger& b) const | ||
| { | ||
| return FastRational::operator/(b); | ||
| } | ||
| void operator/=(const FastInteger&) = delete; | ||
| FastRational& operator/=(const FastRational&) = delete; | ||
|
|
||
| // Return *this % d. The return value will have the sign of d | ||
| FastInteger operator%(const FastInteger& d) const { | ||
| assert(isInteger() && d.isInteger()); | ||
| 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 | ||
| } | ||
| FastInteger r = (*this) / d; | ||
| r = r.floor(); | ||
| r = (*this) - r*d; | ||
| return r; | ||
| } | ||
| FastInteger& operator%=(const FastInteger& 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; | ||
| using FastRational::ceil; | ||
| using FastRational::floor; | ||
|
|
||
| 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>); | ||
|
|
||
| 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); | ||
| } | ||
|
|
||
| #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.