Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
92   232   36   8,36
44   157   0,5   11
11     4,18  
1    
 
  LecteurDimacs       Line # 51 92 36 77,6% 0.7755102
 
  (101)
 
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.BufferedInputStream;
29    import java.io.IOException;
30    import java.io.InputStream;
31    import java.io.PrintWriter;
32    import java.io.Serializable;
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    * Dimacs Reader written by Frederic Laihem. It is much faster than DimacsReader
42    * because it does not split the input file into strings but reads and interpret
43    * the input char by char. Hence, it is a bit more difficult to read and to
44    * modify than DimacsReader.
45    *
46    * This reader is used during the SAT Competitions.
47    *
48    * @author laihem
49    * @author leberre
50    */
 
51    public class LecteurDimacs extends Reader implements Serializable {
52   
53    private static final long serialVersionUID = 1L;
54   
55    /* taille du buffer */
56    private final static int TAILLE_BUF = 16384;
57   
58    private final ISolver s;
59   
60    private transient BufferedInputStream in;
61   
62    /* nombre de literaux dans le fichier */
63    private int nbLit = 0;
64   
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  1673 toggle public LecteurDimacs(ISolver s) {
73  1673 this.s = s;
74    }
75   
 
76  1673 toggle @Override
77    public final IProblem parseInstance(final InputStream in)
78    throws ParseFormatException, ContradictionException, IOException {
79   
80  1673 this.in = new BufferedInputStream(in, LecteurDimacs.TAILLE_BUF);
81  1673 s.reset();
82  1673 passerCommentaire();
83  1673 if (nbLit == 0)
84  0 throw new IOException(
85    "DIMACS non valide (nombre de Literaux non valide)");
86  1673 s.newVar(nbLit);
87  1673 s.setExpectedNumberOfClauses(nbClauses);
88  1673 char car = passerEspaces();
89  1673 if (car == EOF)
90  0 throw new IOException("DIMACS non valide (ou sont les clauses ?)");
91  1673 ajouterClauses(car);
92  1673 in.close();
93  1673 return s;
94    }
95   
 
96  0 toggle @Override
97    public IProblem parseInstance(java.io.Reader in) throws IOException,
98    ContradictionException {
99  0 throw new UnsupportedOperationException();
100    }
101   
102    /** on passe les commentaires et on lit le nombre de literaux */
 
103  1673 toggle private char passerCommentaire() throws IOException {
104  1673 char car;
105  1673 for (;;) {
106  22757 car = passerEspaces();
107  22757 if (car == 'p') {
108  1673 car = lectureNombreLiteraux();
109    }
110  22757 if (car != 'c' && car != 'p')
111  1673 break; /* fin des commentaires */
112  21084 car = nextLine(); /* on passe la ligne de commentaire */
113  21084 if (car == EOF)
114  0 break;
115    }
116  1673 return car;
117    }
118   
119    /** lit le nombre repr?sentant le nombre de literaux */
 
120  1673 toggle private char lectureNombreLiteraux() throws IOException {
121  1673 char car = nextChiffre(); /* on lit le prchain chiffre */
122  1673 if (car != EOF) {
123  1673 nbLit = car - '0';
124  1673 for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */
125  4610 car = (char) in.read();
126  4610 if (car < '0' || car > '9')
127  1673 break;
128  2937 nbLit = 10 * nbLit + (car - '0');
129    }
130  1673 car = nextChiffre();
131  1673 nbClauses = car - '0';
132  1673 for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */
133  5355 car = (char) in.read();
134  5355 if (car < '0' || car > '9')
135  1673 break;
136  3682 nbClauses = 10 * nbClauses + (car - '0');
137    }
138  1673 if (car != '\n' && car != EOF)
139  0 nextLine(); /* on lit la fin de la ligne */
140    }
141  1673 return car;
142    }
143   
144    /** lit les clauses et les ajoute dans le vecteur donn? en param?tre
145    * @throws ParseFormatException */
 
146  1673 toggle private void ajouterClauses(char car) throws IOException,
147    ContradictionException, ParseFormatException {
148  1673 final IVecInt lit = new VecInt();
149  1673 int val = 0;
150  1673 boolean neg = false;
151  1673 for (;;) {
152    /* on lit le signe du literal */
153  16341595 if (car == '-') {
154  7229578 neg = true;
155  7229578 car = (char) in.read();
156  9112017 } else if (car == '+')
157  0 car = (char) in.read();
158    else /* on le 1er chiffre du literal */
159  9112017 if (car >= '0' && car <= '9') {
160  9112017 val = car - '0';
161  9112017 car = (char) in.read();
162    } else
163  0 throw new ParseFormatException("Unknown character "+car);
164    /* on lit la suite du literal */
165  41747295 while (car >= '0' && car <= '9') {
166  25405700 val = (val * 10) + car - '0';
167  25405700 car = (char) in.read();
168    }
169  16341595 if (val == 0) { // on a lu toute la clause
170  4011911 s.addClause(lit);
171  4011911 lit.clear();
172    } else {
173    /* on ajoute le literal au vecteur */
174    // s.newVar(val-1);
175  12329684 lit.push(neg ? -val : val);
176  12329684 neg = false;
177  12329684 val = 0; /* on reinitialise les variables */
178    }
179  16341595 if (car != EOF)
180  16341211 car = passerEspaces();
181  16341595 if (car == EOF)
182  1673 break; /* on a lu tout le fichier */
183    }
184    }
185   
186    /** passe tout les caract?res d'espacement (espace ou \n) */
 
187  16365641 toggle private char passerEspaces() throws IOException {
188  16365641 char car;
189   
190  0 while ((car = (char) in.read()) == ' ' || car == '\n')
191  16239200 ;
192  16365641 return car;
193    }
194   
195    /** passe tout les caract?res jusqu? rencontrer une fin de la ligne */
 
196  21084 toggle private char nextLine() throws IOException {
197  21084 char car;
198  21084 do {
199  558511 car = (char) in.read();
200  558511 } while ((car != '\n') && (car != EOF));
201  21084 return car;
202    }
203   
204    /** passe tout les caract?re jusqu'? rencontrer un chiffre */
 
205  3346 toggle private char nextChiffre() throws IOException {
206  3346 char car;
207  3346 do {
208  11711 car = (char) in.read();
209  11711 } while ((car < '0') || (car > '9') && (car != EOF));
210  3346 return car;
211    }
212   
 
213  0 toggle @Override
214    public String decode(int[] model) {
215  0 StringBuffer stb = new StringBuffer();
216  0 for (int i = 0; i < model.length; i++) {
217  0 stb.append(model[i]);
218  0 stb.append(" ");
219    }
220  0 stb.append("0");
221  0 return stb.toString();
222    }
223   
 
224  0 toggle @Override
225    public void decode(int[] model, PrintWriter out) {
226  0 for (int i = 0; i < model.length; i++) {
227  0 out.print(model[i]);
228  0 out.print(" ");
229    }
230  0 out.print("0");
231    }
232    }