[bug#57181] [PATCH] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat

[mail@maxheisinger.at]

[-- Attachment #1: Type: text/plain, Size: 2156 bytes --]

Hi,

> - fixed the commit message,
> - hard-coded the compression binaries (and made them regular inputs),
> - fixed the actual test failure,
> - used G-Expressions rather than quasiquoting.
>
> See 9ddd37d6ab59e2519bbcefad15ce62561128f0ee.

Thank you very much!  This really is clearer, better, and gives me more
pointers to research about Guix.

> the problem here is rather that cryptominisat seems to pull in lots of
> stuff that we'd rather have packaged separately instead of vendored
> (e.g. googletest).  Could you try unvendoring those things and place
> the remaining parts in the right location without a recursive
> checkout?

Yes, that would be better... Then we have two choices now I think:

 1. Try to unvendor everything and add minisat as transformed package
    with different sources + lingeling as a new package.  This would
    also still require to download the external test files as additional
    source repositories.
 2. Or we rely on using the ~ONLY_SIMPLE~ CMake option CryptoMiniSat
    offers that is meant to build a simpler binary, but also deactivates
    more complex tests.  We still build a complex binary (i.e. Boost
    program options for options parsing) by not setting it, but instead
    substitute the query for the option in the  ~test/CMakeLists.txt~
    file.  Additionally, we substitute some other issues away.

The second option loses some scripts and the more comprehensive tests.
I would argue though, that these would be better suited for developing
the solver and less for such a package management situation.  What is
your opinion about this trade-off?

> "Incremental solving" sounds easier to understand.

Changed it.

> If you have a Python interface, you probably also need python in
> inputs, no?

True - it is better to directly expose it.  I also took another look at
the solver's capabilities and output in more detail and added
python-numpy (required dependency for the py API) and sqlite (optional
dependency used for collecting statistics).

Thank you again for your patience and effort!  You find my updated patch
attached.

Best regards (now even written from an Emacs mail client),
Max


[-- Attachment #2: 0001-gnu-Add-cryptominisat5.patch --]
[-- Type: text/x-patch, Size: 3575 bytes --]

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