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/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()

flake.nix

@@ -77,6 +77,9 @@
         {
           default = self.packages.${system}.d4;
 
+          glucose = pkgs.pkgsStatic.callPackage ./nix/glucose.nix { };
+          glucose-windows = pkgs-windows.callPackage ./nix/glucose.nix { };
+
           cadical = pkgs.pkgsStatic.callPackage ./nix/cadical.nix { };
           cadiback = pkgs.pkgsStatic.callPackage ./nix/cadiback.nix {
             cadical = self.packages.${system}.cadical;
@@ -95,6 +98,7 @@
 
           gpmc = pkgs.pkgsStatic.callPackage ./nix/gpmc.nix {
             arjun = self.packages.${system}.arjun;
+            cryptominisat = self.packages.${system}.cryptominisat;
           };
 
           tbb = tbb pkgs;
@@ -108,12 +112,15 @@
           d4 = pkgs.callPackage ./nix/d4.nix {
             mt-kahypar = self.packages.${system}.mt-kahypar;
             arjun = self.packages.${system}.arjun;
+            gpmc = self.packages.${system}.gpmc;
+            glucose = self.packages.${system}.glucose;
           };
 
-          # TODO: arjun on windows
+          # TODO: arjun + GPMC on windows
           #d4-windows = pkgs-windows.callPackage ./nix/d4.nix {
           #  mt-kahypar = self.packages.${system}.mt-kahypar-windows;
           #  arjun = self.packages.${system}.arjun-windows;
+          #  gmpc = self.packages.${system}.gmpc-windows;
           #};
 
           container = pkgs.dockerTools.buildLayeredImage {

nix/d4.nix

@@ -7,6 +7,8 @@
   gmp,
   mt-kahypar,
   arjun,
+  gpmc,
+  glucose,
 }:
 stdenv.mkDerivation rec {
   pname = "d4";
@@ -21,6 +23,8 @@ stdenv.mkDerivation rec {
     arjun.dev
     boost.dev
     gmp.dev
+    gpmc.dev
+    glucose.dev
   ];
 
   meta = with lib; {

nix/glucose.nix

@@ -0,0 +1,29 @@
+{
+  lib,
+  stdenv,
+  cmake,
+  zlib,
+}:
+stdenv.mkDerivation {
+  pname = "glucose";
+  version = "3.0.0";
+
+  outputs = [
+    "out"
+    "lib"
+    "dev"
+  ];
+
+  src = ./../3rdParty/glucose-3.0;
+
+  nativeBuildInputs = [ cmake ];
+
+  buildInputs = [ zlib.dev ];
+
+  meta = {
+    description = "SAT solver";
+    homepage = "https://github.com/audemard/glucose";
+    license = lib.licenses.mit;
+    platforms = lib.platforms.unix ++ lib.platforms.windows;
+  };
+}

nix/gpmc.nix

@@ -3,10 +3,13 @@
   stdenv,
   cmake,
   gmp,
-  arjun
+  zlib,
+  mpfr,
+  arjun,
+  cryptominisat,
 }:
 stdenv.mkDerivation {
-  pname = "gmpc";
+  pname = "gpmc";
   version = "1.0.1";
 
   outputs = [
@@ -22,7 +25,10 @@ stdenv.mkDerivation {
 
   buildInputs = [
     gmp.dev
+    mpfr.dev
+    zlib.dev
     arjun.dev
+    cryptominisat.dev
   ];
 
   meta = {