Date: Sat, 3 Feb 2018 20:59:14 +0000 (UTC) From: Yuri Victorovich <yuri@FreeBSD.org> To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r460848 - in head/math: . glucose glucose/files Message-ID: <201802032059.w13KxECj023578@repo.freebsd.org>
next in thread | raw e-mail | index | archive | help
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@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/
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201802032059.w13KxECj023578>