From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1.migadu.com ([2001:41d0:1008:1e59::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms8.migadu.com with LMTPS id wAvjFJllnWVuWAEAkFu2QA (envelope-from ) for ; Tue, 09 Jan 2024 16:26:17 +0100 Received: from aspmx1.migadu.com ([2001:41d0:303:e224::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1.migadu.com with LMTPS id AMbwEZllnWXvRQEA62LTzQ (envelope-from ) for ; Tue, 09 Jan 2024 16:26:17 +0100 X-Envelope-To: larch@yhetil.org Authentication-Results: aspmx1.migadu.com; dkim=none; spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org"; dmarc=fail reason="SPF not aligned (relaxed), No valid DKIM" header.from=jku.at (policy=none) ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1704813977; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding:resent-cc: resent-from:resent-sender:resent-message-id:list-id:list-help: list-unsubscribe:list-subscribe:list-post; bh=+7WT+ZiTFWaarwZ0fcu840sHTAOj0KNYhnZaHazE32k=; b=OpvDmfJMQGMVShKi88GlzBrL+7oaRAy2UoFHCiqXVU2drO+h4QZ/Yd+WsLy20nxMA2P2dy eDnWIy03e1iPNOztDLqBh2jtAuxK1yGxuENksYLABtZaQDsbiLkXfUop3/wVLsvvSIWmZm CViK2A1vRQg3nroORMHhf5Tv0p2TWJZKZ5rLp57c9Ox244OzquNtRD6RsXTotAWStakHuB wXT+O7C/N+v/K7+kGdjAaNdPEDlpNIWgQ4vWAKe6T7wRuvihkHGNXdqdA0H2OEmuCnHrHO adfO5sf2Epp/mk3bNZX4Y/6hFgM2SoxVQU17VA2n92o32VCzIxmF79sZDDTavw== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1704813977; a=rsa-sha256; cv=none; b=iyIZzzKzs30s/7gc1NJF14SmwiGBRPTMuMKwmkBjO5m50x3uPpbO3Cp5MAynqDeo50cRs7 rG7V85YM8nmJh51olN3EBtWP+5S693gQMKxHqi4dyRMp+03fqZn6KV45PvuEuW/PDEYdv1 xhgwST2fJZBCp+0YMaMwYjcexn1RZgiSGfMNqjzjXsz1Z0aONQQnaoaP8YxZbfXWByvnXa dndn/qWFrdszQ82diMm7INk6IN/ApMHShdooUvUDOJ7tnod23rdKDaCAeKOwWYdPLYBylY NNLCttlYID6j+Zs6sGhAU68VX4oF7LGe+J4U+vtN+9V210gk2u6FUImOaXHyqg== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=none; spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org"; dmarc=fail reason="SPF not aligned (relaxed), No valid DKIM" header.from=jku.at (policy=none) Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id EDF796669B for ; Tue, 9 Jan 2024 16:26:16 +0100 (CET) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1rNDzR-0000ml-Pf; Tue, 09 Jan 2024 10:26:06 -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 ) id 1rNDex-00086P-Gm for guix-patches@gnu.org; Tue, 09 Jan 2024 10:04:55 -0500 Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1rNDex-0001Od-7v for guix-patches@gnu.org; Tue, 09 Jan 2024 10:04:55 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1rNDf3-0002Dv-Qq for guix-patches@gnu.org; Tue, 09 Jan 2024 10:05:01 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#68347] [PATCH] gnu: Add cadical Resent-From: Max Heisinger Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 09 Jan 2024 15:05:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 68347 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 68347@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.17048126458469 (code B ref -1); Tue, 09 Jan 2024 15:05:01 +0000 Received: (at submit) by debbugs.gnu.org; 9 Jan 2024 15:04:05 +0000 Received: from localhost ([127.0.0.1]:40681 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rNDe2-0002CA-O9 for submit@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 ) id 1rNCMK-0000rQ-A9 for submit@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 ) id 1rNCM7-0006nN-5p for guix-patches@gnu.org; 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 ) id 1rNCM4-00049e-TR for guix-patches@gnu.org; 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 ; Tue, 9 Jan 2024 14:41:01 +0100 (CET) Message-ID: Date: Tue, 9 Jan 2024 14:41:01 +0100 MIME-Version: 1.0 User-Agent: Mozilla Thunderbird From: Max Heisinger 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@jku.at; 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-Mailman-Approved-At: Tue, 09 Jan 2024 10:03:57 -0500 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-Mailman-Approved-At: Tue, 09 Jan 2024 10:26:03 -0500 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: guix-patches-bounces+larch=yhetil.org@gnu.org X-Migadu-Flow: FLOW_IN X-Migadu-Country: US X-Migadu-Spam-Score: -4.90 X-Spam-Score: -4.90 X-Migadu-Queue-Id: EDF796669B X-Migadu-Scanner: mx12.migadu.com X-TUID: JTg/I2q58YV3 From 89b262587c67bb2761f7bf62f3d2f5dfc065c669 Mon Sep 17 00:00:00 2001 Message-ID: <89b262587c67bb2761f7bf62f3d2f5dfc065c669.1704807579.git.maximilian.heisinger@jku.at> From: Max Heisinger 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 = \"\"") + (("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") + "")) + ;; 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