cpet/openbsd-ports
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

update to minisat 2.2.0

Browse Source 
OK jasper@
This commit is contained in:
edd 2010-08-19 14:19:22 +00:00
parent 8057b45281
commit 05dd33cd01
9 changed files with 137 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
math/minisat/Makefile
View File

@ -1,11 +1,8 @@
# $OpenBSD: Makefile,v 1.4 2010/07/18 10:50:12 steven Exp $
# $OpenBSD: Makefile,v 1.5 2010/08/19 14:19:22 edd Exp $
COMMENT= minimalistic Boolean satisfiability solver
V= 1.14
DISTNAME= MiniSat-p_v$V.2006-Sep-07.src
PKGNAME= minisat-$V
REVISION= 1
DISTNAME= minisat-2.2.0
CATEGORIES= math
HOMEPAGE= http://minisat.se/
@ -19,21 +16,23 @@ PERMIT_DISTFILES_CDROM= Yes
PERMIT_DISTFILES_FTP= Yes
MASTER_SITES= ${HOMEPAGE}/downloads/
EXTRACT_SUFX= .zip
DISTFILES= ${DISTNAME}${EXTRACT_SUFX} \
MiniSat.ps.gz
WRKDIST= ${WRKDIR}/MiniSat-p_v$V/
WANTLIB += c m stdc++ z
WANTLIB += c m stdc++ z
USE_GMAKE= Yes
ALL_TARGET= minisat
NO_REGRESS= Yes
MAKE_ENV+= MROOT=${WRKBUILD}
do-build:
cd ${WRKBUILD}/core && ${MAKE_ENV} ${MAKE_PROGRAM} ${MAKE_FLAGS}
cd ${WRKBUILD}/simp && ${MAKE_ENV} ${MAKE_PROGRAM} ${MAKE_FLAGS}
do-install:
${INSTALL_PROGRAM} ${WRKSRC}/minisat ${PREFIX}/bin
${INSTALL_PROGRAM} ${WRKSRC}/core/minisat ${PREFIX}/bin/minisat
${INSTALL_PROGRAM} ${WRKSRC}/simp/minisat ${PREFIX}/bin/minisats
${INSTALL_DATA_DIR} ${PREFIX}/share/doc/minisat
${INSTALL_DATA} ${WRKDIR}/MiniSat.ps ${PREFIX}/share/doc/minisat

10
math/minisat/distinfo
View File

@ -1,10 +1,10 @@
MD5 (MiniSat-p_v1.14.2006-Sep-07.src.zip) = ii82gY3BqA7nOhYt1PfaOA==
MD5 (MiniSat.ps.gz) = h8h2aKzzvzU4Vrzw792zIA==
RMD160 (MiniSat-p_v1.14.2006-Sep-07.src.zip) = cR0jHlbsRyXMOBEPADz79xXw0Rs=
MD5 (minisat-2.2.0.tar.gz) = onsAGvmcBzCP4bGtlOQC2A==
RMD160 (MiniSat.ps.gz) = DvBrRGvaFtTTRBTKdZFfYj4jqbM=
SHA1 (MiniSat-p_v1.14.2006-Sep-07.src.zip) = CSa1GM4cVW2O/2SoTbvKjIB1+0A=
RMD160 (minisat-2.2.0.tar.gz) = L9KpcGUq/DInppnyB5I21Y/DlwY=
SHA1 (MiniSat.ps.gz) = xNWe75xaOpO9nePnHumSdipjdhc=
SHA256 (MiniSat-p_v1.14.2006-Sep-07.src.zip) = j2TOBtKueKZsn/ZAacn0u1obtGu15ulUptMLDZIF36g=
SHA1 (minisat-2.2.0.tar.gz) = HfcyXvII85tEuo8p3xwNrUpATno=
SHA256 (MiniSat.ps.gz) = FVUdwKddyJRGpQCF7yjfK2VJ/bs+SMHvUzFqu6ZTUPI=
SIZE (MiniSat-p_v1.14.2006-Sep-07.src.zip) = 37888
SHA256 (minisat-2.2.0.tar.gz) = JpV/SZ9eVXy0XNuzDoQCt+AzyiCAqYvLFMdpAoKE+wY=
SIZE (MiniSat.ps.gz) = 112951
SIZE (minisat-2.2.0.tar.gz) = 43876

26
math/minisat/patches/patch-Makefile
View File

@ -1,26 +0,0 @@
$OpenBSD: patch-Makefile,v 1.2 2010/05/13 18:29:47 jasper Exp $
--- Makefile.orig Tue Jul 5 09:31:00 2005
+++ Makefile Thu May 13 20:27:45 2010
@@ -15,11 +15,9 @@ RCOBJS = $(addsuffix r, $(COBJS))
EXEC = minisat
-CXX = g++
-CFLAGS = -Wall -ffloat-store
-COPTIMIZE = -O3
+CXX ?= g++
+CFLAGS += -Wall -ffloat-store
-
.PHONY : s p d r build clean depend
s: WAY=standard
@@ -50,7 +48,7 @@ clean:
## Build rule
%.o %.op %.od %.or: %.C
@echo Compiling: $<
- @$(CXX) $(CFLAGS) -c -o $@ $<
+ $(CXX) $(CFLAGS) -c -o $@ $<
## Linking rules (standard/profile/debug/release)
$(EXEC): $(COBJS)

19
math/minisat/patches/patch-core_Main_cc Normal file
View File

@ -0,0 +1,19 @@
$OpenBSD: patch-core_Main_cc,v 1.1 2010/08/19 14:19:22 edd Exp $
OpenBSD has no RLIMIT_AS
--- core/Main.cc.orig Thu Aug 19 14:33:12 2010
+++ core/Main.cc Thu Aug 19 14:34:39 2010
@@ -112,10 +112,10 @@ int main(int argc, char** argv)
if (mem_lim != INT32_MAX){
rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
rlimit rl;
- getrlimit(RLIMIT_AS, &rl);
+ getrlimit(RLIMIT_DATA, &rl);
if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
rl.rlim_cur = new_mem_lim;
- if (setrlimit(RLIMIT_AS, &rl) == -1)
+ if (setrlimit(RLIMIT_DATA, &rl) == -1)
printf("WARNING! Could not set resource limit: Virtual memory.\n");
} }

55
math/minisat/patches/patch-mtl_template_mk Normal file
View File

@ -0,0 +1,55 @@
$OpenBSD: patch-mtl_template_mk,v 1.1 2010/08/19 14:19:22 edd Exp $
Print compiler options and remove OTT optimisation
--- mtl/template.mk.orig Sat Jul 10 17:07:36 2010
+++ mtl/template.mk Tue Jul 13 14:14:42 2010
@@ -22,7 +22,7 @@ CXX ?= g++
CFLAGS ?= -Wall -Wno-parentheses
LFLAGS ?= -Wall
-COPTIMIZE ?= -O3
+#COPTIMIZE ?= -O3
CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
LFLAGS += -lz
@@ -41,13 +41,13 @@ libd: lib$(LIB)_debug.a
libr: lib$(LIB)_release.a
## Compile options
-%.o: CFLAGS +=$(COPTIMIZE) -g -D DEBUG
+%.o: CFLAGS +=$(COPTIMIZE)
%.op: CFLAGS +=$(COPTIMIZE) -pg -g -D NDEBUG
%.od: CFLAGS +=-O0 -g -D DEBUG
%.or: CFLAGS +=$(COPTIMIZE) -g -D NDEBUG
## Link options
-$(EXEC): LFLAGS += -g
+$(EXEC): LFLAGS +=
$(EXEC)_profile: LFLAGS += -g -pg
$(EXEC)_debug: LFLAGS += -g
#$(EXEC)_release: LFLAGS += ...
@@ -69,12 +69,12 @@ lib$(LIB)_release.a: $(filter-out */Main.or, $(RCOBJS)
## Build rule
%.o %.op %.od %.or: %.cc
@echo Compiling: $(subst $(MROOT)/,,$@)
- @$(CXX) $(CFLAGS) -c -o $@ $<
+ $(CXX) $(CFLAGS) -c -o $@ $<
## Linking rules (standard/profile/debug/release)
$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
@echo Linking: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
- @$(CXX) $^ $(LFLAGS) -o $@
+ $(CXX) $^ $(LFLAGS) -o $@
## Library rules (standard/profile/debug/release)
lib$(LIB)_standard.a lib$(LIB)_profile.a lib$(LIB)_release.a lib$(LIB)_debug.a:
@@ -94,7 +94,7 @@ clean:
## Make dependencies
depend.mk: $(CSRCS) $(CHDRS)
@echo Making dependencies
- @$(CXX) $(CFLAGS) -I$(MROOT) \
+ $(CXX) $(CFLAGS) -I$(MROOT) \
$(CSRCS) -MM | sed 's|\(.*\):|$(PWD)/\1 $(PWD)/\1r $(PWD)/\1d $(PWD)/\1p:|' > depend.mk
@for dir in $(DEPDIR); do \
if [ -r $(MROOT)/$${dir}/depend.mk ]; then \

19
math/minisat/patches/patch-simp_Main_cc Normal file
View File

@ -0,0 +1,19 @@
$OpenBSD: patch-simp_Main_cc,v 1.1 2010/08/19 14:19:22 edd Exp $
OpenBSD has no RLIMIT_AS
--- simp/Main.cc.orig Thu Aug 19 14:34:45 2010
+++ simp/Main.cc Thu Aug 19 14:35:07 2010
@@ -116,10 +116,10 @@ int main(int argc, char** argv)
if (mem_lim != INT32_MAX){
rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
rlimit rl;
- getrlimit(RLIMIT_AS, &rl);
+ getrlimit(RLIMIT_DATA, &rl);
if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
rl.rlim_cur = new_mem_lim;
- if (setrlimit(RLIMIT_AS, &rl) == -1)
+ if (setrlimit(RLIMIT_DATA, &rl) == -1)
printf("WARNING! Could not set resource limit: Virtual memory.\n");
} }

23
math/minisat/patches/patch-utils_System_cc Normal file
View File

@ -0,0 +1,23 @@
$OpenBSD: patch-utils_System_cc,v 1.1 2010/08/19 14:19:22 edd Exp $
* memUsed is the same as FreeBSD
* namespace typo
--- utils/System.cc.orig Sat Jul 10 17:07:36 2010
+++ utils/System.cc Tue Jul 13 10:26:09 2010
@@ -72,13 +72,13 @@ double Minisat::memUsedPeak() {
double peak = memReadPeak() / 1024;
return peak == 0 ? memUsed() : peak; }
-#elif defined(__FreeBSD__)
+#elif defined(__FreeBSD__) || defined(__OpenBSD__)
double Minisat::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__)

4
math/minisat/pkg/DESCR
View File

@ -13,3 +13,7 @@ Some key features of MiniSat:
mechanisms for adding non-clausal constraints. By virtue of being easy
to modify, it is a good choice for integrating as a backend to another
tool, such as a model checker or a more generic constraint solver.
The OpenBSD package of MiniSAT installs two binaries:
minisat = A core version of the solver.
minisats = An extended solver with simplification capabilities.

3
math/minisat/pkg/PLIST
View File

@ -1,4 +1,5 @@
@comment $OpenBSD: PLIST,v 1.1.1.1 2009/09/17 21:12:04 jasper Exp $
@comment $OpenBSD: PLIST,v 1.2 2010/08/19 14:19:22 edd Exp $
@bin bin/minisat
@bin bin/minisats
share/doc/minisat/
share/doc/minisat/MiniSat.ps