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.IOException;
33
34 import org.sat4j.specs.ContradictionException;
35 import org.sat4j.specs.IGroupSolver;
36
37 public class GroupedCNFReader extends DimacsReader {
38
39 /**
40 *
41 */
42 private static final long serialVersionUID = 1L;
43
44 private int numberOfComponents;
45
46 private final IGroupSolver groupSolver;
47
48 private int currentComponentIndex;
49
50 public GroupedCNFReader(IGroupSolver solver) {
51 super(solver, "gcnf");
52 this.groupSolver = solver;
53 }
54
55 /**
56 * @param in
57 * the input stream
58 * @throws IOException
59 * iff an IO occurs
60 * @throws ParseFormatException
61 * if the input stream does not comply with the DIMACS format.
62 * @since 2.1
63 */
64 @Override
65 protected void readProblemLine() throws IOException, ParseFormatException {
66
67 String line = this.scanner.nextLine();
68 assert line != null;
69 line = line.trim();
70 String[] tokens = line.split("\\s+");
71 if (tokens.length < 5 || !"p".equals(tokens[0])
72 || !this.formatString.equals(tokens[1])) {
73 throw new ParseFormatException("problem line expected (p "
74 + this.formatString + " ...)");
75 }
76
77 int vars;
78
79 // reads the max var id
80 vars = Integer.parseInt(tokens[2]);
81 assert vars > 0;
82 this.solver.newVar(vars);
83 // reads the number of clauses
84 this.expectedNbOfConstr = Integer.parseInt(tokens[3]);
85 assert this.expectedNbOfConstr > 0;
86 this.numberOfComponents = Integer.parseInt(tokens[4]);
87 this.solver.setExpectedNumberOfClauses(this.expectedNbOfConstr);
88 }
89
90 /**
91 * @since 2.1
92 */
93 @Override
94 protected boolean handleLine() throws ContradictionException, IOException,
95 ParseFormatException {
96 int lit;
97 boolean added = false;
98 String component = this.scanner.next();
99 if (!component.startsWith("{") || !component.endsWith("}")) {
100 throw new ParseFormatException(
101 "Component index required at the beginning of the clause");
102 }
103 this.currentComponentIndex = Integer.valueOf(component.substring(1,
104 component.length() - 1));
105 if (this.currentComponentIndex < 0
106 || this.currentComponentIndex > this.numberOfComponents) {
107 throw new ParseFormatException("wrong component index: "
108 + this.currentComponentIndex);
109 }
110 while (!this.scanner.eof()) {
111 lit = this.scanner.nextInt();
112 if (lit == 0) {
113 if (this.literals.size() > 0) {
114 flushConstraint();
115 this.literals.clear();
116 added = true;
117 }
118 break;
119 }
120 this.literals.push(lit);
121 }
122 return added;
123 }
124
125 /**
126 *
127 * @throws ContradictionException
128 * @since 2.1
129 */
130 @Override
131 protected void flushConstraint() throws ContradictionException {
132 try {
133 if (this.currentComponentIndex == 0) {
134 this.groupSolver.addClause(this.literals);
135 } else {
136 this.groupSolver.addClause(this.literals,
137 this.currentComponentIndex);
138 }
139 } catch (IllegalArgumentException ex) {
140 if (isVerbose()) {
141 System.err.println("c Skipping constraint " + this.literals);
142 }
143 }
144 }
145 }