From 5541a0aeb7660eacd5dbec8ef88db42af7b3b7b5 Mon Sep 17 00:00:00 2001
From: Maximilian Heisinger <mail@maxheisinger.at>
Date: Tue, 16 Aug 2022 20:59:06 +0200
Subject: [PATCH] gnu: Add cryptominisat5
* gnu/packages/maths.scm (cryptominisat5): Add package.
---
gnu/packages/maths.scm | 50 ++++++++++++++++++++++++++++++++++++++++++
1 file changed, 50 insertions(+)
@@ -55,6 +55,7 @@
;;; Copyright © 2022 Philip McGrath <philip@philipmcgrath.com>
;;; Copyright © 2022 Marek Felšöci <marek@felsoci.sk>
;;; Copyright © 2022 vicvbcun <guix@ikherbers.com>
+;;; Copyright © 2022 Maximilian Heisinger <mail@maxheisinger.at>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -159,6 +160,7 @@ (define-module (gnu packages maths)
#:use-module (gnu packages shells)
#:use-module (gnu packages sphinx)
#:use-module (gnu packages swig)
+ #:use-module (gnu packages sqlite)
#:use-module (gnu packages tcl)
#:use-module (gnu packages texinfo)
#:use-module (gnu packages tex)
@@ -7317,6 +7319,54 @@ (define-public minisat
"http://minisat.se/MiniSat.html")
(license license:expat))))
+(define-public cryptominisat5
+ (package
+ (name "cryptominisat5")
+ (version "5.8.0")
+ (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
+ "00hmxdlyhn7pwk9jlvc5g0l5z5xqfchjzf5jgn3pkj9xhl8yqq50"))))
+ (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 <vector>")
+ "#include <vector>\n#include <algorithm>"))
+ (substitute* "tests/CMakeLists.txt"
+ (("add_subdirectory\\(\\$\\{GTEST_PREFIX\\} gtest\\)")
+ "find_package(GTest REQUIRED)")
+ (("if\\(NOT ONLY_SIMPLE\\)") "if(FALSE)")))))))
+ (inputs (list zlib boost sqlite python python-numpy))
+ (native-inputs (list python-lit googletest))
+ (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 kissat
(package
(name "kissat")
--
2.37.2