summaryrefslogtreecommitdiff
path: root/gnu/packages/patches
diff options
context:
space:
mode:
authorRobert Smith <robertsmith@posteo.net>2019-11-16 16:18:43 +0100
committerMathieu Othacehe <m.othacehe@gmail.com>2019-11-19 17:27:58 +0100
commit3b7828cc7f938fcb369976cbe75d9c85f22583a1 (patch)
tree4814e0497cec93b82f6fa2c23d2d87cd20a63733 /gnu/packages/patches
parent5dea5cbc62547f50a793ce905cdd4d1a62be60e1 (diff)
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>
Diffstat (limited to 'gnu/packages/patches')
-rw-r--r--gnu/packages/patches/minisat-friend-declaration.patch25
-rw-r--r--gnu/packages/patches/minisat-install.patch19
2 files changed, 44 insertions, 0 deletions
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)) \