From: Max Heisinger <maximilian.heisinger@jku.at>
To: 68347@debbugs.gnu.org
Subject: [bug#68347] [PATCH] gnu: Add cadical
Date: Tue, 9 Jan 2024 14:41:01 +0100 [thread overview]
Message-ID: <cb61e44b-4ae5-4a78-a90c-8e07baa4c693@jku.at> (raw)
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
next reply other threads:[~2024-01-09 15:26 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2024-01-09 13:41 Max Heisinger [this message]
2024-05-18 20:48 ` [bug#68347] [PATCH] gnu: Add cadical Sören Tempel
2024-05-22 14:22 ` Max Heisinger
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
List information: https://guix.gnu.org/
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=cb61e44b-4ae5-4a78-a90c-8e07baa4c693@jku.at \
--to=maximilian.heisinger@jku.at \
--cc=68347@debbugs.gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).