feat: add projected compilation

SoftVarE-Group · Oct 12, 2024 · 57d1721 · 57d1721
1 parent 639fe80
commit 57d1721
Show file tree

Hide file tree

Showing 65 changed files with 5,733 additions and 257 deletions.
diff --git a/.github/workflows/CI.yaml b/.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

diff --git a/3rdParty/GPMC/CMakeLists.txt b/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)

diff --git a/3rdParty/glucose-3.0/CMakeLists.txt b/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
 )
diff --git a/3rdParty/glucose-3.0/core/Main.cc b/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));

diff --git a/3rdParty/glucose-3.0/simp/Main.cc b/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));

diff --git a/3rdParty/glucose-3.0/utils/System.h b/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"
 
 //-------------------------------------------------------------------------------------------------

diff --git a/CMakeLists.txt b/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)

diff --git a/cmake/FindGPMC.cmake b/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()
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -16,6 +16,9 @@
         "x86_64-linux"
       ];
 
+      # If building for Windows, appends -windows, otherwise nothing.
+      windowsSuffix = pkgs: name: if pkgs.stdenv.hostPlatform.isWindows then "${name}-windows" else name;
+
       # Different platforms require different TBB versions and the Windows one is not in upstream Nixpkgs yet.
       tbb =
         pkgs:
@@ -26,23 +29,23 @@
         else
           pkgs.tbb_2021_11;
 
-      mt-kahypar = pkgs: pkgs.callPackage ./nix/mt-kahypar.nix { tbb = tbb pkgs; };
-      d4 = pkgs: pkgs.callPackage ./nix/d4.nix { mt-kahypar = mt-kahypar pkgs; };
-
       # All required runtime dependencies.
       dependencies =
         pkgs:
+        let
+          system = pkgs.stdenv.system;
+          windowsSuffix' = windowsSuffix pkgs;
+        in
         pkgs.buildEnv {
           name = "d4-dependencies";
           paths = [
-            (mt-kahypar pkgs)
-            (tbb pkgs)
+            self.packages.${system}.${windowsSuffix' "mt-kahypar"}
+            self.packages.${system}.${windowsSuffix' "tbb"}
             pkgs.hwloc.lib
             pkgs.gmp
           ] ++ lib.optionals pkgs.stdenv.cc.isClang [ pkgs.libcxx ];
         };
 
-      # A simple README explaining how to setup the built directories to run the binary.
       documentation =
         pkgs:
         pkgs.stdenv.mkDerivation {
@@ -57,12 +60,16 @@
       # The binary with all dependencies.
       bundled =
         pkgs:
+        let
+          system = pkgs.stdenv.system;
+          windowsSuffix' = windowsSuffix pkgs;
+        in
         pkgs.buildEnv {
           name = "d4";
           paths = [
-            (d4 pkgs)
-            (dependencies pkgs)
-            (documentation pkgs)
+            self.packages.${system}.${windowsSuffix' "d4"}
+            self.packages.${system}.${windowsSuffix' "dependencies"}
+            self.packages.${system}.${windowsSuffix' "documentation"}
           ];
         };
     in
@@ -72,29 +79,57 @@
         system:
         let
           pkgs = nixpkgs.legacyPackages.${system};
+          pkgs-static = if pkgs.stdenv.isDarwin then pkgs else pkgs.pkgsStatic;
           pkgs-windows = pkgs.pkgsCross.mingwW64;
         in
         {
           default = self.packages.${system}.d4;
 
-          cadical = pkgs.pkgsStatic.callPackage ./nix/cadical.nix { };
-          cadiback = pkgs.pkgsStatic.callPackage ./nix/cadiback.nix {
+          glucose = pkgs-static.callPackage ./nix/glucose.nix { };
+          glucose-windows = pkgs-windows.callPackage ./nix/glucose.nix { };
+
+          cadical = pkgs-static.callPackage ./nix/cadical.nix { };
+          cadical-windows = pkgs-windows.callPackage ./nix/cadical.nix { };
+
+          cadiback = pkgs-static.callPackage ./nix/cadiback.nix {
             cadical = self.packages.${system}.cadical;
           };
 
-          cryptominisat = pkgs.pkgsStatic.callPackage ./nix/cryptominisat.nix {
+          cadiback-windows = pkgs-windows.callPackage ./nix/cadiback.nix {
+            cadical = self.packages.${system}.cadical-windows;
+          };
+
+          cryptominisat = pkgs-static.callPackage ./nix/cryptominisat.nix {
+            cadical = self.packages.${system}.cadical;
             cadiback = self.packages.${system}.cadiback;
           };
 
-          sbva = pkgs.pkgsStatic.callPackage ./nix/sbva.nix { };
+          cryptominisat-windows = pkgs-windows.callPackage ./nix/cryptominisat.nix {
+            cadical = self.packages.${system}.cadical-windows;
+            cadiback = self.packages.${system}.cadiback-windows;
+          };
+
+          sbva = pkgs-static.callPackage ./nix/sbva.nix { };
+          sbva-windows = pkgs-windows.callPackage ./nix/sbva.nix { };
 
-          arjun = pkgs.pkgsStatic.callPackage ./nix/arjun.nix {
+          arjun = pkgs-static.callPackage ./nix/arjun.nix {
             cryptominisat = self.packages.${system}.cryptominisat;
             sbva = self.packages.${system}.sbva;
           };
 
-          gpmc = pkgs.pkgsStatic.callPackage ./nix/gpmc.nix {
+          arjun-windows = pkgs-windows.callPackage ./nix/arjun.nix {
+            cryptominisat = self.packages.${system}.cryptominisat-windows;
+            sbva = self.packages.${system}.sbva-windows;
+          };
+
+          gpmc = pkgs-static.callPackage ./nix/gpmc.nix {
             arjun = self.packages.${system}.arjun;
+            cryptominisat = self.packages.${system}.cryptominisat;
+          };
+
+          gpmc-windows = pkgs-windows.callPackage ./nix/gpmc.nix {
+            arjun = self.packages.${system}.arjun-windows;
+            cryptominisat = self.packages.${system}.cryptominisat-windows;
           };
 
           tbb = tbb pkgs;
@@ -108,13 +143,16 @@
           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
-          #d4-windows = pkgs-windows.callPackage ./nix/d4.nix {
-          #  mt-kahypar = self.packages.${system}.mt-kahypar-windows;
-          #  arjun = self.packages.${system}.arjun-windows;
-          #};
+          d4-windows = pkgs-windows.callPackage ./nix/d4.nix {
+            mt-kahypar = self.packages.${system}.mt-kahypar-windows;
+            arjun = self.packages.${system}.arjun-windows;
+            gpmc = self.packages.${system}.gmpc-windows;
+            glucose = self.packages.${system}.glucose-windows;
+          };
 
           container = pkgs.dockerTools.buildLayeredImage {
             name = "d4";
@@ -132,6 +170,9 @@
           dependencies = dependencies pkgs;
           dependencies-windows = dependencies pkgs-windows;
 
+          documentation = documentation pkgs;
+          documentation-windows = documentation pkgs-windows;
+
           bundled = bundled pkgs;
           bundled-windows = bundled pkgs-windows;
         }

diff --git a/nix/cryptominisat.nix b/nix/cryptominisat.nix
@@ -5,6 +5,7 @@
   cmake,
   gmp,
   zlib,
+  cadical,
   cadiback,
 }:
 stdenv.mkDerivation rec {
@@ -30,10 +31,13 @@ stdenv.mkDerivation rec {
 
   buildInputs = [
     zlib.dev
+    cadical.dev
     cadiback.dev
     gmp.dev
   ];
 
+  cmakeFlags = [ "-DBUILD_SHARED_LIBS=OFF" ];
+
   meta = {
     mainProgram = "cryptominisat5";
     description = "An advanced SAT solver";

diff --git a/nix/d4.nix b/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; {