1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
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
42
43
44
45
46
47
48
49
50
51 public class LecteurDimacs extends Reader implements Serializable {
52
53 private static final long serialVersionUID = 1L;
54
55
56 private final static int TAILLE_BUF = 16384;
57
58 private final ISolver s;
59
60 private transient BufferedInputStream in;
61
62
63 private int nbLit = 0;
64
65 private int nbClauses = 0;
66
67 private static final char EOF = (char) -1;
68
69
70
71
72 public LecteurDimacs(ISolver s) {
73 this.s = s;
74 }
75
76 @Override
77 public final IProblem parseInstance(final InputStream in)
78 throws ParseFormatException, ContradictionException, IOException {
79
80 this.in = new BufferedInputStream(in, LecteurDimacs.TAILLE_BUF);
81 s.reset();
82 passerCommentaire();
83 if (nbLit == 0)
84 throw new IOException(
85 "DIMACS non valide (nombre de Literaux non valide)");
86 s.newVar(nbLit);
87 s.setExpectedNumberOfClauses(nbClauses);
88 char car = passerEspaces();
89 if (car == EOF)
90 throw new IOException("DIMACS non valide (ou sont les clauses ?)");
91 ajouterClauses(car);
92 in.close();
93 return s;
94 }
95
96 @Override
97 public IProblem parseInstance(java.io.Reader in) throws IOException,
98 ContradictionException {
99 throw new UnsupportedOperationException();
100 }
101
102
103 private char passerCommentaire() throws IOException {
104 char car;
105 for (;;) {
106 car = passerEspaces();
107 if (car == 'p') {
108 car = lectureNombreLiteraux();
109 }
110 if (car != 'c' && car != 'p')
111 break;
112 car = nextLine();
113 if (car == EOF)
114 break;
115 }
116 return car;
117 }
118
119
120 private char lectureNombreLiteraux() throws IOException {
121 char car = nextChiffre();
122 if (car != EOF) {
123 nbLit = car - '0';
124 for (;;) {
125 car = (char) in.read();
126 if (car < '0' || car > '9')
127 break;
128 nbLit = 10 * nbLit + (car - '0');
129 }
130 car = nextChiffre();
131 nbClauses = car - '0';
132 for (;;) {
133 car = (char) in.read();
134 if (car < '0' || car > '9')
135 break;
136 nbClauses = 10 * nbClauses + (car - '0');
137 }
138 if (car != '\n' && car != EOF)
139 nextLine();
140 }
141 return car;
142 }
143
144
145
146 private void ajouterClauses(char car) throws IOException,
147 ContradictionException, ParseFormatException {
148 final IVecInt lit = new VecInt();
149 int val = 0;
150 boolean neg = false;
151 for (;;) {
152
153 if (car == '-') {
154 neg = true;
155 car = (char) in.read();
156 } else if (car == '+')
157 car = (char) in.read();
158 else
159 if (car >= '0' && car <= '9') {
160 val = car - '0';
161 car = (char) in.read();
162 } else
163 throw new ParseFormatException("Unknown character "+car);
164
165 while (car >= '0' && car <= '9') {
166 val = (val * 10) + car - '0';
167 car = (char) in.read();
168 }
169 if (val == 0) {
170 s.addClause(lit);
171 lit.clear();
172 } else {
173
174
175 lit.push(neg ? -val : val);
176 neg = false;
177 val = 0;
178 }
179 if (car != EOF)
180 car = passerEspaces();
181 if (car == EOF)
182 break;
183 }
184 }
185
186
187 private char passerEspaces() throws IOException {
188 char car;
189
190 while ((car = (char) in.read()) == ' ' || car == '\n')
191 ;
192 return car;
193 }
194
195
196 private char nextLine() throws IOException {
197 char car;
198 do {
199 car = (char) in.read();
200 } while ((car != '\n') && (car != EOF));
201 return car;
202 }
203
204
205 private char nextChiffre() throws IOException {
206 char car;
207 do {
208 car = (char) in.read();
209 } while ((car < '0') || (car > '9') && (car != EOF));
210 return car;
211 }
212
213 @Override
214 public String decode(int[] model) {
215 StringBuffer stb = new StringBuffer();
216 for (int i = 0; i < model.length; i++) {
217 stb.append(model[i]);
218 stb.append(" ");
219 }
220 stb.append("0");
221 return stb.toString();
222 }
223
224 @Override
225 public void decode(int[] model, PrintWriter out) {
226 for (int i = 0; i < model.length; i++) {
227 out.print(model[i]);
228 out.print(" ");
229 }
230 out.print("0");
231 }
232 }