svn commit: r460848 - in head/math: . glucose glucose/files

[Yuri Victorovich]

Author: yuri
Date: Sat Feb  3 20:59:14 2018
New Revision: 460848
URL: https://svnweb.freebsd.org/changeset/ports/460848

Log:
  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

Added:
  head/math/glucose/
  head/math/glucose/Makefile   (contents, props changed)
  head/math/glucose/distinfo   (contents, props changed)
  head/math/glucose/files/
  head/math/glucose/files/patch-mtl_template.mk   (contents, props changed)
  head/math/glucose/files/patch-utils_System.cc   (contents, props changed)
  head/math/glucose/pkg-descr   (contents, props changed)
Modified:
  head/math/Makefile

Modified: head/math/Makefile
==============================================================================
--- head/math/Makefile	Sat Feb  3 20:55:08 2018	(r460847)
+++ head/math/Makefile	Sat Feb  3 20:59:14 2018	(r460848)
@@ -204,6 +204,7 @@
     SUBDIR += glgraph
     SUBDIR += glm
     SUBDIR += glpk
+    SUBDIR += glucose
     SUBDIR += gmm++
     SUBDIR += gmp
     SUBDIR += gmp-ecm

Added: head/math/glucose/Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/glucose/Makefile	Sat Feb  3 20:59:14 2018	(r460848)
@@ -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 at 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>

Added: head/math/glucose/distinfo
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/glucose/distinfo	Sat Feb  3 20:59:14 2018	(r460848)
@@ -0,0 +1,3 @@
+TIMESTAMP = 1517475160
+SHA256 (glucose-syrup-4.1.tgz) = 51aa1cf1bed2b14f1543b099e85a56dd1a92be37e6e3eb0c4a1fd883d5cc5029
+SIZE (glucose-syrup-4.1.tgz) = 82779

Added: head/math/glucose/files/patch-mtl_template.mk
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/glucose/files/patch-mtl_template.mk	Sat Feb  3 20:59:14 2018	(r460848)
@@ -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
+ 

Added: head/math/glucose/files/patch-utils_System.cc
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/glucose/files/patch-utils_System.cc	Sat Feb  3 20:59:14 2018	(r460848)
@@ -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__)

Added: head/math/glucose/pkg-descr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/glucose/pkg-descr	Sat Feb  3 20:59:14 2018	(r460848)
@@ -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/