(address . guix-patches@gnu.org)
cb61e44b-4ae5-4a78-a90c-8e07baa4c693@jku.at
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(+)
Toggle diff (106 lines)
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