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.math.BigInteger;
33 import java.util.regex.Matcher;
34 import java.util.regex.Pattern;
35
36 import org.sat4j.core.Vec;
37 import org.sat4j.core.VecInt;
38 import org.sat4j.pb.IPBSolver;
39 import org.sat4j.pb.ObjectiveFunction;
40 import org.sat4j.reader.JSONReader;
41 import org.sat4j.reader.ParseFormatException;
42 import org.sat4j.specs.ContradictionException;
43 import org.sat4j.specs.IVec;
44 import org.sat4j.specs.IVecInt;
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60 public class JSONPBReader extends JSONReader<IPBSolver> {
61 public static final String WLITERAL = "\\[(-?\\d+),(-?\\d+)\\]";
62 public static final String WCLAUSE = "(\\[(" + WLITERAL + "(," + WLITERAL
63 + ")*)?\\])";
64 public static final String PB = "(\\[" + WCLAUSE + ",'[=<>]=?',-?\\d+\\])";
65
66 public static final String OBJECTIVE_FUNCTION = "(\\[('min'|'max'),"
67 + WCLAUSE + "\\])";
68
69 public static final Pattern PSEUDO_PATTERN = Pattern.compile(PB);
70 public static final Pattern WCLAUSE_PATTERN = Pattern.compile(WCLAUSE);
71 public static final Pattern WLITERAL_PATTERN = Pattern.compile(WLITERAL);
72 public static final Pattern OBJECTIVE_FUNCTION_PATTERN = Pattern
73 .compile(OBJECTIVE_FUNCTION);
74
75 public JSONPBReader(IPBSolver solver) {
76 super(solver);
77 }
78
79 @Override
80 protected void handleNotHandled(String constraint)
81 throws ParseFormatException, ContradictionException {
82 if (PSEUDO_PATTERN.matcher(constraint).matches()) {
83 handlePB(constraint);
84 } else if (OBJECTIVE_FUNCTION_PATTERN.matcher(constraint).matches()) {
85 handleObj(constraint);
86 } else {
87 throw new UnsupportedOperationException("Wrong formula "
88 + constraint);
89 }
90 }
91
92 private void handleObj(String constraint) {
93 Matcher matcher = WCLAUSE_PATTERN.matcher(constraint);
94 if (matcher.find()) {
95 String weightedLiterals = matcher.group();
96 constraint = matcher.replaceFirst("");
97 matcher = WLITERAL_PATTERN.matcher(weightedLiterals);
98 IVecInt literals = new VecInt();
99 String[] pieces = constraint.split(",");
100 boolean negate = pieces[0].contains("max");
101 IVec<BigInteger> coefs = new Vec<BigInteger>();
102 BigInteger coef;
103 while (matcher.find()) {
104 literals.push(Integer.valueOf(matcher.group(2)));
105 coef = new BigInteger(matcher.group(1));
106 coefs.push(negate ? coef.negate() : coef);
107 }
108 solver.setObjectiveFunction(new ObjectiveFunction(literals, coefs));
109 }
110
111 }
112
113 private void handlePB(String constraint) throws ContradictionException {
114 Matcher matcher = WCLAUSE_PATTERN.matcher(constraint);
115 if (matcher.find()) {
116 String weightedLiterals = matcher.group();
117 constraint = matcher.replaceFirst("");
118 matcher = WLITERAL_PATTERN.matcher(weightedLiterals);
119 IVecInt literals = new VecInt();
120 IVecInt coefs = new VecInt();
121 while (matcher.find()) {
122 literals.push(Integer.valueOf(matcher.group(2)));
123 coefs.push(Integer.valueOf(matcher.group(1)));
124 }
125 String[] pieces = constraint.split(",");
126 String comp = pieces[1].substring(1, pieces[1].length() - 1);
127 int degree = Integer.valueOf(pieces[2].substring(0,
128 pieces[2].length() - 1));
129 if ("=".equals(comp) || "==".equals(comp)) {
130 solver.addExactly(literals, coefs, degree);
131 } else if ("<=".equals(comp)) {
132 solver.addAtMost(literals, coefs, degree);
133 } else if ("<".equals(comp)) {
134 solver.addAtMost(literals, coefs, degree - 1);
135 } else if (">=".equals(comp)) {
136 solver.addAtLeast(literals, coefs, degree);
137 } else {
138 assert ">".equals(comp);
139 solver.addAtLeast(literals, coefs, degree + 1);
140 }
141 }
142
143 }
144
145 @Override
146 protected String constraintRegexp() {
147 return "(" + CLAUSE + "|" + CARD + "|" + PB + "|" + OBJECTIVE_FUNCTION
148 + ")";
149 }
150 }