feat(nix): add pd4 dependencies

flake.nix

@@ -77,6 +77,22 @@
         {
           default = self.packages.${system}.d4;
 
+          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;
+          };
+
           mt-kahypar = mt-kahypar pkgs;
           mt-kahypar-windows = mt-kahypar pkgs-windows;
 

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/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;
+  };
+}