diff mbox series

[bug#73551,5/8] gnu: Add cadical.

Message ID 81e078aa4164ee1b92dfdb9f855c025230444d7a.1727601398.git.liliana.prikler@gmail.com
State New
Headers show
Series Update some SAT/ASP solvers | expand

Commit Message

Liliana Marie Prikler Sept. 29, 2024, 9 a.m. UTC 
* gnu/packages/patches/cadical-add-shared-library.patch: New file.
* gnu/local.mk (dist_patch_DATA): Register it here.
* gnu/packages/maths.scm (cadical): New variable.
---
 gnu/local.mk                                  |  1 +
 gnu/packages/maths.scm                        | 52 +++++++++++++++++++
 .../patches/cadical-add-shared-library.patch  | 49 +++++++++++++++++
 3 files changed, 102 insertions(+)
 create mode 100644 gnu/packages/patches/cadical-add-shared-library.patch
diff mbox series

Patch

diff --git a/gnu/local.mk b/gnu/local.mk
index 49660d4b3e..3d39016609 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 ab989e6af6..23015bc86a 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9290,6 +9290,58 @@  (define-public lingeling
 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