mirror/freebsd-ports
1
0
Fork 0
mirror of https://git.FreeBSD.org/ports.git synced 2025-01-31 10:46:16 +00:00
Code Issues Releases Activity

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

Browse Source 
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
This commit is contained in:
Yuri Victorovich 2018-02-03 20:59:14 +00:00
parent 8cb52b6b33
commit eb924c41bc
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=460848
6 changed files with 67 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
math/Makefile
View File

@ -204,6 +204,7 @@
SUBDIR += glgraph
SUBDIR += glm
SUBDIR += glpk
SUBDIR += glucose
SUBDIR += gmm++
SUBDIR += gmp
SUBDIR += gmp-ecm

27
math/glucose/Makefile Normal file
View File

@ -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>

3
math/glucose/distinfo Normal file
View File

@ -0,0 +1,3 @@
TIMESTAMP = 1517475160
SHA256 (glucose-syrup-4.1.tgz) = 51aa1cf1bed2b14f1543b099e85a56dd1a92be37e6e3eb0c4a1fd883d5cc5029
SIZE (glucose-syrup-4.1.tgz) = 82779

13
math/glucose/files/patch-mtl_template.mk Normal file
View File

@ -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

11
math/glucose/files/patch-utils_System.cc Normal file
View File

@ -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__)

12
math/glucose/pkg-descr Normal file
View File

@ -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/