feat(nix): add pd4 dependencies

CMakeLists.txt

@@ -6,7 +6,7 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
 
 include(Solver)
 
-set(CMAKE_CXX_STANDARD 17)
+set(CMAKE_CXX_STANDARD 20)
 set(CMAKE_CXX_STANDARD_REQUIRED ON)
 
 set(CMAKE_POSITION_INDEPENDENT_CODE ON)
@@ -24,6 +24,7 @@ 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)
@@ -32,10 +33,12 @@ if(USE_GLUCOSE)
 endif()
 
 include_directories(${CMAKE_CURRENT_SOURCE_DIR})
+include_directories(${CMAKE_CURRENT_SOURCE_DIR}/3rdParty/glucose-3.0)
 include_directories(${GMP_INCLUDE_DIRS})
 include_directories(${GMPXX_INCLUDE_DIRS})
 include_directories(${Boost_INCLUDE_DIRS})
 include_directories(${MtKaHyPar_INCLUDE_DIR})
+include_directories(${arjun_INCLUDE_DIR})
 
 add_library(caching OBJECT
     src/caching/BucketAllocator.cpp
@@ -62,6 +65,8 @@ add_library(heuristics OBJECT
     src/heuristics/cnf/PhaseSelectorManager.cpp
     src/heuristics/cnf/PhaseSelectorNone.cpp
     src/heuristics/cnf/PhaseSelectorStatic.cpp
+    src/heuristics/cnf/ProjBackupHeuristicComponents.cpp
+    src/heuristics/cnf/ProjBackupHeuristicHypergraph.cpp
     src/heuristics/cnf/ScoringMethodDlcs.cpp
     src/heuristics/cnf/ScoringMethodJwts.cpp
     src/heuristics/cnf/ScoringMethodMom.cpp
@@ -74,13 +79,15 @@ add_library(heuristics OBJECT
     src/heuristics/PhaseHeuristicOccurrence.cpp
     src/heuristics/PhaseHeuristicPolarity.cpp
     src/heuristics/PhaseHeuristicTrue.cpp
+    src/heuristics/ProjBackupHeuristic.cpp
     src/heuristics/ScoringMethod.cpp
 )
 
 add_library(hyperGraph OBJECT
     src/hyperGraph/HyperEdge.cpp
     src/hyperGraph/HyperGraph.cpp
     src/hyperGraph/HyperGraphExtractorDual.cpp
+    src/hyperGraph/HyperGraphExtractorDualProj.cpp
     src/hyperGraph/HyperGraphExtractorPrimal.cpp
 )
 
@@ -95,8 +102,11 @@ add_library(partitioner OBJECT
 )
 
 add_library(preprocs OBJECT
+    src/preprocs/cnf/util/PreprocGPMC.cpp
     src/preprocs/cnf/PreprocBackboneCnf.cpp
     src/preprocs/cnf/PreprocBasicCnf.cpp
+    src/preprocs/cnf/PreprocGPMC.cpp
+    src/preprocs/cnf/PreprocProj.cpp
     src/preprocs/PreprocManager.cpp
 )
 
@@ -144,7 +154,7 @@ add_library(core STATIC
     $<TARGET_OBJECTS:utils>
 )
 
-target_link_libraries(core GMP::GMPXX GMP::GMP MtKaHyPar::MtKaHyPar)
+target_link_libraries(core GMP::GMPXX GMP::GMP MtKaHyPar::MtKaHyPar arjun)
 
 if(USE_GLUCOSE)
     target_link_libraries(core glucose::glucose)

flake.nix

@@ -77,11 +77,40 @@
         {
           default = self.packages.${system}.d4;
 
-          mt-kahypar = mt-kahypar pkgs;
-          mt-kahypar-windows = mt-kahypar pkgs-windows;
+          cadical = pkgs.pkgsStatic.callPackage ./nix/cadical.nix { };
+          cadiback = pkgs.pkgsStatic.callPackage ./nix/cadiback.nix {
+            cadical = self.packages.${system}.cadical;
+          };
+
+          cryptominisat = pkgs.pkgsStatic.callPackage ./nix/cryptominisat.nix {
+            cadiback = self.packages.${system}.cadiback;
+          };
+
+          sbva = pkgs.pkgsStatic.callPackage ./nix/sbva.nix { };
+
+          arjun = pkgs.pkgsStatic.callPackage ./nix/arjun.nix {
+            cryptominisat = self.packages.${system}.cryptominisat;
+            sbva = self.packages.${system}.sbva;
+          };
+
+          tbb = tbb pkgs;
+          tbb-windows = tbb pkgs-windows;
+
+          mt-kahypar = pkgs.callPackage ./nix/mt-kahypar.nix { tbb = self.packages.${system}.tbb; };
+          mt-kahypar-windows = pkgs-windows.callPackage ./nix/mt-kahypar.nix {
+            tbb = self.packages.${system}.tbb-windows;
+          };
+
+          d4 = pkgs.callPackage ./nix/d4.nix {
+            mt-kahypar = self.packages.${system}.mt-kahypar;
+            arjun = self.packages.${system}.arjun;
+          };
 
-          d4 = d4 pkgs;
-          d4-windows = d4 pkgs-windows;
+          # 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;
+          #};
 
           container = pkgs.dockerTools.buildLayeredImage {
             name = "d4";

nix/arjun-remove-feenableexcept.patch

@@ -0,0 +1,14 @@
+diff --git a/src/main.cpp b/src/main.cpp
+index f77514c..7ffae38 100644
+--- a/src/main.cpp
++++ b/src/main.cpp
+@@ -347,9 +347,6 @@ void set_config(ArjunNS::Arjun* arj) {
+
+ int main(int argc, char** argv) {
+     arjun = new ArjunNS::Arjun;
+-    #if defined(__GNUC__) && defined(__linux__)
+-    feenableexcept(FE_INVALID   | FE_DIVBYZERO | FE_OVERFLOW);
+-    #endif
+
+     //Reconstruct the command line so we can emit it later if needed
+     string command_line;

nix/arjun.nix

@@ -0,0 +1,46 @@
+{
+  lib,
+  stdenv,
+  fetchFromGitHub,
+  cmake,
+  boost,
+  mpfr,
+  cryptominisat,
+  sbva,
+}:
+stdenv.mkDerivation {
+  pname = "arjun";
+  version = "2.5.4";
+
+  outputs = [
+    "out"
+    "lib"
+    "dev"
+  ];
+
+  src = fetchFromGitHub {
+    owner = "meelgroup";
+    repo = "arjun";
+    rev = "f2b736f6b49425c95060868a0ec5b69b89c9c3b6";
+    hash = "sha256-80DE1fRY4YKAv7d1YoOioUA7AvFsv5OKOobc/YSoqNo=";
+  };
+
+  patches = [ ./arjun-remove-feenableexcept.patch ];
+
+  nativeBuildInputs = [ cmake ];
+
+  buildInputs = [
+    boost.dev
+    mpfr.dev
+    cryptominisat.dev
+    sbva.dev
+  ];
+
+  meta = {
+    mainProgram = "arjun";
+    description = "CNF minimizer and minimal independent set calculator";
+    homepage = "https://github.com/meelgroup/arjun";
+    license = lib.licenses.mit;
+    platforms = lib.platforms.unix ++ lib.platforms.windows;
+  };
+}

nix/cadiback.nix

@@ -0,0 +1,34 @@
+{
+  lib,
+  stdenv,
+  fetchFromGitHub,
+  cadical,
+  cmake,
+}:
+stdenv.mkDerivation {
+  pname = "cadiback";
+  version = "0.2.1";
+
+  outputs = [
+    "out"
+    "dev"
+  ];
+
+  src = fetchFromGitHub {
+    owner = "uulm-janbaudisch";
+    repo = "cadiback";
+    rev = "f538594d0497a2db127ab9fcfec655aaad5acf04";
+    hash = "sha256-T+bMuQV9CPIidwjnwgVB0RYsKDD6hEVwZrCDrEhlVxk=";
+  };
+
+  nativeBuildInputs = [ cmake ];
+
+  buildInputs = [ cadical.dev ];
+
+  meta = {
+    description = "CaDiCaL BackBone Analyzer";
+    homepage = "https://github.com/meelgroup/cadiback";
+    license = lib.licenses.mit;
+    platforms = lib.platforms.unix ++ lib.platforms.windows;
+  };
+}

nix/cadical.nix

@@ -0,0 +1,33 @@
+{
+  lib,
+  stdenv,
+  fetchFromGitHub,
+  cmake,
+}:
+stdenv.mkDerivation {
+  pname = "cadical";
+  version = "2.0.0";
+
+  outputs = [
+    "out"
+    "lib"
+    "dev"
+  ];
+
+  src = fetchFromGitHub {
+    owner = "uulm-janbaudisch";
+    repo = "cadical";
+    rev = "31c08cf1feca40146b17a0db4d2e669914713183";
+    hash = "sha256-8Grth+su2/oeLxshFxU2oT2VUHdFYdZa7XDaeyiUEJc=";
+  };
+
+  nativeBuildInputs = [ cmake ];
+
+  meta = {
+    mainProgram = "cadical";
+    description = "CaDiCaL SAT Solver";
+    homepage = "https://github.com/arminbiere/cadical";
+    license = lib.licenses.mit;
+    platforms = lib.platforms.unix ++ lib.platforms.windows;
+  };
+}

nix/cryptominisat-cadiback-include.patch

@@ -0,0 +1,13 @@
+diff --git a/src/backbone.cpp b/src/backbone.cpp
+index dc8ec8d4d..e8db1892c 100644
+--- a/src/backbone.cpp
++++ b/src/backbone.cpp
+@@ -21,7 +21,7 @@ THE SOFTWARE.
+ ***********************************************/
+
+ #include "solver.h"
+-#include "../cadiback/cadiback.h"
++#include "cadiback.h"
+
+ using namespace CMSat;
+

nix/cryptominisat.nix

@@ -0,0 +1,44 @@
+{
+  lib,
+  stdenv,
+  fetchFromGitHub,
+  cmake,
+  gmp,
+  zlib,
+  cadiback,
+}:
+stdenv.mkDerivation rec {
+  pname = "cryptominisat";
+  version = "5.11.22";
+
+  outputs = [
+    "out"
+    "lib"
+    "dev"
+  ];
+
+  src = fetchFromGitHub {
+    owner = "msoos";
+    repo = "cryptominisat";
+    rev = version;
+    hash = "sha256-9Uk2exQWCkL/eqF7d1++BkXyl/gxVi4ThB4kv7F7BbE=";
+  };
+
+  patches = [ ./cryptominisat-cadiback-include.patch ];
+
+  nativeBuildInputs = [ cmake ];
+
+  buildInputs = [
+    zlib.dev
+    cadiback.dev
+    gmp.dev
+  ];
+
+  meta = {
+    mainProgram = "cryptominisat5";
+    description = "An advanced SAT solver";
+    homepage = "https://github.com/msoos/cryptominisat";
+    license = lib.licenses.mit;
+    platforms = lib.platforms.unix ++ lib.platforms.windows;
+  };
+}

nix/d4.nix

@@ -6,6 +6,7 @@
   boost,
   gmp,
   mt-kahypar,
+  arjun,
 }:
 stdenv.mkDerivation rec {
   pname = "d4";
@@ -17,6 +18,7 @@ stdenv.mkDerivation rec {
 
   buildInputs = [
     mt-kahypar.dev
+    arjun.dev
     boost.dev
     gmp.dev
   ];

nix/sbva-remove-feenableexcept.patch

@@ -0,0 +1,16 @@
+diff --git a/src/main.cpp b/src/main.cpp
+index f1a0fca..17f442b 100644
+--- a/src/main.cpp
++++ b/src/main.cpp
+@@ -95,11 +95,6 @@ int main(int argc, char **argv) {
+         .help("Preserve model count. Adds additional clauses but allows the tool to be used in propositional model ");
+     program.add_argument("files").remaining().help("input file and output file");
+
+-
+-    #if defined(__GNUC__) && defined(__linux__)
+-    feenableexcept(FE_INVALID   | FE_DIVBYZERO | FE_OVERFLOW);
+-    #endif
+-
+     //Reconstruct the command line so we can emit it later if needed
+     string command_line;
+     for(int i = 0; i < argc; i++) {

nix/sbva.nix

@@ -0,0 +1,35 @@
+{
+  lib,
+  stdenv,
+  fetchFromGitHub,
+  cmake,
+}:
+stdenv.mkDerivation {
+  pname = "sbva";
+  version = "0.0.0";
+
+  outputs = [
+    "out"
+    "lib"
+    "dev"
+  ];
+
+  src = fetchFromGitHub {
+    owner = "meelgroup";
+    repo = "SBVA";
+    rev = "b1c46c0d234c99314f16841e01b874282c94f101";
+    hash = "sha256-6VsxHfPpf7+exdeHDNlYYugtVIm/AIde03jnYmCcgjM=";
+  };
+
+  patches = [ ./sbva-remove-feenableexcept.patch ];
+
+  nativeBuildInputs = [ cmake ];
+
+  meta = {
+    mainProgram = "sbva";
+    description = "Structured BVA CNF rewriter";
+    homepage = "https://github.com/meelgroup/SBVA";
+    license = lib.licenses.mit;
+    platforms = lib.platforms.unix ++ lib.platforms.windows;
+  };
+}