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 package org.sat4j.reader;
26
27 import java.io.IOException;
28 import java.io.LineNumberReader;
29 import java.util.StringTokenizer;
30
31 import org.sat4j.core.VecInt;
32 import org.sat4j.specs.ContradictionException;
33 import org.sat4j.specs.ISolver;
34 import org.sat4j.specs.IVecInt;
35
36 /**
37 * A reader for cardinality contraints.
38 *
39 * @author leberre
40 */
41 @Deprecated
42 public class CardDimacsReader extends DimacsReader {
43
44 /**
45 *
46 */
47 private static final long serialVersionUID = 3258130241376368435L;
48
49 public CardDimacsReader(ISolver solver) {
50 super(solver);
51 }
52
53 /**
54 * @param in
55 * the input stream
56 * @throws IOException
57 * iff an IO problems occurs
58 * @throws ParseFormatException
59 * if the input stream does not comply with the DIMACS format.
60 * @throws ContradictionException
61 * si le probl?me est trivialement inconsistant.
62 */
63 @Override
64 protected void readConstrs(LineNumberReader in) throws IOException,
65 ParseFormatException, ContradictionException {
66 int lit;
67 String line;
68 StringTokenizer stk;
69
70 int realNbOfClauses = 0;
71
72 IVecInt literals = new VecInt();
73
74 while (true) {
75 line = in.readLine();
76
77 if (line == null) {
78 // end of file
79 if (literals.size() > 0) {
80 // no 0 end the last clause
81 solver.addClause(literals);
82 realNbOfClauses++;
83 }
84
85 break;
86 }
87
88 if (line.startsWith("c ")) {
89 // skip commented line
90 continue;
91 }
92 if (line.startsWith("%") && expectedNbOfConstr == realNbOfClauses) {
93 System.out
94 .println("Ignoring the rest of the file (SATLIB format");
95 break;
96 }
97 stk = new StringTokenizer(line);
98 String token;
99
100 while (stk.hasMoreTokens()) {
101 // on lit le prochain token
102 token = stk.nextToken();
103
104 if ("<=".equals(token) || ">=".equals(token)) {
105 // on est sur une contrainte de cardinalit?
106 readCardinalityConstr(token, stk, literals);
107 literals.clear();
108 realNbOfClauses++;
109 } else {
110 lit = Integer.parseInt(token);
111 if (lit == 0) {
112 if (literals.size() > 0) {
113 solver.addClause(literals);
114 literals.clear();
115 realNbOfClauses++;
116 }
117 } else {
118 literals.push(lit);
119 }
120 }
121 }
122 }
123 if (expectedNbOfConstr != realNbOfClauses) {
124 throw new ParseFormatException("wrong nbclauses parameter. Found "
125 + realNbOfClauses + ", " + expectedNbOfConstr + " expected");
126 }
127 }
128
129 private void readCardinalityConstr(String token, StringTokenizer stk,
130 IVecInt literals) throws ContradictionException,
131 ParseFormatException {
132 int card = Integer.parseInt(stk.nextToken());
133 int lit = Integer.parseInt(stk.nextToken());
134 if (lit == 0) {
135 if ("<=".equals(token)) {
136 solver.addAtMost(literals, card);
137 } else if (">=".equals(token)) {
138 solver.addAtLeast(literals, card);
139 }
140 } else
141 throw new ParseFormatException();
142 }
143
144 }