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 <[email protected]> (extracted from upstream git) +Approved: Ralf Treinen <[email protected]> +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 <[email protected]> +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>[email protected]</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 +}
