Fp simplex

.clang-files

@@ -14,6 +14,9 @@
 ./src/common/ApiException.h
 ./src/common/FlaPartitionMap.cc
 ./src/common/FlaPartitionMap.h
+./src/common/Float.cc
+./src/common/Float.h
+./src/common/Integer.h
 ./src/common/InternalException.h
 ./src/common/Number.h
 ./src/common/PartitionInfo.cc

src/common/CMakeLists.txt

@@ -2,7 +2,9 @@ add_library(common OBJECT)
 
 target_sources(common
 PUBLIC
+    "${CMAKE_CURRENT_LIST_DIR}/FastInteger.cc"
     "${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
+    "${CMAKE_CURRENT_LIST_DIR}/Float.cc"
     "${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc"
     "${CMAKE_CURRENT_LIST_DIR}/Real.h"
     "${CMAKE_CURRENT_LIST_DIR}/TermNames.h"
@@ -23,7 +25,7 @@ PRIVATE
 )
 
 install(FILES
-        Integer.h Number.h FastRational.h StringMap.h Timer.h inttypes.h
+        Integer.h Number.h FastInteger.h FastRational.h Float.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)

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

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 <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(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<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(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<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.isInteger());
+    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

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 <sstream>
 #include <algorithm>
@@ -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<FastInteger&&>(res.get_num()), static_cast<FastInteger&&>(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<FastRational>& 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<FastInteger&>(dens[dens.size()-1]), static_cast<FastInteger&>(dens[dens.size()-2]));
             mult *= m;
             for (size_t j = 0; j < dens.size()-2; j++) {
                 FastRational n = (m/dens[j]).get_den();