1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30 package org.sat4j.pb.reader;
31
32 import java.io.IOException;
33 import java.math.BigInteger;
34 import java.util.Iterator;
35
36 import org.sat4j.pb.IPBSolver;
37 import org.sat4j.reader.ParseFormatException;
38 import org.sat4j.specs.ContradictionException;
39 import org.sat4j.specs.IProblem;
40
41
42
43
44 public class OPBReader2010 extends OPBReader2007 {
45
46 public static final BigInteger SAT4J_MAX_BIG_INTEGER = new BigInteger(
47 "100000000000000000000000000000000000000000");
48
49 private boolean isWbo = false;
50
51 private BigInteger softLimit = SAT4J_MAX_BIG_INTEGER;
52
53
54
55
56 private static final long serialVersionUID = 1L;
57
58 public OPBReader2010(IPBSolver solver) {
59 super(solver);
60 }
61
62
63
64
65
66
67
68
69 @Override
70 protected void readMetaData() throws IOException, ParseFormatException {
71 char c;
72 String s;
73
74
75 c = get();
76 if (c != '*') {
77 throw new ParseFormatException(
78 "First line of input file should be a comment");
79 }
80 s = readWord();
81 if (eof() || !"#variable=".equals(s)) {
82 throw new ParseFormatException(
83 "First line should contain #variable= as first keyword");
84 }
85
86 this.nbVars = Integer.parseInt(readWord());
87 this.nbNewSymbols = this.nbVars + 1;
88
89 s = readWord();
90 if (eof() || !"#constraint=".equals(s)) {
91 throw new ParseFormatException(
92 "First line should contain #constraint= as second keyword");
93 }
94
95 this.nbConstr = Integer.parseInt(readWord());
96 this.charAvailable = false;
97 if (!eol()) {
98 String rest = this.in.readLine();
99
100 if (rest != null && rest.contains("#soft")) {
101 this.isWbo = true;
102 this.hasObjFunc = true;
103 }
104 if (rest != null && rest.indexOf("#product=") != -1) {
105 String[] splitted = rest.trim().split(" ");
106 if (splitted[0].equals("#product=")) {
107 Integer.parseInt(splitted[1]);
108 }
109
110
111
112
113 }
114 }
115
116 metaData(this.nbVars, this.nbConstr);
117 }
118
119 @Override
120 protected void readObjective() throws IOException, ParseFormatException {
121 if (this.isWbo) {
122 readSoftLine();
123 } else {
124 super.readObjective();
125 }
126 }
127
128 private void readSoftLine() throws IOException, ParseFormatException {
129 String s = readWord();
130 if (s == null || !"soft:".equals(s)) {
131 throw new ParseFormatException("Did not find expected soft: line");
132 }
133 s = readWord().trim();
134 if (s != null && !";".equals(s)) {
135 this.softLimit = new BigInteger(s);
136 }
137 skipSpaces();
138 if (get() != ';') {
139 throw new ParseFormatException(
140 "soft: line should end with a semicolon");
141 }
142 }
143
144 private boolean softConstraint;
145
146 @Override
147 protected void beginConstraint() {
148 super.beginConstraint();
149 this.softConstraint = false;
150 try {
151 if (this.isWbo) {
152 skipSpaces();
153 char c = get();
154 putback(c);
155 if (c == '[') {
156 this.softConstraint = true;
157 String s = readWord();
158 if (!s.endsWith("]")) {
159 throw new ParseFormatException(
160 "Expecting end of weight ");
161 }
162 BigInteger coeff = new BigInteger(s.substring(1,
163 s.length() - 1));
164 getCoeffs().push(coeff);
165 int varId = this.nbNewSymbols++;
166 getVars().push(varId);
167 }
168
169 }
170 } catch (Exception e) {
171 throw new IllegalStateException(e);
172 }
173 }
174
175 @Override
176 protected void endConstraint() throws ContradictionException {
177 if (this.softConstraint) {
178 int varId = getVars().last();
179 BigInteger constrWeight = this.d;
180 for (Iterator<BigInteger> it = this.coeffs.iterator(); it.hasNext();) {
181 constrWeight = constrWeight.add(it.next().abs());
182 }
183 if ("<=".equals(this.operator)) {
184 constrWeight = constrWeight.negate();
185 }
186 this.coeffs.push(constrWeight);
187 this.lits.push(varId);
188 }
189 super.endConstraint();
190 }
191
192 @Override
193 public IProblem parseInstance(final java.io.Reader input)
194 throws ParseFormatException, ContradictionException {
195 super.parseInstance(input);
196 if (this.isWbo && this.softLimit != SAT4J_MAX_BIG_INTEGER) {
197 this.solver.addPseudoBoolean(getVars(), getCoeffs(), false,
198 this.softLimit.subtract(BigInteger.ONE));
199 }
200 return this.solver;
201 }
202 }