summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorLiliana Marie Prikler <liliana.prikler@gmail.com>2022-10-15 16:47:03 +0200
committerLiliana Marie Prikler <liliana.prikler@gmail.com>2022-11-26 14:03:53 +0100
commit2404afea8b51b5ddf3f29d1f050d6a5a93aeb0b1 (patch)
treeebd86f71fa6aeecf4d86a9f6296c7a71c6fabd6a
parentd3ce4a2619784e58876ae81cef0cf099e9206be4 (diff)
gnu: Add cryptominisat.
* gnu/packages/maths.scm (cryptominisat): New variable. Co-authored-by: Maximilian Heisinger <mail@maxheisinger.at>
-rw-r--r--gnu/packages/maths.scm51
1 files changed, 51 insertions, 0 deletions
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 5fc93fa4d8..531e3f0324 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -56,6 +56,7 @@
;;; Copyright © 2022 Marek Felšöci <marek@felsoci.sk>
;;; Copyright © 2022 vicvbcun <guix@ikherbers.com>
;;; Copyright © 2022 Liliana Marie Prikler <liliana.prikler@gmail.com>
+;;; Copyright © 2022 Maximilian Heisinger <mail@maxheisinger.at>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -159,6 +160,7 @@
#: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)
@@ -7529,6 +7531,55 @@ also included.")
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 <vector>")
+ "#include <vector>\n#include <algorithm>"))
+ (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")