1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
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 * Contributors:
28 * CRIL - initial API and implementation
29 *******************************************************************************/
30 package org.sat4j.reader;
31
32 import java.io.BufferedInputStream;
33 import java.io.IOException;
34 import java.io.InputStream;
35 import java.io.PrintWriter;
36 import java.io.Serializable;
37
38 import org.sat4j.core.VecInt;
39 import org.sat4j.specs.ContradictionException;
40 import org.sat4j.specs.IProblem;
41 import org.sat4j.specs.ISolver;
42 import org.sat4j.specs.IVecInt;
43
44 /**
45 * Dimacs Reader written by Frederic Laihem. It is much faster than DimacsReader
46 * because it does not split the input file into strings but reads and interpret
47 * the input char by char. Hence, it is a bit more difficult to read and to
48 * modify than DimacsReader.
49 *
50 * This reader is used during the SAT Competitions.
51 *
52 * @author laihem
53 * @author leberre
54 */
55 public class LecteurDimacs extends Reader implements Serializable {
56
57 private static final long serialVersionUID = 1L;
58
59 /* taille du buffer */
60 private final static int TAILLE_BUF = 16384;
61
62 private final ISolver s;
63
64 private transient BufferedInputStream in;
65
66 /* nombre de literaux dans le fichier */
67 private int nbVars = -1;
68
69 private int nbClauses = -1;
70
71 private static final char EOF = (char) -1;
72
73 /*
74 * nomFichier repr?sente le nom du fichier ? lire
75 */
76 public LecteurDimacs(ISolver s) {
77 this.s = s;
78 }
79
80 @Override
81 public final IProblem parseInstance(final InputStream input)
82 throws ParseFormatException, ContradictionException, IOException {
83
84 this.in = new BufferedInputStream(input, LecteurDimacs.TAILLE_BUF);
85 this.s.reset();
86 passerCommentaire();
87 if (this.nbVars < 0) {
88 throw new ParseFormatException(
89 "DIMACS error: wrong max number of variables");
90 }
91 this.s.newVar(this.nbVars);
92 this.s.setExpectedNumberOfClauses(this.nbClauses);
93 char car = passerEspaces();
94 if (this.nbClauses > 0) {
95 if (car == EOF) {
96 throw new ParseFormatException(
97 "DIMACS error: the clauses are missing");
98 }
99 ajouterClauses(car);
100 }
101 input.close();
102 return this.s;
103 }
104
105 /** on passe les commentaires et on lit le nombre de literaux */
106 private char passerCommentaire() throws IOException {
107 char car;
108 for (;;) {
109 car = passerEspaces();
110 if (car == 'p') {
111 car = lectureNombreLiteraux();
112 }
113 if (car != 'c' && car != 'p') {
114 break; /* fin des commentaires */
115 }
116 car = nextLine(); /* on passe la ligne de commentaire */
117 if (car == EOF) {
118 break;
119 }
120 }
121 return car;
122 }
123
124 /** lit le nombre repr?sentant le nombre de literaux */
125 private char lectureNombreLiteraux() throws IOException {
126 char car = nextChiffre(); /* on lit le prchain chiffre */
127 if (car != EOF) {
128 this.nbVars = car - '0';
129 for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */
130 car = (char) this.in.read();
131 if (car < '0' || car > '9') {
132 break;
133 }
134 this.nbVars = 10 * this.nbVars + car - '0';
135 }
136 car = nextChiffre();
137 this.nbClauses = car - '0';
138 for (;;) { /* on lit le chiffre repr?sentant le nombre de literaux */
139 car = (char) this.in.read();
140 if (car < '0' || car > '9') {
141 break;
142 }
143 this.nbClauses = 10 * this.nbClauses + car - '0';
144 }
145 if (car != '\n' && car != EOF) {
146 nextLine(); /* on lit la fin de la ligne */
147 }
148 }
149 return car;
150 }
151
152 /**
153 * lit les clauses et les ajoute dans le vecteur donn? en param?tre
154 *
155 * @throws ParseFormatException
156 */
157 private void ajouterClauses(char car) throws IOException,
158 ContradictionException, ParseFormatException {
159 final IVecInt lit = new VecInt();
160 int val = 0;
161 boolean neg = false;
162 for (;;) {
163 /* on lit le signe du literal */
164 if (car == '-') {
165 neg = true;
166 car = (char) this.in.read();
167 } else if (car == '+') {
168 car = (char) this.in.read();
169 } else /* on le 1er chiffre du literal */
170 if (car >= '0' && car <= '9') {
171 val = car - '0';
172 car = (char) this.in.read();
173 } else {
174 throw new ParseFormatException("Unknown character " + car);
175 }
176 /* on lit la suite du literal */
177 while (car >= '0' && car <= '9') {
178 val = val * 10 + car - '0';
179 car = (char) this.in.read();
180 }
181 if (val == 0) { // on a lu toute la clause
182 this.s.addClause(lit);
183 lit.clear();
184 } else {
185 /* on ajoute le literal au vecteur */
186 // s.newVar(val-1);
187 lit.push(neg ? -val : val);
188 neg = false;
189 val = 0; /* on reinitialise les variables */
190 }
191 if (car != EOF) {
192 car = passerEspaces();
193 }
194 if (car == EOF) {
195 if (!lit.isEmpty()) {
196 this.s.addClause(lit);
197 }
198 break; /* on a lu tout le fichier */
199 }
200 }
201 }
202
203 /** passe tout les caract?res d'espacement (espace ou \n) */
204 private char passerEspaces() throws IOException {
205 char car;
206
207 do {
208 car = (char) this.in.read();
209 } while (car == ' ' || car == '\n');
210
211 return car;
212 }
213
214 /** passe tout les caract?res jusqu? rencontrer une fin de la ligne */
215 private char nextLine() throws IOException {
216 char car;
217 do {
218 car = (char) this.in.read();
219 } while (car != '\n' && car != EOF);
220 return car;
221 }
222
223 /** passe tout les caract?re jusqu'? rencontrer un chiffre */
224 private char nextChiffre() throws IOException {
225 char car;
226 do {
227 car = (char) this.in.read();
228 } while (car < '0' || car > '9' && car != EOF);
229 return car;
230 }
231
232 @Override
233 public String decode(int[] model) {
234 StringBuffer stb = new StringBuffer();
235 for (int element : model) {
236 stb.append(element);
237 stb.append(" ");
238 }
239 stb.append("0");
240 return stb.toString();
241 }
242
243 @Override
244 public void decode(int[] model, PrintWriter out) {
245 for (int element : model) {
246 out.print(element);
247 out.print(" ");
248 }
249 out.print("0");
250 }
251 }