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