[[stash]]

.clang-files

@@ -12,11 +12,13 @@
 ./src/cnfizers/Tseitin.h
 
 ./src/common/numbers/Integer.h
+./src/common/numbers/Number.cc
 ./src/common/numbers/Number.h
 ./src/common/numbers/Real.h
 ./src/common/ApiException.h
 ./src/common/FlaPartitionMap.cc
 ./src/common/FlaPartitionMap.h
+./src/common/FunUtils.h
 ./src/common/InternalException.h
 ./src/common/PartitionInfo.cc
 ./src/common/PartitionInfo.h

src/common/FunUtils.h

@@ -0,0 +1,56 @@
+#ifndef OPENSMT_FUNUTILS_H
+#define OPENSMT_FUNUTILS_H
+
+#include <compare>
+#include <concepts>
+#include <functional>
+#include <utility>
+
+#define FORWARD(arg) std::forward<decltype(arg)>(arg)
+
+namespace opensmt {
+template<typename Op>
+struct CompoundAssignOf;
+
+template<>
+struct CompoundAssignOf<std::plus<void>> {
+    constexpr auto & operator()(auto & lhs, auto const & rhs) const {
+        lhs += rhs;
+        return lhs;
+    }
+};
+template<>
+struct CompoundAssignOf<std::minus<void>> {
+    constexpr auto & operator()(auto & lhs, auto const & rhs) const {
+        lhs -= rhs;
+        return lhs;
+    }
+};
+template<>
+struct CompoundAssignOf<std::multiplies<void>> {
+    constexpr auto & operator()(auto & lhs, auto const & rhs) const {
+        lhs *= rhs;
+        return lhs;
+    }
+};
+template<>
+struct CompoundAssignOf<std::divides<void>> {
+    constexpr auto & operator()(auto & lhs, auto const & rhs) const {
+        lhs *= rhs;
+        return lhs;
+    }
+};
+
+template<typename O = std::strong_ordering>
+inline O intToOrdering(std::integral auto cmp) {
+    if (cmp == 0) {
+        return O::equivalent;
+    } else if (cmp < 0) {
+        return O::less;
+    } else {
+        return O::greater;
+    }
+}
+} // namespace opensmt
+
+#endif // OPENSMT_FUNUTILS_H

src/common/TypeUtils.h

@@ -41,6 +41,12 @@ class span {
     T * _beg;
     uint32_t _size;
 };
+
+// This is useful e.g. for std::visit(..., std::variant)
+template<typename... Ts>
+struct Overload : Ts... {
+    using Ts::operator()...;
+};
 } // namespace opensmt
 
 #endif // OPENSMT_TYPEUTILS_H

src/common/numbers/CMakeLists.txt

@@ -1,7 +1,9 @@
 target_sources(common
 PUBLIC
+    "${CMAKE_CURRENT_LIST_DIR}/FastInteger.cc"
     "${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
     "${CMAKE_CURRENT_LIST_DIR}/Integer.h"
+    "${CMAKE_CURRENT_LIST_DIR}/Number.cc"
     "${CMAKE_CURRENT_LIST_DIR}/Number.h"
     "${CMAKE_CURRENT_LIST_DIR}/Real.h"
 PRIVATE
@@ -11,6 +13,7 @@ PRIVATE
 install(FILES
         ${CMAKE_CURRENT_LIST_DIR}/Integer.h
         ${CMAKE_CURRENT_LIST_DIR}/Number.h
+        ${CMAKE_CURRENT_LIST_DIR}/FastInteger.h
         ${CMAKE_CURRENT_LIST_DIR}/FastRational.h
         ${CMAKE_CURRENT_LIST_DIR}/Real.h
         ${CMAKE_CURRENT_LIST_DIR}/NumberUtils.h

src/common/numbers/FastInteger.cc

@@ -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());
+    }
+}
+}

src/common/numbers/FastInteger.h

@@ -0,0 +1,121 @@
+//
+// 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));
+    }
+
+    std::optional<word> tryGetValue() const {
+        if (!wordPartValid()) return {};
+        return num;
+    }
+
+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