From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp10.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id KPtNAhbKSmMGPwEAbAwnHQ (envelope-from ) for ; Sat, 15 Oct 2022 16:56:22 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp10.migadu.com with LMTPS id yGRFARbKSmPKDAAAG6o9tA (envelope-from ) for ; Sat, 15 Oct 2022 16:56:22 +0200 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 9E14A2528F for ; Sat, 15 Oct 2022 16:56:21 +0200 (CEST) Received: from localhost ([::1]:43514 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ojiaK-0001R5-M4 for larch@yhetil.org; Sat, 15 Oct 2022 10:56:20 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:37814) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1ojia4-0001Q9-6w for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:05 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:43345) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1ojia3-0000E1-VT for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ojia3-0001K7-RI for guix-patches@gnu.org; Sat, 15 Oct 2022 10:56:03 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#57181] [PATCH v2 4/4] gnu: Add cryptominisat. References: <923508243.78855.1660404889221@ox93.mailbox.org> In-Reply-To: <923508243.78855.1660404889221@ox93.mailbox.org> Resent-From: Liliana Marie Prikler Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 15 Oct 2022 14:56:03 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 57181 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 57181@debbugs.gnu.org Cc: mail@maxheisinger.at Received: via spool by 57181-submit@debbugs.gnu.org id=B57181.16658457565051 (code B ref 57181); Sat, 15 Oct 2022 14:56:03 +0000 Received: (at 57181) by debbugs.gnu.org; 15 Oct 2022 14:55:56 +0000 Received: from localhost ([127.0.0.1]:42420 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ojiZv-0001JK-Ou for submit@debbugs.gnu.org; Sat, 15 Oct 2022 10:55:56 -0400 Received: from mail-ej1-f68.google.com ([209.85.218.68]:34732) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ojiZs-0001IR-Sj for 57181@debbugs.gnu.org; Sat, 15 Oct 2022 10:55:54 -0400 Received: by mail-ej1-f68.google.com with SMTP id ot12so16207276ejb.1 for <57181@debbugs.gnu.org>; Sat, 15 Oct 2022 07:55:52 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:message-id:content-transfer-encoding:cc:to:subject :date:from:from:to:cc:subject:date:message-id:reply-to; bh=Z1IGjcsbRUZbjBdJTcSrD6Rgzp/fUbn+8c4vSLM0pX8=; b=nOm/5WicCkQk5ciZJCLXTFQhadBWWNlLB9cHx5leqeavruBkEKFmoi9JpHdkkfMTUX /d832YaN7QUTrfVNAw0Rt6aulBeLMf8Zpn2Fh3HRLvq6hJffX3KO2eUD5iVbF9MtmL+z OCrIwJ76WHOWwFQ7oqCAU8yZ3x4lPqxBm7kYfo2PhFM4x+GirY175x+Pud54nKoBpeSu Kp1jidElX7q2LOmGyOkYfePu8Tt3+vtDnfUfS5I4iHTv135WpkbV6Wa5NlcJijNPiUOU TAFmtbuHlcbQUkB0RRnYnIx9NvW3WCtZ9i+gkD30w+yGM4bHt0SYWWfCghaBmfujqkfn EqsQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=mime-version:message-id:content-transfer-encoding:cc:to:subject :date:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=Z1IGjcsbRUZbjBdJTcSrD6Rgzp/fUbn+8c4vSLM0pX8=; b=vd/tthEHNpahN/+nCzDkRshDhRV7QwIU0DfydGJQenuFhQ6DzObu3qb7Gjajgyk6gH mhNcWywh9gL0v8OAowqPvZbGtcAqLrcXq692EOO0YeaCJaTmtDUSiPma3lvjp/KHEqms zq20FmPZuS5uMgUrOlGBNKjJrYKB6s0cZk1gKX+owlKnC3F6urVgWxHXX0azrPWOwlMm u6F7Tu4AKecDv7rVVrozlhHPjKfl2qMcRkmPd16mD+XtUjyXl9Be726gi6SqA/6zckep BvELTyTYGPu3TzDHRYwtE3+5SHcMqJHPezaz+v2+3O1hWkDQjxqYzsXm5BvKE6fdnZdM RMCQ== X-Gm-Message-State: ACrzQf33IIk1+9f93ZU2FSGUrdjHFFppWlTom8+gbw8kWB8DqEIloxUI Ga9QMqwX4sebdtPMb6mGS48OO849nfU= X-Google-Smtp-Source: AMsMyM6E34ZPGbiU8sgUqy093Q9oVgBSDdHTi/XP7EFbMfiN9Sme0GPh1NoDwuHS/mG30n55zZ9KVA== X-Received: by 2002:a17:907:968e:b0:78d:d68d:6751 with SMTP id hd14-20020a170907968e00b0078dd68d6751mr2257485ejc.403.1665845747271; Sat, 15 Oct 2022 07:55:47 -0700 (PDT) Received: from lumine.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id f20-20020a17090631d400b0078a543e9301sm3129583ejf.200.2022.10.15.07.55.46 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 15 Oct 2022 07:55:46 -0700 (PDT) From: Liliana Marie Prikler Date: Sat, 15 Oct 2022 16:47:03 +0200 Content-Transfer-Encoding: 8bit Message-ID: <72146c36adf1eddc32377307b8855038b53e8cba.camel@gmail.com> MIME-Version: 1.0 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list 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" X-Migadu-Flow: FLOW_IN X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1665845781; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding:resent-cc: resent-from:resent-sender:resent-message-id:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=Z1IGjcsbRUZbjBdJTcSrD6Rgzp/fUbn+8c4vSLM0pX8=; b=Tcu27BlipHMPfCLKWvDgB7fyl4ou0NE/ZDj6E1b+aAEuPoOpyXwddbGPiC0cZqwI9nIaoO UaZ2j+Ikm6T4RFN7g0qyL/0IsiA+mPEvFHT415XKX/2YmDDzOtndmxheYTgRvMOSGNLD+X 9jsFMsdDyN6LGUThXATRNyzLJce5T13jPKojQl30/QjYYD7uqf2FxcqXoGGUJbmbEueN/4 JbFsPtsZVbHaFAQBMLwpdCDfKDkiY89mN795+XX5UUQm6HbBO/bbPCMNA/+9VP8Lu5zGKi KpPMw36DFp+1xtx6WVtT9ONRKOjtz0FT0eHK0MWvqvTw3ZvsBnlFJ03NTYSx5w== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1665845781; a=rsa-sha256; cv=none; b=SYQpW5eOniyMxQD0ep8Bl/n2QbxZoI7oR3q6ucKbyUD4ZzAzZ0U22uY4+uTX85PFE0JM9Y o8abF7ebsYt3QIA7tCP8+4LaXnF0DeNbO+08MbUAJxDkHWAateqdXzpnVeCnvicau4agKQ 8fS1C1fnJxu8N8j8Pj4u077ilcufXbRcecLtPfIVQjFGTNc75EU4pFHKEKq7phlmGDzDMu AF0Ae7K/UI/e/uSn+m4Z+NJOVvUNUuiU4BJKv62h6ooSWV9fXdsBNWNZ9Ohg/s336ofq7j 1Xa2uI3OdfpM9V913uDE38k+Oy6zUPNzisplQJy3pbpnhnGFYYgnR0tfjs8bTg== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b="nOm/5Wic"; dmarc=fail reason="SPF not aligned (relaxed)" header.from=gmail.com (policy=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" X-Migadu-Spam-Score: 8.10 X-Spam: Yes Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b="nOm/5Wic"; dmarc=fail reason="SPF not aligned (relaxed)" header.from=gmail.com (policy=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" X-Migadu-Queue-Id: 9E14A2528F X-Spam-Score: 8.10 X-Migadu-Spam: Yes X-Migadu-Scanner: scn0.migadu.com X-TUID: d5OaeXnNgiQE * gnu/packages/maths.scm (cryptominisat): New variable. Co-authored-by: Maximilian Heisinger --- gnu/packages/maths.scm | 51 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 58faa6674b..9db28239fd 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -56,6 +56,7 @@ ;;; Copyright © 2022 Marek Felšöci ;;; Copyright © 2022 vicvbcun ;;; Copyright © 2022 Liliana Marie Prikler +;;; Copyright © 2022 Maximilian Heisinger ;;; ;;; This file is part of GNU Guix. ;;; @@ -159,6 +160,7 @@ (define-module (gnu packages maths) #:use-module (gnu packages serialization) #:use-module (gnu packages shells) #:use-module (gnu packages sphinx) + #:use-module (gnu packages sqlite) #:use-module (gnu packages swig) #:use-module (gnu packages tcl) #:use-module (gnu packages texinfo) @@ -7542,6 +7544,55 @@ (define-public louvain-community community detection algorithm.") (license license:lgpl3+)))) +(define-public cryptominisat + (package + (name "cryptominisat") + (version "5.11.4") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/msoos/cryptominisat") + (commit version))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "1izjn44phjp9670s7bxrdx4p0r59idqwv3bm6sr0qnlqlha5z4zc")))) + (build-system cmake-build-system) + (arguments + (list + #:build-type "Release" + #:test-target "test" + #:configure-flags #~(list "-DENABLE_TESTING=ON" "-DSTATS=ON") + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'patch-source + (lambda* (#:key inputs #:allow-other-keys) + (substitute* "CMakeLists.txt" + (("add_subdirectory\\(utils/lingeling-ala\\)") "")) + ;; Transitively included in vendored gtest.h. Fixed in + ;; upstream: + ;; https://github.com/msoos/cryptominisat/pull/686 + (substitute* "tests/assump_test.cpp" + (("#include ") + "#include \n#include ")) + (substitute* "tests/CMakeLists.txt" + (("add_subdirectory\\(\\$\\{GTEST_PREFIX\\} gtest\\)") + "find_package(GTest REQUIRED)") + (("add_subdirectory\\(\\$\\{PROJECT_SOURCE_DIR\\}/utils/.*\\)") + ""))))))) + (inputs (list boost louvain-community python python-numpy sqlite zlib)) + (native-inputs (list googletest lingeling python python-wrapper python-lit)) + (synopsis "Incremental SAT solver") + (description + "CryptoMiniSat is an incremental SAT solver with both command line and +library (C++, C, Python) interfaces. The command-line interface takes a +@acronym{CNF, Conjunctive Normal Form} as an input in the DIMACS format with +the extension of XOR clauses. The library interfaces mimic this and also +allow incremental solving, including assumptions.") + (home-page "https://github.com/msoos/cryptominisat") + (license license:expat))) + (define-public libqalculate (package (name "libqalculate") -- 2.38.0