New port: math/glucose: Parallel SAT solver based on Minisat, with glue clauses

See the full description here:
http://www.labri.fr/perso/lsimon/glucose/

Patches and build warnings were reported to the authors.

Submitted by:	myself
Approved by:	adamw (mentor)
Differential Revision:	https://reviews.freebsd.org/D14156

6 files changed, 67 insertions, 0 deletions

diff --git a/math/Makefile b/math/Makefile
index 409c832f0e0c..e3849753af1e 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -204,6 +204,7 @@
     SUBDIR += glgraph
     SUBDIR += glm
     SUBDIR += glpk
+    SUBDIR += glucose
     SUBDIR += gmm++
     SUBDIR += gmp
     SUBDIR += gmp-ecm
diff --git a/math/glucose/Makefile b/math/glucose/Makefile
new file mode 100644
index 000000000000..eedde938b1f2
--- /dev/null
+++ b/math/glucose/Makefile
@@ -0,0 +1,27 @@
+# $FreeBSD$
+
+PORTNAME=	glucose
+DISTVERSION=	4.1
+CATEGORIES=	math
+MASTER_SITES=	http://www.labri.fr/perso/lsimon/downloads/softwares/
+DISTNAME=	glucose-syrup-${DISTVERSION}
+
+MAINTAINER=	yuri@FreeBSD.org
+COMMENT=	Parallel SAT solver based on Minisat, with glue clauses
+
+LICENSE=	MIT
+LICENSE_FILE=	${WRKSRC}/LICENCE
+
+USES=		gmake tar:tgz
+
+PLIST_FILES=	bin/glucose bin/glucose-syrup
+
+do-build:
+	@cd ${WRKSRC}/simp && ${SETENV} ${MAKE_ENV} ${MAKE_CMD} ${MAKE_ARGS}
+	@cd ${WRKSRC}/parallel && ${SETENV} ${MAKE_ENV} ${MAKE_CMD} ${MAKE_ARGS}
+
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/simp/glucose ${STAGEDIR}${PREFIX}/bin/
+	${INSTALL_PROGRAM} ${WRKSRC}/parallel/glucose-syrup ${STAGEDIR}${PREFIX}/bin/
+
+.include <bsd.port.mk>
diff --git a/math/glucose/distinfo b/math/glucose/distinfo
new file mode 100644
index 000000000000..aacf46fb8a3d
--- /dev/null
+++ b/math/glucose/distinfo
@@ -0,0 +1,3 @@
+TIMESTAMP = 1517475160
+SHA256 (glucose-syrup-4.1.tgz) = 51aa1cf1bed2b14f1543b099e85a56dd1a92be37e6e3eb0c4a1fd883d5cc5029
+SIZE (glucose-syrup-4.1.tgz) = 82779
diff --git a/math/glucose/files/patch-mtl_template.mk b/math/glucose/files/patch-mtl_template.mk
new file mode 100644
index 000000000000..dea1a4e1981d
--- /dev/null
+++ b/math/glucose/files/patch-mtl_template.mk
@@ -0,0 +1,13 @@
+--- mtl/template.mk.orig	2018-02-03 20:34:58 UTC
++++ mtl/template.mk
+@@ -18,8 +18,8 @@ DCOBJS     = $(addsuffix d,  $(COBJS))
+ RCOBJS     = $(addsuffix r,  $(COBJS))
+ 
+ CXX       ?= g++
+-CFLAGS    ?= -Wall -Wno-parentheses -std=c++11
+-LFLAGS    ?= -Wall -lpthread 
++CFLAGS    += -Wall -Wno-parentheses -std=c++11
++LFLAGS    += -Wall -lpthread 
+ 
+ COPTIMIZE ?= -O3
+ 
diff --git a/math/glucose/files/patch-utils_System.cc b/math/glucose/files/patch-utils_System.cc
new file mode 100644
index 000000000000..3a4d189a61f7
--- /dev/null
+++ b/math/glucose/files/patch-utils_System.cc
@@ -0,0 +1,11 @@
+--- utils/System.cc.orig	2018-02-01 09:11:32 UTC
++++ utils/System.cc
+@@ -78,7 +78,7 @@ double Glucose::memUsed(void) {
+     struct rusage ru;
+     getrusage(RUSAGE_SELF, &ru);
+     return (double)ru.ru_maxrss / 1024; }
+-double MiniSat::memUsedPeak(void) { return memUsed(); }
++//double MiniSat::memUsedPeak(void) { return memUsed(); }
+ 
+ 
+ #elif defined(__APPLE__)
diff --git a/math/glucose/pkg-descr b/math/glucose/pkg-descr
new file mode 100644
index 000000000000..1435ff342bfe
--- /dev/null
+++ b/math/glucose/pkg-descr
@@ -0,0 +1,12 @@
+Glucose is based on the MiniSat solver, and extends it by preserving
+the so-called "glue clauses" and using new scoring scheme.
+
+Glucose is a SAT solver based on a particular scoring scheme for the clause
+learning mechanism, based on the paper Laurent Simon and Gilles Audemard
+presented at IJCAI'09. Solver's name is a contraction of the concept of
+"glue clauses", a particular kind of clauses that glucose detects and preserves
+during search.
+
+Glucose accepts SAT problems in the DIMACS format.
+
+WWW: http://www.labri.fr/perso/lsimon/glucose/