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