|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
LecteurDimacs | Line # 51 | 92 | 36 | 77,6% |
0.7755102
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
(101) | |||
Result | |||
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT12
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH49
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT13
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH50
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT14
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testHole6
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT15
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testHole7
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT8
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testHole8
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT9
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testHole9
![]() |
3 FAIL | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT10
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT11
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH41
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT4
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH42
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT5
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH43
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT6
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH44
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT7
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH45
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT16
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH46
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT1
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH47
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT2
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH48
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT3
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT5
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT4
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT7
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT6
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT1
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT3
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT2
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH23
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH24
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH21
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH22
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH19
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH20
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH17
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH18
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH15
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH16
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH13
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH14
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH11
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH12
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH9
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH10
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH40
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH39
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH38
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH37
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH36
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH35
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH34
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH33
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH32
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH31
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH30
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH29
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH28
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH27
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH26
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH25
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi12
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi13
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi14
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi15
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi8
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi9
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi10
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi11
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi4
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi5
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi6
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi7
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT8
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi1
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi2
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi3
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH6
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH5
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH8
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH7
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH2
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH1
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH4
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testJNH3
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi22
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi21
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi24
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi23
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi17
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi16
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi20
![]() |
1 PASS | |
0.76870745
|
org.sat4j.minisat.AbstractM2Test.testIi18
![]() |
1 PASS | |
1 | /* | |
2 | * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre | |
3 | * | |
4 | * Based on the original minisat specification from: | |
5 | * | |
6 | * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the | |
7 | * Sixth International Conference on Theory and Applications of Satisfiability | |
8 | * Testing, LNCS 2919, pp 502-518, 2003. | |
9 | * | |
10 | * This library is free software; you can redistribute it and/or modify it under | |
11 | * the terms of the GNU Lesser General Public License as published by the Free | |
12 | * Software Foundation; either version 2.1 of the License, or (at your option) | |
13 | * any later version. | |
14 | * | |
15 | * This library is distributed in the hope that it will be useful, but WITHOUT | |
16 | * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS | |
17 | * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more | |
18 | * details. | |
19 | * | |
20 | * You should have received a copy of the GNU Lesser General Public License | |
21 | * along with this library; if not, write to the Free Software Foundation, Inc., | |
22 | * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA | |
23 | * | |
24 | */ | |
25 | ||
26 | package org.sat4j.reader; | |
27 | ||
28 | import java.io.BufferedInputStream; | |
29 | import java.io.IOException; | |
30 | import java.io.InputStream; | |
31 | import java.io.PrintWriter; | |
32 | import java.io.Serializable; | |
33 | ||
34 | import org.sat4j.core.VecInt; | |
35 | import org.sat4j.specs.ContradictionException; | |
36 | import org.sat4j.specs.IProblem; | |
37 | import org.sat4j.specs.ISolver; | |
38 | import org.sat4j.specs.IVecInt; | |
39 | ||
40 | /** | |
41 | * Dimacs Reader written by Frederic Laihem. It is much faster than DimacsReader | |
42 | * because it does not split the input file into strings but reads and interpret | |
43 | * the input char by char. Hence, it is a bit more difficult to read and to | |
44 | * modify than DimacsReader. | |
45 | * | |
46 | * This reader is used during the SAT Competitions. | |
47 | * | |
48 | * @author laihem | |
49 | * @author leberre | |
50 | */ | |
51 | public class LecteurDimacs extends Reader implements Serializable { | |
52 | ||
53 | private static final long serialVersionUID = 1L; | |
54 | ||
55 | /* taille du buffer */ | |
56 | private final static int TAILLE_BUF = 16384; | |
57 | ||
58 | private final ISolver s; | |
59 | ||
60 | private transient BufferedInputStream in; | |
61 | ||
62 | /* nombre de literaux dans le fichier */ | |
63 | private int nbLit = 0; | |
64 | ||
65 | private int nbClauses = 0; | |
66 | ||
67 | private static final char EOF = (char) -1; | |
68 | ||
69 | /* | |
70 | * nomFichier repr?sente le nom du fichier ? lire | |
71 | */ | |
72 | 1673 |
![]() |
73 | 1673 | this.s = s; |
74 | } | |
75 | ||
76 | 1673 |
![]() |
77 | public final IProblem parseInstance(final InputStream in) | |
78 | throws ParseFormatException, ContradictionException, IOException { | |
79 | ||
80 | 1673 | this.in = new BufferedInputStream(in, LecteurDimacs.TAILLE_BUF); |
81 | 1673 | s.reset(); |
82 | 1673 | passerCommentaire(); |
83 | 1673 | if (nbLit == 0) |
84 | 0 | throw new IOException( |
85 | "DIMACS non valide (nombre de Literaux non valide)"); | |
86 | 1673 | s.newVar(nbLit); |
87 | 1673 | s.setExpectedNumberOfClauses(nbClauses); |
88 | 1673 | char car = passerEspaces(); |
89 | 1673 | if (car == EOF) |
90 | 0 | throw new IOException("DIMACS non valide (ou sont les clauses ?)"); |
91 | 1673 | ajouterClauses(car); |
92 | 1673 | in.close(); |
93 | 1673 | return s; |
94 | } | |
95 | ||
96 | 0 |
![]() |
97 | public IProblem parseInstance(java.io.Reader in) throws IOException, | |
98 | ContradictionException { | |
99 | 0 | throw new UnsupportedOperationException(); |
100 | } | |
101 | ||
102 | /** on passe les commentaires et on lit le nombre de literaux */ | |
103 | 1673 |
![]() |
104 | 1673 | char car; |
105 | 1673 | for (;;) { |
106 | 22757 | car = passerEspaces(); |
107 | 22757 | if (car == 'p') { |
108 | 1673 | car = lectureNombreLiteraux(); |
109 | } | |
110 | 22757 | if (car != 'c' && car != 'p') |
111 | 1673 | break; /* fin des commentaires */ |
112 | 21084 | car = nextLine(); /* on passe la ligne de commentaire */ |
113 | 21084 | if (car == EOF) |
114 | 0 | break; |
115 | } | |
116 | 1673 | return car; |
117 | } | |
118 | ||
119 | /** lit le nombre repr?sentant le nombre de literaux */ | |
120 | 1673 |
![]() |
121 | 1673 | char car = nextChiffre(); /* on lit le prchain chiffre */ |
122 | 1673 | if (car != EOF) { |
123 | 1673 | nbLit = car - '0'; |
124 | 1673 | for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */ |
125 | 4610 | car = (char) in.read(); |
126 | 4610 | if (car < '0' || car > '9') |
127 | 1673 | break; |
128 | 2937 | nbLit = 10 * nbLit + (car - '0'); |
129 | } | |
130 | 1673 | car = nextChiffre(); |
131 | 1673 | nbClauses = car - '0'; |
132 | 1673 | for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */ |
133 | 5355 | car = (char) in.read(); |
134 | 5355 | if (car < '0' || car > '9') |
135 | 1673 | break; |
136 | 3682 | nbClauses = 10 * nbClauses + (car - '0'); |
137 | } | |
138 | 1673 | if (car != '\n' && car != EOF) |
139 | 0 | nextLine(); /* on lit la fin de la ligne */ |
140 | } | |
141 | 1673 | return car; |
142 | } | |
143 | ||
144 | /** lit les clauses et les ajoute dans le vecteur donn? en param?tre | |
145 | * @throws ParseFormatException */ | |
146 | 1673 |
![]() |
147 | ContradictionException, ParseFormatException { | |
148 | 1673 | final IVecInt lit = new VecInt(); |
149 | 1673 | int val = 0; |
150 | 1673 | boolean neg = false; |
151 | 1673 | for (;;) { |
152 | /* on lit le signe du literal */ | |
153 | 16341595 | if (car == '-') { |
154 | 7229578 | neg = true; |
155 | 7229578 | car = (char) in.read(); |
156 | 9112017 | } else if (car == '+') |
157 | 0 | car = (char) in.read(); |
158 | else /* on le 1er chiffre du literal */ | |
159 | 9112017 | if (car >= '0' && car <= '9') { |
160 | 9112017 | val = car - '0'; |
161 | 9112017 | car = (char) in.read(); |
162 | } else | |
163 | 0 | throw new ParseFormatException("Unknown character "+car); |
164 | /* on lit la suite du literal */ | |
165 | 41747295 | while (car >= '0' && car <= '9') { |
166 | 25405700 | val = (val * 10) + car - '0'; |
167 | 25405700 | car = (char) in.read(); |
168 | } | |
169 | 16341595 | if (val == 0) { // on a lu toute la clause |
170 | 4011911 | s.addClause(lit); |
171 | 4011911 | lit.clear(); |
172 | } else { | |
173 | /* on ajoute le literal au vecteur */ | |
174 | // s.newVar(val-1); | |
175 | 12329684 | lit.push(neg ? -val : val); |
176 | 12329684 | neg = false; |
177 | 12329684 | val = 0; /* on reinitialise les variables */ |
178 | } | |
179 | 16341595 | if (car != EOF) |
180 | 16341211 | car = passerEspaces(); |
181 | 16341595 | if (car == EOF) |
182 | 1673 | break; /* on a lu tout le fichier */ |
183 | } | |
184 | } | |
185 | ||
186 | /** passe tout les caract?res d'espacement (espace ou \n) */ | |
187 | 16365641 |
![]() |
188 | 16365641 | char car; |
189 | ||
190 | 0 | while ((car = (char) in.read()) == ' ' || car == '\n') |
191 | 16239200 | ; |
192 | 16365641 | return car; |
193 | } | |
194 | ||
195 | /** passe tout les caract?res jusqu? rencontrer une fin de la ligne */ | |
196 | 21084 |
![]() |
197 | 21084 | char car; |
198 | 21084 | do { |
199 | 558511 | car = (char) in.read(); |
200 | 558511 | } while ((car != '\n') && (car != EOF)); |
201 | 21084 | return car; |
202 | } | |
203 | ||
204 | /** passe tout les caract?re jusqu'? rencontrer un chiffre */ | |
205 | 3346 |
![]() |
206 | 3346 | char car; |
207 | 3346 | do { |
208 | 11711 | car = (char) in.read(); |
209 | 11711 | } while ((car < '0') || (car > '9') && (car != EOF)); |
210 | 3346 | return car; |
211 | } | |
212 | ||
213 | 0 |
![]() |
214 | public String decode(int[] model) { | |
215 | 0 | StringBuffer stb = new StringBuffer(); |
216 | 0 | for (int i = 0; i < model.length; i++) { |
217 | 0 | stb.append(model[i]); |
218 | 0 | stb.append(" "); |
219 | } | |
220 | 0 | stb.append("0"); |
221 | 0 | return stb.toString(); |
222 | } | |
223 | ||
224 | 0 |
![]() |
225 | public void decode(int[] model, PrintWriter out) { | |
226 | 0 | for (int i = 0; i < model.length; i++) { |
227 | 0 | out.print(model[i]); |
228 | 0 | out.print(" "); |
229 | } | |
230 | 0 | out.print("0"); |
231 | } | |
232 | } |
|