aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--gnu/local.mk1
-rw-r--r--gnu/packages/maths.scm52
-rw-r--r--gnu/packages/patches/cadical-add-shared-library.patch49
3 files changed, 102 insertions, 0 deletions
diff --git a/gnu/local.mk b/gnu/local.mk
index 2adf196a87..b7a432cc1c 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1027,6 +1027,7 @@ dist_patch_DATA = \
%D%/packages/patches/breezy-fix-gio.patch \
%D%/packages/patches/byobu-writable-status.patch \
%D%/packages/patches/bubblewrap-fix-locale-in-tests.patch \
+ %D%/packages/patches/cadical-add-shared-library.patch \
%D%/packages/patches/calibre-no-updates-dialog.patch \
%D%/packages/patches/calibre-remove-test-sqlite.patch \
%D%/packages/patches/calibre-remove-test-unrar.patch \
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 21adc08a31..d19ffa289c 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9326,6 +9326,58 @@ the sequential @command{lingeling} and its parallel variants
also included.")
(license license:expat)))
+(define-public cadical
+ (package
+ (name "cadical")
+ (version "2.0.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/arminbiere/cadical")
+ (commit (string-append "rel-" version))))
+ (file-name (git-file-name name version))
+ (patches (search-patches "cadical-add-shared-library.patch"))
+ (sha256
+ (base32 "1dzjah3z34v89ka48hncwqkxrwl4xqn9947p0ipf39lxshrq91xa"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:test-target "test"
+ #:modules `(((guix build copy-build-system) #:prefix copy:)
+ (guix build gnu-build-system)
+ (guix build utils)
+ (ice-9 regex))
+ #:imported-modules %copy-build-system-modules
+ #:phases
+ #~(modify-phases %standard-phases
+ (replace 'configure
+ (lambda* (#:key configure-flags #:allow-other-keys)
+ (setenv "CXXFLAGS" "-DPIC -fPIC")
+ (apply invoke "./configure" configure-flags)))
+ (replace 'check
+ (lambda args
+ ;; Tests are incorrectly linked upstream.
+ ;; Since we don't install them, just work around this in the
+ ;; check phase.
+ (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/build"))
+ (apply (assoc-ref %standard-phases 'check) args)
+ (unsetenv "LD_LIBRARY_PATH")))
+ (replace 'install
+ (lambda args
+ (apply
+ (assoc-ref copy:%standard-phases 'install)
+ #:install-plan
+ `(("build" "bin" #:include ("cadical" "mobical"))
+ ("build" "lib" #:include-regexp ("libcadical\\.(a|so)$"))
+ ("src" "include" #:include ("cadical.h"))
+ ;; Internal headers used by cadiback.
+ ("src" "include/cadical" #:include-regexp ("\\.hpp$")))
+ args))))))
+ (home-page "https://github.com/arminbiere/cadical")
+ (synopsis "SAT solver")
+ (description "This package provides a SAT solver based on conflict-driven
+clause learning.")
+ (license license:expat)))
+
(define-public louvain-community
(let ((commit "8cc5382d4844af127b1c1257373740d7e6b76f1e")
(revision "1"))
diff --git a/gnu/packages/patches/cadical-add-shared-library.patch b/gnu/packages/patches/cadical-add-shared-library.patch
new file mode 100644
index 0000000000..a1ae786d13
--- /dev/null
+++ b/gnu/packages/patches/cadical-add-shared-library.patch
@@ -0,0 +1,49 @@
+From fcb865786b524917aa9d3df8745aca66716794bf Mon Sep 17 00:00:00 2001
+From: Mate Soos <soos.mate@gmail.com>
+Date: Sun, 2 Jun 2024 21:50:06 -0400
+Subject: [PATCH] Also add a dynamic library
+
+---
+Liliana Marie Prikler <liliana.prikler@gmail.com>:
+ Added -L.
+ Squashed fix for cadical and mobical.
+
+ makefile.in | 5 ++++-
+ 1 file changed, 4 insertions(+), 1 deletion(-)
+
+diff --git a/makefile.in b/makefile.in
+index 291cb3e3..d179f591 100644
+--- a/makefile.in
++++ b/makefile.in
+@@ -34,7 +34,7 @@ COMPILE=$(CXX) $(CXXFLAGS) -I$(DIR) -I$(ROOT)/src
+
+ #--------------------------------------------------------------------------#
+
+-all: libcadical.a cadical mobical
++all: libcadical.so libcadical.a cadical mobical
+
+ #--------------------------------------------------------------------------#
+
+@@ -54,10 +54,10 @@ contrib/%.o: $(ROOT)/contrib/%.cpp $(ROOT)/contrib/%.hpp $(ROOT)/src/*.hpp makef
+ # tester 'mobical') and the library are the main build targets.
+
+ cadical: src/cadical.o libcadical.a makefile
+- $(COMPILE) -o $@ $< -L. -lcadical $(LIBS)
++ $(COMPILE) -static -o $@ $< -L. -lcadical $(LIBS)
+
+ mobical: src/mobical.o libcadical.a makefile $(LIBS)
+- $(COMPILE) -o $@ $< -L. -lcadical
++ $(COMPILE) -static -o $@ $< -L. -lcadical
+
+ libcadical.a: $(OBJ_SOLVER) $(OBJ_CONTRIB) makefile
+ ar rc $@ $(OBJ_SOLVER) $(OBJ_CONTRIB)
+@@ -62,5 +62,8 @@ mobical: src/mobical.o libcadical.a makefile $(LIBS)
+ libcadical.a: $(OBJ_SOLVER) $(OBJ_CONTRIB) makefile
+ ar rc $@ $(OBJ_SOLVER) $(OBJ_CONTRIB)
+
++libcadical.so: $(OBJ_SOLVER) $(OBJ_CONTRIB) $(LIBS) makefile
++ $(COMPILE) -shared -o $@ $(OBJ_SOLVER) $(OBJ_CONTRIB) $(LIBS)
++
+ #--------------------------------------------------------------------------#
+
+ # Note that 'build.hpp' is generated and resides in the build directory. \ No newline at end of file