[bug#38214] [PATCH v2] gnu: Add minisat.

[Robert Smith]

* gnu/packages/maths.scm (minisat): New variable.
---
I updated the source to the latest commit available, which unfortunately
only gets us from 2010 to 2013. Although the minisat-friend-declaration
patch was written by the original author in 2014, they never committed
it to the repo. Additionally an install patch is still needed to avoid a
dependency on our own shared library. Hopefully all style issues have
been fixed, and a copyright line was added.

 gnu/packages/maths.scm                        | 42 +++++++++++++++++++
 .../patches/minisat-friend-declaration.patch  | 25 +++++++++++
 gnu/packages/patches/minisat-install.patch    | 19 +++++++++
 3 files changed, 86 insertions(+)
 create mode 100644 gnu/packages/patches/minisat-friend-declaration.patch
 create mode 100644 gnu/packages/patches/minisat-install.patch

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 16a9d97a47..42a72737da 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -32,6 +32,7 @@
 ;;; Copyright © 2018 Amin Bandali <address@hidden>
 ;;; Copyright © 2019 Nicolas Goaziou <address@hidden>
 ;;; Copyright © 2019 Steve Sprang <address@hidden>
+;;; Copyright © 2019 Robert Smith <address@hidden>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -5242,3 +5243,44 @@ fields of knowledge.")
     (home-page "http://speedcrunch.org/";)
     (license license:gpl2+)))
 
+(define-public minisat
+  ;; This is the last commit which is available upstream, no
+  ;; release happened since 2010.
+  (let ((commit "37dc6c67e2af26379d88ce349eb9c4c6160e8543")
+        (revision "1"))
+    (package
+      (name "minisat")
+      (version (string-append "2.2.0-" revision "." (string-take commit 7)))
+      (source
+       (origin
+        (method git-fetch)
+        (uri (git-reference
+          (url "https://github.com/niklasso/minisat.git";)
+          (commit commit)))
+        (file-name (string-append name "-" version "-checkout"))
+        (sha256
+         (base32
+          "091hf3qkm197s5r7xcr3m07xsdwyz2rqk1hc9kj0hn13imz09irq"))
+        (patches
+         (search-patches "minisat-friend-declaration.patch"
+                         "minisat-install.patch"))))
+      (build-system gnu-build-system)
+      (arguments
+       '(#:make-flags (list (string-append "prefix=" %output))
+         #:tests? #f ;no check target
+         #:phases
+         (modify-phases %standard-phases
+           (delete 'configure))))
+      (inputs
+       `(("zlib:static" ,zlib "static")
+         ("zlib" ,zlib)))
+      (synopsis
+       "Small, yet efficient, SAT solver with good documentation")
+      (description
+       "MiniSat is a minimalistic, open-source SAT solver, developed to help
+researchers and developers alike to get started on SAT.  It is released under
+the MIT licence, and is currently used in a number of projects.")
+      (home-page
+       "http://minisat.se/MiniSat.html";)
+      (license license:expat))))
+
diff --git a/gnu/packages/patches/minisat-friend-declaration.patch 
b/gnu/packages/patches/minisat-friend-declaration.patch
new file mode 100644
index 0000000000..14a886ae2f
--- /dev/null
+++ b/gnu/packages/patches/minisat-friend-declaration.patch
@@ -0,0 +1,25 @@
+See https://groups.google.com/forum/#!topic/minisat/FCocZsC8oMQ
+This seems to only be a problem with newer versions of g++, and
+upstream development seems to have stopped in 2013.
+
+diff -rupN minisat-2.2.0/core/SolverTypes.h 
minisat-2.2.0.patched/core/SolverTypes.h
+--- a/minisat/core/SolverTypes.h       2010-07-10 17:07:36.000000000 +0100
++++ b/minisat/core/SolverTypes.h       2014-03-29 11:57:49.000000000 +0000
+@@ -47,7 +47,7 @@ struct Lit {
+     int     x;
+
+     // Use this as a constructor:
+-    friend Lit mkLit(Var var, bool sign = false);
++    //friend Lit mkLit(Var var, bool sign = false);
+
+     bool operator == (Lit p) const { return x == p.x; }
+     bool operator != (Lit p) const { return x != p.x; }
+@@ -55,7 +55,7 @@ struct Lit {
+ };
+
+
+-inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + 
(int)sign; return p; }
++inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var 
+ (int)sign; return p; }
+ inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; 
}
+ inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned 
int)b; return q; }
+ inline  bool sign      (Lit p)              { return p.x & 1; }
diff --git a/gnu/packages/patches/minisat-install.patch 
b/gnu/packages/patches/minisat-install.patch
new file mode 100644
index 0000000000..23cde89bec
--- /dev/null
+++ b/gnu/packages/patches/minisat-install.patch
@@ -0,0 +1,19 @@
+Avoid the default dynamic executable, which depends on minisat.so
+Instead install the release version, which is statically linked.
+
+diff --git a/Makefile b/Makefile
+index ceb9d77..7b91906 100644
+--- a/Makefile
++++ b/Makefile
+@@ -191,9 +191,9 @@ install-lib: $(BUILD_DIR)/release/lib/$(MINISAT_SLIB) 
$(BUILD_DIR)/dynamic/lib/$
+       ln -sf $(MINISAT_DLIB).$(SOMAJOR) $(DESTDIR)$(libdir)/$(MINISAT_DLIB)
+       $(INSTALL) -m 644 $(BUILD_DIR)/release/lib/$(MINISAT_SLIB) 
$(DESTDIR)$(libdir)
+ 
+-install-bin: $(BUILD_DIR)/dynamic/bin/$(MINISAT)
++install-bin: $(BUILD_DIR)/release/bin/$(MINISAT)
+       $(INSTALL) -d $(DESTDIR)$(bindir)
+-      $(INSTALL) -m 755 $(BUILD_DIR)/dynamic/bin/$(MINISAT) 
$(DESTDIR)$(bindir)
++      $(INSTALL) -m 755 $(BUILD_DIR)/release/bin/$(MINISAT) 
$(DESTDIR)$(bindir)
+ 
+ clean:
+       rm -f $(foreach t, release debug profile dynamic, $(foreach o, 
$(SRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \
-- 
2.24.0