[bug#68347] [PATCH] gnu: Add cadical

[bug#68347] [PATCH] gnu: Add cadical

[Max Heisinger]

 From 89b262587c67bb2761f7bf62f3d2f5dfc065c669 Mon Sep 17 00:00:00 2001
Message-ID: <89b262587c67bb2761f7bf62f3d2f5dfc065c669.1704807579.git.maximilian.heisinger@jku.at>
From: Max Heisinger <maximilian.heisinger@jku.at>
Date: Tue, 9 Jan 2024 14:26:56 +0100
Subject: [PATCH] gnu: Add CaDiCaL.

* gnu/packages/maths.scm (cadical): Add package.

Change-Id: I300d454ce79623c737b9208623bcce0dde798f14
---
  gnu/packages/maths.scm | 91 ++++++++++++++++++++++++++++++++++++++++++
  1 file changed, 91 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index adc7beb655..2b21ce3db2 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -8925,6 +8925,97 @@ (define-public kissat
  optimized algorithms and implementation.")
      (license license:expat)))
  
+(define-public cadical
+  (package
+    (name "cadical")
+    (version "1.9.4")
+    (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))
+       (sha256
+        (base32 "1sd3r1czgm6h36fa5if2npnjpfnxjnzlnc2srkbwi2ywvsysyavi"))))
+    (build-system gnu-build-system)
+    (inputs (list xz gzip lzip bzip2 p7zip))
+    (arguments
+     (list
+      #:test-target "test"
+      #:phases #~(modify-phases %standard-phases
+                   (add-after 'unpack 'patch-source
+                     (lambda* (#:key inputs outputs source #:allow-other-keys)
+                       (substitute* "src/file.cpp"
+                         (("(bzip2|gzip|lzma|xz) -c" all cmd)
+                          (string-append (search-input-file inputs
+                                                            (string-append
+                                                             "bin/" cmd))
+                                         " -c"))
+                         (("7z ([ax])" all mode)
+                          (string-append (search-input-file inputs "bin/7z")
+                                         " " mode))
+                         ;; Since we hard-coded the paths, we no longer need to find
+                         ;; them.
+                         (("char \\*found = find\\_program \\(prg\\)")
+                          "const char* found = \"<configured-at-build-time>\"")
+                         (("delete\\[\\] found;")
+                          ""))
+                       (substitute* "scripts/make-build-header.sh"
+                         ;; The identifier in Guix is the source, as the input may be
+                         ;; replaced while building.
+                         (("`../scripts/get-git-id.sh`")
+                          source)
+                         ;; Remove non-determinism by removing the date from the
+                         ;; binary.
+                         (("\\$DATE")
+                          "<no non-deterministic timestamp in the binary>"))
+                       ;; Convert the static library to a shared one.
+                       (substitute* "makefile.in"
+                         (("libcadical\\.a")
+                          "libcadical.so")
+                         (("\\$\\(COMPILE\\) -o")
+                          (string-append "$(COMPILE) -Wl,-rpath="
+                                         (assoc-ref outputs "out") "/lib -o"))
+                         (("ar rc")
+                          "$(COMPILE) -shared -o"))
+                       (substitute* "test/api/run.sh"
+                         (("libcadical\\.a")
+                          "libcadical.so"))
+                       (substitute* "configure"
+                         (("-static")
+                          "-shared")
+                         ;; Tests are not written with a shared libcadical.so in
+                         ;; mind, so the LD_LIBRARY_PATH has to be set to the
+                         ;; libcadical.so in the build directory while running
+                         ;; tests. The rpath points to the installed directory and is
+                         ;; only available after installation.
+                         (("\\\\\\$\\(MAKE\\)")
+                          (string-append "export LD_LIBRARY_PATH="
+                                         (getcwd) "/build/ ; \\\\\\$(MAKE)"))
+                         (("CXXFLAGS=\"\\$CXXFLAGS\\$options\"")
+                          "CXXFLAGS=\"$CXXFLAGS$options -fPIC\""))))
+                   (replace 'configure
+                     (lambda* (#:key configure-flags #:allow-other-keys)
+                       ;; The configure script does not support standard GNU options.
+                       (apply invoke "./configure" configure-flags)))
+                   (replace 'install
+                     (lambda* (#:key inputs outputs #:allow-other-keys)
+                       (let ((out (assoc-ref outputs "out")))
+                         (install-file "build/cadical"
+                                       (string-append out "/bin"))
+                         (install-file "build/libcadical.so"
+                                       (string-append out "/lib"))
+                         (install-file "src/cadical.hpp"
+                                       (string-append out "/include"))))))))
+    (home-page "https://github.com/arminbiere/cadical")
+    (synopsis "CaDiCaL Simplified Satisfiability (SAT) Solver")
+    (description
+     "CaDiCaL is a hackable CDCL SAT solver written in C++. It offers an incremental
+API and a library for solving SAT problems given in CNF in the standard DIMACS
+format.")
+    (license license:expat)))
+
  (define-public aiger
    (package
      (name "aiger")

base-commit: 8920cf302c5a2fd457a2629afe24cf4768f1fed7
-- 
2.41.0

[bug#68347] [PATCH] gnu: Add cadical

[Sören Tempel]

Hi,

I also started working on a CaDiCaL package for a channel of mine [1].
My version is very similar but uses a Fedora-based patch to build a
shared library instead of substitutions. However, the approach chosen
here is also fine with me.

Is there a chance that this could get merged so that we can join forces
and maintain a single CaDiCaL package in the main Guix repository? :)

Best,
Sören

[1]: https://github.com/agra-uni-bremen/guix-symex/commit/236b84c15bd7cc51bb935c7d85d2fbb270b30499

[bug#68347] [PATCH] gnu: Add cadical

[Max Heisinger]

Hi,

thank you for your patch-based approach Sören! I think yours is more readable
for the Makefile changes.

We could add the substitutions for 7z, xz, etc. and the changes to
scripts/make-build-header.sh in order to make the build reproducible and not
rely on runtime $PATH searches, then we'd have combined the best from both
patches - however I'd also be fine to start with my original version and add
the patch in a later revision.

I would also be happy if we could maintain a single CaDiCaL package in the main
Guix repository :)

Best,
Max