View Javadoc

1   // TestBDDFactory.java, created Aug 2, 2003 10:02:48 PM by joewhaley
2   // Copyright (C) 2003 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.Arrays;
7   import java.util.Collection;
8   import java.util.Iterator;
9   import java.util.LinkedList;
10  import java.io.IOException;
11  import java.math.BigInteger;
12  
13  /***
14   * <p>
15   * This BDD factory is used to test other BDD factories. It is a wrapper around
16   * two BDD factories, and all operations are performed on both factories. It
17   * throws an exception if the results from the two implementations do not match.
18   * </p>
19   * 
20   * @see net.sf.javabdd.BDDFactory
21   * 
22   * @author John Whaley
23   * @version $Id: TestBDDFactory.java 474 2006-12-05 10:58:16Z joewhaley $
24   */
25  public class TestBDDFactory extends BDDFactory {
26      BDDFactory f1, f2;
27  
28      public TestBDDFactory(BDDFactory a, BDDFactory b) {
29          f1 = a;
30          f2 = b;
31      }
32  
33      public static BDDFactory init(int nodenum, int cachesize) {
34          String bdd1 = getProperty("bdd1", "j");
35          String bdd2 = getProperty("bdd2", "micro");
36          BDDFactory a = BDDFactory.init(bdd1, nodenum, cachesize);
37          BDDFactory b = BDDFactory.init(bdd2, nodenum, cachesize);
38          return new TestBDDFactory(a, b);
39      }
40  
41      public static final void assertSame(boolean b, String s) {
42          if (!b) {
43              throw new InternalError(s);
44          }
45      }
46  
47      public static final void assertSame(BDD b1, BDD b2, String s) {
48          if (!b1.toString().equals(b2.toString())) {
49          //if (b1.nodeCount() != b2.nodeCount()) {
50              System.out.println("b1 = " + b1.nodeCount());
51              System.out.println("b2 = " + b2.nodeCount());
52              System.out.println("b1 = " + b1.toString());
53              System.out.println("b2 = " + b2.toString());
54              throw new InternalError(s);
55          }
56      }
57  
58      public static final void assertSame(boolean b, BDD b1, BDD b2, String s) {
59          if (!b) {
60              System.err.println("b1 = " + b1);
61              System.err.println("b2 = " + b2);
62              throw new InternalError(s);
63          }
64      }
65  
66      public static final void assertSame(BDDVarSet b1, BDDVarSet b2, String s) {
67          if (!b1.toString().equals(b2.toString())) {
68              System.out.println("b1 = " + b1.toString());
69              System.out.println("b2 = " + b2.toString());
70              throw new InternalError(s);
71          }
72      }
73  
74      public static final void assertSame(boolean b, BDDVarSet b1, BDDVarSet b2, String s) {
75          if (!b) {
76              System.err.println("b1 = " + b1);
77              System.err.println("b2 = " + b2);
78              throw new InternalError(s);
79          }
80      }
81      private class TestBDD extends BDD {
82          BDD b1, b2;
83  
84          TestBDD(BDD a, BDD b) {
85              this.b1 = a;
86              this.b2 = b;
87              assertSame(a, b, "constructor");
88          }
89  
90          /*
91           * (non-Javadoc)
92           * 
93           * @see net.sf.javabdd.BDD#getFactory()
94           */
95          public BDDFactory getFactory() {
96              return TestBDDFactory.this;
97          }
98  
99          /*
100          * (non-Javadoc)
101          * 
102          * @see net.sf.javabdd.BDD#toVarSet()
103          */
104         public BDDVarSet toVarSet() {
105             return new TestBDDVarSet(b1.toVarSet(), b2.toVarSet());
106         }
107 
108         /*
109          * (non-Javadoc)
110          * 
111          * @see net.sf.javabdd.BDD#isZero()
112          */
113         public boolean isZero() {
114             boolean r1 = b1.isZero();
115             boolean r2 = b2.isZero();
116             assertSame(r1 == r2, b1, b2, "isZero");
117             return r1;
118         }
119 
120         /*
121          * (non-Javadoc)
122          * 
123          * @see net.sf.javabdd.BDD#isOne()
124          */
125         public boolean isOne() {
126             boolean r1 = b1.isOne();
127             boolean r2 = b2.isOne();
128             assertSame(r1 == r2, b1, b2, "isOne");
129             return r1;
130         }
131 
132         /*
133          * (non-Javadoc)
134          * 
135          * @see net.sf.javabdd.BDD#var()
136          */
137         public int var() {
138             int r1 = b1.var();
139             int r2 = b2.var();
140             assertSame(r1 == r2, b1, b2, "var");
141             return r1;
142         }
143 
144         /*
145          * (non-Javadoc)
146          * 
147          * @see net.sf.javabdd.BDD#high()
148          */
149         public BDD high() {
150             BDD r1 = b1.high();
151             BDD r2 = b2.high();
152             return new TestBDD(r1, r2);
153         }
154 
155         /*
156          * (non-Javadoc)
157          * 
158          * @see net.sf.javabdd.BDD#low()
159          */
160         public BDD low() {
161             BDD r1 = b1.low();
162             BDD r2 = b2.low();
163             return new TestBDD(r1, r2);
164         }
165 
166         /*
167          * (non-Javadoc)
168          * 
169          * @see net.sf.javabdd.BDD#id()
170          */
171         public BDD id() {
172             BDD r1 = b1.id();
173             BDD r2 = b2.id();
174             return new TestBDD(r1, r2);
175         }
176 
177         /*
178          * (non-Javadoc)
179          * 
180          * @see net.sf.javabdd.BDD#not()
181          */
182         public BDD not() {
183             BDD r1 = b1.not();
184             BDD r2 = b2.not();
185             return new TestBDD(r1, r2);
186         }
187 
188         /*
189          * (non-Javadoc)
190          * 
191          * @see net.sf.javabdd.BDD#ite(net.sf.javabdd.BDD, net.sf.javabdd.BDD)
192          */
193         public BDD ite(BDD thenBDD, BDD elseBDD) {
194             BDD c1 = ((TestBDD) thenBDD).b1;
195             BDD c2 = ((TestBDD) thenBDD).b2;
196             BDD d1 = ((TestBDD) elseBDD).b1;
197             BDD d2 = ((TestBDD) elseBDD).b2;
198             BDD r1 = b1.ite(c1, d1);
199             BDD r2 = b2.ite(c2, d2);
200             return new TestBDD(r1, r2);
201         }
202 
203         /*
204          * (non-Javadoc)
205          * 
206          * @see net.sf.javabdd.BDD#relprod(net.sf.javabdd.BDD,
207          *      net.sf.javabdd.BDDVarSet)
208          */
209         public BDD relprod(BDD that, BDDVarSet var) {
210             BDD c1 = ((TestBDD) that).b1;
211             BDD c2 = ((TestBDD) that).b2;
212             BDDVarSet d1 = ((TestBDDVarSet) var).b1;
213             BDDVarSet d2 = ((TestBDDVarSet) var).b2;
214             BDD r1 = b1.relprod(c1, d1);
215             BDD r2 = b2.relprod(c2, d2);
216             return new TestBDD(r1, r2);
217         }
218 
219         /*
220          * (non-Javadoc)
221          * 
222          * @see net.sf.javabdd.BDD#compose(net.sf.javabdd.BDD, int)
223          */
224         public BDD compose(BDD g, int var) {
225             BDD c1 = ((TestBDD) g).b1;
226             BDD c2 = ((TestBDD) g).b2;
227             BDD r1 = b1.compose(c1, var);
228             BDD r2 = b2.compose(c2, var);
229             return new TestBDD(r1, r2);
230         }
231 
232         /*
233          * (non-Javadoc)
234          * 
235          * @see net.sf.javabdd.BDD#veccompose(net.sf.javabdd.BDDPairing)
236          */
237         public BDD veccompose(BDDPairing pair) {
238             BDDPairing c1 = ((TestBDDPairing) pair).b1;
239             BDDPairing c2 = ((TestBDDPairing) pair).b2;
240             BDD r1 = b1.veccompose(c1);
241             BDD r2 = b2.veccompose(c2);
242             return new TestBDD(r1, r2);
243         }
244 
245         /*
246          * (non-Javadoc)
247          * 
248          * @see net.sf.javabdd.BDD#constrain(net.sf.javabdd.BDD)
249          */
250         public BDD constrain(BDD that) {
251             BDD c1 = ((TestBDD) that).b1;
252             BDD c2 = ((TestBDD) that).b2;
253             BDD r1 = b1.constrain(c1);
254             BDD r2 = b2.constrain(c2);
255             return new TestBDD(r1, r2);
256         }
257 
258         /*
259          * (non-Javadoc)
260          * 
261          * @see net.sf.javabdd.BDD#exist(net.sf.javabdd.BDDVarSet)
262          */
263         public BDD exist(BDDVarSet var) {
264             BDDVarSet c1 = ((TestBDDVarSet) var).b1;
265             BDDVarSet c2 = ((TestBDDVarSet) var).b2;
266             BDD r1 = b1.exist(c1);
267             BDD r2 = b2.exist(c2);
268             return new TestBDD(r1, r2);
269         }
270 
271         /*
272          * (non-Javadoc)
273          * 
274          * @see net.sf.javabdd.BDD#forAll(net.sf.javabdd.BDD)
275          */
276         public BDD forAll(BDDVarSet var) {
277             BDDVarSet c1 = ((TestBDDVarSet) var).b1;
278             BDDVarSet c2 = ((TestBDDVarSet) var).b2;
279             BDD r1 = b1.forAll(c1);
280             BDD r2 = b2.forAll(c2);
281             return new TestBDD(r1, r2);
282         }
283 
284         /*
285          * (non-Javadoc)
286          * 
287          * @see net.sf.javabdd.BDD#unique(net.sf.javabdd.BDD)
288          */
289         public BDD unique(BDDVarSet var) {
290             BDDVarSet c1 = ((TestBDDVarSet) var).b1;
291             BDDVarSet c2 = ((TestBDDVarSet) var).b2;
292             BDD r1 = b1.unique(c1);
293             BDD r2 = b2.unique(c2);
294             return new TestBDD(r1, r2);
295         }
296 
297         /*
298          * (non-Javadoc)
299          * 
300          * @see net.sf.javabdd.BDD#restrict(net.sf.javabdd.BDD)
301          */
302         public BDD restrict(BDD var) {
303             BDD c1 = ((TestBDD) var).b1;
304             BDD c2 = ((TestBDD) var).b2;
305             BDD r1 = b1.restrict(c1);
306             BDD r2 = b2.restrict(c2);
307             return new TestBDD(r1, r2);
308         }
309 
310         /*
311          * (non-Javadoc)
312          * 
313          * @see net.sf.javabdd.BDD#restrictWith(net.sf.javabdd.BDD)
314          */
315         public BDD restrictWith(BDD var) {
316             BDD c1 = ((TestBDD) var).b1;
317             BDD c2 = ((TestBDD) var).b2;
318             b1.restrictWith(c1);
319             b2.restrictWith(c2);
320             assertSame(b1, b2, "restrict");
321             return this;
322         }
323 
324         /*
325          * (non-Javadoc)
326          * 
327          * @see net.sf.javabdd.BDD#simplify(net.sf.javabdd.BDDVarSet)
328          */
329         public BDD simplify(BDDVarSet d) {
330             BDDVarSet c1 = ((TestBDDVarSet) d).b1;
331             BDDVarSet c2 = ((TestBDDVarSet) d).b2;
332             BDD r1 = b1.simplify(c1);
333             BDD r2 = b2.simplify(c2);
334             return new TestBDD(r1, r2);
335         }
336 
337         /*
338          * (non-Javadoc)
339          * 
340          * @see net.sf.javabdd.BDD#support()
341          */
342         public BDDVarSet support() {
343             BDDVarSet r1 = b1.support();
344             BDDVarSet r2 = b2.support();
345             return new TestBDDVarSet(r1, r2);
346         }
347 
348         /*
349          * (non-Javadoc)
350          * 
351          * @see net.sf.javabdd.BDD#apply(net.sf.javabdd.BDD,
352          *      net.sf.javabdd.BDDFactory.BDDOp)
353          */
354         public BDD apply(BDD that, BDDOp opr) {
355             BDD c1 = ((TestBDD) that).b1;
356             BDD c2 = ((TestBDD) that).b2;
357             BDD r1 = b1.apply(c1, opr);
358             BDD r2 = b2.apply(c2, opr);
359             return new TestBDD(r1, r2);
360         }
361 
362         /*
363          * (non-Javadoc)
364          * 
365          * @see net.sf.javabdd.BDD#applyWith(net.sf.javabdd.BDD,
366          *      net.sf.javabdd.BDDFactory.BDDOp)
367          */
368         public BDD applyWith(BDD that, BDDOp opr) {
369             BDD c1 = ((TestBDD) that).b1;
370             BDD c2 = ((TestBDD) that).b2;
371             b1.applyWith(c1, opr);
372             b2.applyWith(c2, opr);
373             assertSame(b1, b2, "applyWith " + opr);
374             return this;
375         }
376 
377         /*
378          * (non-Javadoc)
379          * 
380          * @see net.sf.javabdd.BDD#applyAll(net.sf.javabdd.BDD,
381          *      net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
382          */
383         public BDD applyAll(BDD that, BDDOp opr, BDDVarSet var) {
384             BDD c1 = ((TestBDD) that).b1;
385             BDD c2 = ((TestBDD) that).b2;
386             BDDVarSet e1 = ((TestBDDVarSet) var).b1;
387             BDDVarSet e2 = ((TestBDDVarSet) var).b2;
388             BDD r1 = b1.applyAll(c1, opr, e1);
389             BDD r2 = b2.applyAll(c2, opr, e2);
390             return new TestBDD(r1, r2);
391         }
392 
393         /*
394          * (non-Javadoc)
395          * 
396          * @see net.sf.javabdd.BDD#applyEx(net.sf.javabdd.BDD,
397          *      net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
398          */
399         public BDD applyEx(BDD that, BDDOp opr, BDDVarSet var) {
400             BDD c1 = ((TestBDD) that).b1;
401             BDD c2 = ((TestBDD) that).b2;
402             BDDVarSet e1 = ((TestBDDVarSet) var).b1;
403             BDDVarSet e2 = ((TestBDDVarSet) var).b2;
404             BDD r1 = b1.applyEx(c1, opr, e1);
405             BDD r2 = b2.applyEx(c2, opr, e2);
406             return new TestBDD(r1, r2);
407         }
408 
409         /*
410          * (non-Javadoc)
411          * 
412          * @see net.sf.javabdd.BDD#applyUni(net.sf.javabdd.BDD,
413          *      net.sf.javabdd.BDDFactory.BDDOp, net.sf.javabdd.BDDVarSet)
414          */
415         public BDD applyUni(BDD that, BDDOp opr, BDDVarSet var) {
416             BDD c1 = ((TestBDD) that).b1;
417             BDD c2 = ((TestBDD) that).b2;
418             BDDVarSet e1 = ((TestBDDVarSet) var).b1;
419             BDDVarSet e2 = ((TestBDDVarSet) var).b2;
420             BDD r1 = b1.applyUni(c1, opr, e1);
421             BDD r2 = b2.applyUni(c2, opr, e2);
422             return new TestBDD(r1, r2);
423         }
424 
425         /*
426          * (non-Javadoc)
427          * 
428          * @see net.sf.javabdd.BDD#satOne()
429          */
430         public BDD satOne() {
431             BDD r1 = b1.satOne();
432             BDD r2 = b2.satOne();
433             return new TestBDD(r1, r2);
434         }
435 
436         /*
437          * (non-Javadoc)
438          * 
439          * @see net.sf.javabdd.BDD#fullSatOne()
440          */
441         public BDD fullSatOne() {
442             BDD r1 = b1.fullSatOne();
443             BDD r2 = b2.fullSatOne();
444             return new TestBDD(r1, r2);
445         }
446 
447         /*
448          * (non-Javadoc)
449          * 
450          * @see net.sf.javabdd.BDD#satOne(net.sf.javabdd.BDDVarSet, boolean)
451          */
452         public BDD satOne(BDDVarSet var, boolean pol) {
453             BDDVarSet c1 = ((TestBDDVarSet) var).b1;
454             BDDVarSet c2 = ((TestBDDVarSet) var).b2;
455             BDD r1 = b1.satOne(c1, pol);
456             BDD r2 = b2.satOne(c2, pol);
457             return new TestBDD(r1, r2);
458         }
459 
460         /*
461          * (non-Javadoc)
462          * 
463          * @see net.sf.javabdd.BDD#replace(net.sf.javabdd.BDDPairing)
464          */
465         public BDD replace(BDDPairing pair) {
466             BDDPairing c1 = ((TestBDDPairing) pair).b1;
467             BDDPairing c2 = ((TestBDDPairing) pair).b2;
468             BDD r1 = b1.replace(c1);
469             BDD r2 = b2.replace(c2);
470             return new TestBDD(r1, r2);
471         }
472 
473         /*
474          * (non-Javadoc)
475          * 
476          * @see net.sf.javabdd.BDD#replaceWith(net.sf.javabdd.BDDPairing)
477          */
478         public BDD replaceWith(BDDPairing pair) {
479             BDDPairing c1 = ((TestBDDPairing) pair).b1;
480             BDDPairing c2 = ((TestBDDPairing) pair).b2;
481             b1.replaceWith(c1);
482             b2.replaceWith(c2);
483             assertSame(b1, b2, "replaceWith");
484             return this;
485         }
486 
487         /*
488          * (non-Javadoc)
489          * 
490          * @see net.sf.javabdd.BDD#printDot()
491          */
492         public void printDot() {
493             // TODO Compare!
494             b1.printDot();
495         }
496 
497         /*
498          * (non-Javadoc)
499          * 
500          * @see net.sf.javabdd.BDD#toString()
501          */
502         public String toString() {
503             // String already checked.
504             return b1.toString();
505         }
506 
507         /*
508          * (non-Javadoc)
509          * 
510          * @see net.sf.javabdd.BDD#toStringWithDomains(net.sf.javabdd.BDD.BDDToString)
511          */
512         public String toStringWithDomains(BDDToString ts) {
513             String s1 = b1.toStringWithDomains(ts);
514             String s2 = b2.toStringWithDomains(ts);
515             assertSame(s1.equals(s2), "toStringWithDomains");
516             return s1;
517         }
518 
519         /*
520          * (non-Javadoc)
521          * 
522          * @see net.sf.javabdd.BDD#allsat()
523          */
524         public AllSatIterator allsat() {
525             return new AllSatIterator(TestBDDFactory.this, false) {
526                 AllSatIterator i1 = b1.allsat();
527                 AllSatIterator i2 = b2.allsat();
528 
529                 public boolean hasNext() {
530                     boolean r1 = i1.hasNext();
531                     boolean r2 = i2.hasNext();
532                     assertSame(r1 == r2, b1, b2, "allsat.hasNext");
533                     return r1;
534                 }
535 
536                 public byte[] nextSat() {
537                     byte[] r1 = i1.nextSat();
538                     byte[] r2 = i2.nextSat();
539                     assertSame(Arrays.equals(r1, r2), b1, b2, "allsat.nextSat");
540                     return r1;
541                 }
542             };
543         }
544 
545         /*
546          * (non-Javadoc)
547          * 
548          * @see net.sf.javabdd.BDD#scanAllVar()
549          */
550         public BigInteger[] scanAllVar() {
551             BigInteger[] r1 = b1.scanAllVar();
552             BigInteger[] r2 = b2.scanAllVar();
553             assertSame(Arrays.equals(r1, r2), b1, b2, "scanAllVar");
554             return r1;
555         }
556 
557         /*
558          * (non-Javadoc)
559          * 
560          * @see net.sf.javabdd.BDD#nodeCount()
561          */
562         public int nodeCount() {
563             int r1 = b1.nodeCount();
564             int r2 = b2.nodeCount();
565             if (false) assertSame(r1 == r2, b1, b2, "nodeCount");
566             return r1;
567         }
568 
569         /*
570          * (non-Javadoc)
571          * 
572          * @see net.sf.javabdd.BDD#pathCount()
573          */
574         public double pathCount() {
575             double r1 = b1.pathCount();
576             double r2 = b2.pathCount();
577             assertSame(r1 == r2, b1, b2, "pathCount");
578             return r1;
579         }
580 
581         /*
582          * (non-Javadoc)
583          * 
584          * @see net.sf.javabdd.BDD#satCount()
585          */
586         public double satCount() {
587             double r1 = b1.satCount();
588             double r2 = b2.satCount();
589             assertSame(r1 == r2, b1, b2, "satCount");
590             return r1;
591         }
592 
593         /*
594          * (non-Javadoc)
595          * 
596          * @see net.sf.javabdd.BDD#varProfile()
597          */
598         public int[] varProfile() {
599             int[] r1 = b1.varProfile();
600             int[] r2 = b2.varProfile();
601             assertSame(Arrays.equals(r1, r2), "varProfile");
602             return r1;
603         }
604 
605         /*
606          * (non-Javadoc)
607          * 
608          * @see net.sf.javabdd.BDD#equals(net.sf.javabdd.BDD)
609          */
610         public boolean equals(BDD that) {
611             BDD c1 = ((TestBDD) that).b1;
612             BDD c2 = ((TestBDD) that).b2;
613             boolean r1 = b1.equals(c1);
614             boolean r2 = b2.equals(c2);
615             assertSame(r1 == r2, b1, b2, "equals");
616             return r1;
617         }
618 
619         /*
620          * (non-Javadoc)
621          * 
622          * @see net.sf.javabdd.BDD#hashCode()
623          */
624         public int hashCode() {
625             // TODO Compare!
626             b1.hashCode();
627             return b2.hashCode();
628         }
629 
630         /*
631          * (non-Javadoc)
632          * 
633          * @see net.sf.javabdd.BDD#free()
634          */
635         public void free() {
636             b1.free();
637             b2.free();
638         }
639     }
640     private class TestBDDVarSet extends BDDVarSet {
641         BDDVarSet b1, b2;
642 
643         TestBDDVarSet(BDDVarSet a, BDDVarSet b) {
644             this.b1 = a;
645             this.b2 = b;
646             assertSame(a, b, "constructor");
647         }
648 
649         public void free() {
650             b1.free();
651             b2.free();
652         }
653 
654         public BDDFactory getFactory() {
655             return TestBDDFactory.this;
656         }
657 
658         public BDD toBDD() {
659             BDD r1 = b1.toBDD();
660             BDD r2 = b2.toBDD();
661             return new TestBDD(r1, r2);
662         }
663 
664         public BDDVarSet id() {
665             BDDVarSet r1 = b1.id();
666             BDDVarSet r2 = b2.id();
667             return new TestBDDVarSet(r1, r2);
668         }
669 
670         public BDDVarSet intersect(BDDVarSet that) {
671             BDDVarSet c1 = ((TestBDDVarSet) that).b1;
672             BDDVarSet c2 = ((TestBDDVarSet) that).b2;
673             BDDVarSet r1 = b1.intersect(c1);
674             BDDVarSet r2 = b2.intersect(c2);
675             return new TestBDDVarSet(r1, r2);
676         }
677 
678         public BDDVarSet intersectWith(BDDVarSet that) {
679             BDDVarSet c1 = ((TestBDDVarSet) that).b1;
680             BDDVarSet c2 = ((TestBDDVarSet) that).b2;
681             b1.intersectWith(c1);
682             b2.intersectWith(c2);
683             assertSame(b1, b2, "intersectWith");
684             return this;
685         }
686 
687         public boolean isEmpty() {
688             boolean r1 = b1.isEmpty();
689             boolean r2 = b2.isEmpty();
690             assertSame(r1 == r2, b1, b2, "isEmpty");
691             return r1;
692         }
693 
694         public int size() {
695             int r1 = b1.size();
696             int r2 = b2.size();
697             assertSame(r1 == r2, b1, b2, "size");
698             return r1;
699         }
700 
701         public int[] toArray() {
702             int[] r1 = b1.toArray();
703             int[] r2 = b2.toArray();
704             assertSame(Arrays.equals(r1, r2), b1, b2, "toArray");
705             return r1;
706         }
707 
708         public int[] toLevelArray() {
709             int[] r1 = b1.toLevelArray();
710             int[] r2 = b2.toLevelArray();
711             assertSame(Arrays.equals(r1, r2), b1, b2, "toLevelArray");
712             return r1;
713         }
714 
715         public BDDVarSet union(BDDVarSet that) {
716             BDDVarSet c1 = ((TestBDDVarSet) that).b1;
717             BDDVarSet c2 = ((TestBDDVarSet) that).b2;
718             BDDVarSet r1 = b1.union(c1);
719             BDDVarSet r2 = b2.union(c2);
720             return new TestBDDVarSet(r1, r2);
721         }
722 
723         public BDDVarSet union(int var) {
724             BDDVarSet r1 = b1.union(var);
725             BDDVarSet r2 = b2.union(var);
726             return new TestBDDVarSet(r1, r2);
727         }
728 
729         public BDDVarSet unionWith(BDDVarSet that) {
730             BDDVarSet c1 = ((TestBDDVarSet) that).b1;
731             BDDVarSet c2 = ((TestBDDVarSet) that).b2;
732             b1.unionWith(c1);
733             b2.unionWith(c2);
734             assertSame(b1, b2, "unionWith");
735             return this;
736         }
737 
738         public BDDVarSet unionWith(int var) {
739             b1.unionWith(var);
740             b2.unionWith(var);
741             assertSame(b1, b2, "unionWith");
742             return this;
743         }
744 
745         public int hashCode() {
746             // TODO Compare!
747             b1.hashCode();
748             return b2.hashCode();
749         }
750 
751         public boolean equals(BDDVarSet that) {
752             BDDVarSet c1 = ((TestBDDVarSet) that).b1;
753             BDDVarSet c2 = ((TestBDDVarSet) that).b2;
754             boolean r1 = b1.equals(c1);
755             boolean r2 = b2.equals(c2);
756             assertSame(r1 == r2, b1, b2, "equals");
757             return r1;
758         }
759     }
760 
761     /*
762      * (non-Javadoc)
763      * 
764      * @see net.sf.javabdd.BDDFactory#zero()
765      */
766     public BDD zero() {
767         return new TestBDD(f1.zero(), f2.zero());
768     }
769 
770     /*
771      * (non-Javadoc)
772      * 
773      * @see net.sf.javabdd.BDDFactory#one()
774      */
775     public BDD one() {
776         return new TestBDD(f1.one(), f2.one());
777     }
778 
779     /*
780      * (non-Javadoc)
781      * 
782      * @see net.sf.javabdd.BDDFactory#universe()
783      */
784     public BDD universe() {
785         return new TestBDD(f1.universe(), f2.universe());
786     }
787 
788     /*
789      * (non-Javadoc)
790      * 
791      * @see net.sf.javabdd.BDDFactory#emptySet()
792      */
793     public BDDVarSet emptySet() {
794         return new TestBDDVarSet(f1.emptySet(), f2.emptySet());
795     }
796 
797     /*
798      * (non-Javadoc)
799      * 
800      * @see net.sf.javabdd.BDDFactory#initialize(int, int)
801      */
802     protected void initialize(int nodenum, int cachesize) {
803         f1.initialize(nodenum, cachesize);
804         f2.initialize(nodenum, cachesize);
805     }
806 
807     /*
808      * (non-Javadoc)
809      * 
810      * @see net.sf.javabdd.BDDFactory#isInitialized()
811      */
812     public boolean isInitialized() {
813         boolean r1 = f1.isInitialized();
814         boolean r2 = f2.isInitialized();
815         assertSame(r1 == r2, "isInitialized");
816         return r1;
817     }
818 
819     /*
820      * (non-Javadoc)
821      * 
822      * @see net.sf.javabdd.BDDFactory#done()
823      */
824     public void done() {
825         f1.done();
826         f2.done();
827     }
828 
829     /*
830      * (non-Javadoc)
831      * 
832      * @see net.sf.javabdd.BDDFactory#setError(int)
833      */
834     public void setError(int code) {
835         f1.setError(code);
836         f2.setError(code);
837     }
838 
839     /*
840      * (non-Javadoc)
841      * 
842      * @see net.sf.javabdd.BDDFactory#clearError()
843      */
844     public void clearError() {
845         f1.clearError();
846         f2.clearError();
847     }
848 
849     /*
850      * (non-Javadoc)
851      * 
852      * @see net.sf.javabdd.BDDFactory#setMaxNodeNum(int)
853      */
854     public int setMaxNodeNum(int size) {
855         int r1 = f1.setMaxNodeNum(size);
856         int r2 = f2.setMaxNodeNum(size);
857         assertSame(r1 == r2, "setMaxNodeNum");
858         return r1;
859     }
860 
861     /*
862      * (non-Javadoc)
863      * 
864      * @see net.sf.javabdd.BDDFactory#setMinFreeNodes(double)
865      */
866     public double setMinFreeNodes(double x) {
867         double r1 = f1.setMinFreeNodes(x);
868         double r2 = f2.setMinFreeNodes(x);
869         assertSame(r1 == r2, "setMinFreeNodes");
870         return r1;
871     }
872 
873     /*
874      * (non-Javadoc)
875      * 
876      * @see net.sf.javabdd.BDDFactory#setIncreaseFactor(double)
877      */
878     public double setIncreaseFactor(double x) {
879         double r1 = f1.setIncreaseFactor(x);
880         double r2 = f2.setIncreaseFactor(x);
881         if (false) assertSame(r1 == r2, "setIncreaseFactor");
882         return r1;
883     }
884 
885     /*
886      * (non-Javadoc)
887      * 
888      * @see net.sf.javabdd.BDDFactory#setMaxIncrease(int)
889      */
890     public int setMaxIncrease(int x) {
891         int r1 = f1.setMaxIncrease(x);
892         int r2 = f2.setMaxIncrease(x);
893         assertSame(r1 == r2, "setMaxIncrease");
894         return r1;
895     }
896 
897     /*
898      * (non-Javadoc)
899      * 
900      * @see net.sf.javabdd.BDDFactory#setCacheRatio(double)
901      */
902     public double setCacheRatio(double x) {
903         double r1 = f1.setCacheRatio(x);
904         double r2 = f2.setCacheRatio(x);
905         assertSame(r1 == r2, "setCacheRatio");
906         return r1;
907     }
908 
909     /*
910      * (non-Javadoc)
911      * 
912      * @see net.sf.javabdd.BDDFactory#setNodeTableSize(int)
913      */
914     public int setNodeTableSize(int size) {
915         int r1 = f1.setNodeTableSize(size);
916         int r2 = f2.setNodeTableSize(size);
917         if (false) assertSame(r1 == r2, "setNodeTableSize");
918         return r1;
919     }
920 
921     /*
922      * (non-Javadoc)
923      * 
924      * @see net.sf.javabdd.BDDFactory#setCacheSize(int)
925      */
926     public int setCacheSize(int size) {
927         int r1 = f1.setCacheSize(size);
928         int r2 = f2.setCacheSize(size);
929         assertSame(r1 == r2, "setCacheSize");
930         return r1;
931     }
932 
933     /*
934      * (non-Javadoc)
935      * 
936      * @see net.sf.javabdd.BDDFactory#varNum()
937      */
938     public int varNum() {
939         int r1 = f1.varNum();
940         int r2 = f2.varNum();
941         assertSame(r1 == r2, "varNum");
942         return r1;
943     }
944 
945     /*
946      * (non-Javadoc)
947      * 
948      * @see net.sf.javabdd.BDDFactory#setVarNum(int)
949      */
950     public int setVarNum(int num) {
951         int r1 = f1.setVarNum(num);
952         int r2 = f2.setVarNum(num);
953         // assertSame(r1 == r2, "setVarNum");
954         return r1;
955     }
956 
957     /*
958      * (non-Javadoc)
959      * 
960      * @see net.sf.javabdd.BDDFactory#ithVar(int)
961      */
962     public BDD ithVar(int var) {
963         return new TestBDD(f1.ithVar(var), f2.ithVar(var));
964     }
965 
966     /*
967      * (non-Javadoc)
968      * 
969      * @see net.sf.javabdd.BDDFactory#nithVar(int)
970      */
971     public BDD nithVar(int var) {
972         return new TestBDD(f1.nithVar(var), f2.nithVar(var));
973     }
974 
975     /*
976      * (non-Javadoc)
977      * 
978      * @see net.sf.javabdd.BDDFactory#printAll()
979      */
980     public void printAll() {
981         // TODO Compare!
982         f1.printAll();
983     }
984 
985     /*
986      * (non-Javadoc)
987      * 
988      * @see net.sf.javabdd.BDDFactory#printTable(net.sf.javabdd.BDD)
989      */
990     public void printTable(BDD b) {
991         // TODO Compare!
992         BDD b1 = ((TestBDD) b).b1;
993         f1.printTable(b1);
994     }
995 
996     /*
997      * (non-Javadoc)
998      * 
999      * @see net.sf.javabdd.BDDFactory#load(java.lang.String)
1000      */
1001     public BDD load(String filename) throws IOException {
1002         return new TestBDD(f1.load(filename), f2.load(filename));
1003     }
1004 
1005     /*
1006      * (non-Javadoc)
1007      * 
1008      * @see net.sf.javabdd.BDDFactory#save(java.lang.String, net.sf.javabdd.BDD)
1009      */
1010     public void save(String filename, BDD var) throws IOException {
1011         // TODO Compare!
1012         BDD b1 = ((TestBDD) var).b1;
1013         f1.save(filename, b1);
1014     }
1015 
1016     /*
1017      * (non-Javadoc)
1018      * 
1019      * @see net.sf.javabdd.BDDFactory#level2Var(int)
1020      */
1021     public int level2Var(int level) {
1022         int r1 = f1.level2Var(level);
1023         int r2 = f2.level2Var(level);
1024         assertSame(r1 == r2, "level2Var");
1025         return r1;
1026     }
1027 
1028     /*
1029      * (non-Javadoc)
1030      * 
1031      * @see net.sf.javabdd.BDDFactory#var2Level(int)
1032      */
1033     public int var2Level(int var) {
1034         int r1 = f1.var2Level(var);
1035         int r2 = f2.var2Level(var);
1036         assertSame(r1 == r2, "var2Level");
1037         return r1;
1038     }
1039 
1040     /*
1041      * (non-Javadoc)
1042      * 
1043      * @see net.sf.javabdd.BDDFactory#reorder(net.sf.javabdd.BDDFactory.ReorderMethod)
1044      */
1045     public void reorder(ReorderMethod m) {
1046         f1.reorder(m);
1047         f2.reorder(m);
1048     }
1049 
1050     /*
1051      * (non-Javadoc)
1052      * 
1053      * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod)
1054      */
1055     public void autoReorder(ReorderMethod method) {
1056         f1.autoReorder(method);
1057         f2.autoReorder(method);
1058     }
1059 
1060     /*
1061      * (non-Javadoc)
1062      * 
1063      * @see net.sf.javabdd.BDDFactory#autoReorder(net.sf.javabdd.BDDFactory.ReorderMethod,
1064      *      int)
1065      */
1066     public void autoReorder(ReorderMethod method, int max) {
1067         f1.autoReorder(method, max);
1068         f2.autoReorder(method, max);
1069     }
1070 
1071     /*
1072      * (non-Javadoc)
1073      * 
1074      * @see net.sf.javabdd.BDDFactory#getReorderMethod()
1075      */
1076     public ReorderMethod getReorderMethod() {
1077         ReorderMethod r1 = f1.getReorderMethod();
1078         ReorderMethod r2 = f2.getReorderMethod();
1079         assertSame(r1.equals(r2), "getReorderMethod");
1080         return r1;
1081     }
1082 
1083     /*
1084      * (non-Javadoc)
1085      * 
1086      * @see net.sf.javabdd.BDDFactory#getReorderTimes()
1087      */
1088     public int getReorderTimes() {
1089         int r1 = f1.getReorderTimes();
1090         int r2 = f2.getReorderTimes();
1091         assertSame(r1 == r2, "getReorderTimes");
1092         return r1;
1093     }
1094 
1095     /*
1096      * (non-Javadoc)
1097      * 
1098      * @see net.sf.javabdd.BDDFactory#disableReorder()
1099      */
1100     public void disableReorder() {
1101         f1.disableReorder();
1102         f2.disableReorder();
1103     }
1104 
1105     /*
1106      * (non-Javadoc)
1107      * 
1108      * @see net.sf.javabdd.BDDFactory#enableReorder()
1109      */
1110     public void enableReorder() {
1111         f1.enableReorder();
1112         f2.enableReorder();
1113     }
1114 
1115     /*
1116      * (non-Javadoc)
1117      * 
1118      * @see net.sf.javabdd.BDDFactory#reorderVerbose(int)
1119      */
1120     public int reorderVerbose(int v) {
1121         int r1 = f1.reorderVerbose(v);
1122         int r2 = f2.reorderVerbose(v);
1123         assertSame(r1 == r2, "reorderVerbose");
1124         return r1;
1125     }
1126 
1127     /*
1128      * (non-Javadoc)
1129      * 
1130      * @see net.sf.javabdd.BDDFactory#setVarOrder(int[])
1131      */
1132     public void setVarOrder(int[] neworder) {
1133         f1.setVarOrder(neworder);
1134         f2.setVarOrder(neworder);
1135     }
1136 
1137     /*
1138      * (non-Javadoc)
1139      * 
1140      * @see net.sf.javabdd.BDDFactory#addVarBlock(int, int, boolean)
1141      */
1142     public void addVarBlock(int first, int last, boolean fixed) {
1143         f1.addVarBlock(first, last, fixed);
1144         f2.addVarBlock(first, last, fixed);
1145     }
1146 
1147     /*
1148      * (non-Javadoc)
1149      * 
1150      * @see net.sf.javabdd.BDDFactory#varBlockAll()
1151      */
1152     public void varBlockAll() {
1153         f1.varBlockAll();
1154         f2.varBlockAll();
1155     }
1156 
1157     /*
1158      * (non-Javadoc)
1159      * 
1160      * @see net.sf.javabdd.BDDFactory#clearVarBlocks()
1161      */
1162     public void clearVarBlocks() {
1163         f1.clearVarBlocks();
1164         f2.clearVarBlocks();
1165     }
1166 
1167     /*
1168      * (non-Javadoc)
1169      * 
1170      * @see net.sf.javabdd.BDDFactory#printOrder()
1171      */
1172     public void printOrder() {
1173         // TODO Compare!
1174         f1.printOrder();
1175     }
1176 
1177     /*
1178      * (non-Javadoc)
1179      * 
1180      * @see net.sf.javabdd.BDDFactory#nodeCount(java.util.Collection)
1181      */
1182     public int nodeCount(Collection r) {
1183         LinkedList a1 = new LinkedList();
1184         LinkedList a2 = new LinkedList();
1185         for (Iterator i = r.iterator(); i.hasNext();) {
1186             TestBDD b = (TestBDD) i.next();
1187             a1.add(b.b1);
1188             a2.add(b.b2);
1189         }
1190         int r1 = f1.nodeCount(a1);
1191         int r2 = f2.nodeCount(a2);
1192         assertSame(r1 == r2, "nodeCount");
1193         return r1;
1194     }
1195 
1196     /*
1197      * (non-Javadoc)
1198      * 
1199      * @see net.sf.javabdd.BDDFactory#getNodeTableSize()
1200      */
1201     public int getNodeTableSize() {
1202         int r1 = f1.getNodeTableSize();
1203         int r2 = f2.getNodeTableSize();
1204         assertSame(r1 == r2, "getNodeTableSize");
1205         return r1;
1206     }
1207 
1208     /*
1209      * (non-Javadoc)
1210      * 
1211      * @see net.sf.javabdd.BDDFactory#getNodeNum()
1212      */
1213     public int getNodeNum() {
1214         int r1 = f1.getNodeNum();
1215         int r2 = f2.getNodeNum();
1216         assertSame(r1 == r2, "getNodeNum");
1217         return r1;
1218     }
1219 
1220     /*
1221      * (non-Javadoc)
1222      * 
1223      * @see net.sf.javabdd.BDDFactory#getCacheSize()
1224      */
1225     public int getCacheSize() {
1226         int r1 = f1.getCacheSize();
1227         int r2 = f2.getCacheSize();
1228         assertSame(r1 == r2, "getCacheSize");
1229         return r1;
1230     }
1231 
1232     /*
1233      * (non-Javadoc)
1234      * 
1235      * @see net.sf.javabdd.BDDFactory#reorderGain()
1236      */
1237     public int reorderGain() {
1238         int r1 = f1.reorderGain();
1239         int r2 = f2.reorderGain();
1240         assertSame(r1 == r2, "reorderGain");
1241         return r1;
1242     }
1243 
1244     /*
1245      * (non-Javadoc)
1246      * 
1247      * @see net.sf.javabdd.BDDFactory#printStat()
1248      */
1249     public void printStat() {
1250         // TODO Compare!
1251         f1.printStat();
1252     }
1253 
1254     /*
1255      * (non-Javadoc)
1256      * 
1257      * @see net.sf.javabdd.BDDFactory#makePair()
1258      */
1259     public BDDPairing makePair() {
1260         BDDPairing p1 = f1.makePair();
1261         BDDPairing p2 = f2.makePair();
1262         return new TestBDDPairing(p1, p2);
1263     }
1264 
1265     /*
1266      * (non-Javadoc)
1267      * 
1268      * @see net.sf.javabdd.BDDFactory#swapVar(int, int)
1269      */
1270     public void swapVar(int v1, int v2) {
1271         f1.swapVar(v1, v2);
1272         f2.swapVar(v1, v2);
1273     }
1274 
1275     /*
1276      * (non-Javadoc)
1277      * 
1278      * @see net.sf.javabdd.BDDFactory#createDomain(int, BigInteger)
1279      */
1280     protected BDDDomain createDomain(int a, BigInteger b) {
1281         return new TestBDDDomain(a, b);
1282     }
1283 
1284     /*
1285      * (non-Javadoc)
1286      * 
1287      * @see net.sf.javabdd.BDDFactory#createBitVector(int)
1288      */
1289     protected BDDBitVector createBitVector(int a) {
1290         return new TestBDDBitVector(a);
1291     }
1292     private static class TestBDDPairing extends BDDPairing {
1293         BDDPairing b1, b2;
1294 
1295         TestBDDPairing(BDDPairing p1, BDDPairing p2) {
1296             this.b1 = p1;
1297             this.b2 = p2;
1298         }
1299 
1300         /*
1301          * (non-Javadoc)
1302          * 
1303          * @see net.sf.javabdd.BDDPairing#set(int, int)
1304          */
1305         public void set(int oldvar, int newvar) {
1306             b1.set(oldvar, newvar);
1307             b2.set(oldvar, newvar);
1308         }
1309 
1310         /*
1311          * (non-Javadoc)
1312          * 
1313          * @see net.sf.javabdd.BDDPairing#set(int, net.sf.javabdd.BDD)
1314          */
1315         public void set(int oldvar, BDD newvar) {
1316             b1.set(oldvar, newvar);
1317             b2.set(oldvar, newvar);
1318         }
1319 
1320         /*
1321          * (non-Javadoc)
1322          * 
1323          * @see net.sf.javabdd.BDDPairing#reset()
1324          */
1325         public void reset() {
1326             b1.reset();
1327             b2.reset();
1328         }
1329     }
1330     private class TestBDDDomain extends BDDDomain {
1331         private TestBDDDomain(int a, BigInteger b) {
1332             super(a, b);
1333         }
1334 
1335         /*
1336          * (non-Javadoc)
1337          * 
1338          * @see net.sf.javabdd.BDDDomain#getFactory()
1339          */
1340         public BDDFactory getFactory() {
1341             return TestBDDFactory.this;
1342         }
1343     }
1344     private class TestBDDBitVector extends BDDBitVector {
1345         TestBDDBitVector(int a) {
1346             super(a);
1347         }
1348 
1349         /*
1350          * (non-Javadoc)
1351          * 
1352          * @see net.sf.javabdd.BDDBitVector#getFactory()
1353          */
1354         public BDDFactory getFactory() {
1355             return TestBDDFactory.this;
1356         }
1357     }
1358     public static final String REVISION = "$Revision: 474 $";
1359 
1360     /*
1361      * (non-Javadoc)
1362      * 
1363      * @see net.sf.javabdd.BDDFactory#getVersion()
1364      */
1365     public String getVersion() {
1366         return "TestBDD " + REVISION.substring(11, REVISION.length() - 2)
1367             + " of (" + f1.getVersion() + "," + f2.getVersion() + ")";
1368     }
1369 }