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(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 72d5e9a83a..a01f386831 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -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