Refactor including files from minisat component

This is the first step towards cleaning up OpenSMT includes. The goal is to get to a state where the includes would work regardless if OpenSMT is used as a library or included as a subproject in another project. This should also help avoid name clashes with other projects.
usi-verification-and-security · Aug 8, 2024 · f95aeab · f95aeab
1 parent 8a15f5d
commit f95aeab
Show file tree

Hide file tree

Showing 51 changed files with 123 additions and 195 deletions.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -68,8 +68,7 @@ find_package(Threads REQUIRED)
 
 
 include_directories(
-    ${CMAKE_SOURCE_DIR}/minisat/mtl
-    ${CMAKE_SOURCE_DIR}/minisat/core
+    ${CMAKE_SOURCE_DIR}
     ${CMAKE_SOURCE_DIR}/common
     ${CMAKE_SOURCE_DIR}/sorts
     ${CMAKE_SOURCE_DIR}/symbols

diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt
@@ -53,7 +53,7 @@ if (BUILD_SHARED_LIBS)
         LIBRARY DESTINATION lib
         ARCHIVE DESTINATION lib
         RUNTIME DESTINATION bin
-        INCLUDES DESTINATION include
+        INCLUDES DESTINATION include ${INSTALL_HEADERS_DIR}
     )
 
     install(EXPORT OpenSMTTargets

diff --git a/src/cnfizers/TermMapper.h b/src/cnfizers/TermMapper.h
@@ -26,8 +26,8 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef TERMMAPPER_H
 #define TERMMAPPER_H
 #include "Logic.h"
-#include "Map.h"
 #include "PTRef.h"
+#include <minisat/mtl/Map.h>
 
 class TermMapper {
 private:

diff --git a/src/common/CMakeLists.txt b/src/common/CMakeLists.txt
@@ -1,11 +1,11 @@
-add_library(common OBJECT "FastRational.cc" Real.h)
+add_library(common OBJECT "")
 
 target_sources(common
-    PUBLIC "${CMAKE_CURRENT_LIST_DIR}/FastRational.h"
-    PUBLIC "${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc"
+    PUBLIC
+        "${CMAKE_CURRENT_LIST_DIR}/FastRational.cc"
+        "${CMAKE_CURRENT_LIST_DIR}/FlaPartitionMap.cc"
+        "${CMAKE_CURRENT_LIST_DIR}/Real.h"
     PRIVATE
-    "${CMAKE_CURRENT_LIST_DIR}/Alloc.h"
-    "${CMAKE_CURRENT_LIST_DIR}/XAlloc.h"
     "${CMAKE_CURRENT_LIST_DIR}/SystemQueries.h"
     "${CMAKE_CURRENT_LIST_DIR}/Integer.h"
     "${CMAKE_CURRENT_LIST_DIR}/Number.h"
@@ -22,7 +22,7 @@ target_sources(common
 )
 
 install(FILES
-        Integer.h Number.h FastRational.h XAlloc.h Alloc.h StringMap.h Timer.h osmtinttypes.h
+        Integer.h Number.h FastRational.h StringMap.h Timer.h osmtinttypes.h
         TreeOps.h Real.h FlaPartitionMap.h PartitionInfo.h OsmtApiException.h TypeUtils.h
         NumberUtils.h NatSet.h ScopedVector.h
 DESTINATION ${INSTALL_HEADERS_DIR})

diff --git a/src/common/FastRational.h b/src/common/FastRational.h
@@ -6,14 +6,14 @@ Copyright (c) 2008, 2009 Centre national de la recherche scientifique (CNRS)
  */
 #ifndef FAST_RATIONALS_H
 #define FAST_RATIONALS_H
-#include <string>
 #include <gmpxx.h>
 #include <cassert>
 #include <climits>
-#include "Vec.h"
+#include <cstdint>
+#include <optional>
 #include <stack>
+#include <string>
 #include <vector>
-#include <optional>
 
 typedef int32_t  word;
 typedef uint32_t uword;

diff --git a/src/common/PartitionInfo.h b/src/common/PartitionInfo.h
@@ -10,8 +10,8 @@
 #include "InterpolationUtils.h"
 #include "PTRef.h"
 #include "SymRef.h"
-#include "SolverTypes.h"
 #include "FlaPartitionMap.h"
+#include <minisat/core/SolverTypes.h>
 
 
 class PartitionInfo {

diff --git a/src/common/StringMap.h b/src/common/StringMap.h
@@ -27,7 +27,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef STRINGMAP_H
 #define STRINGMAP_H
 
-#include "Map.h"
+#include <minisat/mtl/Map.h>
 
 //===================================================================================================
 // Specializations for string hashing (Map from mtl)

diff --git a/src/common/TreeOps.h b/src/common/TreeOps.h
@@ -13,7 +13,7 @@
 #include "Logic.h"
 #include "NatSet.h"
 #include "Pterm.h"
-#include "Vec.h"
+#include <minisat/mtl/Vec.h>
 
 #include <unordered_set>
 

diff --git a/src/itehandler/CMakeLists.txt b/src/itehandler/CMakeLists.txt
@@ -1,3 +1,5 @@
+
+
 add_library(itehandler OBJECT IteToSwitch.cc IteToSwitchMisc.cc IteHandler.cc)
-install(FILES IteToSwitch.h IteHandler.h DESTINATION ${INSTALL_HEADERS_DIR})
+
 
diff --git a/src/logics/Logic.h b/src/logics/Logic.h
@@ -14,11 +14,11 @@
 #include "SStore.h"
 #include "CgTypes.h"
 #include "LogicFactory.h"
-#include "MapWithKeys.h"
 #include "OsmtApiException.h"
 #include "FunctionTools.h"
 #include "TypeUtils.h"
 #include "NatSet.h"
+#include <minisat/mtl/MapWithKeys.h>
 
 #include <cassert>
 #include <cstring>

diff --git a/src/logics/SubstLoopBreaker.h b/src/logics/SubstLoopBreaker.h
@@ -4,13 +4,14 @@
 
 #ifndef OPENSMT_SUBSTLOOPBREAKER_H
 #define OPENSMT_SUBSTLOOPBREAKER_H
-#include <stdint.h>
+
 #include <PTRef.h>
-#include <Sort.h>
-#include <Alloc.h>
-#include <assert.h>
 #include <PtStructs.h>
 #include <Logic.h>
+#include <minisat/mtl/Sort.h>
+
+#include <cassert>
+#include <cstdint>
 
 // For breaking substitution loops
 enum class NStatus { inStack, complete, unseen };

diff --git a/src/logics/Theory.h b/src/logics/Theory.h
@@ -26,15 +26,12 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef THEORY_H
 #define THEORY_H
 
-#include <memory>
-
-#include "Logic.h"
 #include "BVLogic.h"
-
+#include "Logic.h"
+#include "PartitionManager.h"
 #include "UFTHandler.h"
-#include "Alloc.h"
 
-#include "PartitionManager.h"
+#include <memory>
 
 struct PreprocessingContext {
     std::size_t frameCount {0};

diff --git a/src/minisat/CMakeLists.txt b/src/minisat/CMakeLists.txt
@@ -1,12 +1,20 @@
 add_library(minisat INTERFACE)
 
-target_include_directories(minisat
-    INTERFACE ${CMAKE_CURRENT_LIST_DIR}/mtl
-    INTERFACE ${CMAKE_CURRENT_LIST_DIR}/core
-    )
+install(FILES 
+        mtl/Heap.h
+        mtl/Map.h
+        mtl/Vec.h
+        mtl/Alg.h
+        mtl/Sort.h
+        mtl/Queue.h
+        mtl/MapWithKeys.h
+        DESTINATION ${INSTALL_HEADERS_DIR}/minisat/mtl
+)
 
+install(FILES
+        core/SolverTypes.h
+        core/Alloc.h
+        core/XAlloc.h
+        DESTINATION ${INSTALL_HEADERS_DIR}/minisat/core)
 
-install(FILES 
-mtl/Heap.h mtl/Map.h mtl/Vec.h mtl/Alg.h mtl/Sort.h mtl/Queue.h core/SolverTypes.h mtl/MapWithKeys.h
- DESTINATION ${INSTALL_HEADERS_DIR})
 
diff --git a/src/common/Alloc.h → src/minisat/core/Alloc.h b/src/common/Alloc.h → src/minisat/core/Alloc.h
@@ -20,9 +20,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #ifndef Minisat_Alloc_h
 #define Minisat_Alloc_h
-#include "osmtinttypes.h"
+
 #include "XAlloc.h"
-#include "Vec.h"
+#include <minisat/mtl/Vec.h>
 
 //=================================================================================================
 // Simple Region-based memory allocator:

diff --git a/src/minisat/core/SolverTypes.h b/src/minisat/core/SolverTypes.h
@@ -22,9 +22,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_SolverTypes_h
 #define Minisat_SolverTypes_h
 
-#include "Alg.h"
-#include "Vec.h"
-#include "Map.h"
+#include <minisat/mtl/Alg.h>
+#include <minisat/mtl/Vec.h>
+#include <minisat/mtl/Map.h>
 #include "Alloc.h"
 
 #include <cassert>

diff --git a/src/common/XAlloc.h → src/minisat/core/XAlloc.h b/src/common/XAlloc.h → src/minisat/core/XAlloc.h
@@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_XAlloc_h
 #define Minisat_XAlloc_h
 
-#include <errno.h>
-#include <stdlib.h>
+#include <cerrno>
+#include <cstdlib>
 
 
 //=================================================================================================

diff --git a/src/minisat/mtl/Heap.h b/src/minisat/mtl/Heap.h
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define Minisat_Heap_h
 
 #include "Vec.h"
-#include "stdio.h"
+#include <cstdio>
 
 //=================================================================================================
 // A heap implementation with support for decrease/increase key.

diff --git a/src/minisat/mtl/Map.h b/src/minisat/mtl/Map.h
@@ -20,7 +20,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Map_h
 #define Minisat_Map_h
 
-#include "osmtinttypes.h"
 #include "Vec.h"
 #include <vector>
 

diff --git a/src/minisat/mtl/Vec.h b/src/minisat/mtl/Vec.h
@@ -22,13 +22,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Vec_h
 #define Minisat_Vec_h
 
+#include <minisat/core/XAlloc.h>
+
 #include <cassert>
-#include <new>
+#include <climits>
+#include <cstdint>
 #include <initializer_list>
-#include <vector>
+#include <new>
 #include <utility>
-#include "osmtinttypes.h"
-#include "XAlloc.h"
+#include <vector>
 
 //=================================================================================================
 // Automatically resizable arrays

diff --git a/src/options/SMTConfig.cc b/src/options/SMTConfig.cc
@@ -541,7 +541,6 @@ void
 SMTConfig::initializeConfig( )
 {
   // Set Global Default configuration
-  status                        = l_Undef;
   insertOption(o_produce_stats, new SMTOption(0));
 //  produce_stats                 = 0;
 //  produce_models                = 0;

diff --git a/src/options/SMTConfig.h b/src/options/SMTConfig.h
@@ -27,10 +27,11 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef SMTCONFIG_H
 #define SMTCONFIG_H
 
-#include "SolverTypes.h"
 #include "StringMap.h"
 #include "smt2tokens.h"
 
+#include <minisat/mtl/Vec.h>
+
 #include <cstring>
 #include <libgen.h>
 #include <iostream>
@@ -503,7 +504,6 @@ struct SMTConfig
     }
   }
 
-  lbool        status;                       // Status of the benchmark
 //  int          incremental;                  // Incremental solving
   int           isIncremental() const
      { return optionTable.has(o_incremental) ?

diff --git a/src/parallel/SplitData.h b/src/parallel/SplitData.h
@@ -8,8 +8,8 @@
 #ifndef PARALLEL_SPLITDATA_H
 #define PARALLEL_SPLITDATA_H
 
-#include "SolverTypes.h"
 #include "THandler.h"
+#include <minisat/core/SolverTypes.h>
 
 // -----------------------------------------------------------------------------------------
 // The splits

diff --git a/src/pterms/PtStructs.h b/src/pterms/PtStructs.h
@@ -8,8 +8,8 @@
 #ifndef OPENSMT_PTHELPERSTRUCTS_H
 #define OPENSMT_PTHELPERSTRUCTS_H
 
-#include "SolverTypes.h"
 #include "PTRef.h"
+#include <minisat/core/SolverTypes.h>
 
 class PtAsgn {
 public:

diff --git a/src/pterms/Pterm.h b/src/pterms/Pterm.h
@@ -28,9 +28,9 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef PTERM_H
 #define PTERM_H
 
-#include "Vec.h"
-#include "Sort.h"
-#include "SolverTypes.h"
+#include <minisat/mtl/Vec.h>
+#include <minisat/core/SolverTypes.h>
+#include <minisat/mtl/Sort.h>
 #include "SymRef.h"
 #include "PtStructs.h"
 

diff --git a/src/smtsolvers/CMakeLists.txt b/src/smtsolvers/CMakeLists.txt
@@ -1,6 +1,5 @@
 add_library(smtsolvers OBJECT "")
 
-
 list(APPEND PRIVATE_SOURCES_TO_ADD
 		"${CMAKE_CURRENT_SOURCE_DIR}/SimpSMTSolver.cc"
 		"${CMAKE_CURRENT_SOURCE_DIR}/CoreSMTSolver.cc"
@@ -37,9 +36,5 @@ target_sources(proof
 	PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/ResolutionProof.h"
 	PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}/ResolutionProof.cc")
 
-install(FILES TheoryInterpolator.h
-	 DESTINATION ${INSTALL_HEADERS_DIR})
-
-
-install(FILES SimpSMTSolver.h CoreSMTSolver.h
-		DESTINATION ${INSTALL_HEADERS_DIR})
+install(FILES TheoryInterpolator.h SimpSMTSolver.h CoreSMTSolver.h
+	 DESTINATION ${INSTALL_HEADERS_DIR})
diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc
@@ -48,19 +48,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "ModelBuilder.h"
 #include "OsmtInternalException.h"
-#include "Sort.h"
+#include "Random.h"
+#include "ReportUtils.h"
+#include "ResolutionProof.h"
+#include "SystemQueries.h"
 
 #include <cmath>
 #include <iostream>
 #include <iomanip>
 #include <algorithm>
 
-#include "ResolutionProof.h"
-#include "SystemQueries.h"
-#include "ReportUtils.h"
-
-#include "Random.h"
-
 namespace opensmt {
     extern bool stop;
 }

diff --git a/src/smtsolvers/CoreSMTSolver.h b/src/smtsolvers/CoreSMTSolver.h
@@ -55,11 +55,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <vector>
 
-#include "Vec.h"
-#include "Heap.h"
-#include "Alg.h"
+#include <minisat/mtl/Vec.h>
+#include <minisat/mtl/Heap.h>
+#include <minisat/mtl/Alg.h>
 
-#include "SolverTypes.h"
+#include <minisat/core/SolverTypes.h>
 
 #include "Timer.h"
 

diff --git a/src/smtsolvers/LAScore.h b/src/smtsolvers/LAScore.h
@@ -5,7 +5,7 @@
 #ifndef OPENSMT_LASCORE_H
 #define OPENSMT_LASCORE_H
 
-#include <SolverTypes.h>
+#include <minisat/core/SolverTypes.h>
 #include <SMTConfig.h>
 #include <TypeUtils.h>
 

diff --git a/src/smtsolvers/ResolutionProof.h b/src/smtsolvers/ResolutionProof.h
@@ -26,7 +26,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #ifndef PROOF2_H
 #define PROOF2_H
 
-#include "SolverTypes.h"
+#include <minisat/core/SolverTypes.h>
 #include <vector>
 #include <unordered_map>
 #include <iosfwd>
Original file line number	Diff line number	Diff line change
		@@ -1,3 +1,5 @@


		add_library(itehandler OBJECT IteToSwitch.cc IteToSwitchMisc.cc IteHandler.cc)
		install(FILES IteToSwitch.h IteHandler.h DESTINATION ${INSTALL_HEADERS_DIR})