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
27
28 package org.sat4j.reader;
29
30 import java.io.IOException;
31 import java.io.LineNumberReader;
32 import java.io.PrintWriter;
33 import java.io.Serializable;
34 import java.util.Scanner;
35 import java.util.StringTokenizer;
36
37 import org.sat4j.core.VecInt;
38 import org.sat4j.specs.ContradictionException;
39 import org.sat4j.specs.IProblem;
40 import org.sat4j.specs.ISolver;
41 import org.sat4j.specs.IVecInt;
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64 public class DimacsReader extends Reader implements Serializable {
65
66 private static final long serialVersionUID = 1L;
67
68 protected int expectedNbOfConstr;
69
70 protected final ISolver solver;
71
72 private boolean checkConstrNb = true;
73
74 protected final String formatString;
75
76 public DimacsReader(ISolver solver) {
77 this(solver, "cnf");
78 }
79
80 public DimacsReader(ISolver solver, String format) {
81 this.solver = solver;
82 formatString = format;
83 }
84
85 public void disableNumberOfConstraintCheck() {
86 checkConstrNb = false;
87 }
88
89
90
91
92
93
94
95
96
97 protected void skipComments(final LineNumberReader in) throws IOException {
98 int c;
99
100 do {
101 in.mark(4);
102 c = in.read();
103 if (c == 'c') {
104 in.readLine();
105 } else {
106 in.reset();
107 }
108 } while (c == 'c');
109 }
110
111
112
113
114
115
116
117
118
119 protected void readProblemLine(LineNumberReader in) throws IOException,
120 ParseFormatException {
121
122 String line = in.readLine();
123
124 if (line == null) {
125 throw new ParseFormatException(
126 "premature end of file: <p cnf ...> expected on line "
127 + in.getLineNumber());
128 }
129 StringTokenizer stk = new StringTokenizer(line);
130
131 if (!(stk.hasMoreTokens() && stk.nextToken().equals("p")
132 && stk.hasMoreTokens() && stk.nextToken().equals(formatString))) {
133 throw new ParseFormatException(
134 "problem line expected (p cnf ...) on line "
135 + in.getLineNumber());
136 }
137
138 int vars;
139
140
141 vars = Integer.parseInt(stk.nextToken());
142 assert vars > 0;
143 solver.newVar(vars);
144
145 expectedNbOfConstr = Integer.parseInt(stk.nextToken());
146 assert expectedNbOfConstr > 0;
147 solver.setExpectedNumberOfClauses(expectedNbOfConstr);
148 }
149
150
151
152
153
154
155
156
157
158
159
160 protected void readConstrs(LineNumberReader in) throws IOException,
161 ParseFormatException, ContradictionException {
162 String line;
163
164 int realNbOfConstr = 0;
165
166 IVecInt literals = new VecInt();
167
168 while (true) {
169 line = in.readLine();
170
171 if (line == null) {
172
173 if (literals.size() > 0) {
174
175 solver.addClause(literals);
176 realNbOfConstr++;
177 }
178
179 break;
180 }
181
182 if (line.startsWith("c ")) {
183
184 continue;
185 }
186 if (line.startsWith("%") && expectedNbOfConstr == realNbOfConstr) {
187 System.out
188 .println("Ignoring the rest of the file (SATLIB format");
189 break;
190 }
191 boolean added = handleConstr(line, literals);
192 if (added) {
193 realNbOfConstr++;
194 }
195 }
196 if (checkConstrNb && expectedNbOfConstr != realNbOfConstr) {
197 throw new ParseFormatException("wrong nbclauses parameter. Found "
198 + realNbOfConstr + ", " + expectedNbOfConstr + " expected");
199 }
200 }
201
202 protected boolean handleConstr(String line, IVecInt literals)
203 throws ContradictionException {
204 int lit;
205 boolean added = false;
206 Scanner scan;
207 scan = new Scanner(line);
208 while (scan.hasNext()) {
209 lit = scan.nextInt();
210
211 if (lit == 0) {
212 if (literals.size() > 0) {
213 solver.addClause(literals);
214 literals.clear();
215 added = true;
216 }
217 } else {
218 literals.push(lit);
219 }
220 }
221 return added;
222 }
223
224 @Override
225 public final IProblem parseInstance(final java.io.Reader in)
226 throws ParseFormatException, ContradictionException, IOException {
227 return parseInstance(new LineNumberReader(in));
228
229 }
230
231
232
233
234
235
236
237
238
239 private IProblem parseInstance(LineNumberReader in)
240 throws ParseFormatException, ContradictionException {
241 solver.reset();
242 try {
243 skipComments(in);
244 readProblemLine(in);
245 readConstrs(in);
246 return solver;
247 } catch (IOException e) {
248 throw new ParseFormatException(e);
249 } catch (NumberFormatException e) {
250 throw new ParseFormatException("integer value expected on line "
251 + in.getLineNumber(), e);
252 }
253 }
254
255 @Override
256 public String decode(int[] model) {
257 StringBuffer stb = new StringBuffer();
258 for (int i = 0; i < model.length; i++) {
259 stb.append(model[i]);
260 stb.append(" ");
261 }
262 stb.append("0");
263 return stb.toString();
264 }
265
266 @Override
267 public void decode(int[] model, PrintWriter out) {
268 for (int i = 0; i < model.length; i++) {
269 out.print(model[i]);
270 out.print(" ");
271 }
272 out.print("0");
273 }
274
275 protected ISolver getSolver() {
276 return solver;
277 }
278 }