From 05dd33cd01f6c56227c87c2202b3a382ef81953e Mon Sep 17 00:00:00 2001
From: edd <edd@openbsd.org>
Date: Thu, 19 Aug 2010 14:19:22 +0000
Subject: [PATCH] update to minisat 2.2.0 OK jasper@

---
 math/minisat/Makefile                      | 21 ++++-----
 math/minisat/distinfo                      | 10 ++--
 math/minisat/patches/patch-Makefile        | 26 ----------
 math/minisat/patches/patch-core_Main_cc    | 19 ++++++++
 math/minisat/patches/patch-mtl_template_mk | 55 ++++++++++++++++++++++
 math/minisat/patches/patch-simp_Main_cc    | 19 ++++++++
 math/minisat/patches/patch-utils_System_cc | 23 +++++++++
 math/minisat/pkg/DESCR                     |  4 ++
 math/minisat/pkg/PLIST                     |  3 +-
 9 files changed, 137 insertions(+), 43 deletions(-)
 delete mode 100644 math/minisat/patches/patch-Makefile
 create mode 100644 math/minisat/patches/patch-core_Main_cc
 create mode 100644 math/minisat/patches/patch-mtl_template_mk
 create mode 100644 math/minisat/patches/patch-simp_Main_cc
 create mode 100644 math/minisat/patches/patch-utils_System_cc

diff --git a/math/minisat/Makefile b/math/minisat/Makefile
index cacb78419c0..931599cd1ec 100644
--- a/math/minisat/Makefile
+++ b/math/minisat/Makefile
@@ -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
 
diff --git a/math/minisat/distinfo b/math/minisat/distinfo
index e00640f0212..3da87ecdf62 100644
--- a/math/minisat/distinfo
+++ b/math/minisat/distinfo
@@ -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
diff --git a/math/minisat/patches/patch-Makefile b/math/minisat/patches/patch-Makefile
deleted file mode 100644
index fa051fd61e5..00000000000
--- a/math/minisat/patches/patch-Makefile
+++ /dev/null
@@ -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)
diff --git a/math/minisat/patches/patch-core_Main_cc b/math/minisat/patches/patch-core_Main_cc
new file mode 100644
index 00000000000..1b21a02be1b
--- /dev/null
+++ b/math/minisat/patches/patch-core_Main_cc
@@ -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");
+             } }
+         
diff --git a/math/minisat/patches/patch-mtl_template_mk b/math/minisat/patches/patch-mtl_template_mk
new file mode 100644
index 00000000000..dd597e7b777
--- /dev/null
+++ b/math/minisat/patches/patch-mtl_template_mk
@@ -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 \
diff --git a/math/minisat/patches/patch-simp_Main_cc b/math/minisat/patches/patch-simp_Main_cc
new file mode 100644
index 00000000000..7ea0221e4b6
--- /dev/null
+++ b/math/minisat/patches/patch-simp_Main_cc
@@ -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");
+             } }
+         
diff --git a/math/minisat/patches/patch-utils_System_cc b/math/minisat/patches/patch-utils_System_cc
new file mode 100644
index 00000000000..bfd181ea8fd
--- /dev/null
+++ b/math/minisat/patches/patch-utils_System_cc
@@ -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__)
diff --git a/math/minisat/pkg/DESCR b/math/minisat/pkg/DESCR
index 986ca8030c1..b0286a82208 100644
--- a/math/minisat/pkg/DESCR
+++ b/math/minisat/pkg/DESCR
@@ -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.
diff --git a/math/minisat/pkg/PLIST b/math/minisat/pkg/PLIST
index 871276c353a..a2b741b82d6 100644
--- a/math/minisat/pkg/PLIST
+++ b/math/minisat/pkg/PLIST
@@ -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