diff --git a/nix/cadiback-cmake.patch b/nix/cadiback-cmake.patch new file mode 100644 index 0000000..f85dfe6 --- /dev/null +++ b/nix/cadiback-cmake.patch @@ -0,0 +1,18 @@ +diff --git a/CMakeLists.txt b/CMakeLists.txt +new file mode 100644 +index 0000000..74d5300 +--- /dev/null ++++ b/CMakeLists.txt +@@ -0,0 +1,12 @@ ++cmake_minimum_required(VERSION 3.27) ++ ++project(CaDiBack VERSION 0.2.1 LANGUAGES CXX) ++ ++set(CMAKE_CXX_STANDARD 17) ++set(CMAKE_CXX_STANDARD_REQUIRED ON) ++ ++add_library(cadiback cadiback.cpp) ++target_link_libraries(cadiback cadical) ++set_target_properties(cadiback PROPERTIES PUBLIC_HEADER "cadiback.h") ++ ++install(TARGETS cadiback) diff --git a/nix/cadiback-remove-cadical-internals.patch b/nix/cadiback-remove-cadical-internals.patch new file mode 100644 index 0000000..a3289bd --- /dev/null +++ b/nix/cadiback-remove-cadical-internals.patch @@ -0,0 +1,44 @@ +diff --git a/cadiback.cpp b/cadiback.cpp +index c5135d8..8b6539c 100644 +--- a/cadiback.cpp ++++ b/cadiback.cpp +@@ -13,12 +13,9 @@ + // code from its library (from the 'CaDiCaL' source code directory'). + + #include "cadical.hpp" // Main 'CaDiCaL' API. +-#include "resources.hpp" // Get time and memory usage. +-#include "version.hpp" // Print 'CaDiCaL' version too. + + // 'CadiBack' build information is generated by './generate'. + +-#include "config.hpp" + namespace CadiBack { + + // Verbosity level: -1=quiet, 0=default, 1=verbose, INT_MAX=logging. +@@ -252,7 +249,7 @@ void fatal (const char *fmt, ...) { + double average (double a, double b) { return b ? a / b : 0; } + double percent (double a, double b) { return average (100 * a, b); } + +-double time () { return CaDiCaL::absolute_process_time (); } ++double time () { return 0; } + + void start_timer (double *timer) { + assert (!started); +@@ -1058,9 +1055,6 @@ int doit (const std::vector& cnf, + verbosity = _verb-2; + msg ("CadiBack BackBone Extractor"); + msg ("Copyright (c) 2023 Armin Biere University of Freiburg"); +- msg ("Version " VERSION " " GITID); +- msg ("CaDiCaL %s %s", CaDiCaL::version (), CaDiCaL::identifier ()); +- msg ("Compiled with '%s'", BUILD); + + files.backbone.file = stdout; + files.backbone.path = ""; +@@ -1592,7 +1586,6 @@ int doit (const std::vector& cnf, + /* printf ("s UNSATISFIABLE\n"); */ + } + +- print_statistics (); + dbg ("deleting solver"); + } + diff --git a/nix/cadiback.nix b/nix/cadiback.nix index aa934f2..1dce7bd 100644 --- a/nix/cadiback.nix +++ b/nix/cadiback.nix @@ -15,12 +15,17 @@ stdenv.mkDerivation { ]; src = fetchFromGitHub { - owner = "uulm-janbaudisch"; + owner = "meelgroup"; repo = "cadiback"; - rev = "f538594d0497a2db127ab9fcfec655aaad5acf04"; - hash = "sha256-T+bMuQV9CPIidwjnwgVB0RYsKDD6hEVwZrCDrEhlVxk="; + rev = "ea65a9442fc2604ee5f4ffd0f0fdd0bf481d5b42"; + hash = "sha256-r9SoZMS1vA+Ggfca6lOmAo9zsAqBu0v0YTXcTyTN9v8="; }; + patches = [ + ./cadiback-cmake.patch + ./cadiback-remove-cadical-internals.patch + ]; + nativeBuildInputs = [ cmake ]; buildInputs = [ cadical.dev ]; diff --git a/nix/cadical-cmake.patch b/nix/cadical-cmake.patch new file mode 100644 index 0000000..b5472ee --- /dev/null +++ b/nix/cadical-cmake.patch @@ -0,0 +1,105 @@ +diff --git a/CMakeLists.txt b/CMakeLists.txt +new file mode 100644 +index 0000000..d030bfa +--- /dev/null ++++ b/CMakeLists.txt +@@ -0,0 +1,99 @@ ++cmake_minimum_required(VERSION 3.27) ++ ++project(CaDiCaL VERSION 2.0.0 LANGUAGES CXX) ++ ++add_compile_definitions( ++ NBUILD ++ NUNLOCKED ++) ++ ++add_library(libcadical ++ src/analyze.cpp ++ src/arena.cpp ++ src/assume.cpp ++ src/averages.cpp ++ src/backtrack.cpp ++ src/backward.cpp ++ src/bins.cpp ++ src/block.cpp ++ src/ccadical.cpp ++ src/checker.cpp ++ src/clause.cpp ++ src/collect.cpp ++ src/compact.cpp ++ src/condition.cpp ++ src/config.cpp ++ src/constrain.cpp ++ src/contract.cpp ++ src/cover.cpp ++ src/decide.cpp ++ src/decompose.cpp ++ src/deduplicate.cpp ++ src/drattracer.cpp ++ src/elim.cpp ++ src/ema.cpp ++ src/extend.cpp ++ src/external.cpp ++ src/external_propagate.cpp ++ src/file.cpp ++ src/flags.cpp ++ src/flip.cpp ++ src/format.cpp ++ src/frattracer.cpp ++ src/gates.cpp ++ src/idruptracer.cpp ++ src/instantiate.cpp ++ src/internal.cpp ++ src/ipasir.cpp ++ src/lidruptracer.cpp ++ src/limit.cpp ++ src/logging.cpp ++ src/lookahead.cpp ++ src/lratbuilder.cpp ++ src/lratchecker.cpp ++ src/lrattracer.cpp ++ src/lucky.cpp ++ src/message.cpp ++ src/minimize.cpp ++ src/occs.cpp ++ src/options.cpp ++ src/parse.cpp ++ src/phases.cpp ++ src/probe.cpp ++ src/profile.cpp ++ src/proof.cpp ++ src/propagate.cpp ++ src/queue.cpp ++ src/random.cpp ++ src/reap.cpp ++ src/reduce.cpp ++ src/rephase.cpp ++ src/report.cpp ++ src/resources.cpp ++ src/restart.cpp ++ src/restore.cpp ++ src/score.cpp ++ src/shrink.cpp ++ src/signal.cpp ++ src/solution.cpp ++ src/solver.cpp ++ src/stats.cpp ++ src/subsume.cpp ++ src/terminal.cpp ++ src/ternary.cpp ++ src/transred.cpp ++ src/util.cpp ++ src/var.cpp ++ src/veripbtracer.cpp ++ src/version.cpp ++ src/vivify.cpp ++ src/walk.cpp ++ src/watch.cpp ++) ++ ++set_target_properties(libcadical PROPERTIES ++ OUTPUT_NAME "cadical" ++ PUBLIC_HEADER src/cadical.hpp ++) ++ ++install(TARGETS libcadical) diff --git a/nix/cadical.nix b/nix/cadical.nix index 662de67..f9d16df 100644 --- a/nix/cadical.nix +++ b/nix/cadical.nix @@ -15,12 +15,14 @@ stdenv.mkDerivation { ]; src = fetchFromGitHub { - owner = "uulm-janbaudisch"; + owner = "arminbiere"; repo = "cadical"; - rev = "31c08cf1feca40146b17a0db4d2e669914713183"; - hash = "sha256-8Grth+su2/oeLxshFxU2oT2VUHdFYdZa7XDaeyiUEJc="; + rev = "rel-2.1.0"; + hash = "sha256-sSvJgHxsRaJ/xHEK32fox0MFI7u+pj5ERLfNn2s8kC8="; }; + patches = [ ./cadical-cmake.patch ]; + nativeBuildInputs = [ cmake ]; meta = {