From 1a2c4adb8647fd3ff5ab8965fd40d14bd218360d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Wed, 21 Aug 2024 21:02:14 +0200 Subject: [PATCH] Partially separated integers from rationals and added `FastInteger` wrapper --- .clang-files | 1 + src/common/CMakeLists.txt | 3 +- src/common/FastInteger.cc | 88 ++++++++ src/common/FastInteger.h | 115 +++++++++++ src/common/FastRational.cc | 84 +------- src/common/FastRational.h | 41 +--- src/common/Integer.h | 6 +- src/common/Number.h | 35 ++-- src/common/NumberUtils.h | 18 +- src/common/Real.h | 17 +- src/logics/ArithLogic.cc | 12 +- src/logics/BVLogic.h | 6 +- src/tsolvers/lasolver/LASolver.cc | 7 +- src/tsolvers/lasolver/Simplex.cc | 1 + src/tsolvers/lasolver/SparseMatrix.cc | 8 +- test/unit/CMakeLists.txt | 10 + test/unit/test_Integers.cc | 276 ++++++++++++++++++++++++++ test/unit/test_Rationals.cc | 19 +- 18 files changed, 564 insertions(+), 183 deletions(-) create mode 100644 src/common/FastInteger.cc create mode 100644 src/common/FastInteger.h create mode 100644 test/unit/test_Integers.cc diff --git a/.clang-files b/.clang-files index e3e62a49c..316fbfbf9 100644 --- a/.clang-files +++ b/.clang-files @@ -14,6 +14,7 @@ ./src/common/ApiException.h ./src/common/FlaPartitionMap.cc ./src/common/FlaPartitionMap.h +./src/common/Integer.h ./src/common/InternalException.h ./src/common/Number.h ./src/common/PartitionInfo.cc diff --git a/src/common/CMakeLists.txt b/src/common/CMakeLists.txt index 4c615cd7b..aec29e6a2 100644 --- a/src/common/CMakeLists.txt +++ b/src/common/CMakeLists.txt @@ -2,6 +2,7 @@ add_library(common OBJECT) target_sources(common PUBLIC + "${CMAKE_CURRENT_LIST_DIR}/FastInteger.cc" "${CMAKE_CURRENT_LIST_DIR}/FastRational.cc" "${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc" "${CMAKE_CURRENT_LIST_DIR}/Real.h" @@ -23,7 +24,7 @@ PRIVATE ) install(FILES - Integer.h Number.h FastRational.h StringMap.h Timer.h inttypes.h + Integer.h Number.h FastInteger.h FastRational.h StringMap.h Timer.h inttypes.h TreeOps.h Real.h FlaPartitionMap.h PartitionInfo.h ApiException.h TypeUtils.h NumberUtils.h NatSet.h ScopedVector.h TermNames.h DESTINATION ${INSTALL_HEADERS_DIR}/common) diff --git a/src/common/FastInteger.cc b/src/common/FastInteger.cc new file mode 100644 index 000000000..6b35ac4ef --- /dev/null +++ b/src/common/FastInteger.cc @@ -0,0 +1,88 @@ +#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()) { + // 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.isInteger() and b.isInteger()); + 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.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()); + } +} +} diff --git a/src/common/FastInteger.h b/src/common/FastInteger.h new file mode 100644 index 000000000..d97c08858 --- /dev/null +++ b/src/common/FastInteger.h @@ -0,0 +1,115 @@ +// +// Created by Tomas Kolarik in 08/2024. +// + +#ifndef OPENSMT_FAST_INTEGER_H +#define OPENSMT_FAST_INTEGER_H + +#include "FastRational.h" + +#include + +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(isInteger()); } + explicit FastInteger(char const *, int const base = 10); + FastInteger & operator=(FastRational const & other) { + assert(this != &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 static_cast(FastRational::operator-()); } + FastInteger operator+(FastInteger const & b) const { + return static_cast(FastRational::operator+(b)); + } + FastInteger operator-(FastInteger const & b) const { + return static_cast(FastRational::operator-(b)); + } + FastInteger operator*(FastInteger const & b) const { + return static_cast(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(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 + } + 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::ceil; + using FastRational::floor; + 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); + +// The result could not fit into integer -> FastInteger +template +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.isInteger()); + return static_cast(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 diff --git a/src/common/FastRational.cc b/src/common/FastRational.cc index 68566c05f..e8a459a26 100644 --- a/src/common/FastRational.cc +++ b/src/common/FastRational.cc @@ -6,6 +6,7 @@ Copyright (c) 2008, 2009 Centre national de la recherche scientifique (CNRS) */ #include "FastRational.h" +#include "FastInteger.h" #include #include @@ -112,88 +113,9 @@ std::string FastRational::get_str() const return os.str(); } -FastRational gcd(FastRational const & a, FastRational const & b) -{ - assert(a.isInteger() and b.isInteger()); - if (a.wordPartValid() && b.wordPartValid()) { - return FastRational(gcd(a.num, b.num)); - } - else { - a.ensure_mpq_valid(); - b.ensure_mpq_valid(); - mpz_gcd(FastRational::mpz(), mpq_numref(a.mpq), mpq_numref(b.mpq)); - return FastRational(FastRational::mpz()); - } -} - -FastRational lcm(FastRational const & a, FastRational 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(FastRational::mpz(), mpq_numref(a.mpq), mpq_numref(b.mpq)); - return FastRational(FastRational::mpz()); - } -} - FastRational fastrat_round_to_int(const FastRational& n) { FastRational res = n + FastRational(1, 2); - return fastrat_fdiv_q(res.get_num(), res.get_den()); -} - -// 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) -FastRational fastrat_fdiv_q(FastRational const & n, FastRational 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(FastRational::mpz(), mpq_numref(n.mpq), mpq_numref(d.mpq)); - return FastRational(FastRational::mpz()); -} - -//void mpz_divexact (mpz_ptr, mpz_srcptr, mpz_srcptr); -FastRational divexact(FastRational const & n, FastRational 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 FastRational(0); - } - } else { - assert(n.mpqPartValid() || d.mpqPartValid()); - n.ensure_mpq_valid(); - d.ensure_mpq_valid(); - mpz_divexact(FastRational::mpz(), mpq_numref(n.mpq), mpq_numref(d.mpq)); - return FastRational(FastRational::mpz()); - } + return fastint_fdiv_q(static_cast(res.get_num()), static_cast(res.get_den())); } // Given as input the sequence Reals, return the smallest number m such that for each r in Reals, r*m is an integer @@ -234,7 +156,7 @@ FastRational get_multiplicand(const std::vector& reals) else { // We filter in place the integers in dens. The last two are guaranteed to be ; int k = 0; - FastRational m = lcm(dens[dens.size()-1], dens[dens.size()-2]); + FastRational m = lcm(static_cast(dens[dens.size()-1]), static_cast(dens[dens.size()-2])); mult *= m; for (size_t j = 0; j < dens.size()-2; j++) { FastRational n = (m/dens[j]).get_den(); diff --git a/src/common/FastRational.h b/src/common/FastRational.h index 7948137bf..5d85769e8 100644 --- a/src/common/FastRational.h +++ b/src/common/FastRational.h @@ -15,6 +15,7 @@ Copyright (c) 2008, 2009 Centre national de la recherche scientifique (CNRS) #include #include #include +#include namespace opensmt { @@ -73,6 +74,7 @@ inline ulword absVal(lword x) { class FastRational { +protected: class mpqPool { std::stack store; // uses deque as storage to avoid realloc @@ -90,7 +92,7 @@ class FastRational inline static thread_local mpz_class temp; inline static mpz_ptr mpz() { return temp.get_mpz_t(); } - +private: // Bit masks for questioning state: static const unsigned char wordValidMask = 0x1; static const unsigned char mpqMemoryAllocatedMask = 0x2; @@ -155,6 +157,7 @@ class FastRational state = State::WORD_VALID; } } +protected: void ensure_mpq_valid() const { if (!mpqPartValid()) { assert(wordPartValid()); @@ -202,10 +205,6 @@ class FastRational friend inline void subtractionAssign (FastRational &, const FastRational &); friend inline void multiplicationAssign(FastRational &, const FastRational &); friend inline void divisionAssign (FastRational &, const FastRational &); - friend FastRational gcd (FastRational const &, FastRational const &); - friend FastRational lcm (FastRational const &, FastRational const &); - friend FastRational fastrat_fdiv_q (FastRational const & n, FastRational const & d); - friend FastRational divexact (FastRational const & n, FastRational const & d); static inline int compare(lword a, lword b) { if (a < b) return -1; @@ -395,23 +394,8 @@ class FastRational assert(wordPartValid() or not fitsWord()); return wordPartValid() && num == 1 && den == 1; } - - - // Return *this % d. The return value will have the sign of d - FastRational operator%(const FastRational& d) { - 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 - } - FastRational r = (*this) / d; - r = r.floor(); - r = (*this) - r*d; - return r; - } }; -FastRational fastrat_fdiv_q(FastRational const & n, FastRational const & d); FastRational fastrat_round_to_int(const FastRational& n); struct FastRationalHash { @@ -527,7 +511,10 @@ inline int FastRational::sign() const { } } -template integer gcd(integer a, integer b) { +static_assert(!std::integral); + +template +integer gcd(integer a, integer b) { if (a==0) return b; if (b==0) return a; if (b > a) { @@ -543,16 +530,6 @@ template integer gcd(integer a, integer b) { } } -template -FastRational lcm(integer a, integer b) { - if (a == 0) return 0; - if (b == 0) return 0; - if (b > a) - return FastRational(b / gcd(a, b)) * a; - else - return FastRational(a / gcd(a, b)) * b; -} - // Return 1 if |op1| > |op2|, -1 if |op1| < |op2|, and 0 if op1 = op2 inline int cmpabs(FastRational op1, FastRational op2) { @@ -562,8 +539,6 @@ inline int cmpabs(FastRational op1, FastRational op2) op2 = -op2; return op1.compare(op2); }; -template ulword gcd(ulword a, ulword b); -template uword gcd(uword a, uword b); #define CHECK_WORD(var, value) \ do { \ lword tmp = value; \ diff --git a/src/common/Integer.h b/src/common/Integer.h index 2f5ff3525..bac829aed 100644 --- a/src/common/Integer.h +++ b/src/common/Integer.h @@ -5,10 +5,10 @@ #ifndef OPENSMT_INTEGER_H #define OPENSMT_INTEGER_H -#include "Number.h" +#include "FastInteger.h" namespace opensmt { - typedef Number Integer2; +using Integer = FastInteger; } -#endif //OPENSMT_INTEGER_H +#endif // OPENSMT_INTEGER_H diff --git a/src/common/Number.h b/src/common/Number.h index 77e755f70..7f493bdc3 100644 --- a/src/common/Number.h +++ b/src/common/Number.h @@ -5,35 +5,36 @@ #ifndef OPENSMT_NUMBER_H #define OPENSMT_NUMBER_H -#define FAST_RATIONALS 1 +#include "Integer.h" +#include "Real.h" -#ifdef FAST_RATIONALS -#include "FastRational.h" -#else -#include -#endif +#include +#include namespace opensmt { -#ifdef FAST_RATIONALS -using Number = FastRational; -using NumberHash = FastRationalHash; -#else -using Number = mpq_class; -#endif - -inline bool isNegative(Number const & num) { +// Should be compatible both with `Real` and `Integer` +using Number = Real; + +static_assert(std::constructible_from); +static_assert(std::constructible_from); + +// TK: The current implementation assumes that Real can be directly and safely interpreted as Integer +// This preserves performance of the conversions +static_assert(std::derived_from); + +inline bool isNegative(auto const & num) { return num.sign() < 0; } -inline bool isPositive(Number const & num) { +inline bool isPositive(auto const & num) { return num.sign() > 0; } -inline bool isNonNegative(Number const & num) { +inline bool isNonNegative(auto const & num) { return num.sign() >= 0; } -inline bool isNonPositive(Number const & num) { +inline bool isNonPositive(auto const & num) { return num.sign() <= 0; } } // namespace opensmt diff --git a/src/common/NumberUtils.h b/src/common/NumberUtils.h index bd3c331ee..eeda8eaa1 100644 --- a/src/common/NumberUtils.h +++ b/src/common/NumberUtils.h @@ -12,24 +12,12 @@ #include namespace opensmt { - typedef mpz_class Integer; //PS. related to BV logic - - void static inline wordToBinary(const Integer x, char *&bin, const int width) { - bin = (char *) malloc(width + 1); - - int p = 0; - Integer one = 1; - for (Integer i = (one << (width - 1)); i > 0; i >>= 1) - bin[p++] = ((x & i) == i) ? '1' : '0'; - bin[p] = '\0'; - } - - void static inline wordToBinary(const unsigned x, char *&bin, const int width) { + void static inline wordToBinary(const auto x, char *&bin, const int width) { bin = (char *) malloc(width + 1); int p = 0; - Integer one = 1; - for (Integer i = (one << (width - 1)); i > 0; i >>= 1) + mpz_class one = 1; + for (mpz_class i = (one << (width - 1)); i > 0; i >>= 1) bin[p++] = ((x & i) == i) ? '1' : '0'; bin[p] = '\0'; } diff --git a/src/common/Real.h b/src/common/Real.h index 63ddd22dc..dfdbfb54f 100644 --- a/src/common/Real.h +++ b/src/common/Real.h @@ -5,10 +5,21 @@ #ifndef OPENSMT_REAL_H #define OPENSMT_REAL_H -#include "Number.h" +#define FAST_RATIONALS + +#ifdef FAST_RATIONALS +#include "FastRational.h" +#else +#include +#endif namespace opensmt { -typedef Number Real; -} +#ifdef FAST_RATIONALS +using Real = FastRational; +using RealHash = FastRationalHash; +#else +using Real = mpq_class; +#endif +} // namespace opensmt #endif // OPENSMT_REAL_H diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 06ea34379..b623400f9 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -1,8 +1,9 @@ #include "ArithLogic.h" #include -#include +#include #include +#include #include #include #include @@ -877,6 +878,7 @@ PTRef ArithLogic::mkConst(SRef s, char const * name) { if (s == sort_REAL or s == sort_INT) { char * rat; if (s == sort_REAL) + // TK: Currently this must be consistent with Real::get_str, otherwise it will make duplicates in term_store stringToRational(rat, name); else { if (not isIntString(name)) throw ApiException("Not parseable as an integer"); @@ -1212,15 +1214,13 @@ pair ArithLogic::sumToNormalizedIntPair(PTRef sum) { std::all_of(coeffs.begin(), coeffs.end(), [](Number const & coeff) { return coeff.isInteger(); }); if (not allIntegers) { // first ensure that all coeffs are integers - // this would probably not work when `Number` is not `FastRational` - using Integer = FastRational; // TODO: change when we have FastInteger auto lcmOfDenominators = Integer(1); - auto accumulateLCMofDenominators = [&lcmOfDenominators](FastRational const & next) { + auto accumulateLCMofDenominators = [&lcmOfDenominators](Number const & next) { if (next.isInteger()) { // denominator is 1 => lcm of denominators stays the same return; } - Integer den = next.get_den(); + Integer den = static_cast(next.get_den()); if (lcmOfDenominators == 1) { lcmOfDenominators = std::move(den); return; @@ -1240,7 +1240,7 @@ pair ArithLogic::sumToNormalizedIntPair(PTRef sum) { // Now make sure all coeffs are coprime auto coeffs_gcd = abs(coeffs[0]); for (std::size_t i = 1; i < coeffs.size() && coeffs_gcd != 1; ++i) { - coeffs_gcd = gcd(coeffs_gcd, abs(coeffs[i])); + coeffs_gcd = gcd(static_cast(coeffs_gcd), static_cast(abs(coeffs[i]))); assert(coeffs_gcd.isInteger()); } if (coeffs_gcd != 1) { diff --git a/src/logics/BVLogic.h b/src/logics/BVLogic.h index 6581fc75f..3dd1745cf 100644 --- a/src/logics/BVLogic.h +++ b/src/logics/BVLogic.h @@ -12,6 +12,8 @@ Module: New Logic for BitVector #include +#include + namespace opensmt { class BVLogic: public Logic @@ -93,8 +95,8 @@ class BVLogic: public Logic virtual std::string const getName() const override { return "QF_BV"; } // virtual PTRef insertTerm(SymRef sym, vec& terms, char** msg); - PTRef mkBVConst (const int c) { char* num; wordToBinary(c, num, getBitWidth()); PTRef tr = Logic::mkConst(sort_BVNUM, num); free(num); return tr; } // Convert the int c to binary - PTRef mkBVConst (const char* c) { char* num; wordToBinary(Integer(c), num, getBitWidth()); PTRef tr = Logic::mkConst(sort_BVNUM, num); free(num); return tr; } // Convert the string c to binary + PTRef mkBVConst (const int c) { char* num; wordToBinary(unsigned(c), num, getBitWidth()); PTRef tr = Logic::mkConst(sort_BVNUM, num); free(num); return tr; } // Convert the int c to binary + PTRef mkBVConst (const char* c) { char* num; wordToBinary(mpz_class(c), num, getBitWidth()); PTRef tr = Logic::mkConst(sort_BVNUM, num); free(num); return tr; } // Convert the string c to binary virtual PTRef mkBVNumVar (const char* name) { return mkVar(sort_BVNUM, name); } virtual bool isBuiltinSortSym(SSymRef ssr) const override { return (ssr == sort_store.getSortSym(sort_BVNUM)); } virtual bool isBuiltinSort(SRef sr) const override { return (sr == sort_BVNUM); } diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index f8cc78dac..d723465b8 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -7,12 +7,13 @@ #include "LASolver.h" #include "FarkasInterpolator.h" -#include #include "LIAInterpolator.h" #include "CutCreator.h" -#include +#include #include +#include +#include #include @@ -955,7 +956,7 @@ TRes LASolver::cutFromProof() { vec LASolver::collectEqualitiesFor(vec const & vars, std::unordered_set const & knownEqualities) { struct DeltaHash { std::size_t operator()(Delta const & d) const { - NumberHash hasher; + RealHash hasher; return (hasher(d.R()) ^ hasher(d.D())); } }; diff --git a/src/tsolvers/lasolver/Simplex.cc b/src/tsolvers/lasolver/Simplex.cc index 50536d3f2..0a4b20c7a 100644 --- a/src/tsolvers/lasolver/Simplex.cc +++ b/src/tsolvers/lasolver/Simplex.cc @@ -5,6 +5,7 @@ #include "Simplex.h" #include +#include #include #include diff --git a/src/tsolvers/lasolver/SparseMatrix.cc b/src/tsolvers/lasolver/SparseMatrix.cc index 9fca963b4..dd891bb26 100644 --- a/src/tsolvers/lasolver/SparseMatrix.cc +++ b/src/tsolvers/lasolver/SparseMatrix.cc @@ -7,6 +7,8 @@ #include "SparseMatrix.h" +#include + namespace opensmt { void SparseColMatrix::Col::negate() { this->poly.negate(); @@ -104,7 +106,8 @@ namespace { uint32_t nextColIndex = 1; while (nextColIndex < activeColumns.size()) { auto const & nextCol = A[activeColumns[nextColIndex]]; - auto quotient = -fastrat_fdiv_q(nextCol.getFirstCoeff(), smallestValue); + auto quotient = -fastint_fdiv_q(static_cast(nextCol.getFirstCoeff()), + static_cast(smallestValue)); assert(not quotient.isZero()); addColumnMultiple(A, activeColumns[0], quotient, activeColumns[nextColIndex], U); if (not nextCol.isFirst( @@ -130,7 +133,8 @@ namespace { for (uint32_t col = 0; col < pivotIndex; ++col) { auto const * otherVal = A[col].tryGetCoeffFor(rowIndex); if (not otherVal) { continue; } - auto quotient = -fastrat_fdiv_q(*otherVal, pivotVal); + auto quotient = -fastint_fdiv_q(static_cast(*otherVal), + static_cast(pivotVal)); if (not quotient.isZero()) { addColumnMultiple(A, pivotIndex, quotient, ColIndex{col}, U); } } } diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 5b84844f5..79935970b 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -1,4 +1,5 @@ include(GoogleTest) + add_executable(LRATest) target_sources(LRATest PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/test_Rationals.cc" @@ -10,6 +11,15 @@ target_link_libraries(LRATest OpenSMT gtest gtest_main) gtest_add_tests(TARGET LRATest) +add_executable(LIATest) +target_sources(LIATest + PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/test_Integers.cc" +) + +target_link_libraries(LIATest OpenSMT gtest gtest_main) + +gtest_add_tests(TARGET LIATest) + add_executable(RewritingTest) target_sources(RewritingTest PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/test_SimplifyAssignment.cc" diff --git a/test/unit/test_Integers.cc b/test/unit/test_Integers.cc new file mode 100644 index 000000000..0305aeffd --- /dev/null +++ b/test/unit/test_Integers.cc @@ -0,0 +1,276 @@ +#include +#include +#include + +namespace opensmt { + +TEST(Integers_test, test_negate_int32min) { + // INT32_MIN + Integer i {"-2147483648"}; + i.negate(); + EXPECT_TRUE(i > 0); +} + +TEST(Integers_test, test_negate_minus_int32min) { + // - INT32_MIN = 2^31 + Integer i {"2147483648"}; + Integer neg = -i; + EXPECT_TRUE(neg.isWellFormed()); + EXPECT_TRUE(neg < 0); + i.negate(); + EXPECT_TRUE(i.isWellFormed()); + EXPECT_EQ(i, neg); +} + +TEST(Integers_test, test_additionAssign) { + Integer a {"2147483640"}; + Integer b {"10"}; + additionAssign(a,b); + EXPECT_EQ(a, Integer{"2147483650"} ); +} + +TEST(Integers_test, test_overwrite) +{ + Integer i(INT32_MAX); + Integer q(0); + i *= 10; + // should not compile: + // i *= Real(5, 4); + i = 0; + i = INT32_MAX; + i *= 10; + i = q; +} + +TEST(Integers_test, test_uword) +{ + uint32_t x = 2589903246; + Integer f(x); + ASSERT_TRUE(f.mpqPartValid()); +} + +TEST(Integers_test, test_modulo) +{ + Integer a(-37033300); + Integer b(1); + Integer mod = a % b; + ASSERT_EQ(mod, 0); +} + +TEST(Integers_test, test_creation) +{ + { + Integer a{INT_MIN}; + ASSERT_TRUE(a.wordPartValid()); + ASSERT_FALSE(a.mpqMemoryAllocated()); + ASSERT_EQ(a, Integer{"-2147483648"}); + } + { + Integer a{INT_MAX}; + ASSERT_TRUE(a.wordPartValid()); + ASSERT_FALSE(a.mpqMemoryAllocated()); + ASSERT_EQ(a, Integer{"2147483647"}); + } +} + +TEST(Integers_test, test_addition) +{ + { + Integer a(3); + Integer b(0); + static_assert(std::is_same_v); + ASSERT_EQ(a + b, Integer(3)); + ASSERT_EQ(-a + b, Integer(-3)); + } + + { + Integer a(0); + Integer b(3); + ASSERT_EQ(a + b, Integer(3)); + ASSERT_EQ(a + (-b), Integer(-3)); + } + + { + Integer a(3); + Integer b(-3); + ASSERT_EQ(a+b, 0); + } + + { + Integer a(3); + Integer b(1); + ASSERT_EQ(a+b, Integer(4)); + } + { + Integer a(UINT_MAX); + Integer b(INT_MAX); + Integer sum = a+b; + ASSERT_EQ(sum, Integer("6442450942")); + ASSERT_FALSE(sum.wordPartValid()); + } + { + Integer a(UINT_MAX); + Integer b(INT_MIN); + Integer sum = a+b; + ASSERT_EQ(sum, Integer("2147483647")); + ASSERT_TRUE(sum.wordPartValid()); + } +} + +TEST(Integers_test, test_subtraction) +{ + { + Integer a(10); + Integer b(0); + static_assert(std::is_same_v); + Integer c = a-b; + ASSERT_EQ(c, a); + ASSERT_TRUE(c.wordPartValid()); + ASSERT_FALSE(c.mpqPartValid()); + } + { + Integer a(0); + Integer s = a - Integer(INT_MIN); + ASSERT_FALSE(s.wordPartValid()); + ASSERT_TRUE(s.mpqPartValid()); + ASSERT_EQ(s, Integer(INT_MAX)+1); + } + { + Integer a(INT_MAX); + Integer b(UINT_MAX); + Integer sum = a-b; + ASSERT_EQ(sum, Integer("-2147483648")); + ASSERT_TRUE(sum.wordPartValid()); + } +} + +TEST(Integers_test, test_division) +{ + { + Integer a(-1); + Integer b(-1); + Real c = a / b; + ASSERT_EQ(c, 1); + } + { + Integer a(-3); + Integer b(2); + Real c = a / b; + ASSERT_EQ(c, Real(-3, 2)); + ASSERT_TRUE(c.wordPartValid()); + ASSERT_FALSE(c.mpqMemoryAllocated()); + } +} + +TEST(Integers_test, test_operatorAssign) +{ + { + Integer f(0); + static_assert(std::is_same_v); + f -= Integer(-3) * Integer(-1); + ASSERT_EQ(f, -3); + ASSERT_TRUE(f.wordPartValid()); + ASSERT_FALSE(f.mpqMemoryAllocated()); + } + { + Integer f(0); + f += Integer(-3) * Integer(-1); + ASSERT_EQ(f, 3); + ASSERT_TRUE(f.wordPartValid()); + ASSERT_FALSE(f.mpqMemoryAllocated()); + } +} + +TEST(Integers_test, test_CHECK_WORD) +{ + word a(INT_MAX); + uword b(UINT_MAX); + uword res = 0; + CHECK_WORD(res, lword(a)*b); + ASSERT_EQ(res, (lword)(9223372030412324865)); + overflow: + std::cout << "Overflow" << std::endl; +} + +TEST(Integers_test, test_sub_lword_underflow_min) +{ + lword res; + (void)res; + lword s1 = 0; + lword s2 = LWORD_MIN; + CHECK_SUB_OVERFLOWS_LWORD(res, s1, s2); + ASSERT_TRUE(false); + overflow: + ASSERT_TRUE(true); +} + +TEST(Integers_test, test_sub_lword_nounderflow) +{ + lword res; + (void)res; + lword s1 = 0; + lword s2 = LWORD_MIN+1; + CHECK_SUB_OVERFLOWS_LWORD(res, s1, s2); + return; + overflow: + ASSERT_TRUE(false); +} + +TEST(Integers_test, test_sub_lword_nooverflow) +{ + lword res; + (void)res; + lword s1 = -1; + lword s2 = LWORD_MAX; + CHECK_SUB_OVERFLOWS_LWORD(res, s1, s2); + return; + overflow: + ASSERT_TRUE(false); +} + +TEST(Integers_test, test_sub_lword_overflow) +{ + lword res; + (void)res; + lword s1 = -2; + lword s2 = LWORD_MAX; + CHECK_SUB_OVERFLOWS_LWORD(res, s1, s2); + ASSERT_FALSE(true); + overflow: + ASSERT_TRUE(true); +} + +TEST(Integers_test, test_mod) +{ + Integer a(INT_MAX); + Integer b(INT_MIN); + Integer res = a % b; + ASSERT_EQ(res, (INT_MIN+1)); +} + +TEST(Integers_test, test_addNegated) +{ + { + Integer a(15); + Integer b(-15); + Integer res = a+b; + ASSERT_EQ(res, 0); + } + { + Integer a(INT_MAX); + Integer b(INT_MIN); + Integer res = a + b; + ASSERT_EQ(res, -1); + } +} + +TEST(Integers_test, testWordRepresentation_Negate) { + Integer a(INT_MIN); // a fits into word representation + ASSERT_TRUE(a.wordPartValid()); + a.negate(); // a now does not fit into word representation + ASSERT_FALSE(a.wordPartValid()); + a.negate(); // a now again fits into word representation + ASSERT_TRUE(a.wordPartValid()); +} + +} diff --git a/test/unit/test_Rationals.cc b/test/unit/test_Rationals.cc index 2446a51d0..89872b43f 100644 --- a/test/unit/test_Rationals.cc +++ b/test/unit/test_Rationals.cc @@ -35,7 +35,7 @@ TEST(Rationals_test, test_normalized) TEST(Rationals_test, test_hash_function) { std::vector hashes; - NumberHash hasher; + RealHash hasher; for (int i = 0; i < 10; i++) { Real r((int)random()); hashes.push_back(hasher(r)); @@ -122,6 +122,7 @@ TEST(Rationals_test, test_negate_minus_int32min) { EXPECT_TRUE(neg < 0); r.negate(); EXPECT_TRUE(r.isWellFormed()); + EXPECT_EQ(r, neg); } TEST(Rationals_test, test_additionAssign) { @@ -149,14 +150,6 @@ TEST(Rationals_test, test_uword) ASSERT_TRUE(f.mpqPartValid()); } -TEST(Rationals_test, test_modulo) -{ - Real a(-37033300); - Real b(1); - Real mod = a % b; - ASSERT_EQ(mod, 0); -} - TEST(Rationals_test, test_creation) { { @@ -448,14 +441,6 @@ TEST(Rationals_test, test_ceil) f.ceil(); } -TEST(Rationals_test, test_mod) -{ - Real a(INT_MAX); - Real b(INT_MIN); - Real res = a % b; - ASSERT_EQ(res, (INT_MIN+1)); -} - TEST(Rationals_test, test_addNegated) { {