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

[Robert Smith]

* gnu/packages/maths.scm (minisat): New variable.
---
 gnu/packages/maths.scm                        | 41 +++++++++++++++++++
 .../patches/minisat-friend-declaration.patch  | 23 +++++++++++
 .../patches/minisat-mroot-and-install.patch   | 30 ++++++++++++++
 3 files changed, 94 insertions(+)
 create mode 100644 gnu/packages/patches/minisat-friend-declaration.patch
 create mode 100644 gnu/packages/patches/minisat-mroot-and-install.patch

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 16a9d97a47..9271609843 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -5242,3 +5242,44 @@ fields of knowledge.")
     (home-page "http://speedcrunch.org/";)
     (license license:gpl2+)))
 
+(define-public minisat
+  (package
+    (name "minisat")
+    (version "2.2.0")
+    (source
+      (origin
+        (method url-fetch)
+        (uri (string-append "http://minisat.se/downloads/minisat-";
+                            version ".tar.gz"))
+        (sha256
+          (base32
+            "023qdnsb6i18yrrawlhckm47q8x0sl7chpvvw3gssfyw3j2pv5cj"))
+        (patches
+          (search-patches "minisat-friend-declaration.patch"
+                          "minisat-mroot-and-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)
+           (add-before 'build 'mroot
+             (lambda* (#:key inputs #:allow-other-keys)
+                      (setenv "MROOT" (getcwd))
+                      (chdir "simp")
+                      #t)))))
+    (inputs
+      `(("zlib:static" ,zlib "static")
+        ("zlib" ,zlib)
+        ("kernel-headers" ,linux-libre-headers)))
+    (home-page
+      "http://minisat.se/MiniSat.html";)
+    (synopsis
+      "Small, yet efficient, SAT solver with good documentation")
+    (license license:expat)
+    (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.")))
+
diff --git a/gnu/packages/patches/minisat-friend-declaration.patch 
b/gnu/packages/patches/minisat-friend-declaration.patch
new file mode 100644
index 0000000000..8283084086
--- /dev/null
+++ b/gnu/packages/patches/minisat-friend-declaration.patch
@@ -0,0 +1,23 @@
+See https://groups.google.com/forum/#!topic/minisat/FCocZsC8oMQ
+
+diff -rupN minisat-2.2.0/core/SolverTypes.h 
minisat-2.2.0.patched/core/SolverTypes.h
+--- a/core/SolverTypes.h       2010-07-10 17:07:36.000000000 +0100
++++ b/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-mroot-and-install.patch 
b/gnu/packages/patches/minisat-mroot-and-install.patch
new file mode 100644
index 0000000000..7862314f75
--- /dev/null
+++ b/gnu/packages/patches/minisat-mroot-and-install.patch
@@ -0,0 +1,30 @@
+Add install target, change default
+
+ * rs now default build target
+
+--- a/simp/Makefile
++++ b/simp/Makefile
+@@ -2,3 +2,8 @@
+ DEPDIR    = mtl utils core
+
+ include $(MROOT)/mtl/template.mk
++
++install:
++      mkdir -p $(DESTDIR)$(PREFIX)/bin
++      cp -f $(EXEC)_static $(DESTDIR)$(PREFIX)/bin/minisat
++
+--- a/mtl/template.mk
++++ b/mtl/template.mk
+@@ -29,11 +29,11 @@
+
+ .PHONY : s p d r rs clean
+
++rs:   $(EXEC)_static
+ s:    $(EXEC)
+ p:    $(EXEC)_profile
+ d:    $(EXEC)_debug
+ r:    $(EXEC)_release
+-rs:   $(EXEC)_static
+
+ libs: lib$(LIB)_standard.a
+ libp: lib$(LIB)_profile.a
-- 
2.24.0