Skip to content

Commit

Permalink
fix(cadical): use patches insteads of own repos
Browse files Browse the repository at this point in the history
  • Loading branch information
uulm-janbaudisch committed Oct 15, 2024
1 parent bf051cc commit e2022eb
Show file tree
Hide file tree
Showing 5 changed files with 180 additions and 6 deletions.
18 changes: 18 additions & 0 deletions nix/cadiback-cmake.patch
Original file line number Diff line number Diff line change
@@ -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)
44 changes: 44 additions & 0 deletions nix/cadiback-remove-cadical-internals.patch
Original file line number Diff line number Diff line change
@@ -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<int>& 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 = "<stdout>";
@@ -1592,7 +1586,6 @@ int doit (const std::vector<int>& cnf,
/* printf ("s UNSATISFIABLE\n"); */
}

- print_statistics ();
dbg ("deleting solver");
}

11 changes: 8 additions & 3 deletions nix/cadiback.nix
Original file line number Diff line number Diff line change
Expand Up @@ -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 ];
Expand Down
105 changes: 105 additions & 0 deletions nix/cadical-cmake.patch
Original file line number Diff line number Diff line change
@@ -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)
8 changes: 5 additions & 3 deletions nix/cadical.nix
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand Down

0 comments on commit e2022eb

Please sign in to comment.