mirror of
https://git.in.rschanz.org/ryan77627/guix.git
synced 2024-11-07 07:26:13 -05:00
gnu: Add minisat.
* gnu/packages/patches/minisat-friend-declaration.patch: New file. * gnu/packages/patches/minisat-install.patch: New file. * gnu/local.mk (dist_patch_DATA): Add both files above. * gnu/packages/maths.scm (minisat): New exported variable. Signed-off-by: Mathieu Othacehe <m.othacehe@gmail.com>
This commit is contained in:
parent
5dea5cbc62
commit
3b7828cc7f
4 changed files with 86 additions and 0 deletions
|
@ -1131,6 +1131,8 @@ dist_patch_DATA = \
|
|||
%D%/packages/patches/metabat-fix-compilation.patch \
|
||||
%D%/packages/patches/mhash-keygen-test-segfault.patch \
|
||||
%D%/packages/patches/mingw-w64-6.0.0-gcc.patch \
|
||||
%D%/packages/patches/minisat-friend-declaration.patch \
|
||||
%D%/packages/patches/minisat-install.patch \
|
||||
%D%/packages/patches/mpc123-initialize-ao.patch \
|
||||
%D%/packages/patches/module-init-tools-moduledir.patch \
|
||||
%D%/packages/patches/monero-use-system-miniupnpc.patch \
|
||||
|
|
|
@ -32,6 +32,7 @@
|
|||
;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
|
||||
;;; Copyright © 2019 Nicolas Goaziou <mail@nicolasgoaziou.fr>
|
||||
;;; Copyright © 2019 Steve Sprang <scs@stevesprang.com>
|
||||
;;; Copyright © 2019 Robert Smith <robertsmith@posteo.net>
|
||||
;;;
|
||||
;;; This file is part of GNU Guix.
|
||||
;;;
|
||||
|
@ -5242,3 +5243,42 @@ (define-public speedcrunch
|
|||
(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")
|
||||
(description
|
||||
"MiniSat is a minimalistic, open-source SAT solver, developed to help
|
||||
researchers and developers alike to get started on SAT.")
|
||||
(home-page
|
||||
"http://minisat.se/MiniSat.html")
|
||||
(license license:expat))))
|
||||
|
|
25
gnu/packages/patches/minisat-friend-declaration.patch
Normal file
25
gnu/packages/patches/minisat-friend-declaration.patch
Normal file
|
@ -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; }
|
19
gnu/packages/patches/minisat-install.patch
Normal file
19
gnu/packages/patches/minisat-install.patch
Normal file
|
@ -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)) \
|
Loading…
Reference in a new issue