feat: add projected compilation

.github/workflows/CI.yaml

@@ -18,7 +18,7 @@ jobs:
           - double: x86_64-linux
             system: x86_64-linux
             runner: ubuntu-24.04
-            flake: bundled
+            flake: d4
             interpreter: /lib64/ld-linux-x86-64.so.2
           - double: aarch64-darwin
             system: aarch64-darwin

3rdParty/GPMC/CMakeLists.txt

@@ -21,20 +21,19 @@ add_subdirectory(flow-cutter-pace17)
 add_library(gpmc
 	core/ComponentCache.cc
 	core/ComponentManager.cc
-	core/Counter.cc
 	core/Config.cc
+	core/Counter.cc
+	core/gpmc.cpp
 	core/Instance.cc
+	core/Solver.cc
 	ddnnf/DecisionTree.cc
-	core/Solver.cc 
 	utils/Options.cc
 	utils/System.cc
 	preprocessor/Preprocessor.cc
 	preprocessor/TestSolver.cc
 	preprocessor/lib_sharpsat_td/subsumer.cpp
 	preprocessor/TreeDecomposition.cc
 	preprocessor/IFlowCutter.cc
-    core/gpmc.cpp
-    core/Solver.h
 )
 
 set_target_properties(gpmc PROPERTIES PUBLIC_HEADER include/gpmc.hpp)

3rdParty/GPMC/core/Component.h

@@ -493,9 +493,9 @@ class ComponentCache {
 	inline void cleanAllDescendantsOf(CacheEntryID id);
 
 	void printStats() const {
-		printf("c o Cache lookup          = %"PRIu64"\n", num_cache_look_ups_);
-		printf("c o Cache hit             = %"PRIu64"\n", num_cache_hits_);
-		printf("c o Cache reduce          = %"PRIu64"\n", num_cache_reduce_);
+		printf("c o Cache lookup          = %" PRIu64"\n", num_cache_look_ups_);
+		printf("c o Cache hit             = %" PRIu64"\n", num_cache_hits_);
+		printf("c o Cache reduce          = %" PRIu64"\n", num_cache_reduce_);
 	}
 	// --- Added by k-hasimt --- END
 
@@ -666,8 +666,8 @@ class ComponentManager {
 	void printDimacs(const vec<CRef>& clauses, const ClauseAllocator& ca, const vec<lbool>& assign);
 
 	void printStats() const {
-		printf("c o Components            = %"PRIu64"\n", components);
-		printf("c o Split                 = %"PRIu64"\n", num_try_split);
+		printf("c o Components            = %" PRIu64"\n", components);
+		printf("c o Split                 = %" PRIu64"\n", num_try_split);
 		cache_.printStats();
 	}
 

3rdParty/GPMC/core/Counter.cc

@@ -856,19 +856,19 @@ void Counter<T_data>::printStats() const
 	if(verbosity_c) {
 		if(progress == COMPLETED || progress == FAILED) {
 			printf("c o [Statistics]\n");
-			printf("c o conflicts             = %-11"PRIu64" (count %"PRIu64", sat %"PRIu64")\n", conflicts, conflicts-conflicts_sg, conflicts_sg);
-			printf("c o decisions             = %-11"PRIu64" (count %"PRIu64", sat %"PRIu64")\n", decisions, decisions-decisions_sg, decisions_sg);
-			printf("c o propagations          = %-11"PRIu64" (count %"PRIu64", sat %"PRIu64")\n", propagations, propagations-propagations_sg, propagations_sg);
-			printf("c o simp dbs              = %-11"PRIu64" (%.3f s)\n", simp_dbs, simplify_time);
-			printf("c o reduce dbs            = %-11"PRIu64"\n", nbReduceDB);
-			printf("c o learnts (uni/bin/lbd2)= %"PRIu64"/%"PRIu64"/%"PRIu64"\n", nbUn, nbBin, nbDL2);
-			printf("c o last learnts          = %-11d (%"PRIu64" learnts removed, %4.2f%%)\n", learnts.size(), nbRemovedClauses, nbRemovedClauses * 100 / (double)conflicts);
+			printf("c o conflicts             = %-11" PRIu64" (count %" PRIu64", sat %" PRIu64")\n", conflicts, conflicts-conflicts_sg, conflicts_sg);
+			printf("c o decisions             = %-11" PRIu64" (count %" PRIu64", sat %" PRIu64")\n", decisions, decisions-decisions_sg, decisions_sg);
+			printf("c o propagations          = %-11" PRIu64" (count %" PRIu64", sat %" PRIu64")\n", propagations, propagations-propagations_sg, propagations_sg);
+			printf("c o simp dbs              = %-11" PRIu64" (%.3f s)\n", simp_dbs, simplify_time);
+			printf("c o reduce dbs            = %-11" PRIu64"\n", nbReduceDB);
+			printf("c o learnts (uni/bin/lbd2)= %" PRIu64"/%" PRIu64"/%" PRIu64"\n", nbUn, nbBin, nbDL2);
+			printf("c o last learnts          = %-11d (%" PRIu64" learnts removed, %4.2f%%)\n", learnts.size(), nbRemovedClauses, nbRemovedClauses * 100 / (double)conflicts);
 
 			printStatsOfCM();
-			printf("c o isolated_pvars        = %"PRIu64"\n", nIsoPVars());
-			printf("c o SAT calls             = %-11"PRIu64" (SAT %"PRIu64", UNSAT %"PRIu64")\n", solves, sats, solves-sats);
-			printf("c o SAT starts            = %"PRIu64"\n", starts);
-			printf("c o backjumps             = %-11"PRIu64" (sp %"PRIu64") [init %s / final %s]\n", nbackjumps+nbackjumps_sp, nbackjumps_sp, config.backjump ? "on" : "off", on_bj ? "on" : "off");
+			printf("c o isolated_pvars        = %" PRIu64"\n", nIsoPVars());
+			printf("c o SAT calls             = %-11" PRIu64" (SAT %" PRIu64", UNSAT %" PRIu64")\n", solves, sats, solves-sats);
+			printf("c o SAT starts            = %" PRIu64"\n", starts);
+			printf("c o backjumps             = %-11" PRIu64" (sp %" PRIu64") [init %s / final %s]\n", nbackjumps+nbackjumps_sp, nbackjumps_sp, config.backjump ? "on" : "off", on_bj ? "on" : "off");
 			printf("c o\n");
 		}
 		if(config.ddnnf) {

3rdParty/GPMC/utils/Options.h

@@ -282,15 +282,15 @@ class Int64Option : public Option
         if (range.begin == INT64_MIN)
             fprintf(stderr, "imin");
         else
-            fprintf(stderr, "%4"PRIi64, range.begin);
+            fprintf(stderr, "%4" PRIi64, range.begin);
 
         fprintf(stderr, " .. ");
         if (range.end == INT64_MAX)
             fprintf(stderr, "imax");
         else
-            fprintf(stderr, "%4"PRIi64, range.end);
+            fprintf(stderr, "%4" PRIi64, range.end);
 
-        fprintf(stderr, "] (default: %"PRIi64")\n", value);
+        fprintf(stderr, "] (default: %" PRIi64")\n", value);
         if (verbose){
             fprintf(stderr, "\n        %s\n", description);
             fprintf(stderr, "\n");

3rdParty/glucose-3.0/CMakeLists.txt

@@ -56,6 +56,6 @@ set_target_properties(binary PROPERTIES OUTPUT_NAME glucose)
 target_link_libraries(binary glucose)
 
 install(
-    TARGETS glucose
+    TARGETS glucose binary
     FILE_SET HEADERS DESTINATION include/glucose
 )

3rdParty/glucose-3.0/core/Main.cc

@@ -94,11 +94,6 @@ int main(int argc, char** argv)
         setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
         // printf("This is MiniSat 2.0 beta\n");
 
-#if defined(__linux__)
-        fpu_control_t oldcw, newcw;
-        _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
-        printf("c WARNING: for repeatability, setting FPU to use double precision\n");
-#endif
         // Extra options:
         //
         IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));

3rdParty/glucose-3.0/simp/Main.cc

@@ -96,11 +96,6 @@ int main(int argc, char** argv)
       setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
 
 
-#if defined(__linux__)
-        fpu_control_t oldcw, newcw;
-        _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
-        printf("WARNING: for repeatability, setting FPU to use double precision\n");
-#endif
         // Extra options:
         //
         IntOption    verb   ("MAIN", "verb",   "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));

3rdParty/glucose-3.0/utils/System.h

@@ -21,10 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Glucose_System_h
 #define Glucose_System_h
 
-#if defined(__linux__)
-#include <fpu_control.h>
-#endif
-
 #include "mtl/IntTypes.h"
 
 //-------------------------------------------------------------------------------------------------

CMakeLists.txt

@@ -18,19 +18,16 @@ if(NOT BUILD_SHARED_LIBS)
     set(GMP_USE_STATIC_LIBS ON)
     set(Boost_USE_STATIC_LIBS ON)
     set(MtKaHyPar_USE_STATIC_LIBS ON)
+    set(GPMC_USE_STATIC_LIBS ON)
     set(glucose_USE_STATIC_LIBS ON)
 endif()
 
 find_package(GMP REQUIRED)
 find_package(Boost REQUIRED COMPONENTS program_options)
 find_package(MtKaHyPar REQUIRED)
 find_package(arjun REQUIRED)
-
-# glucose is only needed when requested, which it is not by default.
-if(USE_GLUCOSE)
-    find_package(glucose REQUIRED)
-    include_directories(${glucose_INCLUDE_DIRS})
-endif()
+find_package(GPMC REQUIRED)
+find_package(glucose REQUIRED)
 
 include_directories(${CMAKE_CURRENT_SOURCE_DIR})
 include_directories(${CMAKE_CURRENT_SOURCE_DIR}/3rdParty/glucose-3.0)
@@ -39,6 +36,8 @@ include_directories(${GMPXX_INCLUDE_DIRS})
 include_directories(${Boost_INCLUDE_DIRS})
 include_directories(${MtKaHyPar_INCLUDE_DIR})
 include_directories(${arjun_INCLUDE_DIR})
+include_directories(${GMPC_INCLUDE_DIR})
+include_directories(${glucose_INCLUDE_DIRS})
 
 add_library(caching OBJECT
     src/caching/BucketAllocator.cpp
@@ -102,7 +101,9 @@ add_library(partitioner OBJECT
 )
 
 add_library(preprocs OBJECT
+    src/preprocs/cnf/util/lib_sharpsat_td/subsumer.cpp
     src/preprocs/cnf/util/PreprocGPMC.cpp
+    src/preprocs/cnf/util/TestSolver.cpp
     src/preprocs/cnf/PreprocBackboneCnf.cpp
     src/preprocs/cnf/PreprocBasicCnf.cpp
     src/preprocs/cnf/PreprocGPMC.cpp
@@ -154,7 +155,7 @@ add_library(core STATIC
     $<TARGET_OBJECTS:utils>
 )
 
-target_link_libraries(core GMP::GMPXX GMP::GMP MtKaHyPar::MtKaHyPar arjun)
+target_link_libraries(core MtKaHyPar::MtKaHyPar GPMC::GPMC arjun glucose::glucose GMP::GMPXX GMP::GMP cadiback cadical)
 
 if(USE_GLUCOSE)
     target_link_libraries(core glucose::glucose)

cmake/FindGPMC.cmake

@@ -0,0 +1,54 @@
+include(FindPackageHandleStandardArgs)
+
+# Keep track of the original library suffixes to reset them later.
+set(_gpmc_ORIG_CMAKE_FIND_LIBRARY_SUFFIXES ${CMAKE_FIND_LIBRARY_SUFFIXES})
+
+# Look for .a or .lib libraries in case of a static library.
+if(GPMC_USE_STATIC_LIBS)
+    set(CMAKE_FIND_LIBRARY_SUFFIXES .a .lib)
+endif()
+
+# Find libraries and headers.
+find_library(GPMC_LIBRARY NAMES gpmc)
+find_path(GPMC_INCLUDE_DIR NAMES gpmc.hpp)
+
+# Windows (dynamic): Also find import libraries.
+if(WIN32 AND NOT GPMC_USE_STATIC_LIBS)
+    set(CMAKE_FIND_LIBRARY_SUFFIXES .dll.a .lib)
+    find_library(GPMC_IMPORT_LIBRARY NAMES gpmc)
+endif()
+
+# Reset library suffixes.
+set(CMAKE_FIND_LIBRARY_SUFFIXES ${_gpmc_ORIG_CMAKE_FIND_LIBRARY_SUFFIXES})
+
+# Register the found package.
+if(WIN32 AND NOT GPMC_USE_STATIC_LIBS)
+    # Windows (dynamic): also require import libraries.
+    find_package_handle_standard_args(GPMC REQUIRED_VARS GPMC_LIBRARY GPMC_IMPORT_LIBRARY GPMC_INCLUDE_DIR)
+else()
+    find_package_handle_standard_args(GPMC REQUIRED_VARS GPMC_LIBRARY GPMC_INCLUDE_DIR)
+endif()
+
+if(GPMC_FOUND)
+    mark_as_advanced(GPMC_LIBRARY)
+    mark_as_advanced(GPMC_IMPORT_LIBRARY)
+    mark_as_advanced(GPMC_INCLUDE_DIR)
+
+    # Create targets in case not already done.
+    if(NOT TARGET GPMC::GPMC)
+        if(GPMC_USE_STATIC_LIBS)
+            add_library(GPMC::GPMC STATIC IMPORTED)
+        else()
+            add_library(GPMC::GPMC SHARED IMPORTED)
+        endif()
+
+        # Set library and include paths.
+        set_target_properties(GPMC::GPMC PROPERTIES IMPORTED_LOCATION ${GPMC_LIBRARY})
+        target_include_directories(GPMC::GPMC INTERFACE ${GPMC_INCLUDE_DIR})
+
+        # Windows (dynamic): Also set import library.
+        if(WIN32 AND NOT GPMC_USE_STATIC_LIBS)
+            set_target_properties(GPMC::GPMC PROPERTIES IMPORTED_IMPLIB ${GPMC_IMPORT_LIBRARY})
+        endif()
+    endif()
+endif()