1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20 package org.sat4j.pb.tools;
21
22 import java.math.BigInteger;
23 import java.util.Iterator;
24
25 import org.sat4j.core.ConstrGroup;
26 import org.sat4j.core.VecInt;
27 import org.sat4j.pb.IPBSolver;
28 import org.sat4j.pb.ObjectiveFunction;
29 import org.sat4j.specs.ContradictionException;
30 import org.sat4j.specs.IConstr;
31 import org.sat4j.specs.IVec;
32 import org.sat4j.specs.IVecInt;
33 import org.sat4j.tools.xplain.Xplain;
34
35 public class XplainPB extends Xplain<IPBSolver> implements IPBSolver {
36
37
38
39
40 private static final long serialVersionUID = 1L;
41
42 public XplainPB(IPBSolver solver) {
43 super(solver);
44 }
45
46 @Override
47 public IConstr addAtLeast(IVecInt literals, int degree)
48 throws ContradictionException {
49 IVecInt coeffs = new VecInt(literals.size(), 1);
50 int newvar = createNewVar(literals);
51 literals.push(newvar);
52 coeffs.push(coeffs.size() - degree);
53 IConstr constr = decorated().addAtLeast(literals, coeffs, degree);
54 if (constr == null) {
55
56 discardLastestVar();
57 } else {
58 constrs.put(newvar, constr);
59 }
60 return constr;
61 }
62
63 @Override
64 public IConstr addAtMost(IVecInt literals, int degree)
65 throws ContradictionException {
66 IVecInt coeffs = new VecInt(literals.size(), 1);
67 int newvar = createNewVar(literals);
68 literals.push(newvar);
69 coeffs.push(degree - coeffs.size());
70 IConstr constr = decorated().addAtMost(literals, coeffs, degree);
71 if (constr == null) {
72
73 discardLastestVar();
74 } else {
75 constrs.put(newvar, constr);
76 }
77 return constr;
78 }
79
80 @Override
81 public IConstr addExactly(IVecInt literals, int n)
82 throws ContradictionException {
83 int newvar = createNewVar(literals);
84
85
86 IVecInt coeffs = new VecInt(literals.size(), 1);
87 literals.push(newvar);
88 coeffs.push(n - coeffs.size());
89 IConstr constr1 = decorated().addAtMost(literals, coeffs, n);
90
91 coeffs.pop();
92 coeffs.push(coeffs.size() - n);
93 IConstr constr2 = decorated().addAtLeast(literals, coeffs, n);
94 if (constr1 == null && constr2 == null) {
95 discardLastestVar();
96 return null;
97 }
98 ConstrGroup group = new ConstrGroup();
99 group.add(constr1);
100 group.add(constr2);
101 constrs.put(newvar, group);
102 return group;
103 }
104
105 public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
106 boolean moreThan, BigInteger d) throws ContradictionException {
107 int newvar = createNewVar(lits);
108 lits.push(newvar);
109 if (moreThan && d.signum() >= 0) {
110 coeffs.push(d);
111 } else {
112 BigInteger sum = BigInteger.ZERO;
113 for (Iterator<BigInteger> ite = coeffs.iterator(); ite.hasNext();)
114 sum = sum.add(ite.next());
115 sum = sum.subtract(d);
116 coeffs.push(sum.negate());
117 }
118 IConstr constr = decorated()
119 .addPseudoBoolean(lits, coeffs, moreThan, d);
120 if (constr == null) {
121
122 discardLastestVar();
123
124 } else {
125 constrs.put(newvar, constr);
126 }
127 return constr;
128 }
129
130 public void setObjectiveFunction(ObjectiveFunction obj) {
131 decorated().setObjectiveFunction(obj);
132 }
133
134 public ObjectiveFunction getObjectiveFunction() {
135 return decorated().getObjectiveFunction();
136 }
137
138 public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
139 throws ContradictionException {
140 throw new UnsupportedOperationException();
141 }
142
143 public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
144 BigInteger degree) throws ContradictionException {
145 throw new UnsupportedOperationException();
146 }
147
148 public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
149 throws ContradictionException {
150 throw new UnsupportedOperationException();
151 }
152
153 public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
154 BigInteger degree) throws ContradictionException {
155 throw new UnsupportedOperationException();
156 }
157
158 public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
159 throws ContradictionException {
160 throw new UnsupportedOperationException();
161 }
162
163 public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
164 BigInteger weight) throws ContradictionException {
165 throw new UnsupportedOperationException();
166 }
167 }