diff options
author | Gerhard Bräunlich <wippbox@gmx.net> | 2016-09-09 15:39:34 +0200 |
---|---|---|
committer | David Seifert <soap@gentoo.org> | 2016-09-13 10:03:21 +0200 |
commit | cea4776ca601ecc574478b3ec3a4d7e014e2e710 (patch) | |
tree | 35c42eb4066a44e28445d80f1b14688b71a69b7d /sci-mathematics/minisat | |
parent | sci-mathematics/minisat: Unsiliencing makefile (diff) | |
download | gentoo-cea4776ca601ecc574478b3ec3a4d7e014e2e710.tar.gz gentoo-cea4776ca601ecc574478b3ec3a4d7e014e2e710.tar.bz2 gentoo-cea4776ca601ecc574478b3ec3a4d7e014e2e710.zip |
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@gentoo.org>
Diffstat (limited to 'sci-mathematics/minisat')
-rw-r--r-- | sci-mathematics/minisat/Manifest | 1 | ||||
-rw-r--r-- | sci-mathematics/minisat/files/minisat-2.2.0_p20130925-nusmv.patch | 527 | ||||
-rw-r--r-- | sci-mathematics/minisat/minisat-2.2.0_p20130925.ebuild | 58 |
3 files changed, 586 insertions, 0 deletions
diff --git a/sci-mathematics/minisat/Manifest b/sci-mathematics/minisat/Manifest index 12aa8412d0b2..8b3908e426b3 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 000000000000..96808be3c7f3 --- /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 000000000000..ff47b97ac706 --- /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 +} |