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