diff --git a/flake.lock b/flake.lock index 0d6a636a..5e411f5d 100644 --- a/flake.lock +++ b/flake.lock @@ -2,11 +2,11 @@ "nodes": { "nixpkgs": { "locked": { - "lastModified": 1723556749, - "narHash": "sha256-+CHVZnTnIYRLYsARInHYoWkujzcRkLY/gXm3s5bE52o=", + "lastModified": 1727540905, + "narHash": "sha256-40J9tW7Y794J7Uw4GwcAKlMxlX2xISBl6IBigo83ih8=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "4a92571f9207810b559c9eac203d1f4d79830073", + "rev": "fbca5e745367ae7632731639de5c21f29c8744ed", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 1eb89fd5..6f763f26 100644 --- a/flake.nix +++ b/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; diff --git a/nix/arjun-remove-feenableexcept.patch b/nix/arjun-remove-feenableexcept.patch new file mode 100644 index 00000000..71b76c22 --- /dev/null +++ b/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; diff --git a/nix/arjun.nix b/nix/arjun.nix new file mode 100644 index 00000000..05df6663 --- /dev/null +++ b/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; + }; +} diff --git a/nix/cadiback.nix b/nix/cadiback.nix new file mode 100644 index 00000000..aa934f24 --- /dev/null +++ b/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; + }; +} diff --git a/nix/cadical.nix b/nix/cadical.nix new file mode 100644 index 00000000..662de675 --- /dev/null +++ b/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; + }; +} diff --git a/nix/cryptominisat-cadiback-include.patch b/nix/cryptominisat-cadiback-include.patch new file mode 100644 index 00000000..41401d64 --- /dev/null +++ b/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; + diff --git a/nix/cryptominisat.nix b/nix/cryptominisat.nix new file mode 100644 index 00000000..6deb6ea2 --- /dev/null +++ b/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; + }; +} diff --git a/nix/sbva-remove-feenableexcept.patch b/nix/sbva-remove-feenableexcept.patch new file mode 100644 index 00000000..af5ac847 --- /dev/null +++ b/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++) { diff --git a/nix/sbva.nix b/nix/sbva.nix new file mode 100644 index 00000000..18207318 --- /dev/null +++ b/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; + }; +}