Page MenuHomeFreeBSD
Files F152008618

D14156.id38830.diff
No OneTemporary
Actions

D14156.id38830.diff
View Options

Index: math/Makefile
===================================================================
--- math/Makefile
+++ math/Makefile
@@ -204,6 +204,7 @@
SUBDIR += glgraph
SUBDIR += glm
SUBDIR += glpk
+ SUBDIR += glucose
SUBDIR += gmm++
SUBDIR += gmp
SUBDIR += gmp-ecm
Index: math/glucose/Makefile
===================================================================
--- /dev/null
+++ 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>
Index: math/glucose/distinfo
===================================================================
--- /dev/null
+++ math/glucose/distinfo
@@ -0,0 +1,3 @@
+TIMESTAMP = 1517475160
+SHA256 (glucose-syrup-4.1.tgz) = 51aa1cf1bed2b14f1543b099e85a56dd1a92be37e6e3eb0c4a1fd883d5cc5029
+SIZE (glucose-syrup-4.1.tgz) = 82779
Index: math/glucose/files/patch-mtl_template.mk
===================================================================
--- /dev/null
+++ 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
+
Index: math/glucose/files/patch-utils_System.cc
===================================================================
--- /dev/null
+++ 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__)
Index: math/glucose/pkg-descr
===================================================================
--- /dev/null
+++ 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/

File Metadata

Mime Type
text/plain
Expires
Mon, Apr 13, 1:59 AM (4 h, 18 m)
Storage Engine
blob
Storage Format
Raw Data
Storage Handle
31387692
Default Alt Text
D14156.id38830.diff (3 KB)

Event Timeline