diff --git a/CMakeLists.txt b/CMakeLists.txt index ff5d3a48..00083e83 100644 --- a/CMakeLists.txt +++ b/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,6 +79,7 @@ add_library(heuristics OBJECT src/heuristics/PhaseHeuristicOccurrence.cpp src/heuristics/PhaseHeuristicPolarity.cpp src/heuristics/PhaseHeuristicTrue.cpp + src/heuristics/ProjBackupHeuristic.cpp src/heuristics/ScoringMethod.cpp ) @@ -81,6 +87,7 @@ 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_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) 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..8e2f9630 100644 --- a/flake.nix +++ b/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"; 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/d4.nix b/nix/d4.nix index 9d6d8879..273e9c55 100644 --- a/nix/d4.nix +++ b/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 ]; 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; + }; +}