View Javadoc

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      public LecteurDimacs(ISolver s) {
73          this.s = s;
74      }
75  
76      @Override
77      public final IProblem parseInstance(final InputStream in)
78              throws ParseFormatException, ContradictionException, IOException {
79  
80          this.in = new BufferedInputStream(in, LecteurDimacs.TAILLE_BUF);
81          s.reset();
82          passerCommentaire();
83          if (nbLit == 0)
84              throw new IOException(
85                      "DIMACS non valide (nombre de Literaux non valide)");
86          s.newVar(nbLit);
87          s.setExpectedNumberOfClauses(nbClauses);
88          char car = passerEspaces();
89          if (car == EOF)
90              throw new IOException("DIMACS non valide (ou sont les clauses ?)");
91          ajouterClauses(car);
92          in.close();
93          return s;
94      }
95  
96      @Override
97      public IProblem parseInstance(java.io.Reader in) throws IOException,
98              ContradictionException {
99          throw new UnsupportedOperationException();
100     }
101 
102     /** on passe les commentaires et on lit le nombre de literaux */
103     private char passerCommentaire() throws IOException {
104         char car;
105         for (;;) {
106             car = passerEspaces();
107             if (car == 'p') {
108                 car = lectureNombreLiteraux();
109             }
110             if (car != 'c' && car != 'p')
111                 break; /* fin des commentaires */
112             car = nextLine(); /* on passe la ligne de commentaire */
113             if (car == EOF)
114                 break;
115         }
116         return car;
117     }
118 
119     /** lit le nombre repr?sentant le nombre de literaux */
120     private char lectureNombreLiteraux() throws IOException {
121         char car = nextChiffre(); /* on lit le prchain chiffre */
122         if (car != EOF) {
123             nbLit = car - '0';
124             for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */
125                 car = (char) in.read();
126                 if (car < '0' || car > '9')
127                     break;
128                 nbLit = 10 * nbLit + (car - '0');
129             }
130             car = nextChiffre();
131             nbClauses = car - '0';
132             for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */
133                 car = (char) in.read();
134                 if (car < '0' || car > '9')
135                     break;
136                 nbClauses = 10 * nbClauses + (car - '0');
137             }
138             if (car != '\n' && car != EOF)
139                 nextLine(); /* on lit la fin de la ligne */
140         }
141         return car;
142     }
143 
144     /** lit les clauses et les ajoute dans le vecteur donn? en param?tre 
145      * @throws ParseFormatException */
146     private void ajouterClauses(char car) throws IOException,
147             ContradictionException, ParseFormatException {
148         final IVecInt lit = new VecInt();
149         int val = 0;
150         boolean neg = false;
151         for (;;) {
152             /* on lit le signe du literal */
153             if (car == '-') {
154                 neg = true;
155                 car = (char) in.read();
156             } else if (car == '+')
157                 car = (char) in.read();
158             else /* on le 1er chiffre du literal */
159             if (car >= '0' && car <= '9') {
160                 val = car - '0';
161                 car = (char) in.read();
162             } else
163                 throw new ParseFormatException("Unknown character "+car);
164             /* on lit la suite du literal */
165             while (car >= '0' && car <= '9') {
166                 val = (val * 10) + car - '0';
167                 car = (char) in.read();
168             }
169             if (val == 0) { // on a lu toute la clause
170                 s.addClause(lit);
171                 lit.clear();
172             } else {
173                 /* on ajoute le literal au vecteur */
174                 // s.newVar(val-1);
175                 lit.push(neg ? -val : val);
176                 neg = false;
177                 val = 0; /* on reinitialise les variables */
178             }
179             if (car != EOF)
180                 car = passerEspaces();
181             if (car == EOF)
182                 break; /* on a lu tout le fichier */
183         }
184     }
185 
186     /** passe tout les caract?res d'espacement (espace ou \n) */
187     private char passerEspaces() throws IOException {
188         char car;
189 
190         while ((car = (char) in.read()) == ' ' || car == '\n')
191             ;
192         return car;
193     }
194 
195     /** passe tout les caract?res jusqu? rencontrer une fin de la ligne */
196     private char nextLine() throws IOException {
197         char car;
198         do {
199             car = (char) in.read();
200         } while ((car != '\n') && (car != EOF));
201         return car;
202     }
203 
204     /** passe tout les caract?re jusqu'? rencontrer un chiffre */
205     private char nextChiffre() throws IOException {
206         char car;
207         do {
208             car = (char) in.read();
209         } while ((car < '0') || (car > '9') && (car != EOF));
210         return car;
211     }
212 
213     @Override
214     public String decode(int[] model) {
215         StringBuffer stb = new StringBuffer();
216         for (int i = 0; i < model.length; i++) {
217             stb.append(model[i]);
218             stb.append(" ");
219         }
220         stb.append("0");
221         return stb.toString();
222     }
223 
224     @Override
225     public void decode(int[] model, PrintWriter out) {
226         for (int i = 0; i < model.length; i++) {
227             out.print(model[i]);
228             out.print(" ");
229         }
230         out.print("0");
231     }
232 }