|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
AbstractPseudoBooleanAndPigeonHoleTest | Line # 20 | 43 | 1 | 97,6% |
0.9764706
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
(39) | |||
Result | |||
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncc
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnc8
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnb1
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnC432
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnC17
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testn9symml
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5060
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata103
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata83
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata63
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4050
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata43
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4045
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5055
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc103
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5051
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc83
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3540
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc63
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3536
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc43
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4041
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3545
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2030
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3031
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3035
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3040
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1520
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1525
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2021
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2025
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1011
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1015
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1020
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1516
![]() |
3 FAIL | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncm42a
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncmb
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnmux
![]() |
1 PASS | |
0.023529412
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testnmyadder
![]() |
1 PASS | |
1 | /* | |
2 | * Created on 20 mai 2004 | |
3 | * | |
4 | */ | |
5 | package org.sat4j.minisat.constraints; | |
6 | ||
7 | import java.io.FileNotFoundException; | |
8 | import java.io.IOException; | |
9 | ||
10 | import junit.swingui.TestRunner; | |
11 | ||
12 | import org.sat4j.reader.ParseFormatException; | |
13 | ||
14 | /** | |
15 | * @author leberre | |
16 | * | |
17 | * Those pseudo boolean problems were kindly provided by Niklas Een. | |
18 | * | |
19 | */ | |
20 | public abstract class AbstractPseudoBooleanAndPigeonHoleTest extends | |
21 | AbstractPigeonHoleWithCardinalityTest { | |
22 | ||
23 | protected static final String PREFIX = System.getProperty("test.pbprefix"); | |
24 | ||
25 | /** | |
26 | * Cr?ation d'un test | |
27 | * | |
28 | * @param arg | |
29 | * argument ?ventuel | |
30 | */ | |
31 | 636 |
![]() |
32 | 636 | super(arg); |
33 | } | |
34 | ||
35 | /** | |
36 | * Lancement du test | |
37 | * | |
38 | * @param args | |
39 | */ | |
40 | 0 |
![]() |
41 | 0 | TestRunner.run(AbstractPseudoBooleanAndPigeonHoleTest.class); |
42 | } | |
43 | ||
44 | 636 |
![]() |
45 | protected void tearDown() { | |
46 | 636 | super.tearDown(); |
47 | 636 | System.gc(); |
48 | } | |
49 | ||
50 | // // Tests normalises | |
51 | ||
52 | // public void testnfrb30151() throws FileNotFoundException, IOException, | |
53 | // ParseFormatException { | |
54 | // assertTrue(solveInstance(PREFIX + | |
55 | // "normalized-opb/kexu/normalized-frb30-15-1.opb")); | |
56 | // } | |
57 | // | |
58 | // public void testnfrb30152() throws FileNotFoundException, IOException, | |
59 | // ParseFormatException { | |
60 | // assertTrue(solveInstance(PREFIX + | |
61 | // "normalized-opb/kexu/normalized-frb30-15-2.opb")); | |
62 | // } | |
63 | // | |
64 | // public void testnfrb30153() throws FileNotFoundException, IOException, | |
65 | // ParseFormatException { | |
66 | // assertTrue(solveInstance(PREFIX + | |
67 | // "normalized-opb/kexu/normalized-frb30-15-3.opb")); | |
68 | // } | |
69 | // | |
70 | // public void testnfrb30154() throws FileNotFoundException, IOException, | |
71 | // ParseFormatException { | |
72 | // assertTrue(solveInstance(PREFIX + | |
73 | // "normalized-opb/kexu/normalized-frb30-15-4.opb")); | |
74 | // } | |
75 | // | |
76 | // public void testnfrb30155() throws FileNotFoundException, IOException, | |
77 | // ParseFormatException { | |
78 | // assertTrue(solveInstance(PREFIX + | |
79 | // "normalized-opb/kexu/normalized-frb30-15-5.opb")); | |
80 | // } | |
81 | // | |
82 | // public void testnfrb35171() throws FileNotFoundException, IOException, | |
83 | // ParseFormatException { | |
84 | // assertTrue(solveInstance(PREFIX + | |
85 | // "normalized-opb/kexu/normalized-frb35-17-1.opb")); | |
86 | // } | |
87 | // | |
88 | // public void testnfrb35172() throws FileNotFoundException, IOException, | |
89 | // ParseFormatException { | |
90 | // assertTrue(solveInstance(PREFIX + | |
91 | // "normalized-opb/kexu/normalized-frb35-17-2.opb")); | |
92 | // } | |
93 | // | |
94 | // public void testnfrb35173() throws FileNotFoundException, IOException, | |
95 | // ParseFormatException { | |
96 | // assertTrue(solveInstance(PREFIX + | |
97 | // "normalized-opb/kexu/normalized-frb35-17-3.opb")); | |
98 | // } | |
99 | // | |
100 | // public void testnfrb35174() throws FileNotFoundException, IOException, | |
101 | // ParseFormatException { | |
102 | // assertTrue(solveInstance(PREFIX + | |
103 | // "normalized-opb/kexu/normalized-frb35-17-4.opb")); | |
104 | // } | |
105 | // | |
106 | // public void testnfrb35175() throws FileNotFoundException, IOException, | |
107 | // ParseFormatException { | |
108 | // assertTrue(solveInstance(PREFIX + | |
109 | // "normalized-opb/kexu/normalized-frb35-17-5.opb")); | |
110 | // } | |
111 | // | |
112 | // public void testnfrb40191() throws FileNotFoundException, IOException, | |
113 | // ParseFormatException { | |
114 | // assertTrue(solveInstance(PREFIX + | |
115 | // "normalized-opb/kexu/normalized-frb40-19-1.opb")); | |
116 | // } | |
117 | // | |
118 | // public void testnfrb40192() throws FileNotFoundException, IOException, | |
119 | // ParseFormatException { | |
120 | // assertTrue(solveInstance(PREFIX + | |
121 | // "normalized-opb/kexu/normalized-frb40-19-2.opb")); | |
122 | // } | |
123 | // | |
124 | // public void testnfrb40193() throws FileNotFoundException, IOException, | |
125 | // ParseFormatException { | |
126 | // assertTrue(solveInstance(PREFIX + | |
127 | // "normalized-opb/kexu/normalized-frb40-19-3.opb")); | |
128 | // } | |
129 | // | |
130 | // public void testnfrb40194() throws FileNotFoundException, IOException, | |
131 | // ParseFormatException { | |
132 | // assertTrue(solveInstance(PREFIX + | |
133 | // "normalized-opb/kexu/normalized-frb40-19-4.opb")); | |
134 | // } | |
135 | // | |
136 | // public void testnfrb40195() throws FileNotFoundException, IOException, | |
137 | // ParseFormatException { | |
138 | // assertTrue(solveInstance(PREFIX + | |
139 | // "normalized-opb/kexu/normalized-frb40-19-5.opb")); | |
140 | // } | |
141 | // | |
142 | // public void testnfrb45211() throws FileNotFoundException, IOException, | |
143 | // ParseFormatException { | |
144 | // assertTrue(solveInstance(PREFIX + | |
145 | // "normalized-opb/kexu/normalized-frb45-21-1.opb")); | |
146 | // } | |
147 | // | |
148 | // public void testnfrb45212() throws FileNotFoundException, IOException, | |
149 | // ParseFormatException { | |
150 | // assertTrue(solveInstance(PREFIX + | |
151 | // "normalized-opb/kexu/normalized-frb45-21-2.opb")); | |
152 | // } | |
153 | // | |
154 | // public void testnfrb45213() throws FileNotFoundException, IOException, | |
155 | // ParseFormatException { | |
156 | // assertTrue(solveInstance(PREFIX + | |
157 | // "normalized-opb/kexu/normalized-frb45-21-3.opb")); | |
158 | // } | |
159 | // | |
160 | // public void testnfrb45214() throws FileNotFoundException, IOException, | |
161 | // ParseFormatException { | |
162 | // assertTrue(solveInstance(PREFIX + | |
163 | // "normalized-opb/kexu/normalized-frb45-21-4.opb")); | |
164 | // } | |
165 | // | |
166 | // public void testnfrb45215() throws FileNotFoundException, IOException, | |
167 | // ParseFormatException { | |
168 | // assertTrue(solveInstance(PREFIX + | |
169 | // "normalized-opb/kexu/normalized-frb45-21-5.opb")); | |
170 | // } | |
171 | // | |
172 | // public void testnfrb50231() throws FileNotFoundException, IOException, | |
173 | // ParseFormatException { | |
174 | // assertTrue(solveInstance(PREFIX + | |
175 | // "normalized-opb/kexu/normalized-frb50-23-1.opb")); | |
176 | // } | |
177 | // | |
178 | // | |
179 | // public void testnfrb50232() throws FileNotFoundException, IOException, | |
180 | // ParseFormatException { | |
181 | // assertTrue(solveInstance(PREFIX + | |
182 | // "normalized-opb/kexu/normalized-frb50-23-2.opb")); | |
183 | // } | |
184 | // | |
185 | // | |
186 | // public void testnfrb50233() throws FileNotFoundException, IOException, | |
187 | // ParseFormatException { | |
188 | // assertTrue(solveInstance(PREFIX + | |
189 | // "normalized-opb/kexu/normalized-frb50-23-3.opb")); | |
190 | // } | |
191 | // | |
192 | // public void testnfrb50234() throws FileNotFoundException, IOException, | |
193 | // ParseFormatException { | |
194 | // assertTrue(solveInstance(PREFIX + | |
195 | // "normalized-opb/kexu/normalized-frb50-23-4.opb")); | |
196 | // } | |
197 | // | |
198 | // public void testnfrb50235() throws FileNotFoundException, IOException, | |
199 | // ParseFormatException { | |
200 | // assertTrue(solveInstance(PREFIX + | |
201 | // "normalized-opb/kexu/normalized-frb50-23-5.opb")); | |
202 | // } | |
203 | // | |
204 | // public void testnfrb53241() throws FileNotFoundException, IOException, | |
205 | // ParseFormatException { | |
206 | // assertTrue(solveInstance(PREFIX + | |
207 | // "normalized-opb/kexu/normalized-frb53-24-1.opb")); | |
208 | // } | |
209 | // | |
210 | // public void testnfrb53242() throws FileNotFoundException, IOException, | |
211 | // ParseFormatException { | |
212 | // assertTrue(solveInstance(PREFIX + | |
213 | // "normalized-opb/kexu/normalized-frb53-24-2.opb")); | |
214 | // } | |
215 | // | |
216 | // public void testnfrb53243() throws FileNotFoundException, IOException, | |
217 | // ParseFormatException { | |
218 | // assertTrue(solveInstance(PREFIX + | |
219 | // "normalized-opb/kexu/normalized-frb53-24-3.opb")); | |
220 | // } | |
221 | // | |
222 | // public void testnfrb53244() throws FileNotFoundException, IOException, | |
223 | // ParseFormatException { | |
224 | // assertTrue(solveInstance(PREFIX + | |
225 | // "normalized-opb/kexu/normalized-frb53-24-4.opb")); | |
226 | // } | |
227 | // | |
228 | // public void testnfrb53245() throws FileNotFoundException, IOException, | |
229 | // ParseFormatException { | |
230 | // assertTrue(solveInstance(PREFIX + | |
231 | // "normalized-opb/kexu/normalized-frb53-24-5.opb")); | |
232 | // } | |
233 | // | |
234 | // public void testnfrb56251() throws FileNotFoundException, IOException, | |
235 | // ParseFormatException { | |
236 | // assertTrue(solveInstance(PREFIX + | |
237 | // "normalized-opb/kexu/normalized-frb56-25-1.opb")); | |
238 | // } | |
239 | // | |
240 | // public void testnfrb56252() throws FileNotFoundException, IOException, | |
241 | // ParseFormatException { | |
242 | // assertTrue(solveInstance(PREFIX + | |
243 | // "normalized-opb/kexu/normalized-frb56-25-2.opb")); | |
244 | // } | |
245 | // | |
246 | // public void testnfrb56253() throws FileNotFoundException, IOException, | |
247 | // ParseFormatException { | |
248 | // assertTrue(solveInstance(PREFIX + | |
249 | // "normalized-opb/kexu/normalized-frb56-25-3.opb")); | |
250 | // } | |
251 | // | |
252 | // public void testnfrb56254() throws FileNotFoundException, IOException, | |
253 | // ParseFormatException { | |
254 | // assertTrue(solveInstance(PREFIX + | |
255 | // "normalized-opb/kexu/normalized-frb56-25-4.opb")); | |
256 | // } | |
257 | // | |
258 | // public void testnfrb56255() throws FileNotFoundException, IOException, | |
259 | // ParseFormatException { | |
260 | // assertTrue(solveInstance(PREFIX + | |
261 | // "normalized-opb/kexu/normalized-frb56-25-5.opb")); | |
262 | // } | |
263 | // | |
264 | // public void testnfrb59261() throws FileNotFoundException, IOException, | |
265 | // ParseFormatException { | |
266 | // assertTrue(solveInstance(PREFIX + | |
267 | // "normalized-opb/kexu/normalized-frb59-26-1.opb")); | |
268 | // } | |
269 | // | |
270 | // public void testnfrb59262() throws FileNotFoundException, IOException, | |
271 | // ParseFormatException { | |
272 | // assertTrue(solveInstance(PREFIX + | |
273 | // "normalized-opb/kexu/normalized-frb59-26-2.opb")); | |
274 | // } | |
275 | // | |
276 | // public void testnfrb59263() throws FileNotFoundException, IOException, | |
277 | // ParseFormatException { | |
278 | // assertTrue(solveInstance(PREFIX + | |
279 | // "normalized-opb/kexu/normalized-frb59-26-3.opb")); | |
280 | // } | |
281 | // | |
282 | // public void testnfrb59264() throws FileNotFoundException, IOException, | |
283 | // ParseFormatException { | |
284 | // assertTrue(solveInstance(PREFIX + | |
285 | // "normalized-opb/kexu/normalized-frb59-26-4.opb")); | |
286 | // } | |
287 | // | |
288 | // public void testnfrb59265() throws FileNotFoundException, IOException, | |
289 | // ParseFormatException { | |
290 | // assertTrue(solveInstance(PREFIX + | |
291 | // "normalized-opb/kexu/normalized-frb59-26-5.opb")); | |
292 | // } | |
293 | ||
294 | // // VASCO: Logic synthesis | |
295 | // public void testn5xp1b() throws FileNotFoundException, IOException, | |
296 | // ParseFormatException { | |
297 | // assertTrue(solveInstance(PREFIX + | |
298 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-5xp1.b.opb")); | |
299 | // } | |
300 | // | |
301 | // public void testn9symb() throws FileNotFoundException, IOException, | |
302 | // ParseFormatException { | |
303 | // assertTrue(solveInstance(PREFIX + | |
304 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-9sym.b.opb")); | |
305 | // } | |
306 | // | |
307 | // public void testnalu4b() throws FileNotFoundException, IOException, | |
308 | // ParseFormatException { | |
309 | // assertTrue(solveInstance(PREFIX + | |
310 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-alu4.b.opb")); | |
311 | // } | |
312 | // | |
313 | // public void testnapex4a() throws FileNotFoundException, IOException, | |
314 | // ParseFormatException { | |
315 | // assertTrue(solveInstance(PREFIX + | |
316 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-apex4.a.opb")); | |
317 | // } | |
318 | // | |
319 | // public void testnbench1pi() throws FileNotFoundException, IOException, | |
320 | // ParseFormatException { | |
321 | // assertTrue(solveInstance(PREFIX + | |
322 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-bench1.pi.opb")); | |
323 | // } | |
324 | // | |
325 | // public void testnclipb() throws FileNotFoundException, IOException, | |
326 | // ParseFormatException { | |
327 | // assertTrue(solveInstance(PREFIX + | |
328 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-clip.b.opb")); | |
329 | // } | |
330 | // | |
331 | // public void testncountb() throws FileNotFoundException, IOException, | |
332 | // ParseFormatException { | |
333 | // assertTrue(solveInstance(PREFIX + | |
334 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-count.b.opb")); | |
335 | // } | |
336 | // | |
337 | // public void testne64() throws FileNotFoundException, IOException, | |
338 | // ParseFormatException { | |
339 | // assertTrue(solveInstance(PREFIX + | |
340 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-e64.b.opb")); | |
341 | // } | |
342 | // | |
343 | // public void testnf51mb() throws FileNotFoundException, IOException, | |
344 | // ParseFormatException { | |
345 | // assertTrue(solveInstance(PREFIX + | |
346 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-f51m.b.opb")); | |
347 | // } | |
348 | // | |
349 | // public void testnjac3() throws FileNotFoundException, IOException, | |
350 | // ParseFormatException { | |
351 | // assertTrue(solveInstance(PREFIX + | |
352 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-jac3.opb")); | |
353 | // } | |
354 | // | |
355 | // public void testnrotb() throws FileNotFoundException, IOException, | |
356 | // ParseFormatException { | |
357 | // assertTrue(solveInstance(PREFIX + | |
358 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-rot.b.opb")); | |
359 | // } | |
360 | // | |
361 | // public void testnsao2b() throws FileNotFoundException, IOException, | |
362 | // ParseFormatException { | |
363 | // assertTrue(solveInstance(PREFIX + | |
364 | // "normalized-opb/submitted/manquinho/logic-synthesis/normalized-sao2.b.opb")); | |
365 | // } | |
366 | // | |
367 | // // VASCO: Routing problems | |
368 | // public void testns3331() throws FileNotFoundException, IOException, | |
369 | // ParseFormatException { | |
370 | // assertTrue(solveInstance(PREFIX + | |
371 | // "normalized-opb/submitted/manquinho/routing/normalized-s3-3-3-1pb.opb")); | |
372 | // } | |
373 | // | |
374 | // public void testns3332() throws FileNotFoundException, IOException, | |
375 | // ParseFormatException { | |
376 | // assertTrue(solveInstance(PREFIX + | |
377 | // "normalized-opb/submitted/manquinho/routing/normalized-s3-3-3-2pb.opb")); | |
378 | // } | |
379 | // | |
380 | // public void testns3333() throws FileNotFoundException, IOException, | |
381 | // ParseFormatException { | |
382 | // assertTrue(solveInstance(PREFIX + | |
383 | // "normalized-opb/submitted/manquinho/routing/normalized-s3-3-3-3pb.opb")); | |
384 | // } | |
385 | // | |
386 | // public void testns3334() throws FileNotFoundException, IOException, | |
387 | // ParseFormatException { | |
388 | // assertTrue(solveInstance(PREFIX + | |
389 | // "normalized-opb/submitted/manquinho/routing/normalized-s3-3-3-4pb.opb")); | |
390 | // } | |
391 | // | |
392 | // public void testns3335() throws FileNotFoundException, IOException, | |
393 | // ParseFormatException { | |
394 | // assertTrue(solveInstance(PREFIX + | |
395 | // "normalized-opb/submitted/manquinho/routing/normalized-s3-3-3-5pb.opb")); | |
396 | // } | |
397 | // | |
398 | // public void testns4431() throws FileNotFoundException, IOException, | |
399 | // ParseFormatException { | |
400 | // assertTrue(solveInstance(PREFIX + | |
401 | // "normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-1pb.opb")); | |
402 | // } | |
403 | // | |
404 | // public void testns4432() throws FileNotFoundException, IOException, | |
405 | // ParseFormatException { | |
406 | // assertTrue(solveInstance(PREFIX + | |
407 | // "normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-2pb.opb")); | |
408 | // } | |
409 | // | |
410 | // public void testns4433() throws FileNotFoundException, IOException, | |
411 | // ParseFormatException { | |
412 | // assertTrue(solveInstance(PREFIX + | |
413 | // "normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-3pb.opb")); | |
414 | // } | |
415 | // | |
416 | // public void testns4434() throws FileNotFoundException, IOException, | |
417 | // ParseFormatException { | |
418 | // assertTrue(solveInstance(PREFIX + | |
419 | // "normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-4pb.opb")); | |
420 | // } | |
421 | // | |
422 | // public void testns4435() throws FileNotFoundException, IOException, | |
423 | // ParseFormatException { | |
424 | // assertTrue(solveInstance(PREFIX + | |
425 | // "normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-5pb.opb")); | |
426 | // } | |
427 | // | |
428 | // public void testns4436() throws FileNotFoundException, IOException, | |
429 | // ParseFormatException { | |
430 | // assertTrue(solveInstance(PREFIX + | |
431 | // "normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-6pb.opb")); | |
432 | // } | |
433 | // | |
434 | // public void testns4437() throws FileNotFoundException, IOException, | |
435 | // ParseFormatException { | |
436 | // assertTrue(solveInstance(PREFIX + | |
437 | // "normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-7pb.opb")); | |
438 | // } | |
439 | // | |
440 | // public void testns4438() throws FileNotFoundException, IOException, | |
441 | // ParseFormatException { | |
442 | // assertTrue(solveInstance(PREFIX + | |
443 | // "normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-8pb.opb")); | |
444 | // } | |
445 | // | |
446 | // public void testns4439() throws FileNotFoundException, IOException, | |
447 | // ParseFormatException { | |
448 | // assertTrue(solveInstance(PREFIX + | |
449 | // "normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-9pb.opb")); | |
450 | // } | |
451 | // | |
452 | // public void testns44310() throws FileNotFoundException, IOException, | |
453 | // ParseFormatException { | |
454 | // assertTrue(solveInstance(PREFIX + | |
455 | // "normalized-opb/submitted/manquinho/routing/normalized-s4-4-3-10pb.opb")); | |
456 | // } | |
457 | ||
458 | // VASCO: traveling tournament problem | |
459 | 12 |
![]() |
460 | ParseFormatException { | |
461 | 12 | assertTrue(solveInstance(PREFIX |
462 | + "normalized-opb/submitted/manquinho/ttp/normalized-circ4_3.opb")); | |
463 | } | |
464 | ||
465 | 12 |
![]() |
466 | ParseFormatException { | |
467 | 12 | assertTrue(solveInstance(PREFIX |
468 | + "normalized-opb/submitted/manquinho/ttp/normalized-circ6_3.opb")); | |
469 | } | |
470 | ||
471 | 12 |
![]() |
472 | ParseFormatException { | |
473 | 12 | assertTrue(solveInstance(PREFIX |
474 | + "normalized-opb/submitted/manquinho/ttp/normalized-circ8_3.opb")); | |
475 | } | |
476 | ||
477 | 12 |
![]() |
478 | ParseFormatException { | |
479 | 12 | assertTrue(solveInstance(PREFIX |
480 | + "normalized-opb/submitted/manquinho/ttp/normalized-circ10_3.opb")); | |
481 | } | |
482 | ||
483 | 12 |
![]() |
484 | ParseFormatException { | |
485 | 12 | assertTrue(solveInstance(PREFIX |
486 | + "normalized-opb/submitted/manquinho/ttp/normalized-data4_3.opb")); | |
487 | } | |
488 | ||
489 | 12 |
![]() |
490 | ParseFormatException { | |
491 | 12 | assertTrue(solveInstance(PREFIX |
492 | + "normalized-opb/submitted/manquinho/ttp/normalized-data6_3.opb")); | |
493 | } | |
494 | ||
495 | 12 |
![]() |
496 | ParseFormatException { | |
497 | 12 | assertTrue(solveInstance(PREFIX |
498 | + "normalized-opb/submitted/manquinho/ttp/normalized-data8_3.opb")); | |
499 | } | |
500 | ||
501 | 12 |
![]() |
502 | ParseFormatException { | |
503 | 12 | assertTrue(solveInstance(PREFIX |
504 | + "normalized-opb/submitted/manquinho/ttp/normalized-data10_3.opb")); | |
505 | } | |
506 | ||
507 | 12 |
![]() |
508 | ParseFormatException { | |
509 | 12 | assertTrue(solveInstance(PREFIX |
510 | + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-9symml.opb")); | |
511 | } | |
512 | ||
513 | 12 |
![]() |
514 | ParseFormatException { | |
515 | 12 | assertTrue(solveInstance(PREFIX |
516 | + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-C17.opb")); | |
517 | } | |
518 | ||
519 | 12 |
![]() |
520 | ParseFormatException { | |
521 | 12 | assertTrue(solveInstance(PREFIX |
522 | + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-C432.opb")); | |
523 | } | |
524 | ||
525 | 12 |
![]() |
526 | ParseFormatException { | |
527 | 12 | assertTrue(solveInstance(PREFIX |
528 | + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-b1.opb")); | |
529 | } | |
530 | ||
531 | 12 |
![]() |
532 | ParseFormatException { | |
533 | 12 | assertTrue(solveInstance(PREFIX |
534 | + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-c8.opb")); | |
535 | } | |
536 | ||
537 | 12 |
![]() |
538 | ParseFormatException { | |
539 | 12 | assertTrue(solveInstance(PREFIX |
540 | + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cc.opb")); | |
541 | } | |
542 | ||
543 | 12 |
![]() |
544 | ParseFormatException { | |
545 | 12 | assertTrue(solveInstance(PREFIX |
546 | + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cm42a.opb")); | |
547 | } | |
548 | ||
549 | 12 |
![]() |
550 | ParseFormatException { | |
551 | 12 | assertTrue(solveInstance(PREFIX |
552 | + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cmb.opb")); | |
553 | } | |
554 | ||
555 | 12 |
![]() |
556 | ParseFormatException { | |
557 | 12 | assertTrue(solveInstance(PREFIX |
558 | + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-mux.opb")); | |
559 | } | |
560 | ||
561 | 12 |
![]() |
562 | ParseFormatException { | |
563 | 12 | assertTrue(solveInstance(PREFIX |
564 | + "normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-my_adder.opb")); | |
565 | } | |
566 | ||
567 | // public void test22ssmv() throws FileNotFoundException, IOException, | |
568 | // ParseFormatException { | |
569 | // assertFalse(solveInstance(PREFIX + | |
570 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-22s.smv.opb")); | |
571 | // } | |
572 | // public void test25ssmv() throws FileNotFoundException, IOException, | |
573 | // ParseFormatException { | |
574 | // assertFalse(solveInstance(PREFIX + | |
575 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-25s.smv.opb")); | |
576 | // } | |
577 | // public void test37ssmv() throws FileNotFoundException, IOException, | |
578 | // ParseFormatException { | |
579 | // assertFalse(solveInstance(PREFIX + | |
580 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-37s.smv.opb")); | |
581 | // } | |
582 | // public void test43ssmv() throws FileNotFoundException, IOException, | |
583 | // ParseFormatException { | |
584 | // assertFalse(solveInstance(PREFIX + | |
585 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-43s.smv.opb")); | |
586 | // } | |
587 | // public void test44ssmv() throws FileNotFoundException, IOException, | |
588 | // ParseFormatException { | |
589 | // assertFalse(solveInstance(PREFIX + | |
590 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-44s.smv.opb")); | |
591 | // } | |
592 | // public void test46ssmv() throws FileNotFoundException, IOException, | |
593 | // ParseFormatException { | |
594 | // assertFalse(solveInstance(PREFIX + | |
595 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-46s.smv.opb")); | |
596 | // } | |
597 | // | |
598 | // public void testblastfloppy12() throws FileNotFoundException, | |
599 | // IOException, | |
600 | // ParseFormatException { | |
601 | // assertFalse(solveInstance(PREFIX + | |
602 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-blast-floppy1-2.ucl.opb")); | |
603 | // } | |
604 | // | |
605 | // public void testblastfloppy13() throws FileNotFoundException, | |
606 | // IOException, | |
607 | // ParseFormatException { | |
608 | // assertFalse(solveInstance(PREFIX + | |
609 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-blast-floppy1-3.ucl.opb")); | |
610 | // } | |
611 | // | |
612 | // public void testblastfloppy14() throws FileNotFoundException, | |
613 | // IOException, | |
614 | // ParseFormatException { | |
615 | // assertFalse(solveInstance(PREFIX + | |
616 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-blast-floppy1-4.ucl.opb")); | |
617 | // } | |
618 | // | |
619 | // public void testblastfloppy16() throws FileNotFoundException, | |
620 | // IOException, | |
621 | // ParseFormatException { | |
622 | // assertFalse(solveInstance(PREFIX + | |
623 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-blast-floppy1-6.ucl.opb")); | |
624 | // } | |
625 | // | |
626 | // public void testblastfloppy17() throws FileNotFoundException, | |
627 | // IOException, | |
628 | // ParseFormatException { | |
629 | // assertFalse(solveInstance(PREFIX + | |
630 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-blast-floppy1-7.ucl.opb")); | |
631 | // } | |
632 | // | |
633 | // public void testblastfloppy18() throws FileNotFoundException, | |
634 | // IOException, | |
635 | // ParseFormatException { | |
636 | // assertFalse(solveInstance(PREFIX + | |
637 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-blast-floppy1-8.ucl.opb")); | |
638 | // } | |
639 | // | |
640 | // public void testmpsrd13rplusc21() throws FileNotFoundException, | |
641 | // IOException, | |
642 | // ParseFormatException { | |
643 | // assertTrue(solveInstance(PREFIX + | |
644 | // "normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-rd-rplusc-21.opb")); | |
645 | // } | |
646 | // | |
647 | // public void testmps13core2536() throws FileNotFoundException, | |
648 | // IOException, | |
649 | // ParseFormatException { | |
650 | // assertTrue(solveInstance(PREFIX + | |
651 | // "normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core2536-691.opb")); | |
652 | // } | |
653 | // | |
654 | // public void testmps13core4284() throws FileNotFoundException, | |
655 | // IOException, | |
656 | // ParseFormatException { | |
657 | // assertTrue(solveInstance(PREFIX + | |
658 | // "normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core4284-1064.opb")); | |
659 | // } | |
660 | // | |
661 | // public void testmps13core4872() throws FileNotFoundException, | |
662 | // IOException, | |
663 | // ParseFormatException { | |
664 | // assertTrue(solveInstance(PREFIX + | |
665 | // "normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core4872-1529.opb")); | |
666 | // } | |
667 | // | |
668 | // public void testmps13core2586() throws FileNotFoundException, | |
669 | // IOException, | |
670 | // ParseFormatException { | |
671 | // assertTrue(solveInstance(PREFIX + | |
672 | // "normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core2586-950.opb")); | |
673 | // } | |
674 | // | |
675 | // public void testtlan2() throws FileNotFoundException, IOException, | |
676 | // ParseFormatException { | |
677 | // assertFalse(solveInstance(PREFIX + | |
678 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-blast-tlan2.ucl.opb")); | |
679 | // } | |
680 | // | |
681 | // public void testtlan3() throws FileNotFoundException, IOException, | |
682 | // ParseFormatException { | |
683 | // assertFalse(solveInstance(PREFIX + | |
684 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-blast-tlan3.ucl.opb")); | |
685 | // } | |
686 | // | |
687 | // public void testibmqfull() throws FileNotFoundException, IOException, | |
688 | // ParseFormatException { | |
689 | // assertTrue(solveInstance(PREFIX + | |
690 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-cache-ibm-q-full.all.ucl.opb")); | |
691 | // } | |
692 | // | |
693 | // public void testibmqunboundedic22() throws FileNotFoundException, | |
694 | // IOException, | |
695 | // ParseFormatException { | |
696 | // assertTrue(solveInstance(PREFIX + | |
697 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb")); | |
698 | // } | |
699 | // | |
700 | // public void testibmqunboundedicl2() throws FileNotFoundException, | |
701 | // IOException, | |
702 | // ParseFormatException { | |
703 | // assertTrue(solveInstance(PREFIX + | |
704 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-cache-ibm-q-unbounded.Icl2arity.ucl.opb")); | |
705 | // } | |
706 | // | |
707 | // public void testunboundedIh1() throws FileNotFoundException, IOException, | |
708 | // ParseFormatException { | |
709 | // assertTrue(solveInstance(PREFIX + | |
710 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-cache-ibm-q-unbounded.Ih1arity.ucl.opb")); | |
711 | // } | |
712 | // | |
713 | // public void testunboundedIh2() throws FileNotFoundException, IOException, | |
714 | // ParseFormatException { | |
715 | // assertTrue(solveInstance(PREFIX + | |
716 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-cache-ibm-q-unbounded.Ih2arity.ucl.opb")); | |
717 | // } | |
718 | // | |
719 | // public void testcacheinv10() throws FileNotFoundException, IOException, | |
720 | // ParseFormatException { | |
721 | // assertTrue(solveInstance(PREFIX + | |
722 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-cache.inv10.ucl.opb")); | |
723 | // } | |
724 | // | |
725 | // public void testcacheinv12() throws FileNotFoundException, IOException, | |
726 | // ParseFormatException { | |
727 | // assertTrue(solveInstance(PREFIX + | |
728 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-cache.inv12.ucl.opb")); | |
729 | // } | |
730 | // | |
731 | // public void testcacheinv14() throws FileNotFoundException, IOException, | |
732 | // ParseFormatException { | |
733 | // assertTrue(solveInstance(PREFIX + | |
734 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-cache.inv14.ucl.opb")); | |
735 | // } | |
736 | // | |
737 | // public void testcacheinv8() throws FileNotFoundException, IOException, | |
738 | // ParseFormatException { | |
739 | // assertTrue(solveInstance(PREFIX + | |
740 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-cache.inv8.ucl.opb")); | |
741 | // } | |
742 | // | |
743 | // public void testdlx1crwmrm() throws FileNotFoundException, IOException, | |
744 | // ParseFormatException { | |
745 | // assertTrue(solveInstance(PREFIX + | |
746 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-dlx1c.rwmem.ucl.opb")); | |
747 | // } | |
748 | // | |
749 | // public void testdlx1crwmem1() throws FileNotFoundException, IOException, | |
750 | // ParseFormatException { | |
751 | // assertTrue(solveInstance(PREFIX + | |
752 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-dlx1c.rwmem1.ucl.opb")); | |
753 | // } | |
754 | // | |
755 | // public void testdlx1c() throws FileNotFoundException, IOException, | |
756 | // ParseFormatException { | |
757 | // assertTrue(solveInstance(PREFIX + | |
758 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-dlx1c.ucl.opb")); | |
759 | // } | |
760 | // | |
761 | // public void testelfrf10() throws FileNotFoundException, IOException, | |
762 | // ParseFormatException { | |
763 | // assertTrue(solveInstance(PREFIX + | |
764 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-elf.rf10.ucl.opb")); | |
765 | // } | |
766 | // | |
767 | // public void testelfrf6() throws FileNotFoundException, IOException, | |
768 | // ParseFormatException { | |
769 | // assertTrue(solveInstance(PREFIX + | |
770 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-elf.rf6.ucl.opb")); | |
771 | // } | |
772 | // | |
773 | // public void testelfrf7() throws FileNotFoundException, IOException, | |
774 | // ParseFormatException { | |
775 | // assertTrue(solveInstance(PREFIX + | |
776 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-elf.rf7.ucl.opb")); | |
777 | // } | |
778 | // | |
779 | // public void testelfrf8() throws FileNotFoundException, IOException, | |
780 | // ParseFormatException { | |
781 | // assertTrue(solveInstance(PREFIX + | |
782 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-elf.rf8.ucl.opb")); | |
783 | // } | |
784 | // | |
785 | // public void testelfrf9() throws FileNotFoundException, IOException, | |
786 | // ParseFormatException { | |
787 | // assertTrue(solveInstance(PREFIX + | |
788 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-elf.rf9.ucl.opb")); | |
789 | // } | |
790 | // | |
791 | // public void testburchdill2() throws FileNotFoundException, IOException, | |
792 | // ParseFormatException { | |
793 | // assertTrue(solveInstance(PREFIX + | |
794 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.burch_dill.2.accl.ucl.opb")); | |
795 | // } | |
796 | // | |
797 | // public void testburchdill3() throws FileNotFoundException, IOException, | |
798 | // ParseFormatException { | |
799 | // assertTrue(solveInstance(PREFIX + | |
800 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.burch_dill.3.accl.ucl.opb")); | |
801 | // } | |
802 | // | |
803 | // public void testburchdill4() throws FileNotFoundException, IOException, | |
804 | // ParseFormatException { | |
805 | // assertTrue(solveInstance(PREFIX + | |
806 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.burch_dill.4.accl.ucl.opb")); | |
807 | // } | |
808 | // | |
809 | // public void testburchdill6() throws FileNotFoundException, IOException, | |
810 | // ParseFormatException { | |
811 | // assertTrue(solveInstance(PREFIX + | |
812 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.burch_dill.6.accl.ucl.opb")); | |
813 | // } | |
814 | // | |
815 | // | |
816 | // public void testburchdill8() throws FileNotFoundException, IOException, | |
817 | // ParseFormatException { | |
818 | // assertTrue(solveInstance(PREFIX + | |
819 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.burch_dill.8.accl.ucl.opb")); | |
820 | // } | |
821 | // | |
822 | // | |
823 | // public void testrobregvalid() throws FileNotFoundException, IOException, | |
824 | // ParseFormatException { | |
825 | // assertTrue(solveInstance(PREFIX + | |
826 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb")); | |
827 | // } | |
828 | // | |
829 | // | |
830 | // public void testsrc1validBar() throws FileNotFoundException, IOException, | |
831 | // ParseFormatException { | |
832 | // assertTrue(solveInstance(PREFIX + | |
833 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.ex.br.mem.Src1Valid_Src1ValidBar.ucl.opb")); | |
834 | // } | |
835 | // | |
836 | // | |
837 | // public void testLdValue() throws FileNotFoundException, IOException, | |
838 | // ParseFormatException { | |
839 | // assertTrue(solveInstance(PREFIX + | |
840 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.ex.mem.LdValue.ucl.opb")); | |
841 | // } | |
842 | // | |
843 | // | |
844 | // public void testLsqHdStrong() throws FileNotFoundException, IOException, | |
845 | // ParseFormatException { | |
846 | // assertTrue(solveInstance(PREFIX + | |
847 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb")); | |
848 | // } | |
849 | // | |
850 | // | |
851 | // public void testrf10() throws FileNotFoundException, IOException, | |
852 | // ParseFormatException { | |
853 | // assertTrue(solveInstance(PREFIX + | |
854 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.rf10.ucl.opb")); | |
855 | // } | |
856 | // | |
857 | // | |
858 | // public void testrf6() throws FileNotFoundException, IOException, | |
859 | // ParseFormatException { | |
860 | // assertTrue(solveInstance(PREFIX + | |
861 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.rf6.ucl.opb")); | |
862 | // } | |
863 | // | |
864 | // | |
865 | // public void testrf7() throws FileNotFoundException, IOException, | |
866 | // ParseFormatException { | |
867 | // assertTrue(solveInstance(PREFIX + | |
868 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.rf7.ucl.opb")); | |
869 | // } | |
870 | // | |
871 | // | |
872 | // public void testrf8() throws FileNotFoundException, IOException, | |
873 | // ParseFormatException { | |
874 | // assertTrue(solveInstance(PREFIX + | |
875 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.rf8.ucl.opb")); | |
876 | // } | |
877 | // | |
878 | // | |
879 | // public void testrf9() throws FileNotFoundException, IOException, | |
880 | // ParseFormatException { | |
881 | // assertTrue(solveInstance(PREFIX + | |
882 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.rf9.ucl.opb")); | |
883 | // } | |
884 | // | |
885 | // | |
886 | // public void testtag10() throws FileNotFoundException, IOException, | |
887 | // ParseFormatException { | |
888 | // assertTrue(solveInstance(PREFIX + | |
889 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.tag10.ucl.opb")); | |
890 | // } | |
891 | // | |
892 | // | |
893 | // public void testtag12() throws FileNotFoundException, IOException, | |
894 | // ParseFormatException { | |
895 | // assertTrue(solveInstance(PREFIX + | |
896 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.tag12.ucl.opb")); | |
897 | // } | |
898 | // | |
899 | // | |
900 | // public void testtag14() throws FileNotFoundException, IOException, | |
901 | // ParseFormatException { | |
902 | // assertTrue(solveInstance(PREFIX + | |
903 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.tag14.ucl.opb")); | |
904 | // } | |
905 | // | |
906 | // | |
907 | // public void testtag8() throws FileNotFoundException, IOException, | |
908 | // ParseFormatException { | |
909 | // assertTrue(solveInstance(PREFIX + | |
910 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.tag8.ucl.opb")); | |
911 | // } | |
912 | // | |
913 | // | |
914 | // public void testunboundedallucl() throws FileNotFoundException, | |
915 | // IOException, | |
916 | // ParseFormatException { | |
917 | // assertTrue(solveInstance(PREFIX + | |
918 | // "normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.unbounded.all.ucl.opb")); | |
919 | // } | |
920 | 12 |
![]() |
921 | ParseFormatException { | |
922 | 12 | assertFalse(solveInstance(PREFIX |
923 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl10_11_pb.cnf.cr.opb")); | |
924 | } | |
925 | ||
926 | 12 |
![]() |
927 | ParseFormatException { | |
928 | 12 | assertFalse(solveInstance(PREFIX |
929 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl10_15_pb.cnf.cr.opb")); | |
930 | } | |
931 | ||
932 | 12 |
![]() |
933 | ParseFormatException { | |
934 | 12 | assertFalse(solveInstance(PREFIX |
935 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl10_20_pb.cnf.cr.opb")); | |
936 | } | |
937 | ||
938 | 12 |
![]() |
939 | ParseFormatException { | |
940 | 12 | assertFalse(solveInstance(PREFIX |
941 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl15_16_pb.cnf.cr.opb")); | |
942 | } | |
943 | ||
944 | 12 |
![]() |
945 | ParseFormatException { | |
946 | 12 | assertFalse(solveInstance(PREFIX |
947 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl15_20_pb.cnf.cr.opb")); | |
948 | } | |
949 | ||
950 | 12 |
![]() |
951 | ParseFormatException { | |
952 | 12 | assertFalse(solveInstance(PREFIX |
953 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl15_25_pb.cnf.cr.opb")); | |
954 | } | |
955 | ||
956 | 12 |
![]() |
957 | ParseFormatException { | |
958 | 12 | assertFalse(solveInstance(PREFIX |
959 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl20_21_pb.cnf.cr.opb")); | |
960 | } | |
961 | ||
962 | 12 |
![]() |
963 | ParseFormatException { | |
964 | 12 | assertFalse(solveInstance(PREFIX |
965 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl20_25_pb.cnf.cr.opb")); | |
966 | } | |
967 | ||
968 | 12 |
![]() |
969 | ParseFormatException { | |
970 | 12 | assertFalse(solveInstance(PREFIX |
971 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl20_30_pb.cnf.cr.opb")); | |
972 | } | |
973 | ||
974 | 12 |
![]() |
975 | ParseFormatException { | |
976 | 12 | assertFalse(solveInstance(PREFIX |
977 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl30_31_pb.cnf.cr.opb")); | |
978 | } | |
979 | ||
980 | 12 |
![]() |
981 | ParseFormatException { | |
982 | 12 | assertFalse(solveInstance(PREFIX |
983 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl30_35_pb.cnf.cr.opb")); | |
984 | } | |
985 | ||
986 | 12 |
![]() |
987 | ParseFormatException { | |
988 | 12 | assertFalse(solveInstance(PREFIX |
989 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl30_40_pb.cnf.cr.opb")); | |
990 | } | |
991 | ||
992 | 12 |
![]() |
993 | ParseFormatException { | |
994 | 12 | assertFalse(solveInstance(PREFIX |
995 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl35_36_pb.cnf.cr.opb")); | |
996 | } | |
997 | ||
998 | 12 |
![]() |
999 | ParseFormatException { | |
1000 | 12 | assertFalse(solveInstance(PREFIX |
1001 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl35_40_pb.cnf.cr.opb")); | |
1002 | } | |
1003 | ||
1004 | 12 |
![]() |
1005 | ParseFormatException { | |
1006 | 12 | assertFalse(solveInstance(PREFIX |
1007 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl35_45_pb.cnf.cr.opb")); | |
1008 | } | |
1009 | ||
1010 | 12 |
![]() |
1011 | ParseFormatException { | |
1012 | 12 | assertFalse(solveInstance(PREFIX |
1013 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl40_41_pb.cnf.cr.opb")); | |
1014 | } | |
1015 | ||
1016 | 12 |
![]() |
1017 | ParseFormatException { | |
1018 | 12 | assertFalse(solveInstance(PREFIX |
1019 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl40_45_pb.cnf.cr.opb")); | |
1020 | } | |
1021 | ||
1022 | 12 |
![]() |
1023 | ParseFormatException { | |
1024 | 12 | assertFalse(solveInstance(PREFIX |
1025 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl40_50_pb.cnf.cr.opb")); | |
1026 | } | |
1027 | ||
1028 | 12 |
![]() |
1029 | ParseFormatException { | |
1030 | 12 | assertFalse(solveInstance(PREFIX |
1031 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl50_51_pb.cnf.cr.opb")); | |
1032 | } | |
1033 | ||
1034 | 12 |
![]() |
1035 | ParseFormatException { | |
1036 | 12 | assertFalse(solveInstance(PREFIX |
1037 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl50_55_pb.cnf.cr.opb")); | |
1038 | } | |
1039 | ||
1040 | 12 |
![]() |
1041 | ParseFormatException { | |
1042 | 12 | assertFalse(solveInstance(PREFIX |
1043 | + "normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl50_60_pb.cnf.cr.opb")); | |
1044 | } | |
1045 | // public void testwalser972() throws FileNotFoundException, IOException, | |
1046 | // ParseFormatException { | |
1047 | // assertTrue(solveInstance(PREFIX + | |
1048 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-2.opb")); | |
1049 | // } | |
1050 | // | |
1051 | // public void testwalser973() throws FileNotFoundException, IOException, | |
1052 | // ParseFormatException { | |
1053 | // assertTrue(solveInstance(PREFIX + | |
1054 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-3.opb")); | |
1055 | // } | |
1056 | // | |
1057 | // public void testwalser974() throws FileNotFoundException, IOException, | |
1058 | // ParseFormatException { | |
1059 | // assertTrue(solveInstance(PREFIX + | |
1060 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-4.opb")); | |
1061 | // } | |
1062 | // | |
1063 | // public void testwalser975() throws FileNotFoundException, IOException, | |
1064 | // ParseFormatException { | |
1065 | // assertTrue(solveInstance(PREFIX + | |
1066 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-5.opb")); | |
1067 | // } | |
1068 | // | |
1069 | // public void testwalser976() throws FileNotFoundException, IOException, | |
1070 | // ParseFormatException { | |
1071 | // assertTrue(solveInstance(PREFIX + | |
1072 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-6.opb")); | |
1073 | // } | |
1074 | // | |
1075 | // public void testradar1010_095100() throws FileNotFoundException, | |
1076 | // IOException, | |
1077 | // ParseFormatException { | |
1078 | // assertTrue(solveInstance(PREFIX + | |
1079 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.95:100.opb")); | |
1080 | // } | |
1081 | // | |
1082 | // public void testradar1010_05100() throws FileNotFoundException, | |
1083 | // IOException, | |
1084 | // ParseFormatException { | |
1085 | // assertTrue(solveInstance(PREFIX + | |
1086 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.5:100.opb")); | |
1087 | // } | |
1088 | // | |
1089 | // public void testradar1010_09598() throws FileNotFoundException, | |
1090 | // IOException, | |
1091 | // ParseFormatException { | |
1092 | // assertTrue(solveInstance(PREFIX + | |
1093 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.95:98.opb")); | |
1094 | // } | |
1095 | // | |
1096 | // public void testradar1020_05100() throws FileNotFoundException, | |
1097 | // IOException, | |
1098 | // ParseFormatException { | |
1099 | // assertTrue(solveInstance(PREFIX + | |
1100 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.5:100.opb")); | |
1101 | // } | |
1102 | // | |
1103 | // public void testradar1020_095100() throws FileNotFoundException, | |
1104 | // IOException, | |
1105 | // ParseFormatException { | |
1106 | // assertTrue(solveInstance(PREFIX + | |
1107 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:100.opb")); | |
1108 | // } | |
1109 | // | |
1110 | // public void testradar1020_09598() throws FileNotFoundException, | |
1111 | // IOException, | |
1112 | // ParseFormatException { | |
1113 | // assertTrue(solveInstance(PREFIX + | |
1114 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:98.opb")); | |
1115 | // } | |
1116 | // | |
1117 | // public void testradar3030_05100() throws FileNotFoundException, | |
1118 | // IOException, | |
1119 | // ParseFormatException { | |
1120 | // assertTrue(solveInstance(PREFIX + | |
1121 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.5:100.opb")); | |
1122 | // } | |
1123 | // | |
1124 | // public void testradar3030_095100() throws FileNotFoundException, | |
1125 | // IOException, | |
1126 | // ParseFormatException { | |
1127 | // assertTrue(solveInstance(PREFIX + | |
1128 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.95:100.opb")); | |
1129 | // } | |
1130 | // | |
1131 | // public void testradar3030_09598() throws FileNotFoundException, | |
1132 | // IOException, | |
1133 | // ParseFormatException { | |
1134 | // assertTrue(solveInstance(PREFIX + | |
1135 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.95:98.opb")); | |
1136 | // } | |
1137 | // | |
1138 | // public void testradar3070_05100() throws FileNotFoundException, | |
1139 | // IOException, | |
1140 | // ParseFormatException { | |
1141 | // assertTrue(solveInstance(PREFIX + | |
1142 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:70:4.5:0.5:100.opb")); | |
1143 | // } | |
1144 | // | |
1145 | // public void testradar3070_095100() throws FileNotFoundException, | |
1146 | // IOException, | |
1147 | // ParseFormatException { | |
1148 | // assertTrue(solveInstance(PREFIX + | |
1149 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:70:4.5:0.95:100.opb")); | |
1150 | // } | |
1151 | // | |
1152 | // public void testradar3070_09598() throws FileNotFoundException, | |
1153 | // IOException, | |
1154 | // ParseFormatException { | |
1155 | // assertTrue(solveInstance(PREFIX + | |
1156 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:70:4.5:0.95:98.opb")); | |
1157 | // } | |
1158 | // | |
1159 | // public void testppp13_13_19() throws FileNotFoundException, IOException, | |
1160 | // ParseFormatException { | |
1161 | // assertTrue(solveInstance(PREFIX + | |
1162 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:1,3-13,19.opb")); | |
1163 | // } | |
1164 | // public void testppp1_11_19_21() throws FileNotFoundException, | |
1165 | // IOException, | |
1166 | // ParseFormatException { | |
1167 | // assertTrue(solveInstance(PREFIX + | |
1168 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:1-11,19,21.opb")); | |
1169 | // } | |
1170 | // public void testppp1_12_16() throws FileNotFoundException, IOException, | |
1171 | // ParseFormatException { | |
1172 | // assertTrue(solveInstance(PREFIX + | |
1173 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:1-12,16.opb")); | |
1174 | // } | |
1175 | // public void testppp1_13() throws FileNotFoundException, IOException, | |
1176 | // ParseFormatException { | |
1177 | // assertTrue(solveInstance(PREFIX + | |
1178 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:1-13.opb")); | |
1179 | // } | |
1180 | // public void testppp1_9_16_19() throws FileNotFoundException, IOException, | |
1181 | // ParseFormatException { | |
1182 | // assertTrue(solveInstance(PREFIX + | |
1183 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:1-9,16-19.opb")); | |
1184 | // } | |
1185 | // public void testppp3_13_25_26() throws FileNotFoundException, | |
1186 | // IOException, | |
1187 | // ParseFormatException { | |
1188 | // assertTrue(solveInstance(PREFIX + | |
1189 | // "normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:3-13,25,26.opb")); | |
1190 | // } | |
1191 | // | |
1192 | // | |
1193 | ||
1194 | } |
|