Use CRTP for static polymophism within numbers

.clang-files

@@ -11,15 +11,18 @@
 ./src/cnfizers/Tseitin.cc
 ./src/cnfizers/Tseitin.h
 
+./src/common/numbers/Integer.h
+./src/common/numbers/Number.h
+./src/common/numbers/NumberCRTP.h
+./src/common/numbers/Real.h
 ./src/common/ApiException.h
+./src/common/CRTP.h
 ./src/common/FlaPartitionMap.cc
 ./src/common/FlaPartitionMap.h
 ./src/common/InternalException.h
-./src/common/Number.h
 ./src/common/PartitionInfo.cc
 ./src/common/PartitionInfo.h
 ./src/common/Random.h
-./src/common/Real.h
 ./src/common/ScopedVector.h
 ./src/common/StringMap.h
 ./src/common/TermNames.h

src/common/CMakeLists.txt

@@ -2,15 +2,10 @@ add_library(common OBJECT)
 
 target_sources(common
 PUBLIC
-    "${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
     "${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc"
-    "${CMAKE_CURRENT_LIST_DIR}/Real.h"
     "${CMAKE_CURRENT_LIST_DIR}/TermNames.h"
 PRIVATE
     "${CMAKE_CURRENT_LIST_DIR}/SystemQueries.h"
-    "${CMAKE_CURRENT_LIST_DIR}/Integer.h"
-    "${CMAKE_CURRENT_LIST_DIR}/Number.h"
-    "${CMAKE_CURRENT_LIST_DIR}/NumberUtils.h"
     "${CMAKE_CURRENT_LIST_DIR}/inttypes.h"
     "${CMAKE_CURRENT_LIST_DIR}/StringMap.h"
     "${CMAKE_CURRENT_LIST_DIR}/StringConv.h"
@@ -22,8 +17,10 @@ PRIVATE
     "${CMAKE_CURRENT_LIST_DIR}/ReportUtils.h"
 )
 
+include(numbers/CMakeLists.txt)
+
 install(FILES
-        Integer.h Number.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
+        StringMap.h Timer.h inttypes.h
+        TreeOps.h FlaPartitionMap.h PartitionInfo.h ApiException.h TypeUtils.h
+        NatSet.h ScopedVector.h TermNames.h
 DESTINATION ${INSTALL_HEADERS_DIR}/common)

src/common/CRTP.h

@@ -0,0 +1,26 @@
+#ifndef OPENSMT_CRTP_H
+#define OPENSMT_CRTP_H
+
+namespace opensmt {
+template<typename T>
+class CRTP {
+protected:
+    friend T;
+
+    using Derived = T;
+
+    CRTP() = default;
+    ~CRTP() = default;
+    CRTP(CRTP const &) = default;
+    CRTP & operator=(CRTP const &) = default;
+    CRTP(CRTP &&) = default;
+    CRTP & operator=(CRTP &&) = default;
+
+    auto const & asDerived() const noexcept { return static_cast<Derived const &>(*this); }
+    auto & asDerived() noexcept { return static_cast<Derived &>(*this); }
+    auto asDerivedPtr() const noexcept { return static_cast<Derived const *>(this); }
+    auto asDerivedPtr() noexcept { return static_cast<Derived *>(this); }
+};
+} // namespace opensmt
+
+#endif // OPENSMT_CRTP_H

src/common/StringConv.h

@@ -8,7 +8,7 @@
 #ifndef OPENSMT_STRINGCONV_H
 #define OPENSMT_STRINGCONV_H
 
-#include "NumberUtils.h"
+#include "numbers/NumberUtils.h"
 
 namespace opensmt {
 

src/common/numbers/CMakeLists.txt

@@ -0,0 +1,18 @@
+target_sources(common
+PUBLIC
+    "${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
+    "${CMAKE_CURRENT_LIST_DIR}/Integer.h"
+    "${CMAKE_CURRENT_LIST_DIR}/Number.h"
+    "${CMAKE_CURRENT_LIST_DIR}/Real.h"
+PRIVATE
+    "${CMAKE_CURRENT_LIST_DIR}/NumberUtils.h"
+)
+
+install(FILES
+        ${CMAKE_CURRENT_LIST_DIR}/Integer.h
+        ${CMAKE_CURRENT_LIST_DIR}/Number.h
+        ${CMAKE_CURRENT_LIST_DIR}/NumberCRTP.h
+        ${CMAKE_CURRENT_LIST_DIR}/FastRational.h
+        ${CMAKE_CURRENT_LIST_DIR}/Real.h
+        ${CMAKE_CURRENT_LIST_DIR}/NumberUtils.h
+DESTINATION ${INSTALL_HEADERS_DIR}/common/numbers)

src/common/FastRational.h → src/common/numbers/FastRational.h

@@ -7,6 +7,8 @@ Copyright (c) 2008, 2009 Centre national de la recherche scientifique (CNRS)
 #ifndef FAST_RATIONALS_H
 #define FAST_RATIONALS_H
 
+#include "NumberCRTP.h"
+
 #include <gmpxx.h>
 #include <cassert>
 #include <climits>
@@ -71,7 +73,7 @@ inline ulword absVal(lword x) {
                  : +((ulword)(x));
 }
 
-class FastRational
+class FastRational : public NumberCRTP<FastRational>
 {
     class mpqPool
     {
@@ -268,7 +270,7 @@ class FastRational
     bool operator!=( const FastRational & b ) const { return !(*this == b); }
     inline unsigned size() const;
 
-    uint32_t getHashValue() const {
+    std::size_t hash() const {
         if  (wordPartValid()) {
             return 37*(uint32_t)num + 13*(uint32_t)den;
         }
@@ -414,17 +416,6 @@ class FastRational
 FastRational fastrat_fdiv_q(FastRational const & n, FastRational const & d);
 FastRational fastrat_round_to_int(const FastRational& n);
 
-struct FastRationalHash {
-    uint32_t operator() (const FastRational& s) const {
-        return (uint32_t)s.getHashValue();
-    }
-};
-
-inline std::ostream & operator<<(std::ostream & out, const FastRational & r)
-{
-    r.print(out);
-    return out;
-}
 inline FastRational::FastRational(const FastRational& x) {
     if (x.wordPartValid()) {
         num = x.num;
@@ -1047,14 +1038,6 @@ inline FastRational FastRational::inverse() const {
     return dest;
 }
 
-inline FastRational abs(FastRational const & x) {
-    if (x.sign() >= 0) {
-        return x;
-    } else {
-        return -x;
-    }
-}
-
 FastRational get_multiplicand(const std::vector<FastRational>& reals);
 
 }

src/common/Integer.h → src/common/numbers/Integer.h

@@ -8,7 +8,7 @@
 #include "Number.h"
 
 namespace opensmt {
-    typedef Number Integer2;
+typedef Number Integer2;
 }
 
-#endif //OPENSMT_INTEGER_H
+#endif // OPENSMT_INTEGER_H

src/common/Number.h → src/common/numbers/Number.h

@@ -16,7 +16,6 @@
 namespace opensmt {
 #ifdef FAST_RATIONALS
 using Number = FastRational;
-using NumberHash = FastRationalHash;
 #else
 using Number = mpq_class;
 #endif

src/common/numbers/NumberCRTP.h

@@ -0,0 +1,41 @@
+//
+// Created by Tomas Kolarik on 05.11.24
+//
+
+#ifndef OPENSMT_NUMBERCRTP_H
+#define OPENSMT_NUMBERCRTP_H
+
+#include <common/CRTP.h>
+
+#include <iosfwd>
+#include <utility>
+
+namespace opensmt {
+template<typename T>
+class NumberCRTP : public CRTP<T> {
+public:
+    struct Hash {
+        //- std::size_t operator()(NumberCRTP const & x) const { return x.asDerived().hash(); }
+        std::size_t operator()(NumberCRTP const & x) const { return 0; }
+    };
+};
+
+template<typename T>
+T abs(NumberCRTP<T> const & x) {
+    //- !!!
+    return {};
+}
+
+template<typename T>
+std::ostream & operator<<(std::ostream & os, NumberCRTP<T> const & x) {
+    //- !!!
+    return os;
+}
+} // namespace opensmt
+
+//- namespace std {
+//- template<typename T>
+//- struct hash<opensmt::NumberCRTP<T>> : opensmt::NumberCRTP<T>::Hash {};
+//- } // namespace std
+
+#endif // OPENSMT_NUMBERCRTP_H

src/logics/ArithLogic.cc

@@ -1,10 +1,11 @@
 #include "ArithLogic.h"
 
 #include <common/ApiException.h>
-#include <common/FastRational.h>
 #include <common/InternalException.h>
 #include <common/StringConv.h>
 #include <common/TreeOps.h>
+#include <common/numbers/FastRational.h>
+#include <common/numbers/Number.h>
 #include <pterms/PtStore.h>
 #include <rewriters/Rewriter.h>
 #include <rewriters/Rewritings.h>

src/logics/ArithLogic.h

@@ -3,7 +3,7 @@
 
 #include "Logic.h"
 
-#include <common/Number.h>
+#include <common/numbers/Number.h>
 
 #include <numeric>
 

src/logics/BVLogic.h

@@ -10,7 +10,9 @@ Module: New Logic for BitVector
 
 #include "Logic.h"
 
-#include <common/NumberUtils.h>
+#include <common/numbers/NumberUtils.h>
+
+#include <gmpxx.h>
 
 namespace opensmt {
 

src/simplifiers/LA.h

@@ -29,7 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 
 #include <pterms/PtStructs.h>
 #include <logics/ArithLogic.h>
-#include <common/Real.h>
+#include <common/numbers/Real.h>
 
 #include <map>
 

src/tsolvers/bvsolver/BitBlaster.cc

@@ -29,7 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 
 #include <models/ModelBuilder.h>
 #include <api/MainSolver.h>
-#include <common/Real.h>
+#include <common/numbers/Real.h>
 
 namespace opensmt {
 

src/tsolvers/lasolver/CutCreator.h

@@ -12,8 +12,8 @@
 #include "Polynomial.h"
 #include "SparseMatrix.h"
 
-#include <common/Real.h>
 #include <common/TypeUtils.h>
+#include <common/numbers/Real.h>
 #include <pterms/PTRef.h>
 
 namespace opensmt {

src/tsolvers/lasolver/Delta.h

@@ -29,7 +29,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef DELTA_H
 #define DELTA_H
 
-#include <common/Real.h>
+#include <common/numbers/Real.h>
 
 #include <iosfwd>
 

src/tsolvers/lasolver/FarkasInterpolator.cc

@@ -16,7 +16,7 @@
 
 #include <common/ApiException.h>
 #include <common/InternalException.h>
-#include <common/Real.h>
+#include <common/numbers/Real.h>
 #include <logics/ArithLogic.h>
 #include <simplifiers/LA.h>
 

src/tsolvers/lasolver/FarkasInterpolator.h

@@ -5,7 +5,7 @@
 #ifndef OPENSMT_FARKASINTERPOLATOR_H
 #define OPENSMT_FARKASINTERPOLATOR_H
 
-#include <common/Real.h>
+#include <common/numbers/Real.h>
 #include <pterms/PtStructs.h>
 #include <smtsolvers/TheoryInterpolator.h>
 

src/tsolvers/lasolver/LASolver.cc

@@ -7,12 +7,13 @@
 
 #include "LASolver.h"
 #include "FarkasInterpolator.h"
-#include <simplifiers/LA.h>
 #include "LIAInterpolator.h"
 #include "CutCreator.h"
 
-#include <models/ModelBuilder.h>
+#include <common/numbers/Real.h>
 #include <common/Random.h>
+#include <models/ModelBuilder.h>
+#include <simplifiers/LA.h>
 
 #include <unordered_set>
 
@@ -955,7 +956,7 @@ TRes LASolver::cutFromProof() {
 vec<PTRef> LASolver::collectEqualitiesFor(vec<PTRef> const & vars, std::unordered_set<PTRef, PTRefHash> const & knownEqualities) {
     struct DeltaHash {
         std::size_t operator()(Delta const & d) const {
-            NumberHash hasher;
+            Number::Hash hasher;
             return (hasher(d.R()) ^ hasher(d.D()));
         }
     };

src/tsolvers/lasolver/Polynomial.h

@@ -8,7 +8,7 @@
 #ifndef OPENSMT_POLYNOMIAL_H
 #define OPENSMT_POLYNOMIAL_H
 
-#include <common/Real.h>
+#include <common/numbers/Real.h>
 
 #include <vector>
 #include <unordered_map>

src/tsolvers/lasolver/Simplex.cc

@@ -5,6 +5,7 @@
 #include "Simplex.h"
 
 #include <common/InternalException.h>
+#include <common/numbers/Number.h>
 
 #include <algorithm>
 #include <limits>

src/tsolvers/lasolver/Tableau.h

@@ -10,7 +10,7 @@
 #include "LAVar.h"
 #include "Polynomial.h"
 
-#include <common/Real.h>
+#include <common/numbers/Real.h>
 
 #include <algorithm>
 #include <functional>

src/tsolvers/stpsolver/Converter.h

@@ -1,7 +1,7 @@
 #ifndef OPENSMT_CONVERTER_H
 #define OPENSMT_CONVERTER_H
 
-#include <common/Number.h>
+#include <common/numbers/Number.h>
 
 #include <concepts>
 #include <cstddef>

src/tsolvers/stpsolver/STPStore.h

@@ -1,7 +1,7 @@
 #ifndef OPENSMT_STPSTORE_H
 #define OPENSMT_STPSTORE_H
 
-#include <common/Number.h>
+#include <common/numbers/Number.h>
 #include <pterms/PtStructs.h>
 
 #include <cstdint>

test/unit/test_LIACutSolver.cc

@@ -1,5 +1,5 @@
 #include <gtest/gtest.h>
-#include <common/Real.h>
+#include <common/numbers/Real.h>
 #include <options/SMTConfig.h>
 #include <tsolvers/lasolver/Simplex.h>
 

test/unit/test_LIAStrengthening.cc

@@ -2,7 +2,7 @@
 // Created by prova on 30.09.20.
 //
 #include <gtest/gtest.h>
-#include <common/Real.h>
+#include <common/numbers/Real.h>
 #include <logics/ArithLogic.h>
 
 namespace opensmt {