1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3 *
4 * All rights reserved. This program and the accompanying materials
5 * are made available under the terms of the Eclipse Public License v1.0
6 * which accompanies this distribution, and is available at
7 * http://www.eclipse.org/legal/epl-v10.html
8 *
9 * Alternatively, the contents of this file may be used under the terms of
10 * either the GNU Lesser General Public License Version 2.1 or later (the
11 * "LGPL"), in which case the provisions of the LGPL are applicable instead
12 * of those above. If you wish to allow use of your version of this file only
13 * under the terms of the LGPL, and not to allow others to use your version of
14 * this file under the terms of the EPL, indicate your decision by deleting
15 * the provisions above and replace them with the notice and other provisions
16 * required by the LGPL. If you do not delete the provisions above, a recipient
17 * may use your version of this file under the terms of the EPL or the LGPL.
18 *
19 * Based on the original MiniSat specification from:
20 *
21 * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22 * Sixth International Conference on Theory and Applications of Satisfiability
23 * Testing, LNCS 2919, pp 502-518, 2003.
24 *
25 * See www.minisat.se for the original solver in C++.
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.PrintWriter;
34 import java.io.Serializable;
35
36 import org.sat4j.core.VecInt;
37 import org.sat4j.specs.ContradictionException;
38 import org.sat4j.specs.IProblem;
39 import org.sat4j.specs.ISolver;
40 import org.sat4j.specs.IVecInt;
41
42 /**
43 * Dimacs Reader written by Frederic Laihem. It is much faster than DimacsReader
44 * because it does not split the input file into strings but reads and interpret
45 * the input char by char. Hence, it is a bit more difficult to read and to
46 * modify than DimacsReader.
47 *
48 * This reader is used during the SAT Competitions.
49 *
50 * @author laihem
51 * @author leberre
52 */
53 public class LecteurDimacs extends Reader implements Serializable {
54
55 private static final long serialVersionUID = 1L;
56
57 /* taille du buffer */
58 private final static int TAILLE_BUF = 16384;
59
60 private final ISolver s;
61
62 private transient BufferedInputStream in;
63
64 /* nombre de literaux dans le fichier */
65 private int nbVars = -1;
66
67 private int nbClauses = -1;
68
69 private static final char EOF = (char) -1;
70
71 /*
72 * nomFichier repr?sente le nom du fichier ? lire
73 */
74 public LecteurDimacs(ISolver s) {
75 this.s = s;
76 }
77
78 @Override
79 public final IProblem parseInstance(final InputStream input)
80 throws ParseFormatException, ContradictionException, IOException {
81
82 this.in = new BufferedInputStream(input, LecteurDimacs.TAILLE_BUF);
83 s.reset();
84 passerCommentaire();
85 if (nbVars < 0)
86 throw new ParseFormatException(
87 "DIMACS error: wrong max number of variables");
88 s.newVar(nbVars);
89 s.setExpectedNumberOfClauses(nbClauses);
90 char car = passerEspaces();
91 if (nbClauses>0) {
92 if (car == EOF)
93 throw new ParseFormatException("DIMACS error: the clauses are missing");
94 ajouterClauses(car);
95 }
96 input.close();
97 return s;
98 }
99
100 @Override
101 public IProblem parseInstance(java.io.Reader input) throws IOException,
102 ContradictionException {
103 throw new UnsupportedOperationException();
104 }
105
106 /** on passe les commentaires et on lit le nombre de literaux */
107 private char passerCommentaire() throws IOException {
108 char car;
109 for (;;) {
110 car = passerEspaces();
111 if (car == 'p') {
112 car = lectureNombreLiteraux();
113 }
114 if (car != 'c' && car != 'p')
115 break; /* fin des commentaires */
116 car = nextLine(); /* on passe la ligne de commentaire */
117 if (car == EOF)
118 break;
119 }
120 return car;
121 }
122
123 /** lit le nombre repr?sentant le nombre de literaux */
124 private char lectureNombreLiteraux() throws IOException {
125 char car = nextChiffre(); /* on lit le prchain chiffre */
126 if (car != EOF) {
127 nbVars = car - '0';
128 for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */
129 car = (char) in.read();
130 if (car < '0' || car > '9')
131 break;
132 nbVars = 10 * nbVars + (car - '0');
133 }
134 car = nextChiffre();
135 nbClauses = car - '0';
136 for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */
137 car = (char) in.read();
138 if (car < '0' || car > '9')
139 break;
140 nbClauses = 10 * nbClauses + (car - '0');
141 }
142 if (car != '\n' && car != EOF)
143 nextLine(); /* on lit la fin de la ligne */
144 }
145 return car;
146 }
147
148 /** lit les clauses et les ajoute dans le vecteur donn? en param?tre
149 * @throws ParseFormatException */
150 private void ajouterClauses(char car) throws IOException,
151 ContradictionException, ParseFormatException {
152 final IVecInt lit = new VecInt();
153 int val = 0;
154 boolean neg = false;
155 for (;;) {
156 /* on lit le signe du literal */
157 if (car == '-') {
158 neg = true;
159 car = (char) in.read();
160 } else if (car == '+')
161 car = (char) in.read();
162 else /* on le 1er chiffre du literal */
163 if (car >= '0' && car <= '9') {
164 val = car - '0';
165 car = (char) in.read();
166 } else
167 throw new ParseFormatException("Unknown character "+car);
168 /* on lit la suite du literal */
169 while (car >= '0' && car <= '9') {
170 val = (val * 10) + car - '0';
171 car = (char) in.read();
172 }
173 if (val == 0) { // on a lu toute la clause
174 s.addClause(lit);
175 lit.clear();
176 } else {
177 /* on ajoute le literal au vecteur */
178 // s.newVar(val-1);
179 lit.push(neg ? -val : val);
180 neg = false;
181 val = 0; /* on reinitialise les variables */
182 }
183 if (car != EOF)
184 car = passerEspaces();
185 if (car == EOF) {
186 if (!lit.isEmpty()) {
187 s.addClause(lit);
188 }
189 break; /* on a lu tout le fichier */
190 }
191 }
192 }
193
194 /** passe tout les caract?res d'espacement (espace ou \n) */
195 private char passerEspaces() throws IOException {
196 char car;
197
198 while ((car = (char) in.read()) == ' ' || car == '\n')
199 ;
200 return car;
201 }
202
203 /** passe tout les caract?res jusqu? rencontrer une fin de la ligne */
204 private char nextLine() throws IOException {
205 char car;
206 do {
207 car = (char) in.read();
208 } while ((car != '\n') && (car != EOF));
209 return car;
210 }
211
212 /** passe tout les caract?re jusqu'? rencontrer un chiffre */
213 private char nextChiffre() throws IOException {
214 char car;
215 do {
216 car = (char) in.read();
217 } while ((car < '0') || (car > '9') && (car != EOF));
218 return car;
219 }
220
221 @Override
222 public String decode(int[] model) {
223 StringBuffer stb = new StringBuffer();
224 for (int i = 0; i < model.length; i++) {
225 stb.append(model[i]);
226 stb.append(" ");
227 }
228 stb.append("0");
229 return stb.toString();
230 }
231
232 @Override
233 public void decode(int[] model, PrintWriter out) {
234 for (int i = 0; i < model.length; i++) {
235 out.print(model[i]);
236 out.print(" ");
237 }
238 out.print("0");
239 }
240 }