Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
82   288   26   6,83
38   168   0,45   12
12     3,08  
1    
 
  DimacsReader       Line # 63 82 26 0% 0.0
 
No Tests
 
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.IOException;
29    import java.io.LineNumberReader;
30    import java.io.PrintWriter;
31    import java.io.Serializable;
32    import java.util.Scanner;
33    import java.util.StringTokenizer;
34   
35    import org.sat4j.core.VecInt;
36    import org.sat4j.opt.WeightedMaxSatDecorator;
37    import org.sat4j.specs.ContradictionException;
38    import org.sat4j.specs.IProblem;
39    import org.sat4j.specs.ISolver;
40    import org.sat4j.specs.IVecInt;
41   
42    /**
43    * Very simple Dimacs file parser. Allow solvers to read the constraints from a
44    * Dimacs formatted file. It should be used that way:
45    *
46    * <pre>
47    * DimacsReader solver = new DimacsReader(SolverFactory.OneSolver());
48    * solver.readInstance(&quot;mybench.cnf&quot;);
49    * if (solver.isSatisfiable()) {
50    * // SAT case
51    * } else {
52    * // UNSAT case
53    * }
54    * </pre>
55    *
56    * That parser is not used for efficiency reasons. It will be updated with Java
57    * 1.5 scanner feature.
58    *
59    * @version 1.0
60    * @author dlb
61    * @author or
62    */
 
63    public class DimacsReader extends Reader implements Serializable {
64   
65    private static final long serialVersionUID = 1L;
66   
67    protected int expectedNbOfConstr; // as announced on the p cnf line
68   
69    protected final ISolver solver;
70   
71    private boolean checkConstrNb = true;
72   
73    private final String formatString;
74   
 
75  0 toggle public DimacsReader(ISolver solver) {
76  0 this(solver, "cnf");
77    }
78   
 
79  0 toggle public DimacsReader(ISolver solver, String format) {
80  0 this.solver = solver;
81  0 formatString = format;
82    }
83   
 
84  0 toggle public void disableNumberOfConstraintCheck() {
85  0 checkConstrNb = false;
86    }
87   
88    /**
89    * Skip comments at the beginning of the input stream.
90    *
91    * @param in
92    * the input stream
93    * @throws IOException
94    * if an IO problem occurs.
95    */
 
96  0 toggle protected void skipComments(final LineNumberReader in) throws IOException {
97  0 int c;
98   
99  0 do {
100  0 in.mark(4);
101  0 c = in.read();
102  0 if (c == 'c') {
103  0 in.readLine();
104    } else {
105  0 in.reset();
106    }
107  0 } while (c == 'c');
108    }
109   
110    /**
111    * @param in
112    * the input stream
113    * @throws IOException
114    * iff an IO occurs
115    * @throws ParseFormatException
116    * if the input stream does not comply with the DIMACS format.
117    */
 
118  0 toggle protected void readProblemLine(LineNumberReader in) throws IOException,
119    ParseFormatException {
120   
121  0 String line = in.readLine();
122   
123  0 if (line == null) {
124  0 throw new ParseFormatException(
125    "premature end of file: <p cnf ...> expected on line "
126    + in.getLineNumber());
127    }
128  0 StringTokenizer stk = new StringTokenizer(line);
129   
130  0 if (!(stk.hasMoreTokens() && stk.nextToken().equals("p")
131    && stk.hasMoreTokens() && stk.nextToken().equals(formatString))) {
132  0 throw new ParseFormatException(
133    "problem line expected (p cnf ...) on line "
134    + in.getLineNumber());
135    }
136   
137  0 int vars;
138   
139    // reads the max var id
140  0 vars = Integer.parseInt(stk.nextToken());
141  0 assert vars > 0;
142  0 solver.newVar(vars);
143    // reads the number of clauses
144  0 expectedNbOfConstr = Integer.parseInt(stk.nextToken());
145  0 assert expectedNbOfConstr > 0;
146  0 solver.setExpectedNumberOfClauses(expectedNbOfConstr);
147  0 if ("wcnf".equals(formatString)) {
148    // assume we are in weighted MAXSAT mode
149  0 int top;
150  0 if (stk.hasMoreTokens()) {
151  0 top = Integer.parseInt(stk.nextToken());
152    } else {
153  0 top = Integer.MAX_VALUE;
154    }
155  0 ((WeightedMaxSatDecorator)solver).setTopWeight(top);
156    }
157    }
158   
159    /**
160    * @param in
161    * the input stream
162    * @throws IOException
163    * iff an IO problems occurs
164    * @throws ParseFormatException
165    * if the input stream does not comply with the DIMACS format.
166    * @throws ContradictionException
167    * si le probl?me est trivialement inconsistant.
168    */
 
169  0 toggle protected void readConstrs(LineNumberReader in) throws IOException,
170    ParseFormatException, ContradictionException {
171  0 String line;
172   
173  0 int realNbOfConstr = 0;
174   
175  0 IVecInt literals = new VecInt();
176   
177  0 while (true) {
178  0 line = in.readLine();
179   
180  0 if (line == null) {
181    // end of file
182  0 if (literals.size() > 0) {
183    // no 0 end the last clause
184  0 solver.addClause(literals);
185  0 realNbOfConstr++;
186    }
187   
188  0 break;
189    }
190   
191  0 if (line.startsWith("c ")) {
192    // ignore comment line
193  0 System.out.println("Found commmented line : " + line);
194  0 continue;
195    }
196  0 if (line.startsWith("%") && expectedNbOfConstr == realNbOfConstr) {
197  0 System.out
198    .println("Ignoring the rest of the file (SATLIB format");
199  0 break;
200    }
201  0 boolean added = handleConstr(line, literals);
202  0 if (added) {
203  0 realNbOfConstr++;
204    }
205    }
206  0 if (checkConstrNb && expectedNbOfConstr != realNbOfConstr) {
207  0 throw new ParseFormatException("wrong nbclauses parameter. Found "
208    + realNbOfConstr + ", " + expectedNbOfConstr + " expected");
209    }
210    }
211   
 
212  0 toggle protected boolean handleConstr(String line, IVecInt literals)
213    throws ContradictionException {
214  0 int lit;
215  0 boolean added = false;
216  0 Scanner scan;
217  0 scan = new Scanner(line);
218  0 while (scan.hasNext()) {
219  0 lit = scan.nextInt();
220   
221  0 if (lit == 0) {
222  0 if (literals.size() > 0) {
223  0 solver.addClause(literals);
224  0 literals.clear();
225  0 added = true;
226    }
227    } else {
228  0 literals.push(lit);
229    }
230    }
231  0 return added;
232    }
233   
 
234  0 toggle @Override
235    public final IProblem parseInstance(final java.io.Reader in)
236    throws ParseFormatException, ContradictionException, IOException {
237  0 return parseInstance(new LineNumberReader(in));
238   
239    }
240   
241    /**
242    * @param in
243    * the input stream
244    * @throws ParseFormatException
245    * if the input stream does not comply with the DIMACS format.
246    * @throws ContradictionException
247    * si le probl?me est trivialement inconsitant
248    */
 
249  0 toggle private IProblem parseInstance(LineNumberReader in)
250    throws ParseFormatException, ContradictionException {
251  0 solver.reset();
252  0 try {
253  0 skipComments(in);
254  0 readProblemLine(in);
255  0 readConstrs(in);
256  0 return solver;
257    } catch (IOException e) {
258  0 throw new ParseFormatException(e);
259    } catch (NumberFormatException e) {
260  0 throw new ParseFormatException("integer value expected on line "
261    + in.getLineNumber(), e);
262    }
263    }
264   
 
265  0 toggle @Override
266    public String decode(int[] model) {
267  0 StringBuffer stb = new StringBuffer();
268  0 for (int i = 0; i < model.length; i++) {
269  0 stb.append(model[i]);
270  0 stb.append(" ");
271    }
272  0 stb.append("0");
273  0 return stb.toString();
274    }
275   
 
276  0 toggle @Override
277    public void decode(int[] model, PrintWriter out) {
278  0 for (int i = 0; i < model.length; i++) {
279  0 out.print(model[i]);
280  0 out.print(" ");
281    }
282  0 out.print("0");
283    }
284   
 
285  0 toggle protected ISolver getSolver() {
286  0 return solver;
287    }
288    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.