* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/minisat/, sci-mathematics/minisat/files/
@ 2016-09-13 8:04 David Seifert
0 siblings, 0 replies; 3+ messages in thread
From: David Seifert @ 2016-09-13 8:04 UTC (permalink / raw
To: gentoo-commits
commit: cea4776ca601ecc574478b3ec3a4d7e014e2e710
Author: Gerhard Bräunlich <wippbox <AT> gmx <DOT> net>
AuthorDate: Fri Sep 9 13:39:34 2016 +0000
Commit: David Seifert <soap <AT> gentoo <DOT> org>
CommitDate: Tue Sep 13 08:03:21 2016 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=cea4776c
sci-mathematics/minisat: Adding minisat-2.2.0_p20130925
Package-Manager: portage-2.2.28
Closes: https://github.com/gentoo/gentoo/pull/2282
Signed-off-by: David Seifert <soap <AT> gentoo.org>
sci-mathematics/minisat/Manifest | 1 +
.../files/minisat-2.2.0_p20130925-nusmv.patch | 527 +++++++++++++++++++++
.../minisat/minisat-2.2.0_p20130925.ebuild | 58 +++
3 files changed, 586 insertions(+)
diff --git a/sci-mathematics/minisat/Manifest b/sci-mathematics/minisat/Manifest
index 12aa841..8b3908e 100644
--- a/sci-mathematics/minisat/Manifest
+++ b/sci-mathematics/minisat/Manifest
@@ -1,2 +1,3 @@
DIST MiniSat.pdf 327416 SHA256 53197dbd783c924a2627d75e305706297988494265bd5e5ec873840e5d797ac4 SHA512 94e70c721740c0b7fd52621c7a5e43dd9207eed92e60a1c64ee63b541b9861d2580d14ba64c49c6c4f273ac028ded43bc944c71131e51693cdd7d1763af582f6 WHIRLPOOL a087d8929476fc33464d19432fc05a01797761f695b81c0aa6d35270731b00dabe2402ea2cfd705b49d5d6664a3cbd46bc60147d60934acdfc94a33066316185
DIST minisat-2.2.0.tar.gz 43879 SHA256 92957d851cdc3baddfe07b5fc80ed5a0237c489d0c52ae72f62844b3b46d7808 SHA512 cf79b05d43ebdc8fd8081899a1f853370de051cafe6e5b143eaff9827efc542b58062782a3ce2a3d1a03561a9ffd780c9cdc645bb50036eb61e80fa729136e64 WHIRLPOOL a5117e7bc81aeecb6fa34d8e2dea70b379d9e3463957e7029c80957ff3bcdd3107a99fb0dabfe59b57bfdb16ed51a0a4781c8dbf8e3f6f225ebd5035c1a9ff79
+DIST minisat-2.2.0_p20130925.tar.gz 49544 SHA256 3db05b02f91c4b097b7962e523225aa5e6fa9a6c0d42704a170b01b069cdfcfe SHA512 37fc35cc4f3104d7f0e8ee9f7123fc34e175df578658266799d809d71d6cf081e811919f304a02f6cb9c3827d308e59408149d63d1d1e7c6d0b495350f93b3d9 WHIRLPOOL c976fabadb2149e15260025646e465d7422ffb9fd35e37263766002462de7b8d16db031aacb1458467acd9957eb370894d39ea3a7ddc5c98627f84b0a08b7820
diff --git a/sci-mathematics/minisat/files/minisat-2.2.0_p20130925-nusmv.patch b/sci-mathematics/minisat/files/minisat-2.2.0_p20130925-nusmv.patch
new file mode 100644
index 00000000..96808be
--- /dev/null
+++ b/sci-mathematics/minisat/files/minisat-2.2.0_p20130925-nusmv.patch
@@ -0,0 +1,527 @@
+--- a/Makefile
++++ b/Makefile
+@@ -69,8 +89,8 @@
+ VERB=
+ endif
+
+-SRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc)
+-HDRS = $(wildcard minisat/mtl/*.h) $(wildcard minisat/core/*.h) $(wildcard minisat/simp/*.h) $(wildcard minisat/utils/*.h)
++SRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc) $(wildcard minisat/proof/*.cc)
++HDRS = $(wildcard minisat/mtl/*.h) $(wildcard minisat/core/*.h) $(wildcard minisat/simp/*.h) $(wildcard minisat/utils/*.h) $(wildcard minisat/proof/*.h)
+ OBJS = $(filter-out %Main.o, $(SRCS:.cc=.o))
+
+ r: $(BUILD_DIR)/release/bin/$(MINISAT)
+@@ -89,7 +109,7 @@
+ lsh: $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)
+
+ ## Build-type Compile-flags:
+-$(BUILD_DIR)/release/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_RELSYM)
++$(BUILD_DIR)/release/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_RELSYM) $(MINISAT_FPIC)
+ $(BUILD_DIR)/debug/%.o: MINISAT_CXXFLAGS +=$(MINISAT_DEB) -g
+ $(BUILD_DIR)/profile/%.o: MINISAT_CXXFLAGS +=$(MINISAT_PRF) -pg
+ $(BUILD_DIR)/dynamic/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_FPIC)
+@@ -195,7 +215,7 @@
+ $(INSTALL) -d $(DESTDIR)$(bindir)
+ $(INSTALL) -m 755 $(BUILD_DIR)/dynamic/bin/$(MINISAT) $(DESTDIR)$(bindir)
+
+-clean:
++origclean:
+ rm -f $(foreach t, release debug profile dynamic, $(foreach o, $(SRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \
+ $(foreach t, release debug profile dynamic, $(foreach d, $(SRCS:.cc=.d), $(BUILD_DIR)/$t/$d)) \
+ $(foreach t, release debug profile dynamic, $(BUILD_DIR)/$t/bin/$(MINISAT_CORE) $(BUILD_DIR)/$t/bin/$(MINISAT)) \
+@@ -203,6 +223,7 @@
+ $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\
+ $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\
+ $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB)
++ rm -f $(NUSMV_LIBNAME)
+
+ distclean: clean
+ rm -f config.mk
+--- a/minisat/core/Solver.cc
++++ b/minisat/core/Solver.cc
+@@ -101,7 +101,16 @@
+ , conflict_budget (-1)
+ , propagation_budget (-1)
+ , asynch_interrupt (false)
+-{}
++{
++ // NuSMV: MOD BEGIN
++ /* Disables "progress saving" which relies on last polarity
++ assigned to a var when branching. Polarity for us is forced to
++ be false. See http://reasoning.cs.ucla.edu/fetch.php?id=69&type=pdf
++ */
++ phase_saving = 0;
++ default_polarity = l_Undef;
++ // NuSMV: MOD END
++}
+
+
+ Solver::~Solver()
+@@ -250,8 +259,19 @@
+ {
+ Var next = var_Undef;
+
++ // NuSMV: PREF MOD
++ // Selection from preferred list
++ for (int i = 0; i < preferred.size(); i++) {
++ if (value(preferred[i]) == l_Undef) {
++ next = preferred[i];
++ break;
++ }
++ }
++ // NuSMV: PREF MOD END
++
+ // Random decision:
+- if (drand(random_seed) < random_var_freq && !order_heap.empty()){
++ if (next == var_Undef && // NuSMV: PREF MOD
++ drand(random_seed) < random_var_freq && !order_heap.empty()){
+ next = order_heap[irand(random_seed,order_heap.size())];
+ if (value(next) == l_Undef && decision[next])
+ rnd_decisions++; }
+@@ -269,6 +289,8 @@
+ return lit_Undef;
+ else if (user_pol[next] != l_Undef)
+ return mkLit(next, user_pol[next] == l_True);
++ else if (default_polarity != l_Undef) // NuSMV
++ return mkLit(next, default_polarity == l_True);
+ else if (rnd_pol)
+ return mkLit(next, drand(random_seed) < 0.5);
+ else
+@@ -620,6 +642,19 @@
+ }
+
+
++// NuSMV: PREF MOD
++void Solver::addPreferred(Var v)
++{
++ preferred.push(v);
++}
++
++void Solver::clearPreferred()
++{
++ preferred.clear(0);
++}
++// NuSMV: PREF MOD END
++
++
+ void Solver::rebuildOrderHeap()
+ {
+ vec<Var> vs;
+--- a/minisat/core/Solver.h
++++ b/minisat/core/Solver.h
+@@ -90,6 +90,19 @@
+ void setPolarity (Var v, lbool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
+ void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
+
++ // NuSMV: PREF MOD
++ /*
++ * Add a variable at the end of the list of preferred variables
++ * Does not remove the variable from the standard ordering.
++ */
++ void addPreferred(Var v);
++
++ /*
++ * Clear vector of preferred variables.
++ */
++ void clearPreferred();
++ // NuSMV: PREF MOD END
++
+ // Read state:
+ //
+ lbool value (Var x) const; // The current value of a variable.
+@@ -134,6 +147,8 @@
+ int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
+ int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full).
+ bool rnd_pol; // Use random polarities for branching heuristics.
++ lbool default_polarity; // NuSMV: default polarity for vars
++
+ bool rnd_init_act; // Initialize variable activities with a small random value.
+ double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered.
+ int min_learnts_lim; // Minimum number to set the learnts limit to.
+@@ -215,6 +230,10 @@
+ Var next_var; // Next variable to be created.
+ ClauseAllocator ca;
+
++ // NuSMV: PREF MOD
++ vec<Var> preferred;
++ // NuSMV: PREF MOD END
++
+ vec<Var> released_vars;
+ vec<Var> free_vars;
+
+--- a/minisat/core/SolverTypes.h
++++ b/minisat/core/SolverTypes.h
+@@ -52,7 +52,7 @@
+ int x;
+
+ // Use this as a constructor:
+- friend Lit mkLit(Var var, bool sign = false);
++ friend Lit mkLit(Var var, bool sign);
+
+ bool operator == (Lit p) const { return x == p.x; }
+ bool operator != (Lit p) const { return x != p.x; }
+@@ -61,6 +61,7 @@
+
+
+ inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
++inline Lit mkLit (Var var) { return mkLit(var, false); }
+ inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
+ inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
+ inline bool sign (Lit p) { return p.x & 1; }
+@@ -120,6 +121,7 @@
+ inline int toInt (lbool l) { return l.value; }
+ inline lbool toLbool(int v) { return lbool((uint8_t)v); }
+
++#define MINISAT_CONSTANTS_AS_MACROS
+ #if defined(MINISAT_CONSTANTS_AS_MACROS)
+ #define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
+ #define l_False (lbool((uint8_t)1))
+--- a/minisat/simp/Solver_C.cc
++++ b/minisat/simp/Solver_C.cc
+@@ -0,0 +1,246 @@
++
++/**************************************************************************************************
++
++Solver_C.C
++
++C-wrapper for Solver.C
++
++ This file is part of NuSMV version 2.
++ Copyright (C) 2007 by FBK-irst.
++ Author: Roberto Cavada <cavada@fbk.eu>
++
++ NuSMV version 2 is free software; you can redistribute it and/or
++ modify it under the terms of the GNU Lesser General Public
++ License as published by the Free Software Foundation; either
++ version 2 of the License, or (at your option) any later version.
++
++ NuSMV version 2 is distributed in the hope that it will be useful,
++ but WITHOUT ANY WARRANTY; without even the implied warranty of
++ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
++ Lesser General Public License for more details.
++
++ You should have received a copy of the GNU Lesser General Public
++ License along with this library; if not, write to the Free Software
++ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
++
++ For more information on NuSMV see <http://nusmv.fbk.eu>
++ or email to <nusmv-users@fbk.eu>.
++ Please report bugs to <nusmv-users@fbk.eu>.
++
++ To contact the NuSMV development board, email to <nusmv@fbk.eu>. ]
++
++**************************************************************************************************/
++
++
++#include "SimpSolver.h"
++extern "C" {
++#include "Solver_C.h"
++}
++
++namespace {
++using Minisat::lbool;
++} // namespace
++
++extern "C" MiniSat_ptr MiniSat_Create()
++{
++ Minisat::SimpSolver *s = new Minisat::SimpSolver();
++ s->default_polarity = l_True;
++ return (MiniSat_ptr)s;
++}
++
++extern "C"void MiniSat_Delete(MiniSat_ptr ms)
++{
++ delete (Minisat::SimpSolver *)ms;
++}
++
++extern "C" int MiniSat_Nof_Variables(MiniSat_ptr ms)
++{
++ return ((Minisat::SimpSolver *)ms)->nVars();
++}
++
++extern "C" int MiniSat_Nof_Clauses(MiniSat_ptr ms)
++{
++ return ((Minisat::SimpSolver *)ms)->nClauses();
++}
++
++/* variables are in the range 1...N */
++extern "C" int MiniSat_New_Variable(MiniSat_ptr ms)
++{
++ /* Actually, minisat used variable range 0 .. N-1,
++ so in all function below there is a convertion between
++ input variable (1..N) and internal variables (0..N-1)
++ */
++ Minisat::Var var = ((Minisat::SimpSolver *)ms)->newVar();
++ ((Minisat::SimpSolver *)ms)->setFrozen(var, true);
++ return var+1;
++}
++
++
++/*
++ * Here clauses are in dimacs form, variable indexing is 1...N
++ */
++extern "C" int MiniSat_Add_Clause(MiniSat_ptr ms,
++ int *clause_lits, int num_lits)
++{
++ int i;
++ Minisat::vec<Minisat::Lit> cl;
++ for(i = 0; i < num_lits; ++i) {
++ const int lit = clause_lits[i];
++ assert(abs(lit) > 0);
++ assert(abs(lit) <= MiniSat_Nof_Variables((Minisat::SimpSolver*)ms));
++ int var = abs(lit) - 1;
++ cl.push((lit > 0) ? Minisat::mkLit(var) : ~ Minisat::mkLit(var));
++ }
++ ((Minisat::SimpSolver *)ms)->addClause(cl);
++
++ if(((Minisat::SimpSolver *)ms)->okay()) return 1;
++ return 0;
++}
++
++extern "C" int MiniSat_Solve(MiniSat_ptr ms)
++{
++ bool ret = ((Minisat::SimpSolver *)ms)->solve();
++ if(ret) return 1;
++ return 0;
++}
++
++/*
++ * Here the assumption is in "dimacs form", variable indexing is 1...N
++ */
++extern "C" int MiniSat_Solve_Assume(MiniSat_ptr ms,
++ int nof_assumed_lits,
++ int *assumed_lits)
++{
++ int i;
++ Minisat::vec<Minisat::Lit> cl;
++ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
++ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
++
++ solver.simplify();
++ if(solver.okay() == false) return 0;
++
++ assert(nof_assumed_lits >= 0);
++ for(i = 0; i < nof_assumed_lits; ++i) {
++ const int lit = assumed_lits[i];
++ assert(abs(lit) > 0);
++ assert(abs(lit) <= MiniSat_Nof_Variables((Minisat::SimpSolver*)ms));
++ int var = abs(lit) - 1;
++ cl.push((lit > 0) ? Minisat::mkLit(var) : ~Minisat::mkLit(var));
++ }
++
++ if (solver.solve(cl)) return 1;
++ return 0;
++}
++
++extern "C" int MiniSat_simplifyDB(MiniSat_ptr ms)
++{
++ ((Minisat::SimpSolver *)ms)->simplify();
++ if(((Minisat::SimpSolver *)ms)->okay()) return 1;
++ return 0;
++}
++
++/*
++ * Here variables are numbered 1...N
++ */
++extern "C" int MiniSat_Get_Value(MiniSat_ptr ms, int var_num)
++{
++ assert(var_num > 0);
++ if(var_num > MiniSat_Nof_Variables(ms)) return -1;
++ /* minisat assigns all variables. just check */
++ assert(((Minisat::SimpSolver *)ms)->model[var_num-1] != l_Undef);
++
++ if(((Minisat::SimpSolver *)ms)->model[var_num-1] == l_True) return 1;
++ return 0;
++}
++
++extern "C" int MiniSat_Get_Nof_Conflict_Lits(MiniSat_ptr ms)
++{
++ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
++ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
++
++ return solver.conflict.size();
++}
++
++extern "C" void MiniSat_Get_Conflict_Lits(MiniSat_ptr ms, int* conflict_lits)
++{
++ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
++ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
++
++ Minisat::LSet& cf = solver.conflict;
++
++ for (int i = 0; i < cf.size(); ++i) {
++ int v = Minisat::var(~cf[i]);
++ int s = Minisat::sign(~cf[i]);
++ assert(v != Minisat::var_Undef);
++ conflict_lits[i] = (s == 0) ? (v+1) : -(v+1);
++ }
++}
++
++/** mode can be polarity_user, polarity_rnd */
++extern "C" void MiniSat_Set_Polarity_Mode(MiniSat_ptr ms, int mode)
++{
++ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
++ assert(__polarity_unsupported != mode);
++ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
++ if (polarity_rnd == mode) {
++ solver.rnd_pol = true;
++ solver.default_polarity = l_Undef;
++ }
++ else {
++ // assert(polarity_user == mode);
++ solver.rnd_pol = false;
++ switch (mode) {
++ case polarity_false:
++ solver.default_polarity = l_True;
++ break;
++ case polarity_true:
++ solver.default_polarity = l_False;
++ break;
++ default: // polarity_user
++ solver.default_polarity = l_Undef;
++ break;
++ }
++ }
++}
++
++extern "C" int MiniSat_Get_Polarity_Mode(MiniSat_ptr ms)
++{
++ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
++ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
++ //return solver.rnd_pol ? polarity_rnd : polarity_user;
++ if (solver.rnd_pol) {
++ return polarity_rnd;
++ } else if (solver.default_polarity == l_True) {
++ return polarity_false;
++ } else if (solver.default_polarity == l_False) {
++ return polarity_true;
++ } else {
++ return polarity_user;
++ }
++}
++
++extern "C" void MiniSat_Set_Random_Seed(MiniSat_ptr ms, double seed)
++{
++ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
++ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
++ solver.random_seed = seed;
++}
++
++
++// NuSMV: PREF MOD
++/* variables are in the range 1...N */
++extern "C" void MiniSat_Set_Preferred_Variable(MiniSat_ptr ms, int x)
++{
++ /* Actually, minisat used variable range 0 .. N-1,
++ so in all function below there is a convertion between
++ input variable (1..N) and internal variables (0..N-1)
++ */
++ ((Minisat::SimpSolver *)ms)->addPreferred((Minisat::Var) x);
++}
++
++extern "C" void MiniSat_Clear_Preferred_Variables(MiniSat_ptr ms)
++{
++
++ ((Minisat::SimpSolver *)ms)->clearPreferred();
++}
++// NuSMV: PREF MOD END
+--- a/minisat/simp/Solver_C.h
++++ b/minisat/simp/Solver_C.h
+@@ -0,0 +1,72 @@
++/**************************************************************************************************
++
++Solver_C.h
++
++C-wrapper for Solver.h
++
++ This file is part of NuSMV version 2.
++ Copyright (C) 2007 by FBK-irst.
++ Author: Roberto Cavada <cavada@fbk.eu>
++
++ NuSMV version 2 is free software; you can redistribute it and/or
++ modify it under the terms of the GNU Lesser General Public
++ License as published by the Free Software Foundation; either
++ version 2 of the License, or (at your option) any later version.
++
++ NuSMV version 2 is distributed in the hope that it will be useful,
++ but WITHOUT ANY WARRANTY; without even the implied warranty of
++ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
++ Lesser General Public License for more details.
++
++ You should have received a copy of the GNU Lesser General Public
++ License along with this library; if not, write to the Free Software
++ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
++
++ For more information on NuSMV see <http://nusmv.fbk.eu>
++ or email to <nusmv-users@fbk.eu>.
++ Please report bugs to <nusmv-users@fbk.eu>.
++
++ To contact the NuSMV development board, email to <nusmv@fbk.eu>. ]
++
++**************************************************************************************************/
++
++#ifndef SOLVER_C_h
++#define SOLVER_C_h
++
++//=================================================================================================
++// Solver -- the main class:
++
++#define MiniSat_ptr void *
++
++enum {
++ __polarity_unsupported = -1,
++ polarity_true = 0,
++ polarity_false = 1,
++ polarity_user = 2,
++ polarity_rnd = 3,
++};
++
++MiniSat_ptr MiniSat_Create();
++void MiniSat_Delete(MiniSat_ptr);
++int MiniSat_Nof_Variables(MiniSat_ptr);
++int MiniSat_Nof_Clauses(MiniSat_ptr);
++int MiniSat_New_Variable(MiniSat_ptr);
++int MiniSat_Add_Clause(MiniSat_ptr, int *clause_lits, int num_lits);
++int MiniSat_Solve(MiniSat_ptr);
++int MiniSat_Solve_Assume(MiniSat_ptr, int nof_assumed_lits, int *assumed_lits);
++int MiniSat_simplifyDB(MiniSat_ptr);
++int MiniSat_Get_Value(MiniSat_ptr, int var_num);
++int MiniSat_Get_Nof_Conflict_Lits(MiniSat_ptr ms);
++void MiniSat_Get_Conflict_Lits(MiniSat_ptr ms, int* conflict_lits);
++
++void MiniSat_Set_Polarity_Mode(MiniSat_ptr ms, int mode);
++int MiniSat_Get_Polarity_Mode(MiniSat_ptr ms);
++void MiniSat_Set_Random_Seed(MiniSat_ptr ms, double seed);
++
++// NuSMV: PREF MOD
++void MiniSat_Set_Preferred_Variable(MiniSat_ptr, int);
++void MiniSat_Clear_Preferred_Variables(MiniSat_ptr);
++// NuSMV: PREF MOD END
++
++//=================================================================================================
++#endif
+--- a/minisat/utils/System.cc
++++ b/minisat/utils/System.cc
+@@ -77,7 +77,7 @@
+ struct rusage ru;
+ getrusage(RUSAGE_SELF, &ru);
+ return (double)ru.ru_maxrss / 1024; }
+-double Minisat::memUsedPeak() { return memUsed(); }
++double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); }
+
+
+ #elif defined(__APPLE__)
+@@ -87,11 +87,11 @@
+ malloc_statistics_t t;
+ malloc_zone_statistics(NULL, &t);
+ return (double)t.max_size_in_use / (1024*1024); }
+-double Minisat::memUsedPeak() { return memUsed(); }
++double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); }
+
+ #else
+ double Minisat::memUsed() { return 0; }
+-double Minisat::memUsedPeak() { return 0; }
++double Minisat::memUsedPeak(bool strictlyPeak) { return 0; }
+ #endif
+
+
diff --git a/sci-mathematics/minisat/minisat-2.2.0_p20130925.ebuild b/sci-mathematics/minisat/minisat-2.2.0_p20130925.ebuild
new file mode 100644
index 00000000..ff47b97
--- /dev/null
+++ b/sci-mathematics/minisat/minisat-2.2.0_p20130925.ebuild
@@ -0,0 +1,58 @@
+# Copyright 1999-2016 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Id$
+
+EAPI=6
+
+inherit toolchain-funcs vcs-snapshot
+
+DESCRIPTION="Small yet efficient SAT solver with reference paper"
+HOMEPAGE="http://minisat.se/Main.html"
+COMMIT=37dc6c67e2af26379d88ce349eb9c4c6160e8543
+SRC_URI="https://github.com/niklasso/minisat/archive/${COMMIT}.tar.gz -> ${P}.tar.gz
+ doc? ( http://minisat.se/downloads/MiniSat.pdf )"
+
+SLOT="0"
+KEYWORDS="~amd64 ~x86 ~amd64-linux ~x86-linux"
+LICENSE="MIT"
+
+IUSE="debug doc"
+
+DEPEND="sys-libs/zlib"
+RDEPEND="${DEPEND}"
+DOCS=( README doc/ReleaseNotes-${PV%_*}.txt )
+PATCHES=( "${FILESDIR}"/${P}-nusmv.patch )
+
+src_prepare() {
+ default
+ # Remove makefile silencing and
+ # Remove static linking by default
+ sed -i -e "s/VERB=@/VERB=/" \
+ -e "s/--static //g" \
+ Makefile || die
+
+ sed -i -e "s:\$(exec_prefix)/lib:\$(exec_prefix)/$(get_libdir):" \
+ Makefile || die
+
+ # Fix headers ( #include "minisat/..." -> #include <...> )
+ while IFS="" read -d $'\0' -r file; do
+ einfo Correcting header "$file"
+ sed -i -e 's:#include "minisat/\([^"]*\)":#include <\1>:g' "${file}" || die
+ done < <(find minisat -name "*.h" -print0)
+}
+
+src_configure() {
+ local minisat_cflags="${CFLAGS} -D NDEBUG -I${S}/minisat"
+ emake config prefix="${EPREFIX}"/usr MINISAT_RELSYM="" MINISAT_REL="${minisat_cflags}" MINISAT_PRF="${minisat_cflags}" MINISAT_DEB="${CFLAGS} -D DEBUG -I${S}/minisat"
+}
+
+src_compile() {
+ emake all $(usex debug d "")
+}
+
+src_install() {
+ use doc && DOCS+=( "${DISTDIR}"/MiniSat.pdf )
+ default
+
+ dosym libminisat.a /usr/$(get_libdir)/libMiniSat.a
+}
^ permalink raw reply related [flat|nested] 3+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/minisat/, sci-mathematics/minisat/files/
@ 2022-01-24 9:32 David Seifert
0 siblings, 0 replies; 3+ messages in thread
From: David Seifert @ 2022-01-24 9:32 UTC (permalink / raw
To: gentoo-commits
commit: ba0f1ed8329f945c8d7718ac06a374d8b390828b
Author: David Seifert <soap <AT> gentoo <DOT> org>
AuthorDate: Mon Jan 24 09:32:15 2022 +0000
Commit: David Seifert <soap <AT> gentoo <DOT> org>
CommitDate: Mon Jan 24 09:32:15 2022 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ba0f1ed8
sci-mathematics/minisat: don't install static libraries (pg0204)
Signed-off-by: David Seifert <soap <AT> gentoo.org>
.../minisat/files/minisat-2.2.1-cmake.patch | 54 ++++++++++++++++++++++
...inisat-2.2.1.ebuild => minisat-2.2.1-r1.ebuild} | 10 ++--
2 files changed, 58 insertions(+), 6 deletions(-)
diff --git a/sci-mathematics/minisat/files/minisat-2.2.1-cmake.patch b/sci-mathematics/minisat/files/minisat-2.2.1-cmake.patch
new file mode 100644
index 000000000000..1c875827f6ac
--- /dev/null
+++ b/sci-mathematics/minisat/files/minisat-2.2.1-cmake.patch
@@ -0,0 +1,54 @@
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -2,6 +2,7 @@
+
+ project(minisat)
+
++include(GNUInstallDirs)
+ #--------------------------------------------------------------------------------------------------
+ # Configurable options:
+
+@@ -44,24 +45,16 @@
+ minisat/core/Solver.cc
+ minisat/simp/SimpSolver.cc)
+
+-add_library(minisat-lib-static STATIC ${MINISAT_LIB_SOURCES})
+ add_library(minisat-lib-shared SHARED ${MINISAT_LIB_SOURCES})
+
+ target_link_libraries(minisat-lib-shared ${ZLIB_LIBRARY})
+-target_link_libraries(minisat-lib-static ${ZLIB_LIBRARY})
+
+ add_executable(minisat_core minisat/core/Main.cc)
+ add_executable(minisat_simp minisat/simp/Main.cc)
+
+-if(STATIC_BINARIES)
+- target_link_libraries(minisat_core minisat-lib-static)
+- target_link_libraries(minisat_simp minisat-lib-static)
+-else()
+- target_link_libraries(minisat_core minisat-lib-shared)
+- target_link_libraries(minisat_simp minisat-lib-shared)
+-endif()
++target_link_libraries(minisat_core minisat-lib-shared)
++target_link_libraries(minisat_simp minisat-lib-shared)
+
+-set_target_properties(minisat-lib-static PROPERTIES OUTPUT_NAME "minisat")
+ set_target_properties(minisat-lib-shared
+ PROPERTIES
+ OUTPUT_NAME "minisat"
+@@ -73,11 +66,11 @@
+ #--------------------------------------------------------------------------------------------------
+ # Installation targets:
+
+-install(TARGETS minisat-lib-static minisat-lib-shared minisat_core minisat_simp
+- RUNTIME DESTINATION bin
+- LIBRARY DESTINATION lib
+- ARCHIVE DESTINATION lib)
++install(TARGETS minisat-lib-shared minisat_core minisat_simp
++ RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR}
++ LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
++ ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR})
+
+ install(DIRECTORY minisat/mtl minisat/utils minisat/core minisat/simp
+- DESTINATION include/minisat
++ DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/minisat
+ FILES_MATCHING PATTERN "*.h")
diff --git a/sci-mathematics/minisat/minisat-2.2.1.ebuild b/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
similarity index 79%
rename from sci-mathematics/minisat/minisat-2.2.1.ebuild
rename to sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
index 360c5a33082b..15d260429e0f 100644
--- a/sci-mathematics/minisat/minisat-2.2.1.ebuild
+++ b/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
@@ -11,19 +11,17 @@ SRC_URI="https://github.com/stp/${PN}/archive/releases/${PV}.tar.gz -> ${P}.tar.
doc? ( http://minisat.se/downloads/MiniSat.pdf )"
S="${WORKDIR}/${PN}-releases-${PV}"
+LICENSE="MIT"
SLOT="0/${PV}"
KEYWORDS="~amd64 ~x86"
-LICENSE="MIT"
IUSE="doc"
RDEPEND="sys-libs/zlib:="
DEPEND="${RDEPEND}"
+PATCHES=( "${FILESDIR}"/${P}-cmake.patch )
+
src_install() {
cmake_src_install
-
- mv "${D}"/usr/lib "${D}"/usr/$(get_libdir) || die
- dosym libminisat.a /usr/$(get_libdir)/libMiniSat.a
-
use doc && dodoc "${DISTDIR}"/MiniSat.pdf
}
^ permalink raw reply related [flat|nested] 3+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/minisat/, sci-mathematics/minisat/files/
@ 2023-02-06 17:23 Maciej Barć
0 siblings, 0 replies; 3+ messages in thread
From: Maciej Barć @ 2023-02-06 17:23 UTC (permalink / raw
To: gentoo-commits
commit: 58bf1623e2f1be955a04a7b5adbbb03b79459fbd
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Mon Feb 6 16:14:41 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Mon Feb 6 17:23:18 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=58bf1623
sci-mathematics/minisat: fix build on musl
Bug: https://github.com/stp/minisat/pull/6
Closes: https://bugs.gentoo.org/832519
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
.../minisat/files/minisat-2.2.1-musl.patch | 41 ++++++++++++++++++++++
sci-mathematics/minisat/minisat-2.2.1-r1.ebuild | 13 ++++---
2 files changed, 50 insertions(+), 4 deletions(-)
diff --git a/sci-mathematics/minisat/files/minisat-2.2.1-musl.patch b/sci-mathematics/minisat/files/minisat-2.2.1-musl.patch
new file mode 100644
index 000000000000..3a25d5964318
--- /dev/null
+++ b/sci-mathematics/minisat/files/minisat-2.2.1-musl.patch
@@ -0,0 +1,41 @@
+From 4c8afcd6bfbf2cbdb5ebe271f20503a6d34d7d49 Mon Sep 17 00:00:00 2001
+From: =?UTF-8?q?Maciej=20Bar=C4=87?= <xgqt@gentoo.org>
+Date: Mon, 6 Feb 2023 17:09:18 +0100
+Subject: [PATCH] utils/System.*: use fpu_control only on glibc
+MIME-Version: 1.0
+Content-Type: text/plain; charset=UTF-8
+Content-Transfer-Encoding: 8bit
+
+Bug: https://github.com/vprover/vampire/pull/432
+Signed-off-by: Maciej Barć <xgqt@gentoo.org>
+---
+ minisat/utils/System.cc | 2 +-
+ minisat/utils/System.h | 2 +-
+ 2 files changed, 2 insertions(+), 2 deletions(-)
+
+diff --git a/minisat/utils/System.cc b/minisat/utils/System.cc
+index 282f98ed..112708f7 100644
+--- a/minisat/utils/System.cc
++++ b/minisat/utils/System.cc
+@@ -97,7 +97,7 @@ double Minisat::memUsedPeak(bool /*strictlyPeak*/) { return 0; }
+
+ void Minisat::setX86FPUPrecision()
+ {
+-#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
++#if defined(__GLIBC__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
+ // Only correct FPU precision on Linux architectures that needs and supports it:
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+diff --git a/minisat/utils/System.h b/minisat/utils/System.h
+index a51d4c2e..189fcbff 100644
+--- a/minisat/utils/System.h
++++ b/minisat/utils/System.h
+@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
+ #ifndef Minisat_System_h
+ #define Minisat_System_h
+
+-#if defined(__linux__)
++#if defined(__GLIBC__)
+ #include <fpu_control.h>
+ #endif
+
diff --git a/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild b/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
index 15d260429e0f..ac28363ef0f5 100644
--- a/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
+++ b/sci-mathematics/minisat/minisat-2.2.1-r1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
@@ -6,10 +6,11 @@ EAPI=8
inherit cmake
DESCRIPTION="Small yet efficient SAT solver with reference paper"
-HOMEPAGE="http://minisat.se/Main.html"
+HOMEPAGE="http://minisat.se/Main.html
+ https://github.com/stp/minisat/"
SRC_URI="https://github.com/stp/${PN}/archive/releases/${PV}.tar.gz -> ${P}.tar.gz
doc? ( http://minisat.se/downloads/MiniSat.pdf )"
-S="${WORKDIR}/${PN}-releases-${PV}"
+S="${WORKDIR}"/${PN}-releases-${PV}
LICENSE="MIT"
SLOT="0/${PV}"
@@ -19,9 +20,13 @@ IUSE="doc"
RDEPEND="sys-libs/zlib:="
DEPEND="${RDEPEND}"
-PATCHES=( "${FILESDIR}"/${P}-cmake.patch )
+PATCHES=(
+ "${FILESDIR}"/${P}-cmake.patch
+ "${FILESDIR}"/${P}-musl.patch
+)
src_install() {
cmake_src_install
+
use doc && dodoc "${DISTDIR}"/MiniSat.pdf
}
^ permalink raw reply related [flat|nested] 3+ messages in thread
end of thread, other threads:[~2023-02-06 17:23 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2023-02-06 17:23 [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/minisat/, sci-mathematics/minisat/files/ Maciej Barć
-- strict thread matches above, loose matches on Subject: below --
2022-01-24 9:32 David Seifert
2016-09-13 8:04 David Seifert
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox