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