View Javadoc

1   // BDDFactoryIntImpl.java, created Jul 16, 2006 2:59:55 PM by jwhaley
2   // Copyright (C) 2004-2006 John Whaley <jwhaley@alum.mit.edu>
3   // Licensed under the terms of the GNU LGPL; see COPYING for details.
4   package net.sf.javabdd;
5   
6   import java.util.Collection;
7   import java.util.Iterator;
8   
9   /***
10   * A shared superclass for BDD factories that refer to BDDs as ints.
11   * 
12   * @author jwhaley
13   * @version $Id$
14   */
15  public abstract class BDDFactoryIntImpl extends BDDFactory {
16      
17      static final boolean USE_FINALIZER = false;
18      
19      protected abstract void addref_impl(/*bdd*/int v);
20      protected abstract void delref_impl(/*bdd*/int v);
21      protected abstract /*bdd*/int zero_impl();
22      protected abstract /*bdd*/int one_impl();
23      protected /*bdd*/int universe_impl() { return one_impl(); }
24      protected abstract /*bdd*/int invalid_bdd_impl();
25      protected abstract int var_impl(/*bdd*/int v);
26      protected abstract int level_impl(/*bdd*/int v);
27      protected abstract /*bdd*/int low_impl(/*bdd*/int v);
28      protected abstract /*bdd*/int high_impl(/*bdd*/int v);
29      protected abstract /*bdd*/int ithVar_impl(int var);
30      protected abstract /*bdd*/int nithVar_impl(int var);
31      
32      protected abstract /*bdd*/int makenode_impl(int lev, /*bdd*/int lo, /*bdd*/int hi);
33      protected abstract /*bdd*/int ite_impl(/*bdd*/int v1, /*bdd*/int v2, /*bdd*/int v3);
34      protected abstract /*bdd*/int apply_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr);
35      protected abstract /*bdd*/int not_impl(/*bdd*/int v1);
36      protected abstract /*bdd*/int applyAll_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr, /*bdd*/int v3);
37      protected abstract /*bdd*/int applyEx_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr, /*bdd*/int v3);
38      protected abstract /*bdd*/int applyUni_impl(/*bdd*/int v1, /*bdd*/int v2, BDDOp opr, /*bdd*/int v3);
39      protected abstract /*bdd*/int compose_impl(/*bdd*/int v1, /*bdd*/int v2, int var);
40      protected abstract /*bdd*/int constrain_impl(/*bdd*/int v1, /*bdd*/int v2);
41      protected abstract /*bdd*/int restrict_impl(/*bdd*/int v1, /*bdd*/int v2);
42      protected abstract /*bdd*/int simplify_impl(/*bdd*/int v1, /*bdd*/int v2);
43      protected abstract /*bdd*/int support_impl(/*bdd*/int v);
44      protected abstract /*bdd*/int exist_impl(/*bdd*/int v1, /*bdd*/int v2);
45      protected abstract /*bdd*/int forAll_impl(/*bdd*/int v1, /*bdd*/int v2);
46      protected abstract /*bdd*/int unique_impl(/*bdd*/int v1, /*bdd*/int v2);
47      protected abstract /*bdd*/int fullSatOne_impl(/*bdd*/int v);
48      
49      protected abstract /*bdd*/int replace_impl(/*bdd*/int v, BDDPairing p);
50      protected abstract /*bdd*/int veccompose_impl(/*bdd*/int v, BDDPairing p);
51      
52      protected abstract int nodeCount_impl(/*bdd*/int v);
53      protected abstract double pathCount_impl(/*bdd*/int v);
54      protected abstract double satCount_impl(/*bdd*/int v);
55      protected abstract /*bdd*/int satOne_impl(/*bdd*/int v);
56      protected abstract /*bdd*/int satOne_impl2(/*bdd*/int v1, /*bdd*/int v2, boolean pol);
57      protected abstract int nodeCount_impl2(/*bdd*/int[] v);
58      protected abstract int[] varProfile_impl(/*bdd*/int v);
59      protected abstract void printTable_impl(/*bdd*/int v);
60      
61      public class IntBDD extends BDD {
62          protected /*bdd*/int v;
63          protected IntBDD(/*bdd*/int v) {
64              this.v = v;
65              addref_impl(v);
66          }
67          public BDD apply(BDD that, BDDOp opr) {
68              return makeBDD(apply_impl(v, unwrap(that), opr));
69          }
70          public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) {
71              return makeBDD(applyAll_impl(v, unwrap(that), opr, unwrap(var)));
72          }
73          public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) {
74              return makeBDD(applyEx_impl(v, unwrap(that), opr, unwrap(var)));
75          }
76          public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) {
77              return makeBDD(applyUni_impl(v, unwrap(that), opr, unwrap(var)));
78          }
79          public BDD applyWith(BDD that, BDDOp opr) {
80              /*bdd*/int v2 = unwrap(that);
81              /*bdd*/int v3 = apply_impl(v, v2, opr);
82              addref_impl(v3);
83              delref_impl(v);
84              if (this != that)
85                  that.free();
86              v = v3;
87              return this;
88          }
89          public BDD compose(BDD g, int var) {
90              return makeBDD(compose_impl(v, unwrap(g), var));
91          }
92          public BDD constrain(BDD that) {
93              return makeBDD(constrain_impl(v, unwrap(that)));
94          }
95          public boolean equals(BDD that) {
96              return v == unwrap(that);
97          }
98          public BDD exist(BDDVarSet var) {
99              return makeBDD(exist_impl(v, unwrap(var)));
100         }
101         public BDD forAll(BDDVarSet var) {
102             return makeBDD(forAll_impl(v, unwrap(var)));
103         }
104         public void free() {
105             delref_impl(v);
106             v = invalid_bdd_impl();
107         }
108         public BDD fullSatOne() {
109             return makeBDD(fullSatOne_impl(v));
110         }
111         public BDDFactory getFactory() {
112             return BDDFactoryIntImpl.this;
113         }
114         public int hashCode() {
115             return v;
116         }
117         public BDD high() {
118             return makeBDD(high_impl(v));
119         }
120         public BDD id() {
121             return makeBDD(v);
122         }
123         public boolean isOne() {
124             return v == one_impl();
125         }
126         public boolean isUniverse() {
127             return v == universe_impl();
128         }
129         public boolean isZero() {
130             return v == zero_impl();
131         }
132         public BDD ite(BDD thenBDD, BDD elseBDD) {
133             return makeBDD(ite_impl(v, unwrap(thenBDD), unwrap(elseBDD)));
134         }
135         public BDD low() {
136             return makeBDD(low_impl(v));
137         }
138         public int level() {
139             return level_impl(v);
140         }
141         public int nodeCount() {
142             return nodeCount_impl(v);
143         }
144         public BDD not() {
145             return makeBDD(not_impl(v));
146         }
147         public double pathCount() {
148             return pathCount_impl(v);
149         }
150         public BDD replace(BDDPairing pair) {
151             return makeBDD(replace_impl(v, pair));
152         }
153         public BDD replaceWith(BDDPairing pair) {
154             /*bdd*/int v3 = replace_impl(v, pair);
155             addref_impl(v3);
156             delref_impl(v);
157             v = v3;
158             return this;
159         }
160         public BDD restrict(BDD var) {
161             return makeBDD(restrict_impl(v, unwrap(var)));
162         }
163         public BDD restrictWith(BDD that) {
164             /*bdd*/int v2 = unwrap(that);
165             /*bdd*/int v3 = restrict_impl(v, v2);
166             addref_impl(v3);
167             delref_impl(v);
168             if (this != that)
169                 that.free();
170             v = v3;
171             return this;
172         }
173         public double satCount() {
174             return satCount_impl(v);
175         }
176         public BDD satOne() {
177             return makeBDD(satOne_impl(v));
178         }
179         public BDD satOne(BDDVarSet var, boolean pol) {
180             return makeBDD(satOne_impl2(v, unwrap(var), pol));
181         }
182         public BDD simplify(BDDVarSet d) {
183             return makeBDD(simplify_impl(v, unwrap(d)));
184         }
185         public BDDVarSet support() {
186             return makeBDDVarSet(support_impl(v));
187         }
188         public BDD unique(BDDVarSet var) {
189             return makeBDD(unique_impl(v, unwrap(var)));
190         }
191         public int var() {
192             return var_impl(v);
193         }
194         public int[] varProfile() {
195             return varProfile_impl(v);
196         }
197         public BDD veccompose(BDDPairing pair) {
198             return makeBDD(veccompose_impl(v, pair));
199         }
200         public BDDVarSet toVarSet() {
201             return makeBDDVarSet(v);
202         }
203     }
204     
205     public class IntBDDWithFinalizer extends IntBDD {
206         protected IntBDDWithFinalizer(/*bdd*/int v) {
207             super(v);
208         }
209         
210         protected void finalize() throws Throwable {
211             super.finalize();
212             if (false && v != invalid_bdd_impl()) {
213                 System.out.println("BDD not freed! "+System.identityHashCode(this));
214             }
215             deferredFree(v);
216         }
217         
218     }
219     
220     protected IntBDD makeBDD(/*bdd*/int v) {
221         if (USE_FINALIZER)
222             return new IntBDDWithFinalizer(v);
223         else
224             return new IntBDD(v);
225     }
226     
227     protected static final /*bdd*/int unwrap(BDD b) {
228         return ((IntBDD) b).v;
229     }
230     
231     protected static final /*bdd*/int[] unwrap(Collection/*<BDD>*/ c) {
232         /*bdd*/int[] result = new /*bdd*/int[c.size()];
233         int k = -1;
234         for (Iterator i = c.iterator(); i.hasNext(); ) {
235             result[++k] = ((IntBDD) i.next()).v;
236         }
237         return result;
238     }
239     
240     public class IntBDDVarSet extends BDDVarSet {
241         /*bdd*/int v;
242         protected IntBDDVarSet(/*bdd*/int v) {
243             this.v = v;
244             addref_impl(v);
245         }
246         public boolean equals(BDDVarSet that) {
247             return v == unwrap(that);
248         }
249         public void free() {
250             delref_impl(v);
251             v = invalid_bdd_impl();
252         }
253         public BDDFactory getFactory() {
254             return BDDFactoryIntImpl.this;
255         }
256         public int hashCode() {
257             return v;
258         }
259         public BDDVarSet id() {
260             return makeBDDVarSet(v);
261         }
262         protected int do_intersect(int v1, int v2) {
263             return apply_impl(v1, v2, or);
264         }
265         public BDDVarSet intersect(BDDVarSet b) {
266             return makeBDDVarSet(do_intersect(v, unwrap(b)));
267         }
268         public BDDVarSet intersectWith(BDDVarSet b) {
269             /*bdd*/int v2 = unwrap(b);
270             /*bdd*/int v3 = do_intersect(v, v2);
271             addref_impl(v3);
272             delref_impl(v);
273             if (this != b)
274                 b.free();
275             v = v3;
276             return this;
277         }
278         public boolean isEmpty() {
279             return v == one_impl();
280         }
281         public int size() {
282             int result = 0;
283             for (/*bdd*/int p = v; p != one_impl(); p = high_impl(p)) {
284                 if (p == zero_impl())
285                     throw new BDDException("varset contains zero");
286                 ++result;
287             }
288             return result;
289         }
290         public int[] toArray() {
291             int[] result = new int[size()];
292             int k = -1;
293             for (/*bdd*/int p = v; p != one_impl(); p = high_impl(p)) {
294                 result[++k] = var_impl(p);
295             }
296             return result;
297         }
298         public BDD toBDD() {
299             return makeBDD(v);
300         }
301         public int[] toLevelArray() {
302             int[] result = new int[size()];
303             int k = -1;
304             for (int p = v; p != one_impl(); p = high_impl(p)) {
305                 result[++k] = level_impl(p);
306             }
307             return result;
308         }
309         protected int do_unionvar(int v, int var) {
310             return apply_impl(v, ithVar_impl(var), and);
311         }
312         protected int do_union(int v1, int v2) {
313             return apply_impl(v1, v2, and);
314         }
315         public BDDVarSet union(BDDVarSet b) {
316             return makeBDDVarSet(do_union(v, unwrap(b)));
317         }
318         public BDDVarSet union(int var) {
319             return makeBDDVarSet(do_unionvar(v, var));
320         }
321         public BDDVarSet unionWith(BDDVarSet b) {
322             /*bdd*/int v2 = unwrap(b);
323             /*bdd*/int v3 = do_union(v, v2);
324             addref_impl(v3);
325             delref_impl(v);
326             if (this != b)
327                 b.free();
328             v = v3;
329             return this;
330         }
331         public BDDVarSet unionWith(int var) {
332             /*bdd*/int v3 = do_unionvar(v, var);
333             addref_impl(v3);
334             delref_impl(v);
335             v = v3;
336             return this;
337         }
338     }
339     
340     public class IntBDDVarSetWithFinalizer extends IntBDDVarSet {
341         
342         protected IntBDDVarSetWithFinalizer(int v) {
343             super(v);
344         }
345         
346         protected void finalize() throws Throwable {
347             super.finalize();
348             if (false && v != invalid_bdd_impl()) {
349                 System.out.println("BDD not freed! "+System.identityHashCode(this));
350             }
351             deferredFree(v);
352         }
353         
354     }
355     
356     public class IntZDDVarSet extends IntBDDVarSet {
357         protected IntZDDVarSet(/*bdd*/int v) {
358             super(v);
359         }
360         protected int do_intersect(int v1, int v2) {
361             if (v1 == one_impl()) return v2;
362             if (v2 == one_impl()) return v1;
363             int l1, l2;
364             l1 = level_impl(v1);
365             l2 = level_impl(v2);
366             for (;;) {
367                 if (v1 == v2)
368                     return v1;
369                 if (l1 < l2) {
370                     v1 = high_impl(v1);
371                     if (v1 == one_impl()) return v2;
372                     l1 = level_impl(v1);
373                 } else if (l1 > l2) {
374                     v2 = high_impl(v2);
375                     if (v2 == one_impl()) return v1;
376                     l2 = level_impl(v2);
377                 } else {
378                     int k = do_intersect(high_impl(v1), high_impl(v2));
379                     addref_impl(k);
380                     int result = makenode_impl(l1, zero_impl(), k);
381                     delref_impl(k);
382                     return result;
383                 }
384             }
385         }
386         protected int do_union(int v1, int v2) {
387             if (v1 == v2) return v1;
388             if (v1 == one_impl()) return v2;
389             if (v2 == one_impl()) return v1;
390             int l1, l2;
391             l1 = level_impl(v1);
392             l2 = level_impl(v2);
393             int vv1 = v1, vv2 = v2, lev = l1;
394             if (l1 <= l2)
395                 vv1 = high_impl(v1);
396             if (l1 >= l2) {
397                 vv2 = high_impl(v2);
398                 lev = l2;
399             }
400             int k = do_union(vv1, vv2);
401             addref_impl(k);
402             int result = makenode_impl(lev, zero_impl(), k);
403             delref_impl(k);
404             return result;
405         }
406         protected int do_unionvar(int v, int var) {
407             return do_unionlevel(v, var2Level(var));
408         }
409         private int do_unionlevel(int v, int lev) {
410             if (v == one_impl())
411                 return makenode_impl(lev, zero_impl(), one_impl());
412             int l = level_impl(v);
413             if (l == lev) {
414                 return v;
415             } else if (l > lev) {
416                 return makenode_impl(lev, zero_impl(), v);
417             } else {
418                 int k = do_unionlevel(high_impl(v), lev);
419                 addref_impl(k);
420                 int result = makenode_impl(l, zero_impl(), k);
421                 delref_impl(k);
422                 return result;
423             }
424         }
425     }
426     
427     public class IntZDDVarSetWithFinalizer extends IntZDDVarSet {
428         
429         protected IntZDDVarSetWithFinalizer(int v) {
430             super(v);
431         }
432         
433         protected void finalize() throws Throwable {
434             super.finalize();
435             if (USE_FINALIZER) {
436                 if (false && v != invalid_bdd_impl()) {
437                     System.out.println("BDD not freed! "+System.identityHashCode(this));
438                 }
439                 deferredFree(v);
440             }
441         }
442         
443     }
444     
445     protected IntBDDVarSet makeBDDVarSet(/*bdd*/int v) {
446         if (isZDD()) {
447             if (USE_FINALIZER)
448                 return new IntZDDVarSetWithFinalizer(v);
449             else
450                 return new IntZDDVarSet(v);
451         } else {
452             if (USE_FINALIZER)
453                 return new IntBDDVarSetWithFinalizer(v);
454             else
455                 return new IntBDDVarSet(v);
456         }
457     }
458     
459     protected static final /*bdd*/int unwrap(BDDVarSet b) {
460         return ((IntBDDVarSet) b).v;
461     }
462     
463     public class IntBDDBitVector extends BDDBitVector {
464         
465         protected IntBDDBitVector(int bitnum) {
466             super(bitnum);
467         }
468 
469         public BDDFactory getFactory() {
470             return BDDFactoryIntImpl.this;
471         }
472         
473     }
474     
475     public BDD ithVar(/*bdd*/int var) {
476         return makeBDD(ithVar_impl(var));
477     }
478 
479     public BDD nithVar(/*bdd*/int var) {
480         return makeBDD(nithVar_impl(var));
481     }
482 
483     public int nodeCount(Collection/*<BDD>*/ r) {
484         return nodeCount_impl2(unwrap(r));
485     }
486 
487     public BDD one() {
488         return makeBDD(one_impl());
489     }
490 
491     public BDD universe() {
492         return makeBDD(universe_impl());
493     }
494     
495     public BDDVarSet emptySet() {
496         return makeBDDVarSet(one_impl());
497     }
498     
499     public void printTable(BDD b) {
500         printTable_impl(unwrap(b));
501     }
502 
503     public BDD zero() {
504         return makeBDD(zero_impl());
505     }
506     
507     public void done() {
508         if (USE_FINALIZER) {
509             System.gc();
510             System.runFinalization();
511             handleDeferredFree();
512         }
513     }
514     
515     protected void finalize() throws Throwable {
516         super.finalize();
517         this.done();
518     }
519     
520     protected /*bdd*/int[] to_free = new /*bdd*/int[8];
521     protected /*bdd*/int to_free_length = 0;
522     public void deferredFree(int v) {
523         if (v == invalid_bdd_impl())
524             return;
525         synchronized(to_free) {
526             if (to_free_length == to_free.length) {
527                 /*bdd*/int[] t = new /*bdd*/int[to_free.length * 2];
528                 System.arraycopy(to_free, 0, t, 0, to_free.length);
529                 to_free = t;
530             }
531             to_free[to_free_length++] = v;
532         }
533     }
534     public void handleDeferredFree() {
535         synchronized(to_free) {
536             while (to_free_length > 0) {
537                 delref_impl(to_free[--to_free_length]);
538             }
539         }
540     }
541 }