diff mbox series

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

Message ID 87wnb74c7n.fsf@maxheisinger.at
State New
Headers show
Series [bug#57181] gnu: maths: Add newer SAT solvers cryptominisat5 and kissat | expand

Checks

Context Check Description
cbaines/comparison success View comparision
cbaines/git-branch success View Git branch
cbaines/applying patch success View Laminar job
cbaines/issue success View issue

Commit Message

Maximilian Heisinger Aug. 17, 2022, 6:26 a.m. UTC 
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

Comments

Liliana Marie Prikler Aug. 17, 2022, 8:16 p.m. UTC | #1 
Hi,

Am Mittwoch, dem 17.08.2022 um 08:26 +0200 schrieb
mail@maxheisinger.at:
> [...] [W]e 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?
Only running simple tests is preferable to running no tests at all.  If
you think that unvendoring everything is an unreasonable amount of
work, that's a viable solution.  However, we do strive to offer
complete packages, so feel free to do 1. :)

If you need some pointers as for the test files, ppsspp includes both
another package's source (not so great, needs better unvendoring) and
test files, and there's probably some other packages you could consult
as well.

> > "Incremental solving" sounds easier to understand.
> 
> Changed it.
LGTM.

> > 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).
Note that python is now missing from native-inputs, but python-lit is
in there.  I suppose you need python both as input (for linking) and
native-input (to run whatever python-lit is supposed to do).


Cheers
diff mbox series

Patch

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