From 2a1a5176241c2062b1d4b1f379ca6fb945fb701f Mon Sep 17 00:00:00 2001
From: Maximilian Heisinger <mail@maxheisinger.at>
Date: Sun, 14 Aug 2022 21:09:59 +0200
Subject: [PATCH 2/2] PATCH] gnu: Add modern SAT solver kissat

* gnu/packages/maths.scm (kissat): Add package.
---
 gnu/packages/maths.scm | 55 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index f69c6ce6de..580751e516 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -7345,6 +7345,61 @@ (define-public cryptominisat5
     (home-page "https://github.com/msoos/cryptominisat")
     (license license:expat)))
 
+(define-public kissat
+  (package
+    (name "kissat")
+    (version "3.0.0")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/arminbiere/kissat")
+             (commit (string-append "rel-" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32
+         "04x4w760srbdi4zci0s747qxk717x5d2x59ixraxh5104s9nyn8b"))))
+    (build-system gnu-build-system)
+    (native-inputs (list xz gzip lzip bzip2))
+    (arguments
+     `(#:test-target "test"
+       #:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key configure-flags #:allow-other-keys)
+             ;; The configure script of kissat is custom and does not support
+             ;; standard GNU options like CONFIG_SHELL.  We therefore overwrite
+             ;; the default.
+             (apply invoke "./configure" "-shared" configure-flags)))
+         (add-before 'check 'patch-test
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             ;; "main" test fails in build container.  The list below includes
+             ;; all tests but the failing one.
+             (substitute* "build/makefile"
+               (("./tissat")
+                 "./tissat error utilities endianness ceil format references \\
+\treluctant random queue allocate array stack arena heap vector rank sort bump \\
+\toptions config init add file parse collect kitten solve coverage usage \\
+\tterminate"))))
+         (replace 'install
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (install-file
+              "build/kissat"
+              (string-append (assoc-ref outputs "out") "/bin"))
+             (install-file
+              "build/libkissat.so"
+              (string-append (assoc-ref outputs "out") "/lib"))
+             (install-file
+              "src/kissat.h"
+              (string-append (assoc-ref outputs "out") "/include/kissat")))))))
+    (home-page "https://github.com/arminbiere/kissat")
+    (synopsis "Bare-metal SAT solver")
+    (description
+     "Kissat is a bare-metal SAT-solver written in C.  It is a port of CaDiCaL
+back to C with improved data structures, better scheduling of inprocessing and
+optimized algorithms and implementation.")
+    (license license:expat)))
+
 (define-public libqalculate
   (package
     (name "libqalculate")
-- 
2.37.1