Moved number-related files into separate directory

usi-verification-and-security · Nov 6, 2024 · 3ab79fd · 3ab79fd
1 parent d80158a
commit 3ab79fd
Show file tree

Hide file tree

Showing 28 changed files with 51 additions and 31 deletions.
diff --git a/.clang-files b/.clang-files
@@ -11,15 +11,16 @@
 ./src/cnfizers/Tseitin.cc
 ./src/cnfizers/Tseitin.h
 
+./src/common/numbers/Integer.h
+./src/common/numbers/Number.h
+./src/common/numbers/Real.h
 ./src/common/ApiException.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

diff --git a/src/common/CMakeLists.txt b/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)
diff --git a/src/common/StringConv.h b/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 {
 

diff --git a/src/common/numbers/CMakeLists.txt b/src/common/numbers/CMakeLists.txt
@@ -0,0 +1,17 @@
+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
+        Integer.h
+        Number.h
+        FastRational.h
+        Real.h
+        NumberUtils.h
+DESTINATION ${INSTALL_HEADERS_DIR}/common/numbers)
diff --git a/src/common/FastRational.cc → src/common/numbers/FastRational.cc b/src/common/FastRational.cc → src/common/numbers/FastRational.cc
diff --git a/src/common/FastRational.h → src/common/numbers/FastRational.h b/src/common/FastRational.h → src/common/numbers/FastRational.h
diff --git a/src/common/Integer.h → src/common/numbers/Integer.h b/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
diff --git a/src/common/Number.h → src/common/numbers/Number.h b/src/common/Number.h → src/common/numbers/Number.h
diff --git a/src/common/NumberUtils.h → src/common/numbers/NumberUtils.h b/src/common/NumberUtils.h → src/common/numbers/NumberUtils.h
diff --git a/src/common/Real.h → src/common/numbers/Real.h b/src/common/Real.h → src/common/numbers/Real.h
diff --git a/src/logics/ArithLogic.cc b/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>

diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h
@@ -3,7 +3,7 @@
 
 #include "Logic.h"
 
-#include <common/Number.h>
+#include <common/numbers/Number.h>
 
 #include <numeric>
 

diff --git a/src/logics/BVLogic.h b/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 {
 

diff --git a/src/simplifiers/LA.h b/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>
 

diff --git a/src/tsolvers/bvsolver/BitBlaster.cc b/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 {
 

diff --git a/src/tsolvers/lasolver/CutCreator.h b/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 {

diff --git a/src/tsolvers/lasolver/Delta.h b/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>
 

diff --git a/src/tsolvers/lasolver/FarkasInterpolator.cc b/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>
 

diff --git a/src/tsolvers/lasolver/FarkasInterpolator.h b/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>
 

diff --git a/src/tsolvers/lasolver/LASolver.cc b/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>
 

diff --git a/src/tsolvers/lasolver/Polynomial.h b/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>

diff --git a/src/tsolvers/lasolver/Simplex.cc b/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>

diff --git a/src/tsolvers/lasolver/Tableau.h b/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>

diff --git a/src/tsolvers/stpsolver/Converter.h b/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>

diff --git a/src/tsolvers/stpsolver/STPStore.h b/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>

diff --git a/test/unit/test_LIACutSolver.cc b/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>
 

diff --git a/test/unit/test_LIAStrengthening.cc b/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 {

diff --git a/test/unit/test_Rationals.cc b/test/unit/test_Rationals.cc
@@ -1,5 +1,5 @@
 #include <gtest/gtest.h>
-#include <common/Real.h>
+#include <common/numbers/Real.h>
 
 #include <vector>