View Javadoc

1   // CALFactory.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 CAL library through a
11   * native interface.  You can use this by calling the "CALFactory.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>CAL 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 CAL 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: CALFactory.java 454 2006-07-17 03:45:42Z joewhaley $
36   */
37  public class CALFactory extends BDDFactory {
38  
39      public static BDDFactory init(int nodenum, int cachesize) {
40          CALFactory f = new CALFactory();
41          f.initialize(nodenum/256, cachesize);
42          return f;
43      }
44      
45      private static CALFactory INSTANCE;
46      
47      static {
48          String libname = "cal";
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 CALFactory() {}
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 CALBDD(zero);
73      }
74  
75      /* (non-Javadoc)
76       * @see net.sf.javabdd.BDDFactory#one()
77       */
78      public BDD one() {
79          return new CALBDD(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: CALFactory 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#setMinFreeNodes(double)
136      */
137     public double setMinFreeNodes(double x) {
138         // TODO Implement this.
139         System.err.println("Warning: setMinFreeNodes() not yet implemented");
140         return 0.;
141     }
142 
143     /* (non-Javadoc)
144      * @see net.sf.javabdd.BDDFactory#setMaxIncrease(int)
145      */
146     public int setMaxIncrease(int x) {
147         // TODO Implement this.
148         System.err.println("Warning: setMaxIncrease() not yet implemented");
149         return 50000;
150     }
151 
152     /* (non-Javadoc)
153      * @see net.sf.javabdd.BDDFactory#setCacheRatio(double)
154      */
155     public double setCacheRatio(double x) {
156         // TODO Implement this.
157         System.err.println("Warning: setCacheRatio() not yet implemented");
158         return 0;
159     }
160 
161     /* (non-Javadoc)
162      * @see net.sf.javabdd.BDDFactory#varNum()
163      */
164     public int varNum() {
165         return varNum0();
166     }
167     private static native int varNum0();
168 
169     /* (non-Javadoc)
170      * @see net.sf.javabdd.BDDFactory#setVarNum(int)
171      */
172     public int setVarNum(int num) {
173         return setVarNum0(num);
174     }
175     private static native int setVarNum0(int num);
176 
177     /* (non-Javadoc)
178      * @see net.sf.javabdd.BDDFactory#duplicateVar(int)
179      */
180     public int duplicateVar(int var) {
181         // TODO Implement this.
182         throw new UnsupportedOperationException();
183     }
184     
185     /* (non-Javadoc)
186      * @see net.sf.javabdd.BDDFactory#ithVar(int)
187      */
188     public BDD ithVar(int var) {
189         long id = ithVar0(var);
190         return new CALBDD(id);
191     }
192     private static native long ithVar0(int var);
193 
194     /* (non-Javadoc)
195      * @see net.sf.javabdd.BDDFactory#nithVar(int)
196      */
197     public BDD nithVar(int var) {
198         BDD b = ithVar(var);
199         BDD c = b.not(); b.free();
200         return c;
201     }
202 
203     /* (non-Javadoc)
204      * @see net.sf.javabdd.BDDFactory#swapVar(int, int)
205      */
206     public void swapVar(int v1, int v2) {
207         // TODO Implement this.
208         throw new UnsupportedOperationException();
209     }
210 
211     /* (non-Javadoc)
212      * @see net.sf.javabdd.BDDFactory#makePair()
213      */
214     public BDDPairing makePair() {
215         return new CALBDDPairing();
216     }
217 
218     /* (non-Javadoc)
219      * @see net.sf.javabdd.BDDFactory#printAll()
220      */
221     public void printAll() {
222         // TODO Implement this.
223         throw new UnsupportedOperationException();
224     }
225 
226     /* (non-Javadoc)
227      * @see net.sf.javabdd.BDDFactory#printTable(net.sf.javabdd.BDD)
228      */
229     public void printTable(BDD b) {
230         // TODO Implement this.
231         throw new UnsupportedOperationException();
232     }
233 
234     /* (non-Javadoc)
235      * @see net.sf.javabdd.BDDFactory#level2Var(int)
236      */
237     public int level2Var(int level) {
238         return level2Var0(level);
239     }
240     private static native int level2Var0(int level);
241 
242     /* (non-Javadoc)
243      * @see net.sf.javabdd.BDDFactory#var2Level(int)
244      */
245     public int var2Level(int var) {
246         return var2Level0(var);
247     }
248     private static native int var2Level0(int var);
249 
250     /* (non-Javadoc)
251      * @see net.sf.javabdd.BDDFactory#reorder(net.sf.javabdd.BDDFactory.ReorderMethod)
252      */
253     public void reorder(ReorderMethod m) {
254         // TODO Implement this.
255         throw new UnsupportedOperationException();
256     }
257 
258     /* (non-Javadoc)
259      * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod)
260      */
261     public void autoReorder(ReorderMethod method) {
262         // TODO Implement this.
263         throw new UnsupportedOperationException();
264     }
265 
266     /* (non-Javadoc)
267      * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod, int)
268      */
269     public void autoReorder(ReorderMethod method, int max) {
270         // TODO Implement this.
271         throw new UnsupportedOperationException();
272     }
273 
274     /* (non-Javadoc)
275      * @see net.sf.javabdd.BDDFactory#getReorderMethod()
276      */
277     public ReorderMethod getReorderMethod() {
278         // TODO Implement this.
279         throw new UnsupportedOperationException();
280     }
281 
282     /* (non-Javadoc)
283      * @see net.sf.javabdd.BDDFactory#getReorderTimes()
284      */
285     public int getReorderTimes() {
286         // TODO Implement this.
287         throw new UnsupportedOperationException();
288     }
289 
290     /* (non-Javadoc)
291      * @see net.sf.javabdd.BDDFactory#disableReorder()
292      */
293     public void disableReorder() {
294         // TODO Implement this.
295         System.err.println("Warning: disableReorder() not yet implemented");
296     }
297 
298     /* (non-Javadoc)
299      * @see net.sf.javabdd.BDDFactory#enableReorder()
300      */
301     public void enableReorder() {
302         // TODO Implement this.
303         System.err.println("Warning: enableReorder() not yet implemented");
304     }
305 
306     /* (non-Javadoc)
307      * @see net.sf.javabdd.BDDFactory#reorderVerbose(int)
308      */
309     public int reorderVerbose(int v) {
310         // TODO Implement this.
311         throw new UnsupportedOperationException();
312     }
313 
314     /* (non-Javadoc)
315      * @see net.sf.javabdd.BDDFactory#setVarOrder(int[])
316      */
317     public void setVarOrder(int[] neworder) {
318         setVarOrder0(neworder);
319     }
320     private static native void setVarOrder0(int[] neworder);
321 
322     /* (non-Javadoc)
323      * @see net.sf.javabdd.BDDFactory#addVarBlock(net.sf.javabdd.BDD, boolean)
324      */
325     public void addVarBlock(BDD var, boolean fixed) {
326         // TODO Implement this.
327         throw new UnsupportedOperationException();
328     }
329 
330     /* (non-Javadoc)
331      * @see net.sf.javabdd.BDDFactory#addVarBlock(int, int, boolean)
332      */
333     public void addVarBlock(int first, int last, boolean fixed) {
334         // TODO Implement this.
335         throw new UnsupportedOperationException();
336     }
337 
338     /* (non-Javadoc)
339      * @see net.sf.javabdd.BDDFactory#varBlockAll()
340      */
341     public void varBlockAll() {
342         // TODO Implement this.
343         throw new UnsupportedOperationException();
344     }
345 
346     /* (non-Javadoc)
347      * @see net.sf.javabdd.BDDFactory#clearVarBlocks()
348      */
349     public void clearVarBlocks() {
350         // TODO Implement this.
351         throw new UnsupportedOperationException();
352     }
353 
354     /* (non-Javadoc)
355      * @see net.sf.javabdd.BDDFactory#printOrder()
356      */
357     public void printOrder() {
358         // TODO Implement this.
359         throw new UnsupportedOperationException();
360     }
361 
362     /* (non-Javadoc)
363      * @see net.sf.javabdd.BDDFactory#nodeCount(java.util.Collection)
364      */
365     public int nodeCount(Collection r) {
366         // TODO Implement this.
367         throw new UnsupportedOperationException();
368     }
369 
370     /* (non-Javadoc)
371      * @see net.sf.javabdd.BDDFactory#getNodeTableSize()
372      */
373     public int getNodeTableSize() {
374         // TODO Implement this.
375         throw new UnsupportedOperationException();
376     }
377 
378     /* (non-Javadoc)
379      * @see net.sf.javabdd.BDDFactory#getCacheSize()
380      */
381     public int getCacheSize() {
382         // TODO Implement this.
383         throw new UnsupportedOperationException();
384     }
385     
386     /* (non-Javadoc)
387      * @see net.sf.javabdd.BDDFactory#getNodeNum()
388      */
389     public int getNodeNum() {
390         // TODO Implement this.
391         throw new UnsupportedOperationException();
392     }
393 
394     /* (non-Javadoc)
395      * @see net.sf.javabdd.BDDFactory#reorderGain()
396      */
397     public int reorderGain() {
398         // TODO Implement this.
399         throw new UnsupportedOperationException();
400     }
401 
402     /* (non-Javadoc)
403      * @see net.sf.javabdd.BDDFactory#printStat()
404      */
405     public void printStat() {
406         // TODO Implement this.
407         throw new UnsupportedOperationException();
408     }
409 
410     /* (non-Javadoc)
411      * @see net.sf.javabdd.BDDFactory#createDomain(int, BigInteger)
412      */
413     protected BDDDomain createDomain(int a, BigInteger b) {
414         return new CALBDDDomain(a, b);
415     }
416 
417     /* (non-Javadoc)
418      * An implementation of a BDD class, used by the CAL interface.
419      */
420     private static class CALBDD extends BDD {
421 
422         /*** The pointer used by the BDD library. */
423         private long _ddnode_ptr;
424         
425         /*** An invalid id, for use in invalidating BDDs. */
426         static final long INVALID_BDD = -1;
427         
428         private CALBDD(long ddnode) {
429             this._ddnode_ptr = ddnode;
430             addRef(ddnode);
431         }
432 
433         /* (non-Javadoc)
434          * @see net.sf.javabdd.BDD#getFactory()
435          */
436         public BDDFactory getFactory() {
437             return INSTANCE;
438         }
439         
440         /* (non-Javadoc)
441          * @see net.sf.javabdd.BDD#isZero()
442          */
443         public boolean isZero() {
444             return this._ddnode_ptr == zero;
445         }
446 
447         /* (non-Javadoc)
448          * @see net.sf.javabdd.BDD#isOne()
449          */
450         public boolean isOne() {
451             return this._ddnode_ptr == one;
452         }
453 
454         /* (non-Javadoc)
455          * @see net.sf.javabdd.BDD#var()
456          */
457         public int var() {
458             return var0(_ddnode_ptr);
459         }
460         private static native int var0(long b);
461         
462         /* (non-Javadoc)
463          * @see net.sf.javabdd.BDD#high()
464          */
465         public BDD high() {
466             long b = high0(_ddnode_ptr);
467             return new CALBDD(b);
468         }
469         private static native long high0(long b);
470         
471         /* (non-Javadoc)
472          * @see net.sf.javabdd.BDD#low()
473          */
474         public BDD low() {
475             long b = low0(_ddnode_ptr);
476             return new CALBDD(b);
477         }
478         private static native long low0(long b);
479         
480         /* (non-Javadoc)
481          * @see net.sf.javabdd.BDD#id()
482          */
483         public BDD id() {
484             return new CALBDD(_ddnode_ptr);
485         }
486 
487         /* (non-Javadoc)
488          * @see net.sf.javabdd.BDD#not()
489          */
490         public BDD not() {
491             long b = not0(_ddnode_ptr);
492             return new CALBDD(b);
493         }
494         private static native long not0(long b);
495         
496         /* (non-Javadoc)
497          * @see net.sf.javabdd.BDD#ite(net.sf.javabdd.BDD, net.sf.javabdd.BDD)
498          */
499         public BDD ite(BDD thenBDD, BDD elseBDD) {
500             CALBDD c = (CALBDD) thenBDD;
501             CALBDD d = (CALBDD) elseBDD;
502             long b = ite0(_ddnode_ptr, c._ddnode_ptr, d._ddnode_ptr);
503             return new CALBDD(b);
504         }
505         private static native long ite0(long b, long c, long d);
506         
507         /* (non-Javadoc)
508          * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD, net.sf.javabdd.BDDVarSet)
509          */
510         public BDD relprod(BDD that, BDDVarSet var) {
511             CALBDD c = (CALBDD) that;
512             CALBDD d = (CALBDD) ((BDDVarSet.DefaultImpl) var).b;
513             long b = relprod0(_ddnode_ptr, c._ddnode_ptr, d._ddnode_ptr);
514             return new CALBDD(b);
515         }
516         private static native long relprod0(long b, long c, long d);
517         
518         /* (non-Javadoc)
519          * @see net.sf.javabdd.BDD#compose(net.sf.javabdd.BDD, int)
520          */
521         public BDD compose(BDD that, int var) {
522             CALBDD c = (CALBDD) that;
523             long b = compose0(_ddnode_ptr, c._ddnode_ptr, var);
524             return new CALBDD(b);
525         }
526         private static native long compose0(long b, long c, int var);
527 
528         /* (non-Javadoc)
529          * @see net.sf.javabdd.BDD#constrain(net.sf.javabdd.BDD)
530          */
531         public BDD constrain(BDD that) {
532             // TODO Implement this.
533             throw new UnsupportedOperationException();
534         }
535 
536         /* (non-Javadoc)
537          * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet)
538          */
539         public BDD exist(BDDVarSet var) {
540             // TODO Implement this.
541             throw new UnsupportedOperationException();
542         }
543 
544         /* (non-Javadoc)
545          * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDDVarSet)
546          */
547         public BDD forAll(BDDVarSet var) {
548             // TODO Implement this.
549             throw new UnsupportedOperationException();
550         }
551 
552         /* (non-Javadoc)
553          * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDDVarSet)
554          */
555         public BDD unique(BDDVarSet var) {
556             // TODO Implement this.
557             throw new UnsupportedOperationException();
558         }
559 
560         /* (non-Javadoc)
561          * @see net.sf.javabdd.BDD#restrict(net.sf.javabdd.BDD)
562          */
563         public BDD restrict(BDD var) {
564             CALBDD c = (CALBDD) var;
565             long b = restrict0(_ddnode_ptr, c._ddnode_ptr);
566             return new CALBDD(b);
567         }
568         private static native long restrict0(long b, long var);
569         
570         /* (non-Javadoc)
571          * @see net.sf.javabdd.BDD#restrictWith(net.sf.javabdd.BDD)
572          */
573         public BDD restrictWith(BDD var) {
574             CALBDD c = (CALBDD) var;
575             long b = restrict0(_ddnode_ptr, c._ddnode_ptr);
576             addRef(b);
577             delRef(_ddnode_ptr);
578             if (this != c) {
579                 delRef(c._ddnode_ptr);
580                 c._ddnode_ptr = INVALID_BDD;
581             }
582             _ddnode_ptr = b;
583             return this;
584         }
585         
586         /* (non-Javadoc)
587          * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet)
588          */
589         public BDD simplify(BDDVarSet d) {
590             // TODO Implement this.
591             throw new UnsupportedOperationException();
592         }
593 
594         /* (non-Javadoc)
595          * @see net.sf.javabdd.BDD#support()
596          */
597         public BDDVarSet support() {
598             long b = support0(_ddnode_ptr);
599             return new BDDVarSet.DefaultImpl(new CALBDD(b));
600         }
601         private static native long support0(long b);
602         
603         /* (non-Javadoc)
604          * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp)
605          */
606         public BDD apply(BDD that, BDDFactory.BDDOp opr) {
607             CALBDD c = (CALBDD) that;
608             long b = apply0(_ddnode_ptr, c._ddnode_ptr, opr.id);
609             return new CALBDD(b);
610         }
611         private static native long apply0(long b, long c, int opr);
612         
613         /* (non-Javadoc)
614          * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp)
615          */
616         public BDD applyWith(BDD that, BDDFactory.BDDOp opr) {
617             CALBDD c = (CALBDD) that;
618             long b = apply0(_ddnode_ptr, c._ddnode_ptr, opr.id);
619             addRef(b);
620             delRef(_ddnode_ptr);
621             if (this != c) {
622                 delRef(c._ddnode_ptr);
623                 c._ddnode_ptr = INVALID_BDD;
624             }
625             _ddnode_ptr = b;
626             return this;
627         }
628         
629         /* (non-Javadoc)
630          * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
631          */
632         public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) {
633             // TODO Implement this.
634             throw new UnsupportedOperationException();
635         }
636 
637         /* (non-Javadoc)
638          * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
639          */
640         public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) {
641             // TODO Implement this.
642             throw new UnsupportedOperationException();
643         }
644 
645         /* (non-Javadoc)
646          * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD, net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
647          */
648         public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) {
649             // TODO Implement this.
650             throw new UnsupportedOperationException();
651         }
652 
653         /* (non-Javadoc)
654          * @see net.sf.javabdd.BDD#satOne()
655          */
656         public BDD satOne() {
657             long b = satOne0(_ddnode_ptr);
658             return new CALBDD(b);
659         }
660         private static native long satOne0(long b);
661         
662         /* (non-Javadoc)
663          * @see net.sf.javabdd.BDD#fullSatOne()
664          */
665         public BDD fullSatOne() {
666             // TODO Implement this.
667             throw new UnsupportedOperationException();
668         }
669 
670         /* (non-Javadoc)
671          * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean)
672          */
673         public BDD satOne(BDDVarSet var, boolean pol) {
674             // TODO Implement this.
675             throw new UnsupportedOperationException();
676         }
677 
678         /* (non-Javadoc)
679          * @see net.sf.javabdd.BDD#nodeCount()
680          */
681         public int nodeCount() {
682             return nodeCount0(_ddnode_ptr);
683         }
684         private static native int nodeCount0(long b);
685         
686         /* (non-Javadoc)
687          * @see net.sf.javabdd.BDD#pathCount()
688          */
689         public double pathCount() {
690             return pathCount0(_ddnode_ptr);
691         }
692         private static native double pathCount0(long b);
693         
694         /* (non-Javadoc)
695          * @see net.sf.javabdd.BDD#satCount()
696          */
697         public double satCount() {
698             return satCount0(_ddnode_ptr);
699         }
700         // TODO: debug CAL satCount.
701         private static native double satCount0(long b);
702         
703         /* (non-Javadoc)
704          * @see net.sf.javabdd.BDD#varProfile()
705          */
706         public int[] varProfile() {
707             // TODO Implement this.
708             throw new UnsupportedOperationException();
709         }
710 
711         private static native void addRef(long p);
712 
713         private static native void delRef(long p);
714         
715         static final boolean USE_FINALIZER = false;
716         
717         /* Finalizer runs in different thread, and CAL is not thread-safe.
718          * Also, the existence of any finalize() method hurts performance
719          * considerably.
720          */
721         /* (non-Javadoc)
722          * @see java.lang.Object#finalize()
723          */
724         /*
725         protected void finalize() throws Throwable {
726             super.finalize();
727             if (USE_FINALIZER) {
728                 if (false && _ddnode_ptr >= 0) {
729                     System.out.println("BDD not freed! "+System.identityHashCode(this));
730                 }
731                 this.free();
732             }
733         }
734         */
735         
736         /* (non-Javadoc)
737          * @see net.sf.javabdd.BDD#free()
738          */
739         public void free() {
740             delRef(_ddnode_ptr);
741             _ddnode_ptr = INVALID_BDD;
742         }
743         
744         /* (non-Javadoc)
745          * @see net.sf.javabdd.BDD#veccompose(net.sf.javabdd.BDDPairing)
746          */
747         public BDD veccompose(BDDPairing pair) {
748             CALBDDPairing p = (CALBDDPairing) pair;
749             long b = veccompose0(_ddnode_ptr, p._ptr);
750             return new CALBDD(b);
751         }
752         private static native long veccompose0(long b, long p);
753         
754         /* (non-Javadoc)
755          * @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing)
756          */
757         public BDD replace(BDDPairing pair) {
758             CALBDDPairing p = (CALBDDPairing) pair;
759             long b = replace0(_ddnode_ptr, p._ptr);
760             return new CALBDD(b);
761         }
762         private static native long replace0(long b, long p);
763         
764         /* (non-Javadoc)
765          * @see net.sf.javabdd.BDD#replaceWith(net.sf.javabdd.BDDPairing)
766          */
767         public BDD replaceWith(BDDPairing pair) {
768             CALBDDPairing p = (CALBDDPairing) pair;
769             long b = replace0(_ddnode_ptr, p._ptr);
770             addRef(b);
771             delRef(_ddnode_ptr);
772             _ddnode_ptr = b;
773             return this;
774         }
775 
776         /* (non-Javadoc)
777          * @see net.sf.javabdd.BDD#equals(net.sf.javabdd.BDD)
778          */
779         public boolean equals(BDD that) {
780             return this._ddnode_ptr == ((CALBDD) that)._ddnode_ptr;
781         }
782 
783         /* (non-Javadoc)
784          * @see net.sf.javabdd.BDD#hashCode()
785          */
786         public int hashCode() {
787             return (int) this._ddnode_ptr;
788         }
789 
790         public BDDVarSet toVarSet() {
791             return new BDDVarSet.DefaultImpl(new CALBDD(this._ddnode_ptr));
792         }
793 
794     }
795     
796     /* (non-Javadoc)
797      * An implementation of a BDDDomain, used by the CAL interface.
798      */
799     private static class CALBDDDomain extends BDDDomain {
800 
801         private CALBDDDomain(int index, BigInteger range) {
802             super(index, range);
803         }
804 
805         /* (non-Javadoc)
806          * @see net.sf.javabdd.BDDDomain#getFactory()
807          */
808         public BDDFactory getFactory() {
809             return INSTANCE;
810         }
811         
812     }
813 
814     /* (non-Javadoc)
815      * An implementation of a BDDPairing, used by the CAL interface.
816      */
817     private static class CALBDDPairing extends BDDPairing {
818 
819         long _ptr;
820 
821         private CALBDDPairing() {
822             _ptr = alloc();
823         }
824 
825         private static native long alloc();
826 
827         /* (non-Javadoc)
828          * @see net.sf.javabdd.BDDPairing#set(int, int)
829          */
830         public void set(int oldvar, int newvar) {
831             set0(_ptr, oldvar, newvar);
832         }
833         private static native void set0(long p, int oldvar, int newvar);
834 
835         /* (non-Javadoc)
836          * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD)
837          */
838         public void set(int oldvar, BDD newvar) {
839             CALBDD c = (CALBDD) newvar;
840             set2(_ptr, oldvar, c._ddnode_ptr);
841         }
842         private static native void set2(long p, int oldvar, long newbdd);
843         
844         /* (non-Javadoc)
845          * @see net.sf.javabdd.BDDPairing#reset()
846          */
847         public void reset() {
848             reset0(_ptr);
849         }
850         private static native void reset0(long ptr);
851         
852         /***
853          * Free the memory allocated for this pair.
854          */
855         private static native void free0(long ptr);
856     }
857 
858     /* (non-Javadoc)
859      * @see net.sf.javabdd.BDDFactory#createBitVector(int)
860      */
861     protected BDDBitVector createBitVector(int a) {
862         return new CALBDDBitVector(a);
863     }
864     
865     /* (non-Javadoc)
866      * An implementation of a BDDBitVector, used by the CAL interface.
867      */
868     private static class CALBDDBitVector extends BDDBitVector {
869 
870         private CALBDDBitVector(int a) {
871             super(a);
872         }
873 
874         public BDDFactory getFactory() { return INSTANCE; }
875 
876     }
877 
878     /* (non-Javadoc)
879      * @see net.sf.javabdd.BDDFactory#setIncreaseFactor(double)
880      */
881     public double setIncreaseFactor(double x) {
882         System.err.println("Warning: setIncreaseFactor() not yet implemented");
883         return 0;
884     }
885 
886     /* (non-Javadoc)
887      * @see net.sf.javabdd.BDDFactory#setNodeTableSize(int)
888      */
889     public int setNodeTableSize(int n) {
890         System.err.println("Warning: setNodeTableSize() not yet implemented");
891         return 0;
892     }
893 
894     /* (non-Javadoc)
895      * @see net.sf.javabdd.BDDFactory#setCacheSize(int)
896      */
897     public int setCacheSize(int n) {
898         System.err.println("Warning: setCacheSize() not yet implemented");
899         return 0;
900     }
901 
902     public static final String REVISION = "$Revision: 454 $";
903     
904     /* (non-Javadoc)
905      * @see net.sf.javabdd.BDDFactory#getVersion()
906      */
907     public String getVersion() {
908         return "CAL "+REVISION.substring(11, REVISION.length()-2);
909     }
910     
911 }