[gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/minisat+/, sci-mathematics/minisat+/files/

[Alessandro Barbieri]

commit:     1d6017d59522445fb112b9fc0d8bd8e379e81211
Author:     Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
AuthorDate: Thu Apr 28 14:39:38 2022 +0000
Commit:     Alessandro Barbieri <lssndrbarbieri <AT> gmail <DOT> com>
CommitDate: Fri Apr 29 01:47:58 2022 +0000
URL:        https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=1d6017d5

sci-mathematics/minisat+: new package, add 2007.01.05

Signed-off-by: Alessandro Barbieri <lssndrbarbieri <AT> gmail.com>

 sci-mathematics/minisat+/Manifest                  |  1 +
 .../files/minisat+-2007.01.05-exitcode.patch       | 39 +++++++++
 .../files/minisat+-2007.01.05-makefile.patch       | 98 ++++++++++++++++++++++
 .../files/minisat+-2007.01.05-script.patch         | 17 ++++
 .../files/minisat+-2007.01.05-spelling.patch       | 16 ++++
 sci-mathematics/minisat+/metadata.xml              | 16 ++++
 .../minisat+/minisat+-2007.01.05.ebuild            | 50 +++++++++++
 7 files changed, 237 insertions(+)

diff --git a/sci-mathematics/minisat+/Manifest b/sci-mathematics/minisat+/Manifest
new file mode 100644
index 000000000..bd6a3947f
--- /dev/null
+++ b/sci-mathematics/minisat+/Manifest
@@ -0,0 +1 @@
+DIST minisat+_2007-Jan-05.zip 920081 BLAKE2B 4b133a3c06ffe8539a26c7f39f4734d8115053df299bfcd002e97ea00a104abf326633120371560d71cf2700ed02be8891ef78c185f16b516da818269b1101c9 SHA512 deee0cce2882fad8c175c7ca061d7952a243d00119e8d7fcf9ed0260db874a2e5bb846cb9513aa43163735406aebf5cd8ac01000621e2db37da0dc5d5de3854d

diff --git a/sci-mathematics/minisat+/files/minisat+-2007.01.05-exitcode.patch b/sci-mathematics/minisat+/files/minisat+-2007.01.05-exitcode.patch
new file mode 100644
index 000000000..6321a1969
--- /dev/null
+++ b/sci-mathematics/minisat+/files/minisat+-2007.01.05-exitcode.patch
@@ -0,0 +1,39 @@
+Author: Niklas Sorensson <nik@××××××××.se> (extracted from upstream git)
+Approved: Ralf Treinen <treinen@××××××.org>
+Description: use exitcode to indicate error
+
+Index: minisat+/Main.C
+===================================================================
+--- minisat+.orig/Main.C	2011-05-24 20:48:23.000000000 +0200
++++ minisat+/Main.C	2011-05-24 20:50:13.000000000 +0200
+@@ -261,7 +261,7 @@
+     reportf("*** TERMINATED ***\n");
+     outputResult(*pb_solver, false);
+     SatELite::deleteTmpFiles();
+-    _exit(pb_solver->best_goalvalue == Int_MAX ? 0 : 10); }
++    _exit(0); }
+ 
+ 
+ void printStats(BasicSolverStats& stats, double cpu_time)
+@@ -324,7 +324,7 @@
+         reportf("_______________________________________________________________________________\n");
+     }
+ 
+-    exit(pb_solver->best_goalvalue == Int_MAX ? 20 : (pb_solver->goal == NULL || opt_command == cmd_FirstSolution) ? 10 : 30);    // (faster than "return", which will invoke the destructor for 'PbSolver')
++    exit(0);    // (faster than "return", which will invoke the destructor for 'PbSolver')
+ }
+ 
+ 
+Index: minisat+/PbParser.C
+===================================================================
+--- minisat+.orig/PbParser.C	2011-05-24 20:48:23.000000000 +0200
++++ minisat+/PbParser.C	2011-05-24 20:50:13.000000000 +0200
+@@ -282,7 +282,7 @@
+             xfree(msg);
+             if (opt_satlive && !opt_try)
+                 printf("s UNKNOWN\n");
+-            exit(opt_try ? 5 : 0);
++            exit(5);
+         }else
+             throw msg;
+     }

diff --git a/sci-mathematics/minisat+/files/minisat+-2007.01.05-makefile.patch b/sci-mathematics/minisat+/files/minisat+-2007.01.05-makefile.patch
new file mode 100644
index 000000000..ca3f43f93
--- /dev/null
+++ b/sci-mathematics/minisat+/files/minisat+-2007.01.05-makefile.patch
@@ -0,0 +1,98 @@
+--- a/Makefile
++++ b/Makefile
+@@ -13,11 +13,8 @@
+ 
+ EXEC      = minisat+
+ 
+-CXX       = g++
+ #CXX      = icpc
+-CFLAGS    = -Wall -ffloat-store 
+-CFLAGS   += -IADTs -include Global.h -include Main.h -D_FILE_OFFSET_BITS=64 
+-COPTIMIZE = -O3 #-fomit-frame-pointer # -falign-loops=4 -falign-functions=16 -foptimize-sibling-calls -finline-functions -fcse-follow-jumps -fcse-skip-blocks -frerun-cse-after-loop -frerun-loop-opt -fgcse
++CXXFLAGS   += -IADTs -include Global.h -include Main.h -D_FILE_OFFSET_BITS=64 
+ 
+ 
+ .PHONY : s p d r build clean depend
+@@ -26,22 +23,22 @@
+ p:	WAY=profile
+ d:	WAY=debug
+ r:	WAY=release
+-rs:	WAY="release static / bignums"
+-rx:	WAY="release static / 64-bit integers"
++rs:	WAY="release / bignums"
++rx:	WAY="release / 64-bit integers"
+ 
+-s:	CFLAGS+=$(COPTIMIZE) -ggdb -D DEBUG
+-p:	CFLAGS+=$(COPTIMIZE) -pg -ggdb -D DEBUG
+-d:	CFLAGS+=-O0 -ggdb -D DEBUG
+-r:	CFLAGS+=$(COPTIMIZE) -D NDEBUG
+-rs:	CFLAGS+=$(COPTIMIZE) -D NDEBUG
+-rx:	CFLAGS+=$(COPTIMIZE) -D NDEBUG -D NO_GMP
++s:	CXXFLAGS+=-ggdb -D DEBUG
++p:	CXXFLAGS+=-pg -ggdb -D DEBUG
++d:	CXXFLAGS+=-O0 -ggdb -D DEBUG
++r:	CXXFLAGS+=-D NDEBUG
++rs:	CXXFLAGS+=-D NDEBUG
++rx:	CXXFLAGS+=-D NDEBUG -D NO_GMP
+ 
+ s:	build $(EXEC)
+ p:	build $(EXEC)_profile
+ d:	build $(EXEC)_debug
+ r:	build $(EXEC)_release
+-rs:	build $(EXEC)_bignum_static
+-rx:	build $(EXEC)_64-bit_static
++rs:	build $(EXEC)_bignum
++rx:	build $(EXEC)_64-bit
+ 
+ build:
+ 	@echo Building $(EXEC) "("$(WAY)")"
+@@ -53,39 +50,39 @@
+ ## Build rule
+ %.o %.op %.od %.or %.ox: %.C
+ 	@echo Compiling: $<
+-	@$(CXX) $(CFLAGS) -c -o $@ $<
++	@$(CXX) $(CXXFLAGS) -fPIC -c -o $@ $<
+ 
+ ## Linking rules (standard/profile/debug/release)
+ $(EXEC): $(COBJS)
+ 	@echo Linking $(EXEC)
+-	@$(CXX) $(COBJS) -lz -lgmp -ggdb -Wall -o $@ 
++	@$(CXX) $(CXXFLAGS) $(LDFLAGS) -fPIE $(COBJS) -lz -lgmp -ggdb -Wall -o $@ 
+ 
+ $(EXEC)_profile: $(PCOBJS)
+ 	@echo Linking $@
+-	@$(CXX) $(PCOBJS) -lz -lgmp -ggdb -Wall -pg -o $@
++	@$(CXX) $(CXXFLAGS) $(LDFLAGS) -fPIE $(PCOBJS) -lz -lgmp -ggdb -Wall -pg -o $@
+ 
+ $(EXEC)_debug:	$(DCOBJS)
+ 	@echo Linking $@
+-	@$(CXX) $(DCOBJS) -lz -lgmp -ggdb -Wall -o $@
++	@$(CXX) $(CXXFLAGS) $(LDFLAGS) -fPIE $(DCOBJS) -lz -lgmp -ggdb -Wall -o $@
+ 
+ $(EXEC)_release: $(RCOBJS)
+ 	@echo Linking $@
+-	@$(CXX) $(RCOBJS) -lz -lgmp -Wall -o $@
++	@$(CXX) $(CXXFLAGS) $(LDFLAGS) -fPIE $(RCOBJS) -lz -lgmp -Wall -o $@
+ 
+-$(EXEC)_bignum_static: $(RCOBJS)
++$(EXEC)_bignum: $(RCOBJS)
+ 	@echo Linking $@
+-	@$(CXX) --static $(RCOBJS) -lz -lgmp -Wall -o $@
++	@$(CXX) $(CXXFLAGS) $(LDFLAGS) -fPIE $(RCOBJS) -lz -lgmp -Wall -o $@
+ 
+-$(EXEC)_64-bit_static: $(R64COBJS)
++$(EXEC)_64-bit: $(R64COBJS)
+ 	@echo Linking $@
+-	@$(CXX) --static $(R64COBJS) -lz -Wall -o $@
++	@$(CXX) $(CXXFLAGS) $(LDFLAGS) -fPIE $(R64COBJS) -lz -Wall -o $@
+ 
+ 
+ ## Make dependencies
+ depend:	depend.mak
+ depend.mak:	$(CSRCS) $(CHDRS)
+ 	@echo Making dependencies...
+-	@$(CXX) -MM $(CSRCS) $(CFLAGS) > depend.mak
++	@$(CXX) -MM $(CSRCS) $(CXXFLAGS) > depend.mak
+ 	@cp depend.mak /tmp/depend.mak.tmp
+ 	@sed "s/o:/op:/" /tmp/depend.mak.tmp >> depend.mak
+ 	@sed "s/o:/od:/" /tmp/depend.mak.tmp >> depend.mak

diff --git a/sci-mathematics/minisat+/files/minisat+-2007.01.05-script.patch b/sci-mathematics/minisat+/files/minisat+-2007.01.05-script.patch
new file mode 100644
index 000000000..38af57bc7
--- /dev/null
+++ b/sci-mathematics/minisat+/files/minisat+-2007.01.05-script.patch
@@ -0,0 +1,17 @@
+--- a/minisat+_script
++++ b/minisat+_script
+@@ -6,12 +6,12 @@
+   XDIR=`echo $0 | sed "s%\(.*\)/.*$%\1%"`
+ fi
+ 
+-$XDIR/minisat+_64-bit_static -try "$@"
++$XDIR/minisat+_64-bit -try "$@"
+ EXIT=$?
+ 
+ if [ $EXIT = 5 ]; then
+   echo "c OK -- Running BigNum-version instead..."
+-  $XDIR/minisat+_bignum_static* "$@"
++  $XDIR/minisat+_bignum* "$@"
+   EXIT=$?
+ fi
+ exit $EXIT

diff --git a/sci-mathematics/minisat+/files/minisat+-2007.01.05-spelling.patch b/sci-mathematics/minisat+/files/minisat+-2007.01.05-spelling.patch
new file mode 100644
index 000000000..51ebe70ec
--- /dev/null
+++ b/sci-mathematics/minisat+/files/minisat+-2007.01.05-spelling.patch
@@ -0,0 +1,16 @@
+Author: Ralf Treinen <treinen@××××××.org>
+Description: fix a spelling error in help text
+
+Index: minisat+/Main.C
+===================================================================
+--- minisat+.orig/Main.C	2011-05-24 20:59:49.000000000 +0200
++++ minisat+/Main.C	2016-12-19 07:29:13.894553743 +0100
+@@ -79,7 +79,7 @@
+     "\n"
+     "  -bdd-thres=   Threshold for prefering BDDs in mixed mode.        [def: %g]\n"
+     "  -sort-thres=  Threshold for prefering sorters. Tried after BDDs. [def: %g]\n"
+-    "  -goal-bias=   Bias goal function convertion towards sorters.     [def: %g]\n"
++    "  -goal-bias=   Bias goal function conversion towards sorters.     [def: %g]\n"
+     "\n"
+     "  -1 -first     Don\'t minimize, just give first solution found\n"
+     "  -A -all       Don\'t minimize, give all solutions\n"

diff --git a/sci-mathematics/minisat+/metadata.xml b/sci-mathematics/minisat+/metadata.xml
new file mode 100644
index 000000000..a3ac64a0d
--- /dev/null
+++ b/sci-mathematics/minisat+/metadata.xml
@@ -0,0 +1,16 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+  <maintainer type="person">
+    <email>lssndrbarbieri@×××××.com</email>
+    <name>Alessandro Barbieri</name>
+  </maintainer>
+  <use>
+    <flag name="bignum">Build the bignum variant of minisat+</flag>
+  </use>
+  <longdescription lang="en">
+MiniSat+ is a two-week hack done to enable MiniSat to compete in the new categories of the SAT 2005 competition. Initially, we intended to support both Pseudo-Boolean constraints (i.e. linear constraints over boolean variables) and circuit based SAT input (as opposed to CNF). However, after we finished the conversion of PB-constraints to SAT, we ran out of steam and never finished the other part.
+However, the PB part is, arguably, the more interesting one. A number of generalizations of SAT solvers to PB solvers have been proposed (Pueblo, Galena, OPBDP and more), but we felt that the other approach — converting the problem to SAT — had not been invesigated adequately. Our hope was to provide a point of reference for the proper generalizations of SAT to PB, so that the merit of such an approach could be evaluated. Therefore MiniSat+ provides multiple ways of translating PB constraints to clauses.
+For the PB evaluation 2005, we provided a top-level heuristic to choose between the translation methods. To our surprise, MiniSat+ solved more problem than any of the other 6 dedicated PB solvers did, and also seemed to one of the few solvers not being visibly buggy (modulo giving the wrong exitcode for SATISFIABLE instances without an objective function).
+  </longdescription>
+</pkgmetadata>

diff --git a/sci-mathematics/minisat+/minisat+-2007.01.05.ebuild b/sci-mathematics/minisat+/minisat+-2007.01.05.ebuild
new file mode 100644
index 000000000..b97a3b908
--- /dev/null
+++ b/sci-mathematics/minisat+/minisat+-2007.01.05.ebuild
@@ -0,0 +1,50 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+MYPV="${PV/.01./-Jan-}"
+MYP="${PN}_${MYPV}"
+
+inherit toolchain-funcs
+
+DESCRIPTION="solver for pseudo-Boolean constraints"
+HOMEPAGE="https://minisat.se/MiniSat+.html"
+SRC_URI="https://minisat.se/downloads/${MYP}.zip"
+S="${WORKDIR}/${PN}"
+
+LICENSE="MIT"
+SLOT="0"
+KEYWORDS="~amd64"
+IUSE="bignum"
+
+RDEPEND="
+	bignum? ( dev-libs/gmp )
+	sys-libs/zlib
+"
+DEPEND="${RDEPEND}"
+BDEPEND="app-arch/unzip"
+
+PATCHES=(
+	"${FILESDIR}/${P}-makefile.patch"
+	"${FILESDIR}/${P}-script.patch"
+	"${FILESDIR}/${P}-exitcode.patch"
+	"${FILESDIR}/${P}-spelling.patch"
+)
+
+src_compile() {
+	tc-export CXX
+	emake rx
+	use bignum && emake rs
+}
+
+src_install() {
+	dodoc -r Examples
+	dobin minisat+_64-bit
+	use bignum && dobin minisat+_bignum
+	if use bignum; then
+		dosym ./minisat+_bignum "${EPREFIX}/usr/bin/minisat+"
+	else
+		dosym ./minisat+_64-bit "${EPREFIX}/usr/bin/minisat+"
+	fi
+}