1
2
3
4 package net.sf.javabdd;
5
6 import java.math.BigInteger;
7
8 /***
9 * <p>Bit vector implementation for BDDs.</p>
10 *
11 * @author John Whaley
12 * @version $Id: BDDBitVector.java 287 2004-10-18 09:35:20Z joewhaley $
13 */
14 public abstract class BDDBitVector {
15
16 protected BDD[] bitvec;
17
18 protected BDDBitVector(int bitnum) {
19 bitvec = new BDD[bitnum];
20 }
21
22 protected void initialize(boolean isTrue) {
23 BDDFactory bdd = getFactory();
24 for (int n = 0; n < bitvec.length; n++)
25 if (isTrue)
26 bitvec[n] = bdd.one();
27 else
28 bitvec[n] = bdd.zero();
29 }
30
31 protected void initialize(int val) {
32 BDDFactory bdd = getFactory();
33 for (int n = 0; n < bitvec.length; n++) {
34 if ((val & 0x1) != 0)
35 bitvec[n] = bdd.one();
36 else
37 bitvec[n] = bdd.zero();
38 val >>= 1;
39 }
40 }
41
42 protected void initialize(long val) {
43 BDDFactory bdd = getFactory();
44 for (int n = 0; n < bitvec.length; n++) {
45 if ((val & 0x1) != 0)
46 bitvec[n] = bdd.one();
47 else
48 bitvec[n] = bdd.zero();
49 val >>= 1;
50 }
51 }
52
53 protected void initialize(BigInteger val) {
54 BDDFactory bdd = getFactory();
55 for (int n = 0; n < bitvec.length; n++) {
56 if (val.testBit(0))
57 bitvec[n] = bdd.one();
58 else
59 bitvec[n] = bdd.zero();
60 val = val.shiftRight(1);
61 }
62 }
63
64 protected void initialize(int offset, int step) {
65 BDDFactory bdd = getFactory();
66 for (int n=0 ; n<bitvec.length ; n++)
67 bitvec[n] = bdd.ithVar(offset+n*step);
68 }
69
70 protected void initialize(BDDDomain d) {
71 initialize(d.vars());
72 }
73
74 protected void initialize(int[] var) {
75 BDDFactory bdd = getFactory();
76 for (int n=0 ; n<bitvec.length ; n++)
77 bitvec[n] = bdd.ithVar(var[n]);
78 }
79
80 public abstract BDDFactory getFactory();
81
82 public BDDBitVector copy() {
83 BDDFactory bdd = getFactory();
84 BDDBitVector dst = bdd.createBitVector(bitvec.length);
85
86 for (int n = 0; n < bitvec.length; n++)
87 dst.bitvec[n] = bitvec[n].id();
88
89 return dst;
90 }
91
92 public BDDBitVector coerce(int bitnum) {
93 BDDFactory bdd = getFactory();
94 BDDBitVector dst = bdd.createBitVector(bitnum);
95 int minnum = Math.min(bitnum, bitvec.length);
96 int n;
97 for (n = 0; n < minnum; n++)
98 dst.bitvec[n] = bitvec[n].id();
99 for (; n < minnum; n++)
100 dst.bitvec[n] = bdd.zero();
101 return dst;
102 }
103
104 public boolean isConst() {
105 for (int n = 0; n < bitvec.length; n++) {
106 BDD b = bitvec[n];
107 if (!b.isOne() && !b.isZero()) return false;
108 }
109 return true;
110 }
111
112 public int val() {
113 int n, val = 0;
114
115 for (n = bitvec.length - 1; n >= 0; n--)
116 if (bitvec[n].isOne())
117 val = (val << 1) | 1;
118 else if (bitvec[n].isZero())
119 val = val << 1;
120 else
121 return 0;
122
123 return val;
124 }
125
126 public void free() {
127 for (int n = 0; n < bitvec.length; n++) {
128 bitvec[n].free();
129 }
130 bitvec = null;
131 }
132
133 public BDDBitVector map2(BDDBitVector that, BDDFactory.BDDOp op) {
134 if (bitvec.length != that.bitvec.length)
135 throw new BDDException();
136
137 BDDFactory bdd = getFactory();
138 BDDBitVector res = bdd.createBitVector(bitvec.length);
139 for (int n=0 ; n < bitvec.length ; n++)
140 res.bitvec[n] = bitvec[n].apply(that.bitvec[n], op);
141
142 return res;
143 }
144
145 public BDDBitVector add(BDDBitVector that) {
146
147 if (bitvec.length != that.bitvec.length)
148 throw new BDDException();
149
150 BDDFactory bdd = getFactory();
151
152 BDD c = bdd.zero();
153 BDDBitVector res = bdd.createBitVector(bitvec.length);
154
155 for (int n = 0; n < res.bitvec.length; n++) {
156
157 res.bitvec[n] = bitvec[n].xor(that.bitvec[n]);
158 res.bitvec[n].xorWith(c.id());
159
160
161 BDD tmp1 = bitvec[n].or(that.bitvec[n]);
162 tmp1.andWith(c);
163 BDD tmp2 = bitvec[n].and(that.bitvec[n]);
164 tmp2.orWith(tmp1);
165 c = tmp2;
166 }
167 c.free();
168
169 return res;
170 }
171
172 public BDDBitVector sub(BDDBitVector that) {
173
174 if (bitvec.length != that.bitvec.length)
175 throw new BDDException();
176
177 BDDFactory bdd = getFactory();
178
179 BDD c = bdd.zero();
180 BDDBitVector res = bdd.createBitVector(bitvec.length);
181
182 for (int n = 0; n < res.bitvec.length; n++) {
183
184 res.bitvec[n] = bitvec[n].xor(that.bitvec[n]);
185 res.bitvec[n].xorWith(c.id());
186
187
188 BDD tmp1 = that.bitvec[n].or(c);
189 BDD tmp2 = this.bitvec[n].apply(tmp1, BDDFactory.less);
190 tmp1.free();
191 tmp1 = this.bitvec[n].and(that.bitvec[n]);
192 tmp1.andWith(c);
193 tmp1.orWith(tmp2);
194
195 c = tmp1;
196 }
197 c.free();
198
199 return res;
200 }
201
202 BDD lte(BDDBitVector r)
203 {
204 if (this.bitvec.length != r.bitvec.length)
205 throw new BDDException();
206
207 BDDFactory bdd = getFactory();
208 BDD p = bdd.one();
209 for (int n=0 ; n<bitvec.length ; n++) {
210
211
212
213 BDD tmp1 = bitvec[n].apply(r.bitvec[n], BDDFactory.less);
214 BDD tmp2 = bitvec[n].apply(r.bitvec[n], BDDFactory.biimp);
215 tmp2.andWith(p);
216 tmp1.orWith(tmp2);
217 p = tmp1;
218 }
219 return p;
220 }
221
222 static void div_rec(BDDBitVector divisor,
223 BDDBitVector remainder,
224 BDDBitVector result,
225 int step) {
226 BDD isSmaller = divisor.lte(remainder);
227 BDDBitVector newResult = result.shl(1, isSmaller);
228 BDDFactory bdd = divisor.getFactory();
229 BDDBitVector zero = bdd.buildVector(divisor.bitvec.length, false);
230 BDDBitVector sub = bdd.buildVector(divisor.bitvec.length, false);
231
232 for (int n = 0; n < divisor.bitvec.length; n++)
233 sub.bitvec[n] = isSmaller.ite(divisor.bitvec[n], zero.bitvec[n]);
234
235 BDDBitVector tmp = remainder.sub(sub);
236 BDDBitVector newRemainder =
237 tmp.shl(1, result.bitvec[divisor.bitvec.length - 1]);
238
239 if (step > 1)
240 div_rec(divisor, newRemainder, newResult, step - 1);
241
242 tmp.free();
243 sub.free();
244 zero.free();
245 isSmaller.free();
246
247 result.replaceWith(newResult);
248 remainder.replaceWith(newRemainder);
249 }
250
251 public void replaceWith(BDDBitVector that) {
252 if (bitvec.length != that.bitvec.length)
253 throw new BDDException();
254 free();
255 this.bitvec = that.bitvec;
256 that.bitvec = null;
257 }
258
259 public BDDBitVector shl(int pos, BDD c) {
260 int minnum = Math.min(bitvec.length, pos);
261 if (minnum < 0)
262 throw new BDDException();
263
264 BDDFactory bdd = getFactory();
265 BDDBitVector res = bdd.createBitVector(bitvec.length);
266
267 int n;
268 for (n = 0; n < minnum; n++)
269 res.bitvec[n] = c.id();
270
271 for (n = minnum; n < bitvec.length; n++)
272 res.bitvec[n] = bitvec[n - pos].id();
273
274 return res;
275 }
276
277 BDDBitVector shr(int pos, BDD c) {
278 int maxnum = Math.max(0, bitvec.length - pos);
279 if (maxnum < 0)
280 throw new BDDException();
281
282 BDDFactory bdd = getFactory();
283 BDDBitVector res = bdd.createBitVector(bitvec.length);
284
285 int n;
286 for (n=maxnum ; n<bitvec.length ; n++)
287 res.bitvec[n] = c.id();
288
289 for (n=0 ; n<maxnum ; n++)
290 res.bitvec[n] = bitvec[n+pos].id();
291
292 return res;
293 }
294
295 public BDDBitVector divmod(long c, boolean which) {
296 if (c <= 0L)
297 throw new BDDException();
298 BDDFactory bdd = getFactory();
299 BDDBitVector divisor = bdd.constantVector(bitvec.length, c);
300 BDDBitVector tmp = bdd.buildVector(bitvec.length, false);
301 BDDBitVector tmpremainder = tmp.shl(1, bitvec[bitvec.length-1]);
302 BDDBitVector result = this.shl(1, bdd.zero());
303
304 BDDBitVector remainder;
305
306 div_rec(divisor, tmpremainder, result, divisor.bitvec.length);
307 remainder = tmpremainder.shr(1, bdd.zero());
308
309 tmp.free();
310 tmpremainder.free();
311 divisor.free();
312
313 if (which) {
314 remainder.free();
315 return result;
316 } else {
317 result.free();
318 return remainder;
319 }
320 }
321
322 public int size() {
323 return bitvec.length;
324 }
325
326 public BDD getBit(int n) {
327 return bitvec[n];
328 }
329 }