Gentoo Archives: gentoo-commits

From: "Maciej Barć" <xgqt@g.o>
To: gentoo-commits@l.g.o
Subject: [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/minisat/files/, sci-mathematics/minisat/
Date: Mon, 17 Jan 2022 18:06:30
Message-Id: 1642442761.403dbc431f544038e9c5d44e563194f0bf395c02.xgqt@gentoo
1 commit: 403dbc431f544038e9c5d44e563194f0bf395c02
2 Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
3 AuthorDate: Mon Jan 17 18:00:34 2022 +0000
4 Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
5 CommitDate: Mon Jan 17 18:06:01 2022 +0000
6 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=403dbc43
7
8 sci-mathematics/minisat: drop old 2.2.0_p20130925 version
9
10 Closes: https://bugs.gentoo.org/741598
11 Closes: https://bugs.gentoo.org/713420
12 Package-Manager: Portage-3.0.28, Repoman-3.0.3
13 Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
14
15 sci-mathematics/minisat/Manifest | 1 -
16 .../files/minisat-2.2.0_p20130925-nusmv.patch | 527 ---------------------
17 .../minisat/minisat-2.2.0_p20130925-r1.ebuild | 57 ---
18 3 files changed, 585 deletions(-)
19
20 diff --git a/sci-mathematics/minisat/Manifest b/sci-mathematics/minisat/Manifest
21 index 672e6b24bfa1..e4f1fa8b5352 100644
22 --- a/sci-mathematics/minisat/Manifest
23 +++ b/sci-mathematics/minisat/Manifest
24 @@ -1,3 +1,2 @@
25 DIST MiniSat.pdf 327416 BLAKE2B 77f77d763c9554680b4c5e1688801e8462102e8ddbcc3b53badccee17a98f935ef0e971a636abeb04021a2b3a3e9d6acfe4828b5dd20e6ef8733d71788cc31b0 SHA512 94e70c721740c0b7fd52621c7a5e43dd9207eed92e60a1c64ee63b541b9861d2580d14ba64c49c6c4f273ac028ded43bc944c71131e51693cdd7d1763af582f6
26 -DIST minisat-2.2.0_p20130925.tar.gz 49544 BLAKE2B 8c6893fb6c604140609c36cc912c02a73c1f2726d7f399595c50d674aff69c57f9c4914da6d95c37a46fefc218dd4b0550645bd7058d46640d08103e2a4ec333 SHA512 37fc35cc4f3104d7f0e8ee9f7123fc34e175df578658266799d809d71d6cf081e811919f304a02f6cb9c3827d308e59408149d63d1d1e7c6d0b495350f93b3d9
27 DIST minisat-2.2.1.tar.gz 50485 BLAKE2B 58c292f0b90dd459fa29fadbf9e2b20106406c08df9ce98f40138b12a8f001b4ab72f661815d1254c6c90158c3d6e3df339c784552605a935ebc5e703b2d8768 SHA512 a69734e1a70fe056f9dfd479fe4e6e25bc418d3631c1c2d0dea1190ffe9f86b1fc5e9aabaf3772a752fe654551f1e84e47fcb8655f6fe25176efc8d8bc96c663
28
29 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
30 deleted file mode 100644
31 index 4b17c8fb44bb..000000000000
32 --- a/sci-mathematics/minisat/files/minisat-2.2.0_p20130925-nusmv.patch
33 +++ /dev/null
34 @@ -1,527 +0,0 @@
35 ---- a/Makefile
36 -+++ b/Makefile
37 -@@ -69,8 +89,8 @@
38 - VERB=
39 - endif
40 -
41 --SRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc)
42 --HDRS = $(wildcard minisat/mtl/*.h) $(wildcard minisat/core/*.h) $(wildcard minisat/simp/*.h) $(wildcard minisat/utils/*.h)
43 -+SRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc) $(wildcard minisat/proof/*.cc)
44 -+HDRS = $(wildcard minisat/mtl/*.h) $(wildcard minisat/core/*.h) $(wildcard minisat/simp/*.h) $(wildcard minisat/utils/*.h) $(wildcard minisat/proof/*.h)
45 - OBJS = $(filter-out %Main.o, $(SRCS:.cc=.o))
46 -
47 - r: $(BUILD_DIR)/release/bin/$(MINISAT)
48 -@@ -89,7 +109,7 @@
49 - lsh: $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)
50 -
51 - ## Build-type Compile-flags:
52 --$(BUILD_DIR)/release/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_RELSYM)
53 -+$(BUILD_DIR)/release/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_RELSYM) $(MINISAT_FPIC)
54 - $(BUILD_DIR)/debug/%.o: MINISAT_CXXFLAGS +=$(MINISAT_DEB) -g
55 - $(BUILD_DIR)/profile/%.o: MINISAT_CXXFLAGS +=$(MINISAT_PRF) -pg
56 - $(BUILD_DIR)/dynamic/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_FPIC)
57 -@@ -195,7 +215,7 @@
58 - $(INSTALL) -d $(DESTDIR)$(bindir)
59 - $(INSTALL) -m 755 $(BUILD_DIR)/dynamic/bin/$(MINISAT) $(DESTDIR)$(bindir)
60 -
61 --clean:
62 -+origclean:
63 - rm -f $(foreach t, release debug profile dynamic, $(foreach o, $(SRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \
64 - $(foreach t, release debug profile dynamic, $(foreach d, $(SRCS:.cc=.d), $(BUILD_DIR)/$t/$d)) \
65 - $(foreach t, release debug profile dynamic, $(BUILD_DIR)/$t/bin/$(MINISAT_CORE) $(BUILD_DIR)/$t/bin/$(MINISAT)) \
66 -@@ -203,6 +223,7 @@
67 - $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\
68 - $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\
69 - $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB)
70 -+ rm -f $(NUSMV_LIBNAME)
71 -
72 - distclean: clean
73 - rm -f config.mk
74 ---- a/minisat/core/Solver.cc
75 -+++ b/minisat/core/Solver.cc
76 -@@ -101,7 +101,16 @@
77 - , conflict_budget (-1)
78 - , propagation_budget (-1)
79 - , asynch_interrupt (false)
80 --{}
81 -+{
82 -+ // NuSMV: MOD BEGIN
83 -+ /* Disables "progress saving" which relies on last polarity
84 -+ assigned to a var when branching. Polarity for us is forced to
85 -+ be false. See http://reasoning.cs.ucla.edu/fetch.php?id=69&type=pdf
86 -+ */
87 -+ phase_saving = 0;
88 -+ default_polarity = l_Undef;
89 -+ // NuSMV: MOD END
90 -+}
91 -
92 -
93 - Solver::~Solver()
94 -@@ -250,8 +259,19 @@
95 - {
96 - Var next = var_Undef;
97 -
98 -+ // NuSMV: PREF MOD
99 -+ // Selection from preferred list
100 -+ for (int i = 0; i < preferred.size(); i++) {
101 -+ if (value(preferred[i]) == l_Undef) {
102 -+ next = preferred[i];
103 -+ break;
104 -+ }
105 -+ }
106 -+ // NuSMV: PREF MOD END
107 -+
108 - // Random decision:
109 -- if (drand(random_seed) < random_var_freq && !order_heap.empty()){
110 -+ if (next == var_Undef && // NuSMV: PREF MOD
111 -+ drand(random_seed) < random_var_freq && !order_heap.empty()){
112 - next = order_heap[irand(random_seed,order_heap.size())];
113 - if (value(next) == l_Undef && decision[next])
114 - rnd_decisions++; }
115 -@@ -269,6 +289,8 @@
116 - return lit_Undef;
117 - else if (user_pol[next] != l_Undef)
118 - return mkLit(next, user_pol[next] == l_True);
119 -+ else if (default_polarity != l_Undef) // NuSMV
120 -+ return mkLit(next, default_polarity == l_True);
121 - else if (rnd_pol)
122 - return mkLit(next, drand(random_seed) < 0.5);
123 - else
124 -@@ -620,6 +642,19 @@
125 - }
126 -
127 -
128 -+// NuSMV: PREF MOD
129 -+void Solver::addPreferred(Var v)
130 -+{
131 -+ preferred.push(v);
132 -+}
133 -+
134 -+void Solver::clearPreferred()
135 -+{
136 -+ preferred.clear(0);
137 -+}
138 -+// NuSMV: PREF MOD END
139 -+
140 -+
141 - void Solver::rebuildOrderHeap()
142 - {
143 - vec<Var> vs;
144 ---- a/minisat/core/Solver.h
145 -+++ b/minisat/core/Solver.h
146 -@@ -90,6 +90,19 @@
147 - void setPolarity (Var v, lbool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
148 - void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
149 -
150 -+ // NuSMV: PREF MOD
151 -+ /*
152 -+ * Add a variable at the end of the list of preferred variables
153 -+ * Does not remove the variable from the standard ordering.
154 -+ */
155 -+ void addPreferred(Var v);
156 -+
157 -+ /*
158 -+ * Clear vector of preferred variables.
159 -+ */
160 -+ void clearPreferred();
161 -+ // NuSMV: PREF MOD END
162 -+
163 - // Read state:
164 - //
165 - lbool value (Var x) const; // The current value of a variable.
166 -@@ -134,6 +147,8 @@
167 - int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
168 - int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full).
169 - bool rnd_pol; // Use random polarities for branching heuristics.
170 -+ lbool default_polarity; // NuSMV: default polarity for vars
171 -+
172 - bool rnd_init_act; // Initialize variable activities with a small random value.
173 - double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered.
174 - int min_learnts_lim; // Minimum number to set the learnts limit to.
175 -@@ -215,6 +230,10 @@
176 - Var next_var; // Next variable to be created.
177 - ClauseAllocator ca;
178 -
179 -+ // NuSMV: PREF MOD
180 -+ vec<Var> preferred;
181 -+ // NuSMV: PREF MOD END
182 -+
183 - vec<Var> released_vars;
184 - vec<Var> free_vars;
185 -
186 ---- a/minisat/core/SolverTypes.h
187 -+++ b/minisat/core/SolverTypes.h
188 -@@ -52,7 +52,7 @@
189 - int x;
190 -
191 - // Use this as a constructor:
192 -- friend Lit mkLit(Var var, bool sign = false);
193 -+ friend Lit mkLit(Var var, bool sign);
194 -
195 - bool operator == (Lit p) const { return x == p.x; }
196 - bool operator != (Lit p) const { return x != p.x; }
197 -@@ -61,6 +61,7 @@
198 -
199 -
200 - inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
201 -+inline Lit mkLit (Var var) { return mkLit(var, false); }
202 - inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
203 - inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
204 - inline bool sign (Lit p) { return p.x & 1; }
205 -@@ -120,6 +121,7 @@
206 - inline int toInt (lbool l) { return l.value; }
207 - inline lbool toLbool(int v) { return lbool((uint8_t)v); }
208 -
209 -+#define MINISAT_CONSTANTS_AS_MACROS
210 - #if defined(MINISAT_CONSTANTS_AS_MACROS)
211 - #define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
212 - #define l_False (lbool((uint8_t)1))
213 ---- a/minisat/simp/Solver_C.cc
214 -+++ b/minisat/simp/Solver_C.cc
215 -@@ -0,0 +1,246 @@
216 -+
217 -+/**************************************************************************************************
218 -+
219 -+Solver_C.C
220 -+
221 -+C-wrapper for Solver.C
222 -+
223 -+ This file is part of NuSMV version 2.
224 -+ Copyright (C) 2007 by FBK-irst.
225 -+ Author: Roberto Cavada <cavada@×××.eu>
226 -+
227 -+ NuSMV version 2 is free software; you can redistribute it and/or
228 -+ modify it under the terms of the GNU Lesser General Public
229 -+ License as published by the Free Software Foundation; either
230 -+ version 2 of the License, or (at your option) any later version.
231 -+
232 -+ NuSMV version 2 is distributed in the hope that it will be useful,
233 -+ but WITHOUT ANY WARRANTY; without even the implied warranty of
234 -+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
235 -+ Lesser General Public License for more details.
236 -+
237 -+ You should have received a copy of the GNU Lesser General Public
238 -+ License along with this library; if not, write to the Free Software
239 -+ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
240 -+
241 -+ For more information on NuSMV see <http://nusmv.fbk.eu>
242 -+ or email to <nusmv-users@×××.eu>.
243 -+ Please report bugs to <nusmv-users@×××.eu>.
244 -+
245 -+ To contact the NuSMV development board, email to <nusmv@×××.eu>. ]
246 -+
247 -+**************************************************************************************************/
248 -+
249 -+
250 -+#include "SimpSolver.h"
251 -+extern "C" {
252 -+#include "Solver_C.h"
253 -+}
254 -+
255 -+namespace {
256 -+using Minisat::lbool;
257 -+} // namespace
258 -+
259 -+extern "C" MiniSat_ptr MiniSat_Create()
260 -+{
261 -+ Minisat::SimpSolver *s = new Minisat::SimpSolver();
262 -+ s->default_polarity = l_True;
263 -+ return (MiniSat_ptr)s;
264 -+}
265 -+
266 -+extern "C" void MiniSat_Delete(MiniSat_ptr ms)
267 -+{
268 -+ delete (Minisat::SimpSolver *)ms;
269 -+}
270 -+
271 -+extern "C" int MiniSat_Nof_Variables(MiniSat_ptr ms)
272 -+{
273 -+ return ((Minisat::SimpSolver *)ms)->nVars();
274 -+}
275 -+
276 -+extern "C" int MiniSat_Nof_Clauses(MiniSat_ptr ms)
277 -+{
278 -+ return ((Minisat::SimpSolver *)ms)->nClauses();
279 -+}
280 -+
281 -+/* variables are in the range 1...N */
282 -+extern "C" int MiniSat_New_Variable(MiniSat_ptr ms)
283 -+{
284 -+ /* Actually, minisat used variable range 0 .. N-1,
285 -+ so in all function below there is a convertion between
286 -+ input variable (1..N) and internal variables (0..N-1)
287 -+ */
288 -+ Minisat::Var var = ((Minisat::SimpSolver *)ms)->newVar();
289 -+ ((Minisat::SimpSolver *)ms)->setFrozen(var, true);
290 -+ return var+1;
291 -+}
292 -+
293 -+
294 -+/*
295 -+ * Here clauses are in dimacs form, variable indexing is 1...N
296 -+ */
297 -+extern "C" int MiniSat_Add_Clause(MiniSat_ptr ms,
298 -+ int *clause_lits, int num_lits)
299 -+{
300 -+ int i;
301 -+ Minisat::vec<Minisat::Lit> cl;
302 -+ for(i = 0; i < num_lits; ++i) {
303 -+ const int lit = clause_lits[i];
304 -+ assert(abs(lit) > 0);
305 -+ assert(abs(lit) <= MiniSat_Nof_Variables((Minisat::SimpSolver*)ms));
306 -+ int var = abs(lit) - 1;
307 -+ cl.push((lit > 0) ? Minisat::mkLit(var) : ~ Minisat::mkLit(var));
308 -+ }
309 -+ ((Minisat::SimpSolver *)ms)->addClause(cl);
310 -+
311 -+ if(((Minisat::SimpSolver *)ms)->okay()) return 1;
312 -+ return 0;
313 -+}
314 -+
315 -+extern "C" int MiniSat_Solve(MiniSat_ptr ms)
316 -+{
317 -+ bool ret = ((Minisat::SimpSolver *)ms)->solve();
318 -+ if(ret) return 1;
319 -+ return 0;
320 -+}
321 -+
322 -+/*
323 -+ * Here the assumption is in "dimacs form", variable indexing is 1...N
324 -+ */
325 -+extern "C" int MiniSat_Solve_Assume(MiniSat_ptr ms,
326 -+ int nof_assumed_lits,
327 -+ int *assumed_lits)
328 -+{
329 -+ int i;
330 -+ Minisat::vec<Minisat::Lit> cl;
331 -+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
332 -+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
333 -+
334 -+ solver.simplify();
335 -+ if(solver.okay() == false) return 0;
336 -+
337 -+ assert(nof_assumed_lits >= 0);
338 -+ for(i = 0; i < nof_assumed_lits; ++i) {
339 -+ const int lit = assumed_lits[i];
340 -+ assert(abs(lit) > 0);
341 -+ assert(abs(lit) <= MiniSat_Nof_Variables((Minisat::SimpSolver*)ms));
342 -+ int var = abs(lit) - 1;
343 -+ cl.push((lit > 0) ? Minisat::mkLit(var) : ~Minisat::mkLit(var));
344 -+ }
345 -+
346 -+ if (solver.solve(cl)) return 1;
347 -+ return 0;
348 -+}
349 -+
350 -+extern "C" int MiniSat_simplifyDB(MiniSat_ptr ms)
351 -+{
352 -+ ((Minisat::SimpSolver *)ms)->simplify();
353 -+ if(((Minisat::SimpSolver *)ms)->okay()) return 1;
354 -+ return 0;
355 -+}
356 -+
357 -+/*
358 -+ * Here variables are numbered 1...N
359 -+ */
360 -+extern "C" int MiniSat_Get_Value(MiniSat_ptr ms, int var_num)
361 -+{
362 -+ assert(var_num > 0);
363 -+ if(var_num > MiniSat_Nof_Variables(ms)) return -1;
364 -+ /* minisat assigns all variables. just check */
365 -+ assert(((Minisat::SimpSolver *)ms)->model[var_num-1] != l_Undef);
366 -+
367 -+ if(((Minisat::SimpSolver *)ms)->model[var_num-1] == l_True) return 1;
368 -+ return 0;
369 -+}
370 -+
371 -+extern "C" int MiniSat_Get_Nof_Conflict_Lits(MiniSat_ptr ms)
372 -+{
373 -+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
374 -+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
375 -+
376 -+ return solver.conflict.size();
377 -+}
378 -+
379 -+extern "C" void MiniSat_Get_Conflict_Lits(MiniSat_ptr ms, int* conflict_lits)
380 -+{
381 -+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
382 -+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
383 -+
384 -+ Minisat::LSet& cf = solver.conflict;
385 -+
386 -+ for (int i = 0; i < cf.size(); ++i) {
387 -+ int v = Minisat::var(~cf[i]);
388 -+ int s = Minisat::sign(~cf[i]);
389 -+ assert(v != Minisat::var_Undef);
390 -+ conflict_lits[i] = (s == 0) ? (v+1) : -(v+1);
391 -+ }
392 -+}
393 -+
394 -+/** mode can be polarity_user, polarity_rnd */
395 -+extern "C" void MiniSat_Set_Polarity_Mode(MiniSat_ptr ms, int mode)
396 -+{
397 -+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
398 -+ assert(__polarity_unsupported != mode);
399 -+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
400 -+ if (polarity_rnd == mode) {
401 -+ solver.rnd_pol = true;
402 -+ solver.default_polarity = l_Undef;
403 -+ }
404 -+ else {
405 -+ // assert(polarity_user == mode);
406 -+ solver.rnd_pol = false;
407 -+ switch (mode) {
408 -+ case polarity_false:
409 -+ solver.default_polarity = l_True;
410 -+ break;
411 -+ case polarity_true:
412 -+ solver.default_polarity = l_False;
413 -+ break;
414 -+ default: // polarity_user
415 -+ solver.default_polarity = l_Undef;
416 -+ break;
417 -+ }
418 -+ }
419 -+}
420 -+
421 -+extern "C" int MiniSat_Get_Polarity_Mode(MiniSat_ptr ms)
422 -+{
423 -+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
424 -+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
425 -+ //return solver.rnd_pol ? polarity_rnd : polarity_user;
426 -+ if (solver.rnd_pol) {
427 -+ return polarity_rnd;
428 -+ } else if (solver.default_polarity == l_True) {
429 -+ return polarity_false;
430 -+ } else if (solver.default_polarity == l_False) {
431 -+ return polarity_true;
432 -+ } else {
433 -+ return polarity_user;
434 -+ }
435 -+}
436 -+
437 -+extern "C" void MiniSat_Set_Random_Seed(MiniSat_ptr ms, double seed)
438 -+{
439 -+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
440 -+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
441 -+ solver.random_seed = seed;
442 -+}
443 -+
444 -+
445 -+// NuSMV: PREF MOD
446 -+/* variables are in the range 1...N */
447 -+extern "C" void MiniSat_Set_Preferred_Variable(MiniSat_ptr ms, int x)
448 -+{
449 -+ /* Actually, minisat used variable range 0 .. N-1,
450 -+ so in all function below there is a convertion between
451 -+ input variable (1..N) and internal variables (0..N-1)
452 -+ */
453 -+ ((Minisat::SimpSolver *)ms)->addPreferred((Minisat::Var) x);
454 -+}
455 -+
456 -+extern "C" void MiniSat_Clear_Preferred_Variables(MiniSat_ptr ms)
457 -+{
458 -+
459 -+ ((Minisat::SimpSolver *)ms)->clearPreferred();
460 -+}
461 -+// NuSMV: PREF MOD END
462 ---- a/minisat/simp/Solver_C.h
463 -+++ b/minisat/simp/Solver_C.h
464 -@@ -0,0 +1,72 @@
465 -+/**************************************************************************************************
466 -+
467 -+Solver_C.h
468 -+
469 -+C-wrapper for Solver.h
470 -+
471 -+ This file is part of NuSMV version 2.
472 -+ Copyright (C) 2007 by FBK-irst.
473 -+ Author: Roberto Cavada <cavada@×××.eu>
474 -+
475 -+ NuSMV version 2 is free software; you can redistribute it and/or
476 -+ modify it under the terms of the GNU Lesser General Public
477 -+ License as published by the Free Software Foundation; either
478 -+ version 2 of the License, or (at your option) any later version.
479 -+
480 -+ NuSMV version 2 is distributed in the hope that it will be useful,
481 -+ but WITHOUT ANY WARRANTY; without even the implied warranty of
482 -+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
483 -+ Lesser General Public License for more details.
484 -+
485 -+ You should have received a copy of the GNU Lesser General Public
486 -+ License along with this library; if not, write to the Free Software
487 -+ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
488 -+
489 -+ For more information on NuSMV see <http://nusmv.fbk.eu>
490 -+ or email to <nusmv-users@×××.eu>.
491 -+ Please report bugs to <nusmv-users@×××.eu>.
492 -+
493 -+ To contact the NuSMV development board, email to <nusmv@×××.eu>. ]
494 -+
495 -+**************************************************************************************************/
496 -+
497 -+#ifndef SOLVER_C_h
498 -+#define SOLVER_C_h
499 -+
500 -+//=================================================================================================
501 -+// Solver -- the main class:
502 -+
503 -+#define MiniSat_ptr void *
504 -+
505 -+enum {
506 -+ __polarity_unsupported = -1,
507 -+ polarity_true = 0,
508 -+ polarity_false = 1,
509 -+ polarity_user = 2,
510 -+ polarity_rnd = 3,
511 -+};
512 -+
513 -+MiniSat_ptr MiniSat_Create();
514 -+void MiniSat_Delete(MiniSat_ptr);
515 -+int MiniSat_Nof_Variables(MiniSat_ptr);
516 -+int MiniSat_Nof_Clauses(MiniSat_ptr);
517 -+int MiniSat_New_Variable(MiniSat_ptr);
518 -+int MiniSat_Add_Clause(MiniSat_ptr, int *clause_lits, int num_lits);
519 -+int MiniSat_Solve(MiniSat_ptr);
520 -+int MiniSat_Solve_Assume(MiniSat_ptr, int nof_assumed_lits, int *assumed_lits);
521 -+int MiniSat_simplifyDB(MiniSat_ptr);
522 -+int MiniSat_Get_Value(MiniSat_ptr, int var_num);
523 -+int MiniSat_Get_Nof_Conflict_Lits(MiniSat_ptr ms);
524 -+void MiniSat_Get_Conflict_Lits(MiniSat_ptr ms, int* conflict_lits);
525 -+
526 -+void MiniSat_Set_Polarity_Mode(MiniSat_ptr ms, int mode);
527 -+int MiniSat_Get_Polarity_Mode(MiniSat_ptr ms);
528 -+void MiniSat_Set_Random_Seed(MiniSat_ptr ms, double seed);
529 -+
530 -+// NuSMV: PREF MOD
531 -+void MiniSat_Set_Preferred_Variable(MiniSat_ptr, int);
532 -+void MiniSat_Clear_Preferred_Variables(MiniSat_ptr);
533 -+// NuSMV: PREF MOD END
534 -+
535 -+//=================================================================================================
536 -+#endif
537 ---- a/minisat/utils/System.cc
538 -+++ b/minisat/utils/System.cc
539 -@@ -77,7 +77,7 @@
540 - struct rusage ru;
541 - getrusage(RUSAGE_SELF, &ru);
542 - return (double)ru.ru_maxrss / 1024; }
543 --double Minisat::memUsedPeak() { return memUsed(); }
544 -+double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); }
545 -
546 -
547 - #elif defined(__APPLE__)
548 -@@ -87,11 +87,11 @@
549 - malloc_statistics_t t;
550 - malloc_zone_statistics(NULL, &t);
551 - return (double)t.max_size_in_use / (1024*1024); }
552 --double Minisat::memUsedPeak() { return memUsed(); }
553 -+double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); }
554 -
555 - #else
556 - double Minisat::memUsed() { return 0; }
557 --double Minisat::memUsedPeak() { return 0; }
558 -+double Minisat::memUsedPeak(bool strictlyPeak) { return 0; }
559 - #endif
560 -
561 -
562
563 diff --git a/sci-mathematics/minisat/minisat-2.2.0_p20130925-r1.ebuild b/sci-mathematics/minisat/minisat-2.2.0_p20130925-r1.ebuild
564 deleted file mode 100644
565 index 39e62e229e7d..000000000000
566 --- a/sci-mathematics/minisat/minisat-2.2.0_p20130925-r1.ebuild
567 +++ /dev/null
568 @@ -1,57 +0,0 @@
569 -# Copyright 1999-2016 Gentoo Foundation
570 -# Distributed under the terms of the GNU General Public License v2
571 -
572 -EAPI=6
573 -
574 -inherit toolchain-funcs vcs-snapshot
575 -
576 -DESCRIPTION="Small yet efficient SAT solver with reference paper"
577 -HOMEPAGE="http://minisat.se/Main.html"
578 -COMMIT=37dc6c67e2af26379d88ce349eb9c4c6160e8543
579 -SRC_URI="https://github.com/niklasso/minisat/archive/${COMMIT}.tar.gz -> ${P}.tar.gz
580 - doc? ( http://minisat.se/downloads/MiniSat.pdf )"
581 -
582 -SLOT="0"
583 -KEYWORDS="~amd64 ~x86 ~amd64-linux ~x86-linux"
584 -LICENSE="MIT"
585 -
586 -IUSE="debug doc"
587 -
588 -DEPEND="sys-libs/zlib"
589 -RDEPEND="${DEPEND}"
590 -DOCS=( README doc/ReleaseNotes-${PV%_*}.txt )
591 -PATCHES=( "${FILESDIR}"/${P}-nusmv.patch )
592 -
593 -src_prepare() {
594 - default
595 - # Remove makefile silencing and
596 - # Remove static linking by default
597 - sed -i -e "s/VERB=@/VERB=/" \
598 - -e "s/--static //g" \
599 - Makefile || die
600 -
601 - sed -i -e "s:\$(exec_prefix)/lib:\$(exec_prefix)/$(get_libdir):" \
602 - Makefile || die
603 -
604 - # Fix headers ( #include "minisat/..." -> #include <...> )
605 - while IFS="" read -d $'\0' -r file; do
606 - einfo Correcting header "$file"
607 - sed -i -e 's:#include "minisat/\([^"]*\)":#include <minisat/\1>:g' "${file}" || die
608 - done < <(find minisat -name "*.h" -print0)
609 -}
610 -
611 -src_configure() {
612 - local minisat_cflags="${CFLAGS} -D NDEBUG -I${S}/minisat"
613 - emake config prefix="${EPREFIX}"/usr MINISAT_RELSYM="" MINISAT_REL="${minisat_cflags}" MINISAT_PRF="${minisat_cflags}" MINISAT_DEB="${CFLAGS} -D DEBUG -I${S}/minisat"
614 -}
615 -
616 -src_compile() {
617 - emake all $(usex debug d "")
618 -}
619 -
620 -src_install() {
621 - use doc && DOCS+=( "${DISTDIR}"/MiniSat.pdf )
622 - default
623 -
624 - dosym libminisat.a /usr/$(get_libdir)/libMiniSat.a
625 -}