05/09: gnu: Add cadical.

[guix-commits]

lilyp pushed a commit to branch master
in repository guix.

commit dcf77f8fca7754fbf873b8849044f44826d9fca1
Author: Liliana Marie Prikler <liliana.prikler@gmail.com>
AuthorDate: Sun Sep 29 11:00:56 2024 +0200

    gnu: Add cadical.
    
    * 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(+)

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