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