1
2
3
4 package net.sf.javabdd;
5
6 import java.util.Arrays;
7
8 /***
9 * <p>Some BDD methods, namely <tt>exist()</tt>, <tt>forall()</tt>, <tt>unique()</tt>,
10 * <tt>relprod()</tt>, <tt>applyAll()</tt>, <tt>applyEx()</tt>, <tt>applyUni()</tt>,
11 * and <tt>satCount()</tt> take a BDDVarSet argument.</p>
12 *
13 * @author jwhaley
14 * @version $Id$
15 */
16 public abstract class BDDVarSet {
17
18 /***
19 * <p>Returns the factory that created this BDDVarSet.</p>
20 *
21 * @return factory that created this BDDVarSet
22 */
23 public abstract BDDFactory getFactory();
24
25 public abstract BDD toBDD();
26
27 public abstract BDDVarSet id();
28 public abstract void free();
29
30 public abstract int size();
31 public abstract boolean isEmpty();
32
33 public abstract int[] toArray();
34 public abstract int[] toLevelArray();
35
36 public String toString() {
37
38 int[] a = toArray();
39 StringBuffer sb = new StringBuffer(a.length * 4 + 2);
40 sb.append('[');
41 for (int i = 0; i < a.length; ++i) {
42 if (i != 0) sb.append(',');
43 sb.append(a[i]);
44 }
45 sb.append(']');
46 return sb.toString();
47 }
48
49 /***
50 * <p>Scans this BDD and copies the stored variables into an array of BDDDomains.
51 * The domains returned are guaranteed to be in ascending order.</p>
52 *
53 * <p>Compare to fdd_scanset.</p>
54 *
55 * @return int[]
56 */
57 public BDDDomain[] getDomains() {
58 int[] fv;
59 BDDDomain[] varset;
60 int fn;
61 int num, n, m, i;
62
63 fv = this.toArray();
64 fn = fv.length;
65
66 BDDFactory factory = getFactory();
67
68 for (n = 0, num = 0; n < factory.numberOfDomains(); n++) {
69 BDDDomain dom = factory.getDomain(n);
70 int[] ivar = dom.vars();
71 boolean found = false;
72 for (m = 0; m < dom.varNum() && !found; m++) {
73 for (i = 0; i < fn && !found; i++) {
74 if (ivar[m] == fv[i]) {
75 num++;
76 found = true;
77 }
78 }
79 }
80 }
81
82 varset = new BDDDomain[num];
83
84 for (n = 0, num = 0; n < factory.numberOfDomains(); n++) {
85 BDDDomain dom = factory.getDomain(n);
86 int[] ivar = dom.vars();
87 boolean found = false;
88 for (m = 0; m < dom.varNum() && !found; m++) {
89 for (i = 0; i < fn && !found; i++) {
90 if (ivar[m] == fv[i]) {
91 varset[num++] = dom;
92 found = true;
93 }
94 }
95 }
96 }
97
98 return varset;
99 }
100
101 /***
102 * <p>Returns a new BDDVarSet that is the union of the current BDDVarSet
103 * and the given BDDVarSet. This constructs a new set; neither the current
104 * nor the given BDDVarSet is modified.</p>
105 *
106 * @param b BDDVarSet to union with
107 * @return a new BDDVarSet that is the union of the two sets
108 */
109 public abstract BDDVarSet union(BDDVarSet b);
110
111 /***
112 * <p>Returns a new BDDVarSet that is the union of the current BDDVarSet
113 * and the given variable. This constructs a new set; the current BDDVarSet
114 * is not modified.</p>
115 *
116 * @param b variable to add to set
117 * @return a new BDDVarSet that includes the given variable
118 */
119 public abstract BDDVarSet union(int var);
120
121 /***
122 * <p>Modifies this BDDVarSet to include all of the vars in the given set.
123 * This modifies the current set in place and consumes the given set.</p>
124 *
125 * @param b BDDVarSet to union in
126 * @return this
127 */
128 public abstract BDDVarSet unionWith(BDDVarSet b);
129
130 /***
131 * <p>Modifies this BDDVarSet to include the given variable. This modifies
132 * the current set in place.</p>
133 *
134 * @param b variable to add to set
135 * @return this
136 */
137 public abstract BDDVarSet unionWith(int var);
138
139 /***
140 * <p>Returns a new BDDVarSet that is the union of the current BDDVarSet
141 * and the given BDDVarSet. This constructs a new set; neither the current
142 * nor the given BDDVarSet is modified.</p>
143 *
144 * @param b BDDVarSet to union with
145 * @return a new BDDVarSet that is the union of the two sets
146 */
147 public abstract BDDVarSet intersect(BDDVarSet b);
148
149 /***
150 * <p>Modifies this BDDVarSet to include all of the vars in the given set.
151 * This modifies the current set in place and consumes the given set.</p>
152 *
153 * @param b BDDVarSet to union in
154 * @return this
155 */
156 public abstract BDDVarSet intersectWith(BDDVarSet b);
157
158
159
160
161 public abstract int hashCode();
162
163 /***
164 * Returns true if the sets are equal.
165 *
166 * @param that other set
167 * @return true if the sets are equal
168 */
169 public abstract boolean equals(BDDVarSet that);
170
171
172
173
174 public final boolean equals(Object o) {
175 if (o instanceof BDDVarSet)
176 return equals((BDDVarSet) o);
177 return false;
178 }
179
180 /***
181 * Default implementation of BDDVarSet based on BDDs.
182 *
183 * @author jwhaley
184 * @version $Id$
185 */
186 public static class DefaultImpl extends BDDVarSet {
187
188 /***
189 * BDD representation of the set of variables.
190 * Treated like a linked list of variables.
191 */
192 protected BDD b;
193
194 /***
195 * Construct a BDDVarSet backed by the given BDD.
196 * Ownership of the given BDD is transferred to this BDDVarSet,
197 * so you should not touch it after construction!
198 *
199 * @param b BDD to use in constructing BDDVarSet
200 */
201 public DefaultImpl(BDD b) {
202 this.b = b;
203 }
204
205
206
207
208 public void free() {
209 if (b != null) {
210 b.free();
211 b = null;
212 }
213 }
214
215
216
217
218 public BDDFactory getFactory() {
219 return b.getFactory();
220 }
221
222
223
224
225 public BDDVarSet id() {
226 return new DefaultImpl(b.id());
227 }
228
229
230
231
232 public BDDVarSet intersect(BDDVarSet s) {
233 DefaultImpl i = (DefaultImpl) s;
234 return new DefaultImpl(b.or(i.b));
235 }
236
237
238
239
240 public BDDVarSet intersectWith(BDDVarSet s) {
241 DefaultImpl i = (DefaultImpl) s;
242 b.orWith(i.b); i.b = null;
243 return this;
244 }
245
246
247
248
249 public boolean isEmpty() {
250 return b.isOne();
251 }
252
253
254
255
256 public int size() {
257 int result = 0;
258 BDD r = b.id();
259 while (!r.isOne()) {
260 if (r.isZero()) throw new BDDException("varset contains zero");
261 ++result;
262 BDD q = r.high();
263 r.free();
264 r = q;
265 }
266 r.free();
267 return result;
268 }
269
270
271
272
273 public int[] toArray() {
274 int[] result = new int[size()];
275 int i = -1;
276 BDD r = b.id();
277 while (!r.isOne()) {
278 if (r.isZero()) throw new BDDException("varset contains zero");
279 result[++i] = r.var();
280 BDD q = r.high();
281 r.free();
282 r = q;
283 }
284 r.free();
285 return result;
286 }
287
288
289
290
291 public BDD toBDD() {
292 return b.id();
293 }
294
295
296
297
298 public int[] toLevelArray() {
299 int[] result = new int[size()];
300 int i = -1;
301 BDD r = b.id();
302 while (!r.isOne()) {
303 if (r.isZero()) throw new BDDException("varset contains zero");
304 result[++i] = r.level();
305 BDD q = r.high();
306 r.free();
307 r = q;
308 }
309 r.free();
310 return result;
311 }
312
313
314
315
316 public BDDVarSet union(BDDVarSet s) {
317 DefaultImpl i = (DefaultImpl) s;
318 return new DefaultImpl(b.and(i.b));
319 }
320
321
322
323
324 public BDDVarSet union(int var) {
325 BDD ith = b.getFactory().ithVar(var);
326 DefaultImpl j = new DefaultImpl(b.and(ith));
327 ith.free();
328 return j;
329 }
330
331
332
333
334 public BDDVarSet unionWith(BDDVarSet s) {
335 DefaultImpl i = (DefaultImpl) s;
336 b.andWith(i.b); i.b = null;
337 return this;
338 }
339
340
341
342
343 public BDDVarSet unionWith(int var) {
344 b.andWith(b.getFactory().ithVar(var));
345 return this;
346 }
347
348
349
350
351 public int hashCode() {
352 return b.hashCode();
353 }
354
355
356
357
358 public boolean equals(BDDVarSet s) {
359 if (s instanceof DefaultImpl)
360 return equals((DefaultImpl) s);
361 return false;
362 }
363
364 public boolean equals(DefaultImpl s) {
365 return b.equals(s.b);
366 }
367 }
368
369 }