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 |
-} |