Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 222   Methods: 10
NCLOC: 147   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
LecteurDimacs.java 73,8% 85,1% 80% 81,3%
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.BufferedInputStream;
 31    import java.io.IOException;
 32    import java.io.InputStream;
 33    import java.io.Serializable;
 34   
 35    import org.sat4j.core.VecInt;
 36    import org.sat4j.specs.ContradictionException;
 37    import org.sat4j.specs.IProblem;
 38    import org.sat4j.specs.ISolver;
 39    import org.sat4j.specs.IVecInt;
 40   
 41    /**
 42    * Dimacs Reader written by Frederic Laihem. It is much faster than
 43    * DimacsReader because it does not split the input file into strings
 44    * but reads and interpret the input char by char. Hence, it is a bit more
 45    * difficult to read and to modify than DimacsReader.
 46    *
 47    * This reader is used during the SAT Competitions.
 48    *
 49    * @author laihem
 50    * @author leberre
 51    */
 52    public class LecteurDimacs extends Reader implements Serializable {
 53   
 54    private static final long serialVersionUID = 1L;
 55   
 56    /* taille du buffer */
 57    private final static int TAILLE_BUF = 16384;
 58   
 59    private final ISolver s;
 60   
 61    private transient BufferedInputStream in;
 62   
 63    /* nombre de literaux dans le fichier */
 64    private int nbLit = 0;
 65    private int nbClauses=0;
 66   
 67    private static final char EOF = (char) -1;
 68   
 69    /*
 70    * nomFichier repr?sente le nom du fichier ? lire
 71    */
 72  1663 public LecteurDimacs(ISolver s) {
 73  1663 this.s = s;
 74    }
 75   
 76  1663 @Override
 77    public final IProblem parseInstance(final InputStream in)
 78    throws ParseFormatException, ContradictionException, IOException {
 79   
 80  1663 this.in = new BufferedInputStream(in, LecteurDimacs.TAILLE_BUF);
 81  1663 s.reset();
 82  1663 char car = passerCommentaire();
 83  1663 if (nbLit == 0)
 84  0 throw new IOException(
 85    "DIMACS non valide (nombre de Literaux non valide)");
 86  1663 s.newVar(nbLit);
 87  1663 s.setExpectedNumberOfClauses(nbClauses);
 88  1663 car = passerEspaces();
 89  1663 if (car == EOF)
 90  0 throw new IOException("DIMACS non valide (o? sont les clauses ?)");
 91  1663 ajouterClauses(car);
 92  1663 in.close();
 93  1663 return s;
 94    }
 95   
 96  0 @Override
 97    public IProblem parseInstance(java.io.Reader in) throws IOException, ContradictionException {
 98  0 throw new UnsupportedOperationException();
 99    }
 100   
 101    /** on passe les commentaires et on lit le nombre de literaux */
 102  1663 private char passerCommentaire() throws IOException {
 103  1663 char car;
 104  1663 for (;;) {
 105  22627 car = passerEspaces();
 106  22627 if (car == 'p') {
 107  1663 car = lectureNombreLiteraux();
 108    }
 109  22627 if (car != 'c' && car != 'p')
 110  1663 break; /* fin des commentaires */
 111  20964 car = nextLine(); /* on passe la ligne de commentaire */
 112  20964 if (car == EOF)
 113  0 break;
 114    }
 115  1663 return car;
 116    }
 117   
 118    /** lit le nombre repr?sentant le nombre de literaux */
 119  1663 private char lectureNombreLiteraux() throws IOException {
 120  1663 char car = nextChiffre(); /* on lit le prchain chiffre */
 121  1663 if (car != EOF) {
 122  1663 nbLit = car - '0';
 123  1663 for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */
 124  4590 car = (char) in.read();
 125  4590 if (car < '0' || car > '9')
 126  1663 break;
 127  2927 nbLit = 10 * nbLit + (car - '0');
 128    }
 129  1663 car = nextChiffre();
 130  1663 nbClauses = car - '0';
 131  1663 for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */
 132  5325 car = (char) in.read();
 133  5325 if (car < '0' || car > '9')
 134  1663 break;
 135  3662 nbClauses = 10 * nbClauses + (car - '0');
 136    }
 137  1663 if (car != '\n' && car != EOF)
 138  0 nextLine(); /* on lit la fin de la ligne */
 139    }
 140  1663 return car;
 141    }
 142   
 143    /** lit les clauses et les ajoute dans le vecteur donn? en param?tre */
 144  1663 private void ajouterClauses(char car) throws IOException,
 145    ContradictionException {
 146  1663 final IVecInt lit = new VecInt();
 147  1663 int val = 0;
 148  1663 boolean neg = false;
 149  1663 for (;;) {
 150    /* on lit le signe du literal */
 151  16328445 if (car == '-') {
 152  7221478 neg = true;
 153  7221478 car = (char) in.read();
 154  9106967 } else if (car == '+')
 155  0 car = (char) in.read();
 156    else /* on le 1er chiffre du literal */
 157  9106967 if (car >= '0' && car <= '9') {
 158  9106967 val = car - '0';
 159  9106967 car = (char) in.read();
 160    } else
 161  0 break;
 162    /* on lit la suite du literal */
 163  16328445 while (car >= '0' && car <= '9') {
 164  25389500 val = (val * 10) + car - '0';
 165  25389500 car = (char) in.read();
 166    }
 167  16328445 if (val == 0) { // on a lu toute la clause
 168  4007761 s.addClause(lit);
 169  4007761 lit.clear();
 170    } else {
 171    /* on ajoute le literal au vecteur */
 172    // s.newVar(val-1);
 173  12320684 lit.push(neg ? -val : val);
 174  12320684 neg = false;
 175  12320684 val = 0; /* on reinitialise les variables */
 176    }
 177  16328445 if (car != EOF)
 178  16328061 car = passerEspaces();
 179  16328445 if (car == EOF)
 180  1663 break; /* on a lu tout le fichier */
 181    }
 182    }
 183   
 184    /** passe tout les caract?res d'espacement (espace ou \n) */
 185  16352351 private char passerEspaces() throws IOException {
 186  16352351 char car;
 187   
 188  ? while ((car = (char) in.read()) == ' ' || car == '\n')
 189    ;
 190  16352351 return car;
 191    }
 192   
 193    /** passe tout les caract?res jusqu? rencontrer une fin de la ligne */
 194  20964 private char nextLine() throws IOException {
 195  20964 char car;
 196  20964 do {
 197  554921 car = (char) in.read();
 198  554921 } while ((car != '\n') && (car != EOF));
 199  20964 return car;
 200    }
 201   
 202    /** passe tout les caract?re jusqu'? rencontrer un chiffre */
 203  3326 private char nextChiffre() throws IOException {
 204  3326 char car;
 205  3326 do {
 206  11641 car = (char) in.read();
 207  11641 } while ((car < '0') || (car > '9') && (car != EOF));
 208  3326 return car;
 209    }
 210   
 211  0 @Override
 212    public String decode(int[] model) {
 213  0 StringBuffer stb = new StringBuffer();
 214  0 for (int i = 0; i < model.length; i++) {
 215  0 stb.append(model[i]);
 216  0 stb.append(" ");
 217    }
 218  0 stb.append("0");
 219  0 return stb.toString();
 220    }
 221   
 222    }
 
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.