From e8eb84bb481cf5311ce810735e36c5f326761c2c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Wed, 6 Nov 2024 15:59:14 +0100 Subject: [PATCH] Moved number-related files into separate directory --- .clang-files | 5 +++-- src/common/CMakeLists.txt | 13 +++++-------- src/common/StringConv.h | 2 +- src/common/numbers/CMakeLists.txt | 17 +++++++++++++++++ src/common/{ => numbers}/FastRational.cc | 0 src/common/{ => numbers}/FastRational.h | 0 src/common/{ => numbers}/Integer.h | 4 ++-- src/common/{ => numbers}/Number.h | 0 src/common/{ => numbers}/NumberUtils.h | 0 src/common/{ => numbers}/Real.h | 0 src/logics/ArithLogic.cc | 1 - src/logics/ArithLogic.h | 2 +- src/logics/BVLogic.h | 2 +- src/simplifiers/LA.h | 2 +- src/tsolvers/bvsolver/BitBlaster.cc | 2 +- src/tsolvers/lasolver/CutCreator.h | 2 +- src/tsolvers/lasolver/Delta.h | 2 +- src/tsolvers/lasolver/FarkasInterpolator.cc | 2 +- src/tsolvers/lasolver/FarkasInterpolator.h | 2 +- src/tsolvers/lasolver/LASolver.cc | 4 ++-- src/tsolvers/lasolver/LASolver.h | 1 + src/tsolvers/lasolver/Polynomial.h | 2 +- src/tsolvers/lasolver/Simplex.h | 1 + src/tsolvers/lasolver/Tableau.h | 2 +- src/tsolvers/stpsolver/Converter.h | 2 +- src/tsolvers/stpsolver/STPStore.h | 2 +- test/unit/test_LIACutSolver.cc | 2 +- test/unit/test_LIAStrengthening.cc | 2 +- test/unit/test_Rationals.cc | 2 +- 29 files changed, 47 insertions(+), 31 deletions(-) create mode 100644 src/common/numbers/CMakeLists.txt rename src/common/{ => numbers}/FastRational.cc (100%) rename src/common/{ => numbers}/FastRational.h (100%) rename src/common/{ => numbers}/Integer.h (72%) rename src/common/{ => numbers}/Number.h (100%) rename src/common/{ => numbers}/NumberUtils.h (100%) rename src/common/{ => numbers}/Real.h (100%) diff --git a/.clang-files b/.clang-files index e3e62a49c..6a96950bd 100644 --- 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 index 4c615cd7b..85ddf6d9b 100644 --- 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 index 322811947..cd7815cd7 100644 --- 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 new file mode 100644 index 000000000..e103a21fd --- /dev/null +++ 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 + ${CMAKE_CURRENT_LIST_DIR}/Integer.h + ${CMAKE_CURRENT_LIST_DIR}/Number.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) diff --git a/src/common/FastRational.cc b/src/common/numbers/FastRational.cc similarity index 100% rename from src/common/FastRational.cc rename to src/common/numbers/FastRational.cc diff --git a/src/common/FastRational.h b/src/common/numbers/FastRational.h similarity index 100% rename from src/common/FastRational.h rename to src/common/numbers/FastRational.h diff --git a/src/common/Integer.h b/src/common/numbers/Integer.h similarity index 72% rename from src/common/Integer.h rename to src/common/numbers/Integer.h index 2f5ff3525..7d8e6c563 100644 --- a/src/common/Integer.h +++ b/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 b/src/common/numbers/Number.h similarity index 100% rename from src/common/Number.h rename to src/common/numbers/Number.h diff --git a/src/common/NumberUtils.h b/src/common/numbers/NumberUtils.h similarity index 100% rename from src/common/NumberUtils.h rename to src/common/numbers/NumberUtils.h diff --git a/src/common/Real.h b/src/common/numbers/Real.h similarity index 100% rename from src/common/Real.h rename to src/common/numbers/Real.h diff --git a/src/logics/ArithLogic.cc b/src/logics/ArithLogic.cc index 06ea34379..74c8b86c7 100644 --- a/src/logics/ArithLogic.cc +++ b/src/logics/ArithLogic.cc @@ -1,7 +1,6 @@ #include "ArithLogic.h" #include -#include #include #include #include diff --git a/src/logics/ArithLogic.h b/src/logics/ArithLogic.h index 12792de00..ecbdc9348 100644 --- a/src/logics/ArithLogic.h +++ b/src/logics/ArithLogic.h @@ -3,7 +3,7 @@ #include "Logic.h" -#include +#include #include diff --git a/src/logics/BVLogic.h b/src/logics/BVLogic.h index 6581fc75f..9103642dc 100644 --- a/src/logics/BVLogic.h +++ b/src/logics/BVLogic.h @@ -10,7 +10,7 @@ Module: New Logic for BitVector #include "Logic.h" -#include +#include namespace opensmt { diff --git a/src/simplifiers/LA.h b/src/simplifiers/LA.h index 9e41654d3..55d8391f1 100644 --- 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 #include -#include +#include #include diff --git a/src/tsolvers/bvsolver/BitBlaster.cc b/src/tsolvers/bvsolver/BitBlaster.cc index 3bd1b3219..b4f31cd18 100644 --- 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 #include -#include +#include namespace opensmt { diff --git a/src/tsolvers/lasolver/CutCreator.h b/src/tsolvers/lasolver/CutCreator.h index 5210964a6..f7c282964 100644 --- a/src/tsolvers/lasolver/CutCreator.h +++ b/src/tsolvers/lasolver/CutCreator.h @@ -12,8 +12,8 @@ #include "Polynomial.h" #include "SparseMatrix.h" -#include #include +#include #include namespace opensmt { diff --git a/src/tsolvers/lasolver/Delta.h b/src/tsolvers/lasolver/Delta.h index b44818922..5e3dbad02 100644 --- 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 +#include #include diff --git a/src/tsolvers/lasolver/FarkasInterpolator.cc b/src/tsolvers/lasolver/FarkasInterpolator.cc index d9f1dce3b..2628287df 100644 --- a/src/tsolvers/lasolver/FarkasInterpolator.cc +++ b/src/tsolvers/lasolver/FarkasInterpolator.cc @@ -16,7 +16,7 @@ #include #include -#include +#include #include #include diff --git a/src/tsolvers/lasolver/FarkasInterpolator.h b/src/tsolvers/lasolver/FarkasInterpolator.h index 8395f0986..f57658ce4 100644 --- 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 +#include #include #include diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc index f8cc78dac..1d11eaea0 100644 --- a/src/tsolvers/lasolver/LASolver.cc +++ b/src/tsolvers/lasolver/LASolver.cc @@ -7,12 +7,12 @@ #include "LASolver.h" #include "FarkasInterpolator.h" -#include #include "LIAInterpolator.h" #include "CutCreator.h" -#include #include +#include +#include #include diff --git a/src/tsolvers/lasolver/LASolver.h b/src/tsolvers/lasolver/LASolver.h index b24ef232c..eb09515b9 100644 --- a/src/tsolvers/lasolver/LASolver.h +++ b/src/tsolvers/lasolver/LASolver.h @@ -16,6 +16,7 @@ #include "Tableau.h" #include +#include #include #include diff --git a/src/tsolvers/lasolver/Polynomial.h b/src/tsolvers/lasolver/Polynomial.h index b67b9c108..e0e3da6c4 100644 --- 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 +#include #include #include diff --git a/src/tsolvers/lasolver/Simplex.h b/src/tsolvers/lasolver/Simplex.h index bc586096f..a8195ec89 100644 --- a/src/tsolvers/lasolver/Simplex.h +++ b/src/tsolvers/lasolver/Simplex.h @@ -10,6 +10,7 @@ #include "LRAModel.h" #include "Tableau.h" +#include #include namespace opensmt { diff --git a/src/tsolvers/lasolver/Tableau.h b/src/tsolvers/lasolver/Tableau.h index 97fe0256e..0dd26627b 100644 --- a/src/tsolvers/lasolver/Tableau.h +++ b/src/tsolvers/lasolver/Tableau.h @@ -10,7 +10,7 @@ #include "LAVar.h" #include "Polynomial.h" -#include +#include #include #include diff --git a/src/tsolvers/stpsolver/Converter.h b/src/tsolvers/stpsolver/Converter.h index 8e7c586ce..b196631b0 100644 --- 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 +#include #include #include diff --git a/src/tsolvers/stpsolver/STPStore.h b/src/tsolvers/stpsolver/STPStore.h index b9fafd304..3b7dae0fe 100644 --- 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 +#include #include #include diff --git a/test/unit/test_LIACutSolver.cc b/test/unit/test_LIACutSolver.cc index 4167865c6..86e71c235 100644 --- a/test/unit/test_LIACutSolver.cc +++ b/test/unit/test_LIACutSolver.cc @@ -1,5 +1,5 @@ #include -#include +#include #include #include diff --git a/test/unit/test_LIAStrengthening.cc b/test/unit/test_LIAStrengthening.cc index 0e6df84b5..b0608b25d 100644 --- a/test/unit/test_LIAStrengthening.cc +++ b/test/unit/test_LIAStrengthening.cc @@ -2,7 +2,7 @@ // Created by prova on 30.09.20. // #include -#include +#include #include namespace opensmt { diff --git a/test/unit/test_Rationals.cc b/test/unit/test_Rationals.cc index 2446a51d0..508a305e7 100644 --- a/test/unit/test_Rationals.cc +++ b/test/unit/test_Rationals.cc @@ -1,5 +1,5 @@ #include -#include +#include #include