Received: (at submit) by debbugs.gnu.org; 9 Jan 2024 15:04:05 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Tue Jan 09 10:04:05 2024
Received: from localhost ([127.0.0.1]:40681 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1rNDe2-0002CA-O9
for submit <at> debbugs.gnu.org; Tue, 09 Jan 2024 10:04:04 -0500
Received: from lists.gnu.org ([2001:470:142::17]:58366)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <maximilian.heisinger@HIDDEN>) id 1rNCMK-0000rQ-A9
for submit <at> debbugs.gnu.org; Tue, 09 Jan 2024 08:41:37 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10])
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <maximilian.heisinger@HIDDEN>)
id 1rNCM7-0006nN-5p
for guix-patches@HIDDEN; Tue, 09 Jan 2024 08:41:23 -0500
Received: from emailsecure.uni-linz.ac.at ([140.78.3.66])
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from <maximilian.heisinger@HIDDEN>)
id 1rNCM4-00049e-TR
for guix-patches@HIDDEN; Tue, 09 Jan 2024 08:41:22 -0500
Received: from [140.78.11.12] (unknown [140.78.11.12])
(using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits))
(No client certificate requested)
by emailsecure.uni-linz.ac.at (Postfix) with ESMTPSA id 4T8XBj28Lrz2PRX
for <guix-patches@HIDDEN>; Tue, 9 Jan 2024 14:41:01 +0100 (CET)
Message-ID: <cb61e44b-4ae5-4a78-a90c-8e07baa4c693@HIDDEN>
Date: Tue, 9 Jan 2024 14:41:01 +0100
MIME-Version: 1.0
User-Agent: Mozilla Thunderbird
From: Max Heisinger <maximilian.heisinger@HIDDEN>
Subject: [PATCH] gnu: Add cadical
To: guix-patches@HIDDEN
Content-Language: en-US
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Received-SPF: pass client-ip=140.78.3.66;
envelope-from=maximilian.heisinger@HIDDEN; helo=emailsecure.uni-linz.ac.at
X-Spam_score_int: -41
X-Spam_score: -4.2
X-Spam_bar: ----
X-Spam_report: (-4.2 / 5.0 requ) BAYES_00=-1.9, RCVD_IN_DNSWL_MED=-2.3,
RCVD_IN_MSPIKE_H3=0.001, RCVD_IN_MSPIKE_WL=0.001, SPF_HELO_NONE=0.001,
SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: 1.7 (+)
X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org",
has NOT identified this incoming email as spam. The original
message has been attached to this so you can view it or label
similar future email. If you have any questions, see
the administrator of that system for details.
Content preview: From 89b262587c67bb2761f7bf62f3d2f5dfc065c669 Mon Sep 17
00:00:00 2001 Message-ID:
<89b262587c67bb2761f7bf62f3d2f5dfc065c669.1704807579.git.maximilian.heisinger@HIDDEN>
From: Max Heisinger <maximilia [...]
Content analysis details: (1.7 points, 10.0 required)
pts rule name description
---- ---------------------- --------------------------------------------------
1.7 URIBL_BLACK Contains an URL listed in the URIBL blacklist
[URIs: run.sh]
0.0 T_SPF_PERMERROR SPF: test of record failed (permerror)
-0.0 SPF_HELO_PASS SPF: HELO matches SPF record
-0.0 T_SCC_BODY_TEXT_LINE No description available.
X-Debbugs-Envelope-To: submit
X-Mailman-Approved-At: Tue, 09 Jan 2024 10:03:57 -0500
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>,
<mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: 0.7 (/)
From 89b262587c67bb2761f7bf62f3d2f5dfc065c669 Mon Sep 17 00:00:00 2001
Message-ID: <89b262587c67bb2761f7bf62f3d2f5dfc065c669.1704807579.git.maximilian.heisinger@HIDDEN>
From: Max Heisinger <maximilian.heisinger@HIDDEN>
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
Max Heisinger <maximilian.heisinger@HIDDEN>:guix-patches@HIDDEN.
Full text available.guix-patches@HIDDEN:bug#68347; Package guix-patches.
Full text available.
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997 nCipher Corporation Ltd,
1994-97 Ian Jackson.