View Javadoc

1   // CUDDFactory.java, created Jan 29, 2003 9:50:57 PM by jwhaley
2   // Copyright (C) 2003 John Whaley
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.math.BigInteger;
8   
9   /***
10   * <p>An implementation of BDDFactory that relies on the CUDD library through a
11   * native interface.  You can use this by calling the "CUDDFactory.init()"
12   * method with the desired arguments.  This will return you an instance of the
13   * BDDFactory class that you can use.  Call "done()" on that instance when you
14   * are finished.</p>
15   * 
16   * <p>CUDD does not have much of the functionality that BuDDy has, and it has
17   * not been well-tested.  Furthermore, it is slower than BuDDy.  Therefore, it
18   * is recommended that you use the BuDDy library instead.</p>
19   * 
20   * <p>This class (and the CUDD library) do NOT support multithreading.
21   * Furthermore, there can be only one instance active at a time.  You can only
22   * call "init()" again after you have called "done()" on the original instance.
23   * It is not recommended to call "init()" again after calling "done()" unless
24   * you are _completely_ sure that all BDD objects that reference the old
25   * factory have been freed.</p>
26   * 
27   * <p>If you really need multiple BDD factories, consider using the JavaFactory
28   * class for the additional BDD factories --- JavaFactory can have multiple
29   * factory instances active at a time.</p>
30   * 
31   * @see net.sf.javabdd.BDDFactory
32   * @see net.sf.javabdd.BuDDyFactory
33   * 
34   * @author John Whaley
35   * @version $Id: CUDDFactory.java 454 2006-07-17 03:45:42Z joewhaley $
36   */
37  public class CUDDFactory extends BDDFactory {
38  
39      public static BDDFactory init(int nodenum, int cachesize) {
40          CUDDFactory f = new CUDDFactory();
41          f.initialize(nodenum/256, cachesize);
42          return f;
43      }
44      
45      private static CUDDFactory INSTANCE;
46      
47      static {
48          String libname = "cudd";
49          try {
50              System.loadLibrary(libname);
51          } catch (java.lang.UnsatisfiedLinkError x) {
52              // Cannot find library, try loading it from the current directory...
53              libname = System.mapLibraryName(libname);
54              String currentdir = getProperty("user.dir", ".");
55              String sep = getProperty("file.separator", "/");
56              System.load(currentdir+sep+libname);
57          }
58          registerNatives();
59      }
60      
61      private static native void registerNatives();
62      
63      private CUDDFactory() {}
64      
65      private static long zero;
66      private static long one;
67      
68      /* (non-Javadoc)
69       * @see net.sf.javabdd.BDDFactory#zero()
70       */
71      public BDD zero() {
72          return new CUDDBDD(zero);
73      }
74  
75      /* (non-Javadoc)
76       * @see net.sf.javabdd.BDDFactory#one()
77       */
78      public BDD one() {
79          return new CUDDBDD(one);
80      }
81  
82      /* (non-Javadoc)
83       * @see net.sf.javabdd.BDDFactory#initialize(int, int)
84       */
85      protected void initialize(int nodenum, int cachesize) {
86          if (INSTANCE != null) {
87              throw new InternalError("Error: CUDDFactory already initialized.");
88          }
89          INSTANCE = this;
90          initialize0(nodenum, cachesize);
91      }
92      private static native void initialize0(int nodenum, int cachesize);
93  
94      /* (non-Javadoc)
95       * @see net.sf.javabdd.BDDFactory#isInitialized()
96       */
97      public boolean isInitialized() {
98          return isInitialized0();
99      }
100     private static native boolean isInitialized0();
101 
102     /* (non-Javadoc)
103      * @see net.sf.javabdd.BDDFactory#done()
104      */
105     public void done() {
106         INSTANCE = null;
107         done0();
108     }
109     private static native void done0();
110 
111     /* (non-Javadoc)
112      * @see net.sf.javabdd.BDDFactory#setError(int)
113      */
114     public void setError(int code) {
115         // TODO Implement this.
116     }
117     
118     /* (non-Javadoc)
119      * @see net.sf.javabdd.BDDFactory#clearError()
120      */
121     public void clearError() {
122         // TODO Implement this.
123     }
124     
125     /* (non-Javadoc)
126      * @see net.sf.javabdd.BDDFactory#setMaxNodeNum(int)
127      */
128     public int setMaxNodeNum(int size) {
129         // TODO Implement this.
130         System.err.println("Warning: setMaxNodeNum() not yet implemented");
131         return 1000000;
132     }
133 
134     /* (non-Javadoc)
135      * @see net.sf.javabdd.BDDFactory#setNodeTableSize(int)
136      */
137     public int setNodeTableSize(int size) {
138         // TODO Implement this.
139         System.err.println("Warning: setNodeTableSize() not yet implemented");
140         return getNodeTableSize();
141     }
142     
143     /* (non-Javadoc)
144      * @see net.sf.javabdd.BDDFactory#setCacheSize(int)
145      */
146     public int setCacheSize(int size) {
147         // TODO Implement this.
148         System.err.println("Warning: setCacheSize() not yet implemented");
149         return 0;
150     }
151     
152     /* (non-Javadoc)
153      * @see net.sf.javabdd.BDDFactory#setMinFreeNodes(double)
154      */
155     public double setMinFreeNodes(double x) {
156         // TODO Implement this.
157         System.err.println("Warning: setMinFreeNodes() not yet implemented");
158         return 0;
159     }
160 
161     /* (non-Javadoc)
162      * @see net.sf.javabdd.BDDFactory#setMaxIncrease(int)
163      */
164     public int setMaxIncrease(int x) {
165         // TODO Implement this.
166         System.err.println("Warning: setMaxIncrease() not yet implemented");
167         return 50000;
168     }
169 
170     /* (non-Javadoc)
171      * @see net.sf.javabdd.BDDFactory#setCacheRatio(double)
172      */
173     public double setCacheRatio(double x) {
174         // TODO Implement this.
175         System.err.println("Warning: setCacheRatio() not yet implemented");
176         return 0;
177     }
178 
179     /* (non-Javadoc)
180      * @see net.sf.javabdd.BDDFactory#setIncreaseFactor(double)
181      */
182     public double setIncreaseFactor(double x) {
183         // TODO Implement this.
184         System.err.println("Warning: setIncreaseFactor() not yet implemented");
185         return 0;
186     }
187     
188     /* (non-Javadoc)
189      * @see net.sf.javabdd.BDDFactory#varNum()
190      */
191     public int varNum() {
192         return varNum0();
193     }
194     private static native int varNum0();
195 
196     /* (non-Javadoc)
197      * @see net.sf.javabdd.BDDFactory#setVarNum(int)
198      */
199     public int setVarNum(int num) {
200         return setVarNum0(num);
201     }
202     private static native int setVarNum0(int num);
203 
204     /* (non-Javadoc)
205      * @see net.sf.javabdd.BDDFactory#duplicateVar(int)
206      */
207     public int duplicateVar(int var) {
208         // TODO Implement this.
209         throw new UnsupportedOperationException();
210     }
211     
212     /* (non-Javadoc)
213      * @see net.sf.javabdd.BDDFactory#ithVar(int)
214      */
215     public BDD ithVar(int var) {
216         long id = ithVar0(var);
217         return new CUDDBDD(id);
218     }
219     private static native long ithVar0(int var);
220 
221     /* (non-Javadoc)
222      * @see net.sf.javabdd.BDDFactory#nithVar(int)
223      */
224     public BDD nithVar(int var) {
225         BDD b = ithVar(var);
226         BDD c = b.not(); b.free();
227         return c;
228     }
229 
230     /* (non-Javadoc)
231      * @see net.sf.javabdd.BDDFactory#swapVar(int, int)
232      */
233     public void swapVar(int v1, int v2) {
234         // TODO Implement this.
235         throw new UnsupportedOperationException();
236     }
237 
238     /* (non-Javadoc)
239      * @see net.sf.javabdd.BDDFactory#makePair()
240      */
241     public BDDPairing makePair() {
242         return new CUDDBDDPairing();
243     }
244 
245     /* (non-Javadoc)
246      * @see net.sf.javabdd.BDDFactory#printAll()
247      */
248     public void printAll() {
249         // TODO Implement this.
250         throw new UnsupportedOperationException();
251     }
252 
253     /* (non-Javadoc)
254      * @see net.sf.javabdd.BDDFactory#printTable(net.sf.javabdd.BDD)
255      */
256     public void printTable(BDD b) {
257         // TODO Implement this.
258         throw new UnsupportedOperationException();
259     }
260 
261     /* (non-Javadoc)
262      * @see net.sf.javabdd.BDDFactory#level2Var(int)
263      */
264     public int level2Var(int level) {
265         return level2Var0(level);
266     }
267     private static native int level2Var0(int level);
268 
269     /* (non-Javadoc)
270      * @see net.sf.javabdd.BDDFactory#var2Level(int)
271      */
272     public int var2Level(int var) {
273         return var2Level0(var);
274     }
275     private static native int var2Level0(int var);
276 
277     /* (non-Javadoc)
278      * @see net.sf.javabdd.BDDFactory#reorder(net.sf.javabdd.BDDFactory.ReorderMethod)
279      */
280     public void reorder(ReorderMethod m) {
281         // TODO Implement this.
282         throw new UnsupportedOperationException();
283     }
284 
285     /* (non-Javadoc)
286      * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod)
287      */
288     public void autoReorder(ReorderMethod method) {
289         // TODO Implement this.
290         throw new UnsupportedOperationException();
291     }
292 
293     /* (non-Javadoc)
294      * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod, int)
295      */
296     public void autoReorder(ReorderMethod method, int max) {
297         // TODO Implement this.
298         throw new UnsupportedOperationException();
299     }
300 
301     /* (non-Javadoc)
302      * @see net.sf.javabdd.BDDFactory#getReorderMethod()
303      */
304     public ReorderMethod getReorderMethod() {
305         // TODO Implement this.
306         throw new UnsupportedOperationException();
307     }
308 
309     /* (non-Javadoc)
310      * @see net.sf.javabdd.BDDFactory#getReorderTimes()
311      */
312     public int getReorderTimes() {
313         // TODO Implement this.
314         throw new UnsupportedOperationException();
315     }
316 
317     /* (non-Javadoc)
318      * @see net.sf.javabdd.BDDFactory#disableReorder()
319      */
320     public void disableReorder() {
321         // TODO Implement this.
322         System.err.println("Warning: disableReorder() not yet implemented");
323     }
324 
325     /* (non-Javadoc)
326      * @see net.sf.javabdd.BDDFactory#enableReorder()
327      */
328     public void enableReorder() {
329         // TODO Implement this.
330         System.err.println("Warning: enableReorder() not yet implemented");
331     }
332 
333     /* (non-Javadoc)
334      * @see net.sf.javabdd.BDDFactory#reorderVerbose(int)
335      */
336     public int reorderVerbose(int v) {
337         // TODO Implement this.
338         throw new UnsupportedOperationException();
339     }
340 
341     /* (non-Javadoc)
342      * @see net.sf.javabdd.BDDFactory#setVarOrder(int[])
343      */
344     public void setVarOrder(int[] neworder) {
345         setVarOrder0(neworder);
346     }
347     private static native void setVarOrder0(int[] neworder);
348 
349     /* (non-Javadoc)
350      * @see net.sf.javabdd.BDDFactory#addVarBlock(net.sf.javabdd.BDD, boolean)
351      */
352     public void addVarBlock(BDD var, boolean fixed) {
353         // TODO Implement this.
354         throw new UnsupportedOperationException();
355     }
356 
357     /* (non-Javadoc)
358      * @see net.sf.javabdd.BDDFactory#addVarBlock(int, int, boolean)
359      */
360     public void addVarBlock(int first, int last, boolean fixed) {
361         // TODO Implement this.
362         throw new UnsupportedOperationException();
363     }
364 
365     /* (non-Javadoc)
366      * @see net.sf.javabdd.BDDFactory#varBlockAll()
367      */
368     public void varBlockAll() {
369         // TODO Implement this.
370         throw new UnsupportedOperationException();
371     }
372 
373     /* (non-Javadoc)
374      * @see net.sf.javabdd.BDDFactory#clearVarBlocks()
375      */
376     public void clearVarBlocks() {
377         // TODO Implement this.
378         throw new UnsupportedOperationException();
379     }
380 
381     /* (non-Javadoc)
382      * @see net.sf.javabdd.BDDFactory#printOrder()
383      */
384     public void printOrder() {
385         // TODO Implement this.
386         throw new UnsupportedOperationException();
387     }
388 
389     /* (non-Javadoc)
390      * @see net.sf.javabdd.BDDFactory#nodeCount(java.util.Collection)
391      */
392     public int nodeCount(Collection r) {
393         // TODO Implement this.
394         throw new UnsupportedOperationException();
395     }
396 
397     /* (non-Javadoc)
398      * @see net.sf.javabdd.BDDFactory#getNodeTableSize()
399      */
400     public int getNodeTableSize() {
401         return getAllocNum0();
402     }
403     private static native int getAllocNum0();
404 
405     /* (non-Javadoc)
406      * @see net.sf.javabdd.BDDFactory#getNodeNum()
407      */
408     public int getNodeNum() {
409         return getNodeNum0();
410     }
411     private static native int getNodeNum0();
412 
413     /* (non-Javadoc)
414      * @see net.sf.javabdd.BDDFactory#getCacheSize()
415      */
416     public int getCacheSize() {
417         return getCacheSize0();
418     }
419     private static native int getCacheSize0();
420     
421     /* (non-Javadoc)
422      * @see net.sf.javabdd.BDDFactory#reorderGain()
423      */
424     public int reorderGain() {
425         // TODO Implement this.
426         throw new UnsupportedOperationException();
427     }
428 
429     /* (non-Javadoc)
430      * @see net.sf.javabdd.BDDFactory#printStat()
431      */
432     public void printStat() {
433         // TODO Implement this.
434         throw new UnsupportedOperationException();
435     }
436 
437     /* (non-Javadoc)
438      * @see net.sf.javabdd.BDDFactory#createDomain(int, BigInteger)
439      */
440     protected BDDDomain createDomain(int a, BigInteger b) {
441         return new CUDDBDDDomain(a, b);
442     }
443 
444     /* (non-Javadoc)
445      * An implementation of a BDD class, used by the CUDD interface.
446      */
447     private static class CUDDBDD extends BDD {
448 
449         /*** The pointer used by the BDD library. */
450         private long _ddnode_ptr;
451         
452         /*** An invalid id, for use in invalidating BDDs. */
453         static final long INVALID_BDD = -1;
454         
455         private CUDDBDD(long ddnode) {
456             this._ddnode_ptr = ddnode;
457             addRef(ddnode);
458         }
459 
460         /* (non-Javadoc)
461          * @see net.sf.javabdd.BDD#getFactory()
462          */
463         public BDDFactory getFactory() {
464             return INSTANCE;
465         }
466         
467         /* (non-Javadoc)
468          * @see net.sf.javabdd.BDD#isZero()
469          */
470         public boolean isZero() {
471             return this._ddnode_ptr == zero;
472         }
473 
474         /* (non-Javadoc)
475          * @see net.sf.javabdd.BDD#isOne()
476          */
477         public boolean isOne() {
478             return this._ddnode_ptr == one;
479         }
480 
481         /* (non-Javadoc)
482          * @see net.sf.javabdd.BDD#var()
483          */
484         public int var() {
485             if (isZero() || isOne())
486                 throw new BDDException("cannot get var of terminal");
487             return var0(_ddnode_ptr);
488         }
489         private static native int var0(long b);
490         
491         /* (non-Javadoc)
492          * @see net.sf.javabdd.BDD#high()
493          */
494         public BDD high() {
495             long b = high0(_ddnode_ptr);
496             return new CUDDBDD(b);
497         }
498         private static native long high0(long b);
499         
500         /* (non-Javadoc)
501          * @see net.sf.javabdd.BDD#low()
502          */
503         public BDD low() {
504             long b = low0(_ddnode_ptr);
505             return new CUDDBDD(b);
506         }
507         private static native long low0(long b);
508         
509         /* (non-Javadoc)
510          * @see net.sf.javabdd.BDD#id()
511          */
512         public BDD id() {
513             return new CUDDBDD(_ddnode_ptr);
514         }
515 
516         /* (non-Javadoc)
517          * @see net.sf.javabdd.BDD#not()
518          */
519         public BDD not() {
520             long b = not0(_ddnode_ptr);
521             return new CUDDBDD(b);
522         }
523         private static native long not0(long b);
524         
525         /* (non-Javadoc)
526          * @see net.sf.javabdd.BDD#ite(net.sf.javabdd.BDD, net.sf.javabdd.BDD)
527          */
528         public BDD ite(BDD thenBDD, BDD elseBDD) {
529             CUDDBDD c = (CUDDBDD) thenBDD;
530             CUDDBDD d = (CUDDBDD) elseBDD;
531             long b = ite0(_ddnode_ptr, c._ddnode_ptr, d._ddnode_ptr);
532             return new CUDDBDD(b);
533         }
534         private static native long ite0(long b, long c, long d);
535         
536         /* (non-Javadoc)
537          * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet)
538          */
539         public BDD relprod(BDD that, BDDVarSet var) {
540             CUDDBDD c = (CUDDBDD) that;
541             CUDDBDD d = (CUDDBDD) ((BDDVarSet.DefaultImpl) var).b;
542             long b = relprod0(_ddnode_ptr, c._ddnode_ptr, d._ddnode_ptr);
543             return new CUDDBDD(b);
544         }
545         private static native long relprod0(long b, long c, long d);
546         
547         /* (non-Javadoc)
548          * @see net.sf.javabdd.BDD#compose(net.sf.javabdd.BDD, int)
549          */
550         public BDD compose(BDD that, int var) {
551             CUDDBDD c = (CUDDBDD) that;
552             long b = compose0(_ddnode_ptr, c._ddnode_ptr, var);
553             return new CUDDBDD(b);
554         }
555         private static native long compose0(long b, long c, int var);
556 
557         /* (non-Javadoc)
558          * @see net.sf.javabdd.BDD#constrain(net.sf.javabdd.BDD)
559          */
560         public BDD constrain(BDD that) {
561             // TODO Implement this.
562             throw new UnsupportedOperationException();
563         }
564 
565         /* (non-Javadoc)
566          * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet)
567          */
568         public BDD exist(BDDVarSet var) {
569             CUDDBDD c = (CUDDBDD) ((BDDVarSet.DefaultImpl) var).b;
570             long b = exist0(_ddnode_ptr, c._ddnode_ptr);
571             return new CUDDBDD(b);
572         }
573         private static native long exist0(long b, long c);
574 
575         /* (non-Javadoc)
576          * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet)
577          */
578         public BDD forAll(BDDVarSet var) {
579             CUDDBDD c = (CUDDBDD) ((BDDVarSet.DefaultImpl) var).b;
580             long b = forAll0(_ddnode_ptr, c._ddnode_ptr);
581             return new CUDDBDD(b);
582         }
583         private static native long forAll0(long b, long c);
584 
585         /* (non-Javadoc)
586          * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet)
587          */
588         public BDD unique(BDDVarSet var) {
589             // TODO Implement this.
590             throw new UnsupportedOperationException();
591         }
592 
593         /* (non-Javadoc)
594          * @see net.sf.javabdd.BDD#restrict(net.sf.javabdd.BDD)
595          */
596         public BDD restrict(BDD var) {
597             CUDDBDD c = (CUDDBDD) var;
598             long b = restrict0(_ddnode_ptr, c._ddnode_ptr);
599             return new CUDDBDD(b);
600         }
601         private static native long restrict0(long b, long var);
602         
603         /* (non-Javadoc)
604          * @see net.sf.javabdd.BDD#restrictWith(net.sf.javabdd.BDD)
605          */
606         public BDD restrictWith(BDD var) {
607             CUDDBDD c = (CUDDBDD) var;
608             long b = restrict0(_ddnode_ptr, c._ddnode_ptr);
609             addRef(b);
610             delRef(_ddnode_ptr);
611             if (this != c) {
612                 delRef(c._ddnode_ptr);
613                 c._ddnode_ptr = INVALID_BDD;
614             }
615             _ddnode_ptr = b;
616             return this;
617         }
618         
619         /* (non-Javadoc)
620          * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet)
621          */
622         public BDD simplify(BDDVarSet d) {
623             // TODO Implement this.
624             throw new UnsupportedOperationException();
625         }
626 
627         /* (non-Javadoc)
628          * @see net.sf.javabdd.BDD#support()
629          */
630         public BDDVarSet support() {
631             long b = support0(_ddnode_ptr);
632             return new BDDVarSet.DefaultImpl(new CUDDBDD(b));
633         }
634         private static native long support0(long b);
635         
636         /* (non-Javadoc)
637          * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp)
638          */
639         public BDD apply(BDD that, BDDFactory.BDDOp opr) {
640             CUDDBDD c = (CUDDBDD) that;
641             long b = apply0(_ddnode_ptr, c._ddnode_ptr, opr.id);
642             return new CUDDBDD(b);
643         }
644         private static native long apply0(long b, long c, int opr);
645         
646         /* (non-Javadoc)
647          * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp)
648          */
649         public BDD applyWith(BDD that, BDDFactory.BDDOp opr) {
650             CUDDBDD c = (CUDDBDD) that;
651             long b = apply0(_ddnode_ptr, c._ddnode_ptr, opr.id);
652             addRef(b);
653             delRef(_ddnode_ptr);
654             if (this != c) {
655                 delRef(c._ddnode_ptr);
656                 c._ddnode_ptr = INVALID_BDD;
657             }
658             _ddnode_ptr = b;
659             return this;
660         }
661         
662         /* (non-Javadoc)
663          * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
664          */
665         public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) {
666             // TODO Implement this.
667             throw new UnsupportedOperationException();
668         }
669 
670         /* (non-Javadoc)
671          * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
672          */
673         public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) {
674             // TODO Implement this.
675             throw new UnsupportedOperationException();
676         }
677 
678         /* (non-Javadoc)
679          * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
680          */
681         public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) {
682             // TODO Implement this.
683             throw new UnsupportedOperationException();
684         }
685 
686         /* (non-Javadoc)
687          * @see net.sf.javabdd.BDD#satOne()
688          */
689         public BDD satOne() {
690             long b = satOne0(_ddnode_ptr);
691             return new CUDDBDD(b);
692         }
693         private static native long satOne0(long b);
694         
695         /* (non-Javadoc)
696          * @see net.sf.javabdd.BDD#fullSatOne()
697          */
698         public BDD fullSatOne() {
699             // TODO Implement this.
700             throw new UnsupportedOperationException();
701         }
702 
703         /* (non-Javadoc)
704          * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean)
705          */
706         public BDD satOne(BDDVarSet var, boolean pol) {
707             // TODO Implement this.
708             throw new UnsupportedOperationException();
709         }
710 
711         /* (non-Javadoc)
712          * @see net.sf.javabdd.BDD#nodeCount()
713          */
714         public int nodeCount() {
715             return nodeCount0(_ddnode_ptr);
716         }
717         private static native int nodeCount0(long b);
718         
719         /* (non-Javadoc)
720          * @see net.sf.javabdd.BDD#pathCount()
721          */
722         public double pathCount() {
723             return pathCount0(_ddnode_ptr);
724         }
725         private static native double pathCount0(long b);
726         
727         /* (non-Javadoc)
728          * @see net.sf.javabdd.BDD#satCount()
729          */
730         public double satCount() {
731             return satCount0(_ddnode_ptr);
732         }
733         private static native double satCount0(long b);
734         
735         /* (non-Javadoc)
736          * @see net.sf.javabdd.BDD#varProfile()
737          */
738         public int[] varProfile() {
739             // TODO Implement this.
740             throw new UnsupportedOperationException();
741         }
742 
743         private static native void addRef(long p);
744 
745         private static native void delRef(long p);
746         
747         static final boolean USE_FINALIZER = false;
748         
749         /* Finalizer runs in different thread, and CUDD is not thread-safe.
750          * Also, the existence of any finalize() method hurts performance
751          * considerably.
752          */
753         /* (non-Javadoc)
754          * @see java.lang.Object#finalize()
755          */
756         /*
757         protected void finalize() throws Throwable {
758             super.finalize();
759             if (USE_FINALIZER) {
760                 if (false && _ddnode_ptr >= 0) {
761                     System.out.println("BDD not freed! "+System.identityHashCode(this));
762                 }
763                 this.free();
764             }
765         }
766         */
767         
768         /* (non-Javadoc)
769          * @see net.sf.javabdd.BDD#free()
770          */
771         public void free() {
772             delRef(_ddnode_ptr);
773             _ddnode_ptr = INVALID_BDD;
774         }
775         
776         /* (non-Javadoc)
777          * @see net.sf.javabdd.BDD#veccompose(net.sf.javabdd.BDDPairing)
778          */
779         public BDD veccompose(BDDPairing pair) {
780             CUDDBDDPairing p = (CUDDBDDPairing) pair;
781             long b = veccompose0(_ddnode_ptr, p._ptr);
782             return new CUDDBDD(b);
783         }
784         private static native long veccompose0(long b, long p);
785         
786         /* (non-Javadoc)
787          * @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing)
788          */
789         public BDD replace(BDDPairing pair) {
790             CUDDBDDPairing p = (CUDDBDDPairing) pair;
791             long b = replace0(_ddnode_ptr, p._ptr);
792             return new CUDDBDD(b);
793         }
794         private static native long replace0(long b, long p);
795         
796         /* (non-Javadoc)
797          * @see net.sf.javabdd.BDD#replaceWith(net.sf.javabdd.BDDPairing)
798          */
799         public BDD replaceWith(BDDPairing pair) {
800             CUDDBDDPairing p = (CUDDBDDPairing) pair;
801             long b = replace0(_ddnode_ptr, p._ptr);
802             addRef(b);
803             delRef(_ddnode_ptr);
804             _ddnode_ptr = b;
805             return this;
806         }
807 
808         /* (non-Javadoc)
809          * @see net.sf.javabdd.BDD#equals(net.sf.javabdd.BDD)
810          */
811         public boolean equals(BDD that) {
812             return this._ddnode_ptr == ((CUDDBDD) that)._ddnode_ptr;
813         }
814 
815         /* (non-Javadoc)
816          * @see net.sf.javabdd.BDD#hashCode()
817          */
818         public int hashCode() {
819             return (int) this._ddnode_ptr;
820         }
821 
822         /* (non-Javadoc)
823          * @see net.sf.javabdd.BDD#toVarSet()
824          */
825         public BDDVarSet toVarSet() {
826             return new BDDVarSet.DefaultImpl(new CUDDBDD(this._ddnode_ptr));
827         }
828 
829     }
830     
831     /* (non-Javadoc)
832      * An implementation of a BDDDomain, used by the CUDD interface.
833      */
834     private static class CUDDBDDDomain extends BDDDomain {
835 
836         private CUDDBDDDomain(int index, BigInteger range) {
837             super(index, range);
838         }
839 
840         /* (non-Javadoc)
841          * @see net.sf.javabdd.BDDDomain#getFactory()
842          */
843         public BDDFactory getFactory() {
844             return INSTANCE;
845         }
846         
847     }
848 
849     /* (non-Javadoc)
850      * An implementation of a BDDPairing, used by the CUDD interface.
851      */
852     private static class CUDDBDDPairing extends BDDPairing {
853 
854         long _ptr;
855 
856         private CUDDBDDPairing() {
857             _ptr = alloc();
858         }
859 
860         private static native long alloc();
861 
862         /* (non-Javadoc)
863          * @see net.sf.javabdd.BDDPairing#set(int, int)
864          */
865         public void set(int oldvar, int newvar) {
866             set0(_ptr, oldvar, newvar);
867         }
868         private static native void set0(long p, int oldvar, int newvar);
869 
870         /* (non-Javadoc)
871          * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD)
872          */
873         public void set(int oldvar, BDD newvar) {
874             CUDDBDD c = (CUDDBDD) newvar;
875             set2(_ptr, oldvar, c._ddnode_ptr);
876         }
877         private static native void set2(long p, int oldvar, long newbdd);
878         
879         /* (non-Javadoc)
880          * @see net.sf.javabdd.BDDPairing#reset()
881          */
882         public void reset() {
883             reset0(_ptr);
884         }
885         private static native void reset0(long ptr);
886         
887         /***
888          * Free the memory allocated for this pair.
889          */
890         private static native void free0(long ptr);
891     }
892 
893     /* (non-Javadoc)
894      * @see net.sf.javabdd.BDDFactory#createBitVector(int)
895      */
896     protected BDDBitVector createBitVector(int a) {
897         return new CUDDBDDBitVector(a);
898     }
899     
900     /* (non-Javadoc)
901      * An implementation of a BDDBitVector, used by the CUDD interface.
902      */
903     private static class CUDDBDDBitVector extends BDDBitVector {
904 
905         private CUDDBDDBitVector(int a) {
906             super(a);
907         }
908 
909         public BDDFactory getFactory() { return INSTANCE; }
910 
911     }
912     
913     public static void main(String[] args) {
914         BDDFactory bdd = init(1000000, 100000);
915         
916         System.out.println("One: "+CUDDFactory.one);
917         System.out.println("Zero: "+CUDDFactory.zero);
918         
919         BDDDomain[] doms = bdd.extDomain(new int[] {50, 10, 15, 20, 15});
920         
921         BDD b = bdd.one();
922         for (int i=0; i<doms.length-1; ++i) {
923             b.andWith(doms[i].ithVar(i));
924         }
925         
926         for (int i=0; i<bdd.numberOfDomains(); ++i) {
927             BDDDomain d = bdd.getDomain(i);
928             int[] ivar = d.vars();
929             System.out.print("Domain #"+i+":");
930             for (int j=0; j<ivar.length; ++j) {
931                 System.out.print(' ');
932                 System.out.print(j);
933                 System.out.print(':');
934                 System.out.print(ivar[j]);
935             }
936             System.out.println();
937         }
938         
939         BDDPairing p = bdd.makePair(doms[2], doms[doms.length-1]);
940         System.out.println("Pairing: "+p);
941         
942         System.out.println("Before replace(): "+b);
943         BDD c = b.replace(p);
944         System.out.println("After replace(): "+c);
945         
946         c.printDot();
947     }
948 
949     public static final String REVISION = "$Revision: 454 $";
950     
951     /* (non-Javadoc)
952      * @see net.sf.javabdd.BDDFactory#getVersion()
953      */
954     public String getVersion() {
955         return "CUDD "+REVISION.substring(11, REVISION.length()-2);
956     }
957     
958 }