Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 290   Methods: 10
NCLOC: 157   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
DimacsReader.java 0% 1,4% 10% 1,8%
coverage coverage
 1    /*
 2    * SAT4J: a SATisfiability library for Java
 3    * Copyright (C) 2004 Daniel Le Berre
 4    *
 5    * Based on the original minisat specification from:
 6    *
 7    * An extensible SAT solver. Niklas E?n and Niklas S?rensson.
 8    * Proceedings of the Sixth International Conference on Theory
 9    * and Applications of Satisfiability Testing, LNCS 2919,
 10    * pp 502-518, 2003.
 11    *
 12    * This library is free software; you can redistribute it and/or
 13    * modify it under the terms of the GNU Lesser General Public
 14    * License as published by the Free Software Foundation; either
 15    * version 2.1 of the License, or (at your option) any later version.
 16    *
 17    * This library is distributed in the hope that it will be useful,
 18    * but WITHOUT ANY WARRANTY; without even the implied warranty of
 19    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
 20    * Lesser General Public License for more details.
 21    *
 22    * You should have received a copy of the GNU Lesser General Public
 23    * License along with this library; if not, write to the Free Software
 24    * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 25    *
 26    */
 27   
 28    package org.sat4j.reader;
 29   
 30    import java.io.FileInputStream;
 31    import java.io.FileNotFoundException;
 32    import java.io.FileReader;
 33    import java.io.IOException;
 34    import java.io.InputStreamReader;
 35    import java.io.LineNumberReader;
 36    import java.io.Serializable;
 37    import java.util.Scanner;
 38    import java.util.StringTokenizer;
 39    import java.util.zip.GZIPInputStream;
 40   
 41    import org.sat4j.core.VecInt;
 42    import org.sat4j.specs.ContradictionException;
 43    import org.sat4j.specs.IProblem;
 44    import org.sat4j.specs.ISolver;
 45    import org.sat4j.specs.IVecInt;
 46   
 47    /**
 48    * Very simple Dimacs file parser. Allow solvers to read the constraints from a
 49    * Dimacs formatted file. It should be used that way:
 50    *
 51    * <pre>
 52    * DimacsReader solver = new DimacsReader(SolverFactory.OneSolver());
 53    * solver.readInstance(&quot;mybench.cnf&quot;);
 54    * if (solver.isSatisfiable()) {
 55    * // SAT case
 56    * } else {
 57    * // UNSAT case
 58    * }
 59    * </pre>
 60    *
 61    * That parser is not used for efficiency reasons. It will be updated with Java
 62    * 1.5 scanner feature.
 63    *
 64    * @version 1.0
 65    * @author dlb
 66    * @author or
 67    */
 68    public class DimacsReader implements Reader, Serializable {
 69   
 70    private static final long serialVersionUID = 1L;
 71   
 72    protected int expectedNbOfConstr; // as announced on the p cnf line
 73   
 74    protected final ISolver solver;
 75   
 76    private boolean checkConstrNb = true;
 77   
 78  2026 public DimacsReader(ISolver solver) {
 79  2026 this.solver = solver;
 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
 90    * the input stream
 91    * @throws IOException
 92    * if an IO problem occurs.
 93    */
 94  0 protected void skipComments(final LineNumberReader in) throws IOException {
 95  0 int c;
 96   
 97  0 do {
 98  0 in.mark(4);
 99  0 c = in.read();
 100  0 if (c == 'c') {
 101  0 in.readLine();
 102    } else {
 103  0 in.reset();
 104    }
 105  0 } while (c == 'c');
 106    }
 107   
 108    /**
 109    * @param in
 110    * the input stream
 111    * @throws IOException
 112    * iff an IO occurs
 113    * @throws ParseFormatException
 114    * if the input stream does not comply with the DIMACS format.
 115    */
 116  0 protected void readProblemLine(LineNumberReader in) throws IOException,
 117    ParseFormatException {
 118   
 119  0 String line = in.readLine();
 120   
 121  0 if (line == null) {
 122  0 throw new ParseFormatException(
 123    "premature end of file: <p cnf ...> expected on line "
 124    + in.getLineNumber());
 125    }
 126  0 StringTokenizer stk = new StringTokenizer(line);
 127   
 128  0 if (!(stk.hasMoreTokens() && stk.nextToken().equals("p")
 129    && stk.hasMoreTokens() && stk.nextToken().equals("cnf"))) {
 130  0 throw new ParseFormatException(
 131    "problem line expected (p cnf ...) on line "
 132    + in.getLineNumber());
 133    }
 134   
 135  0 int vars;
 136   
 137    // reads the max var id
 138  0 vars = Integer.parseInt(stk.nextToken());
 139    assert vars > 0;
 140  0 solver.newVar(vars);
 141    // reads the number of clauses
 142  0 expectedNbOfConstr = Integer.parseInt(stk.nextToken());
 143    assert expectedNbOfConstr > 0;
 144   
 145    }
 146   
 147    /**
 148    * @param in
 149    * the input stream
 150    * @throws IOException
 151    * iff an IO problems occurs
 152    * @throws ParseFormatException
 153    * if the input stream does not comply with the DIMACS format.
 154    * @throws ContradictionException
 155    * si le probl?me est trivialement inconsistant.
 156    */
 157  0 protected void readConstrs(LineNumberReader in) throws IOException,
 158    ParseFormatException, ContradictionException {
 159  0 int lit;
 160  0 String line;
 161  0 Scanner scan;
 162   
 163  0 int realNbOfConstr = 0;
 164   
 165  0 IVecInt literals = new VecInt();
 166   
 167  0 while (true) {
 168  0 line = in.readLine();
 169   
 170  0 if (line == null) {
 171    // end of file
 172  0 if (literals.size() > 0) {
 173    // no 0 end the last clause
 174  0 solver.addClause(literals);
 175  0 realNbOfConstr++;
 176    }
 177   
 178  0 break;
 179    }
 180   
 181  0 if (line.startsWith("c ")) {
 182    // ignore comment line
 183  0 System.out.println("Found commmented line : " + line);
 184  0 continue;
 185    }
 186  0 if (line.startsWith("%") && expectedNbOfConstr == realNbOfConstr) {
 187  0 System.out
 188    .println("Ignoring the rest of the file (SATLIB format");
 189  0 break;
 190    }
 191  0 boolean added = handleConstr(line, literals);
 192  0 if (added) {
 193  0 realNbOfConstr++;
 194    }
 195    }
 196  0 if (checkConstrNb && expectedNbOfConstr != realNbOfConstr) {
 197  0 throw new ParseFormatException("wrong nbclauses parameter. Found "
 198    + realNbOfConstr + ", " + expectedNbOfConstr + " expected");
 199    }
 200    }
 201   
 202  0 protected boolean handleConstr(String line, IVecInt literals)
 203    throws ContradictionException {
 204  0 int lit;
 205  0 boolean added = false;
 206  0 Scanner scan;
 207  0 scan = new Scanner(line);
 208  0 while (scan.hasNext()) {
 209  0 lit = scan.nextInt();
 210   
 211  0 if (lit != 0) {
 212  0 literals.push(lit);
 213    } else {
 214  0 if (literals.size() > 0) {
 215  0 solver.addClause(literals);
 216  0 literals.clear();
 217  0 added = true;
 218    }
 219    }
 220    }
 221  0 return added;
 222    }
 223   
 224    /**
 225    * Remplit un prouveur ? partir d'un fichier Dimacs.
 226    *
 227    * @param filename
 228    * le nom du fichier Dimacs (?ventuellement compress?)
 229    * @throws FileNotFoundException
 230    * si le fichier n'est pas trouv?
 231    * @throws ParseFormatException
 232    * si le fichier ne respecte pas le format Dimacs
 233    * @throws IOException
 234    * pour un autre probl?me d'entr?e/sortie
 235    * @throws ContradictionException
 236    * si le probl?me est trivialement inconsitant
 237    */
 238  0 public IProblem parseInstance(String filename)
 239    throws FileNotFoundException, ParseFormatException, IOException,
 240    ContradictionException {
 241   
 242  0 if (filename.endsWith(".gz")) {
 243  0 parseInstance(
 244    new LineNumberReader(
 245    new InputStreamReader(
 246    new GZIPInputStream(new FileInputStream(filename)))));
 247    } else {
 248  0 parseInstance(
 249    new LineNumberReader(new FileReader(filename)));
 250    }
 251  0 return solver;
 252    }
 253   
 254    /**
 255    * @param in
 256    * the input stream
 257    * @throws ParseFormatException
 258    * if the input stream does not comply with the DIMACS format.
 259    * @throws ContradictionException
 260    * si le probl?me est trivialement inconsitant
 261    */
 262  0 public void parseInstance(LineNumberReader in) throws ParseFormatException,
 263    ContradictionException {
 264  0 solver.reset();
 265  0 try {
 266  0 skipComments(in);
 267  0 readProblemLine(in);
 268  0 readConstrs(in);
 269    } catch (IOException e) {
 270  0 throw new ParseFormatException(e);
 271    } catch (NumberFormatException e) {
 272  0 throw new ParseFormatException("integer value expected on line "
 273    + in.getLineNumber(), e);
 274    }
 275    }
 276   
 277  0 public String decode(int[] model) {
 278  0 StringBuffer stb = new StringBuffer();
 279  0 for (int i = 0; i < model.length; i++) {
 280  0 stb.append(model[i]);
 281  0 stb.append(" ");
 282    }
 283  0 stb.append("0");
 284  0 return stb.toString();
 285    }
 286   
 287  0 protected ISolver getSolver() {
 288  0 return solver;
 289    }
 290    }
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. sept. 29 2005 23:57:47 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.