From owner-svn-ports-all@freebsd.org Sat Feb 3 20:59:16 2018 Return-Path: Delivered-To: svn-ports-all@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id D98E2EEC25B; Sat, 3 Feb 2018 20:59:15 +0000 (UTC) (envelope-from yuri@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client CN "mxrelay.nyi.freebsd.org", Issuer "Let's Encrypt Authority X3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 8367F7AC51; Sat, 3 Feb 2018 20:59:15 +0000 (UTC) (envelope-from yuri@FreeBSD.org) Received: from repo.freebsd.org (repo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:0]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mxrelay.nyi.freebsd.org (Postfix) with ESMTPS id 75DE310349; Sat, 3 Feb 2018 20:59:15 +0000 (UTC) (envelope-from yuri@FreeBSD.org) Received: from repo.freebsd.org ([127.0.1.37]) by repo.freebsd.org (8.15.2/8.15.2) with ESMTP id w13KxFP3023585; Sat, 3 Feb 2018 20:59:15 GMT (envelope-from yuri@FreeBSD.org) Received: (from yuri@localhost) by repo.freebsd.org (8.15.2/8.15.2/Submit) id w13KxECj023578; Sat, 3 Feb 2018 20:59:14 GMT (envelope-from yuri@FreeBSD.org) Message-Id: <201802032059.w13KxECj023578@repo.freebsd.org> X-Authentication-Warning: repo.freebsd.org: yuri set sender to yuri@FreeBSD.org using -f From: Yuri Victorovich Date: Sat, 3 Feb 2018 20:59:14 +0000 (UTC) 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 X-SVN-Group: ports-head X-SVN-Commit-Author: yuri X-SVN-Commit-Paths: in head/math: . glucose glucose/files X-SVN-Commit-Revision: 460848 X-SVN-Commit-Repository: ports MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-BeenThere: svn-ports-all@freebsd.org X-Mailman-Version: 2.1.25 Precedence: list List-Id: SVN commit messages for the ports tree List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sat, 03 Feb 2018 20:59:16 -0000 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 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/