1
2
3
4 package net.sf.javabdd;
5
6 import java.util.Arrays;
7 import java.util.BitSet;
8 import java.util.Collection;
9 import java.util.Iterator;
10 import java.util.LinkedList;
11 import java.util.List;
12 import java.util.Map;
13 import java.util.StringTokenizer;
14 import java.io.BufferedReader;
15 import java.io.BufferedWriter;
16 import java.io.FileReader;
17 import java.io.FileWriter;
18 import java.io.IOException;
19 import java.lang.reflect.InvocationTargetException;
20 import java.lang.reflect.Method;
21 import java.lang.reflect.Modifier;
22 import java.math.BigInteger;
23 import java.security.AccessControlException;
24
25 /***
26 * <p>Interface for the creation and manipulation of BDDs.</p>
27 *
28 * @see net.sf.javabdd.BDD
29 *
30 * @author John Whaley
31 * @version $Id: BDDFactory.java 476 2007-03-06 06:08:40Z joewhaley $
32 */
33 public abstract class BDDFactory {
34
35 public static final String getProperty(String key, String def) {
36 try {
37 return System.getProperty(key, def);
38 } catch (AccessControlException _) {
39 return def;
40 }
41 }
42
43 /***
44 * <p>Initializes a BDD factory with the given initial node table size
45 * and operation cache size. Tries to use the "buddy" native library;
46 * if it fails, it falls back to the "java" library.</p>
47 *
48 * @param nodenum initial node table size
49 * @param cachesize operation cache size
50 * @return BDD factory object
51 */
52 public static BDDFactory init(int nodenum, int cachesize) {
53 String bddpackage = getProperty("bdd", "buddy");
54 return init(bddpackage, nodenum, cachesize);
55 }
56
57 /***
58 * <p>Initializes a BDD factory of the given type with the given initial
59 * node table size and operation cache size. The type is a string that
60 * can be "buddy", "cudd", "cal", "j", "java", "jdd", "test", "typed", or
61 * a name of a class that has an init() method that returns a BDDFactory.
62 * If it fails, it falls back to the "java" factory.</p>
63 *
64 * @param bddpackage BDD package string identifier
65 * @param nodenum initial node table size
66 * @param cachesize operation cache size
67 * @return BDD factory object
68 */
69 public static BDDFactory init(String bddpackage, int nodenum, int cachesize) {
70 try {
71 if (bddpackage.equals("buddy"))
72 return BuDDyFactory.init(nodenum, cachesize);
73 if (bddpackage.equals("cudd"))
74 return CUDDFactory.init(nodenum, cachesize);
75 if (bddpackage.equals("cal"))
76 return CALFactory.init(nodenum, cachesize);
77 if (bddpackage.equals("j") || bddpackage.equals("java"))
78 return JFactory.init(nodenum, cachesize);
79 if (bddpackage.equals("u"))
80 return UberMicroFactory.init(nodenum, cachesize);
81 if (bddpackage.equals("micro"))
82 return MicroFactory.init(nodenum, cachesize);
83 if (bddpackage.equals("jdd"))
84 return JDDFactory.init(nodenum, cachesize);
85 if (bddpackage.equals("test"))
86 return TestBDDFactory.init(nodenum, cachesize);
87 if (bddpackage.equals("typed"))
88 return TypedBDDFactory.init(nodenum, cachesize);
89 if (bddpackage.equals("zdd")) {
90 BDDFactory bdd = JFactory.init(nodenum, cachesize);
91 ((JFactory)bdd).ZDD = true;
92 return bdd;
93 }
94 } catch (LinkageError e) {
95 System.out.println("Could not load BDD package "+bddpackage+": "+e.getLocalizedMessage());
96 }
97 try {
98 Class c = Class.forName(bddpackage);
99 Method m = c.getMethod("init", new Class[] { int.class, int.class });
100 return (BDDFactory) m.invoke(null, new Object[] { new Integer(nodenum), new Integer(cachesize) });
101 }
102 catch (ClassNotFoundException _) {}
103 catch (NoSuchMethodException _) {}
104 catch (IllegalAccessException _) {}
105 catch (InvocationTargetException _) {}
106
107 return JFactory.init(nodenum, cachesize);
108 }
109
110 /***
111 * Logical 'and'.
112 */
113 public static final BDDOp and = new BDDOp(0, "and");
114
115 /***
116 * Logical 'xor'.
117 */
118 public static final BDDOp xor = new BDDOp(1, "xor");
119
120 /***
121 * Logical 'or'.
122 */
123 public static final BDDOp or = new BDDOp(2, "or");
124
125 /***
126 * Logical 'nand'.
127 */
128 public static final BDDOp nand = new BDDOp(3, "nand");
129
130 /***
131 * Logical 'nor'.
132 */
133 public static final BDDOp nor = new BDDOp(4, "nor");
134
135 /***
136 * Logical 'implication'.
137 */
138 public static final BDDOp imp = new BDDOp(5, "imp");
139
140 /***
141 * Logical 'bi-implication'.
142 */
143 public static final BDDOp biimp = new BDDOp(6, "biimp");
144
145 /***
146 * Set difference.
147 */
148 public static final BDDOp diff = new BDDOp(7, "diff");
149
150 /***
151 * Less than.
152 */
153 public static final BDDOp less = new BDDOp(8, "less");
154
155 /***
156 * Inverse implication.
157 */
158 public static final BDDOp invimp = new BDDOp(9, "invimp");
159
160 /***
161 * <p>Enumeration class for binary operations on BDDs. Use the static
162 * fields in BDDFactory to access the different binary operations.</p>
163 */
164 public static class BDDOp {
165 final int id; final String name;
166 private BDDOp(int id, String name) {
167 this.id = id;
168 this.name = name;
169 }
170 public String toString() {
171 return name;
172 }
173 }
174
175 /***
176 * <p>Construct a new BDDFactory.</p>
177 */
178 protected BDDFactory() {
179 String s = this.getClass().toString();
180 if (false) {
181 s = s.substring(s.lastIndexOf('.')+1);
182 System.out.println("Using BDD package: "+s);
183 }
184 }
185
186 /***
187 * <p>Returns true if this is a ZDD factory, false otherwise.</p>
188 */
189 public boolean isZDD() { return false; }
190
191 /***
192 * <p>Get the constant false BDD.</p>
193 *
194 * <p>Compare to bdd_false.</p>
195 */
196 public abstract BDD zero();
197
198 /***
199 * <p>Get the constant true BDD.</p>
200 *
201 * <p>Compare to bdd_true.</p>
202 */
203 public abstract BDD one();
204
205 /***
206 * <p>Get the constant universe BDD.
207 * (The universe BDD differs from the one BDD in ZDD mode.)</p>
208 *
209 * <p>Compare to bdd_true.</p>
210 */
211 public BDD universe() { return one(); }
212
213 /***
214 * <p>Get an empty BDDVarSet.</p>
215 *
216 * <p>Compare to bdd_true.</p>
217 */
218 public BDDVarSet emptySet() {
219 return new BDDVarSet.DefaultImpl(one());
220 }
221
222 /***
223 * <p>Build a cube from an array of variables.</p>
224 *
225 * <p>Compare to bdd_buildcube.</p>
226 */
227 public BDD buildCube(int value, List
228 BDD result = universe();
229 Iterator i = variables.iterator();
230 int z = 0;
231 while (i.hasNext()) {
232 BDD var = (BDD) i.next();
233 if ((value & 0x1) != 0)
234 var = var.id();
235 else
236 var = var.not();
237 result.andWith(var);
238 ++z;
239 value >>= 1;
240 }
241 return result;
242 }
243
244 /***
245 * <p>Build a cube from an array of variables.</p>
246 *
247 * <p>Compare to bdd_ibuildcube./p>
248 */
249 public BDD buildCube(int value, int[] variables) {
250 BDD result = universe();
251 for (int z = 0; z < variables.length; z++, value >>= 1) {
252 BDD v;
253 if ((value & 0x1) != 0)
254 v = ithVar(variables[variables.length - z - 1]);
255 else
256 v = nithVar(variables[variables.length - z - 1]);
257 result.andWith(v);
258 }
259 return result;
260 }
261
262 /***
263 * <p>Builds a BDD variable set from an integer array. The integer array
264 * <tt>varset</tt> holds the variable numbers. The BDD variable set is
265 * represented by a conjunction of all the variables in their positive
266 * form.</p>
267 *
268 * <p>Compare to bdd_makeset.</p>
269 */
270 public BDDVarSet makeSet(int[] varset) {
271 BDDVarSet res = emptySet();
272 int varnum = varset.length;
273 for (int v = varnum-1; v >= 0; --v) {
274 res.unionWith(varset[v]);
275 }
276 return res;
277 }
278
279
280
281 /***** STARTUP / SHUTDOWN ****/
282
283 /***
284 * <p>Compare to bdd_init.</p>
285 *
286 * @param nodenum the initial number of BDD nodes
287 * @param cachesize the size of caches used by the BDD operators
288 */
289 protected abstract void initialize(int nodenum, int cachesize);
290
291 /***
292 * <p>Returns true if this BDD factory is initialized, false otherwise.</p>
293 *
294 * <p>Compare to bdd_isrunning.</p>
295 *
296 * @return true if this BDD factory is initialized
297 */
298 public abstract boolean isInitialized();
299
300 /***
301 * <p>Reset the BDD factory to its initial state. Everything
302 * is reallocated from scratch. This is like calling done()
303 * followed by initialize().</p>
304 */
305 public void reset() {
306 int nodes = getNodeTableSize();
307 int cache = getCacheSize();
308 domain = null;
309 fdvarnum = 0;
310 firstbddvar = 0;
311 done();
312 initialize(nodes, cache);
313 }
314
315 /***
316 * <p>This function frees all memory used by the BDD
317 * package and resets the package to its uninitialized state.
318 * The BDD package is no longer usable after this call.</p>
319 *
320 * <p>Compare to bdd_done.</p>
321 */
322 public abstract void done();
323
324 /***
325 * <p>Sets the error condition. This will cause the BDD package to throw an
326 * exception at the next garbage collection.</p>
327 *
328 * @param code the error code to set
329 */
330 public abstract void setError(int code);
331
332 /***
333 * <p>Clears any outstanding error condition.</p>
334 */
335 public abstract void clearError();
336
337
338
339 /***** CACHE/TABLE PARAMETERS ****/
340
341 /***
342 * <p>Set the maximum available number of BDD nodes.</p>
343 *
344 * <p>Compare to bdd_setmaxnodenum.</p>
345 *
346 * @param size maximum number of nodes
347 * @return old value
348 */
349 public abstract int setMaxNodeNum(int size);
350
351 /***
352 * <p>Set minimum percentage of nodes to be reclaimed after a garbage
353 * collection. If this percentage is not reclaimed, the node table
354 * will be grown. The range of x is 0..1. The default is .20.</p>
355 *
356 * <p>Compare to bdd_setminfreenodes.</p>
357 *
358 * @param x number from 0 to 1
359 * @return old value
360 */
361 public abstract double setMinFreeNodes(double x);
362
363 /***
364 * <p>Set maximum number of nodes by which to increase node table after
365 * a garbage collection.</p>
366 *
367 * <p>Compare to bdd_setmaxincrease.</p>
368 *
369 * @param x maximum number of nodes by which to increase node table
370 * @return old value
371 */
372 public abstract int setMaxIncrease(int x);
373
374 /***
375 * <p>Set factor by which to increase node table after a garbage
376 * collection. The amount of growth is still limited by
377 * <tt>setMaxIncrease()</tt>.</p>
378 *
379 * @param x factor by which to increase node table after GC
380 * @return old value
381 */
382 public abstract double setIncreaseFactor(double x);
383
384 /***
385 * <p>Sets the cache ratio for the operator caches. When the node table
386 * grows, operator caches will also grow to maintain the ratio.</p>
387 *
388 * <p>Compare to bdd_setcacheratio.</p>
389 *
390 * @param x cache ratio
391 */
392 public abstract double setCacheRatio(double x);
393
394 /***
395 * <p>Sets the node table size.</p>
396 *
397 * @param n new size of table
398 * @return old size of table
399 */
400 public abstract int setNodeTableSize(int n);
401
402 /***
403 * <p>Sets cache size.</p>
404 *
405 * @return old cache size
406 */
407 public abstract int setCacheSize(int n);
408
409
410
411 /***** VARIABLE NUMBERS ****/
412
413 /***
414 * <p>Returns the number of defined variables.</p>
415 *
416 * <p>Compare to bdd_varnum.</p>
417 */
418 public abstract int varNum();
419
420 /***
421 * <p>Set the number of used BDD variables. It can be called more than one
422 * time, but only to increase the number of variables.</p>
423 *
424 * <p>Compare to bdd_setvarnum.</p>
425 *
426 * @param num new number of BDD variables
427 * @return old number of BDD variables
428 */
429 public abstract int setVarNum(int num);
430
431 /***
432 * <p>Add extra BDD variables. Extends the current number of allocated BDD
433 * variables with num extra variables.</p>
434 *
435 * <p>Compare to bdd_extvarnum.</p>
436 *
437 * @param num number of BDD variables to add
438 * @return old number of BDD variables
439 */
440 public int extVarNum(int num) {
441 int start = varNum();
442 if (num < 0 || num > 0x3FFFFFFF)
443 throw new BDDException();
444 setVarNum(start+num);
445 return start;
446 }
447
448 /***
449 * <p>Returns a BDD representing the I'th variable. (One node with the
450 * children true and false.) The requested variable must be in the
451 * (zero-indexed) range defined by <tt>setVarNum</tt>.</p>
452 *
453 * <p>Compare to bdd_ithvar.</p>
454 *
455 * @param var the variable number
456 * @return the I'th variable on success, otherwise the constant false BDD
457 */
458 public abstract BDD ithVar(int var);
459
460 /***
461 * <p>Returns a BDD representing the negation of the I'th variable. (One node
462 * with the children false and true.) The requested variable must be in the
463 * (zero-indexed) range defined by <tt>setVarNum</tt>.</p>
464 *
465 * <p>Compare to bdd_nithvar.</p>
466 *
467 * @param var the variable number
468 * @return the negated I'th variable on success, otherwise the constant false BDD
469 */
470 public abstract BDD nithVar(int var);
471
472
473
474 /***** INPUT / OUTPUT ****/
475
476 /***
477 * <p>Prints all used entries in the node table.</p>
478 *
479 * <p>Compare to bdd_printall.</p>
480 */
481 public abstract void printAll();
482
483 /***
484 * <p>Prints the node table entries used by a BDD.</p>
485 *
486 * <p>Compare to bdd_printtable.</p>
487 */
488 public abstract void printTable(BDD b);
489
490 /***
491 * <p>Loads a BDD from a file.</p>
492 *
493 * <p>Compare to bdd_load.</p>
494 */
495 public BDD load(String filename) throws IOException {
496 BufferedReader r = null;
497 try {
498 r = new BufferedReader(new FileReader(filename));
499 BDD result = load(r);
500 return result;
501 } finally {
502 if (r != null) try { r.close(); } catch (IOException _) { }
503 }
504 }
505
506
507 /***
508 * <p>Loads a BDD from the given input.</p>
509 *
510 * <p>Compare to bdd_load.</p>
511 *
512 * @param ifile reader
513 * @return BDD
514 */
515 public BDD load(BufferedReader ifile) throws IOException {
516 return load(ifile, null);
517 }
518
519 /***
520 * <p>Loads a BDD from the given input, translating BDD variables according
521 * to the given map.</p>
522 *
523 * <p>Compare to bdd_load.</p>
524 *
525 * @param ifile reader
526 * @param translate variable translation map
527 * @return BDD
528 */
529 public BDD load(BufferedReader ifile, int[] translate) throws IOException {
530
531 tokenizer = null;
532
533 int lh_nodenum = Integer.parseInt(readNext(ifile));
534 int vnum = Integer.parseInt(readNext(ifile));
535
536
537 if (lh_nodenum == 0 && vnum == 0) {
538 int r = Integer.parseInt(readNext(ifile));
539 return r == 0 ? zero() : universe();
540 }
541
542
543 int[] loadvar2level = new int[vnum];
544 for (int n = 0; n < vnum; n++) {
545 loadvar2level[n] = Integer.parseInt(readNext(ifile));
546 }
547
548 if (vnum > varNum())
549 setVarNum(vnum);
550
551 LoadHash[] lh_table = new LoadHash[lh_nodenum];
552 for (int n = 0; n < lh_nodenum; n++) {
553 lh_table[n] = new LoadHash();
554 lh_table[n].first = -1;
555 lh_table[n].next = n + 1;
556 }
557 lh_table[lh_nodenum - 1].next = -1;
558 int lh_freepos = 0;
559
560 BDD root = null;
561 for (int n = 0; n < lh_nodenum; n++) {
562 int key = Integer.parseInt(readNext(ifile));
563 int var = Integer.parseInt(readNext(ifile));
564 if (translate != null)
565 var = translate[var];
566 int lowi = Integer.parseInt(readNext(ifile));
567 int highi = Integer.parseInt(readNext(ifile));
568
569 BDD low, high;
570
571 low = loadhash_get(lh_table, lh_nodenum, lowi);
572 high = loadhash_get(lh_table, lh_nodenum, highi);
573
574 if (low == null || high == null || var < 0)
575 throw new BDDException("Incorrect file format");
576
577 BDD b = ithVar(var);
578 root = b.ite(high, low);
579 b.free();
580 if (low.isZero() || low.isOne()) low.free();
581 if (high.isZero() || high.isOne()) high.free();
582
583 int hash = key % lh_nodenum;
584 int pos = lh_freepos;
585
586 lh_freepos = lh_table[pos].next;
587 lh_table[pos].next = lh_table[hash].first;
588 lh_table[hash].first = pos;
589
590 lh_table[pos].key = key;
591 lh_table[pos].data = root;
592 }
593 BDD tmproot = root.id();
594
595 for (int n = 0; n < lh_nodenum; n++)
596 lh_table[n].data.free();
597
598 lh_table = null;
599 loadvar2level = null;
600
601 return tmproot;
602 }
603
604 /***
605 * Used for tokenization during loading.
606 */
607 protected StringTokenizer tokenizer;
608
609 /***
610 * Read the next token from the file.
611 *
612 * @param ifile reader
613 * @return next string token
614 */
615 protected String readNext(BufferedReader ifile) throws IOException {
616 while (tokenizer == null || !tokenizer.hasMoreTokens()) {
617 String s = ifile.readLine();
618 if (s == null)
619 throw new BDDException("Incorrect file format");
620 tokenizer = new StringTokenizer(s);
621 }
622 return tokenizer.nextToken();
623 }
624
625 /***
626 * LoadHash is used to hash during loading.
627 */
628 protected static class LoadHash {
629 int key;
630 BDD data;
631 int first;
632 int next;
633 }
634
635 /***
636 * Gets a BDD from the load hash table.
637 */
638 protected BDD loadhash_get(LoadHash[] lh_table, int lh_nodenum, int key) {
639 if (key < 0) return null;
640 if (key == 0) return zero();
641 if (key == 1) return universe();
642
643 int hash = lh_table[key % lh_nodenum].first;
644
645 while (hash != -1 && lh_table[hash].key != key)
646 hash = lh_table[hash].next;
647
648 if (hash == -1)
649 return null;
650 return lh_table[hash].data;
651 }
652
653 /***
654 * <p>Saves a BDD to a file.</p>
655 *
656 * <p>Compare to bdd_save.</p>
657 */
658 public void save(String filename, BDD var) throws IOException {
659 BufferedWriter is = null;
660 try {
661 is = new BufferedWriter(new FileWriter(filename));
662 save(is, var);
663 } finally {
664 if (is != null) try { is.close(); } catch (IOException _) { }
665 }
666 }
667
668
669 /***
670 * <p>Saves a BDD to an output writer.</p>
671 *
672 * <p>Compare to bdd_save.</p>
673 */
674 public void save(BufferedWriter out, BDD r) throws IOException {
675 if (r.isOne() || r.isZero()) {
676 out.write("0 0 " + (r.isOne()?1:0) + "\n");
677 return;
678 }
679
680 out.write(r.nodeCount() + " " + varNum() + "\n");
681
682 for (int x = 0; x < varNum(); x++)
683 out.write(var2Level(x) + " ");
684 out.write("\n");
685
686
687 BitSet visited = new BitSet(getNodeTableSize());
688 save_rec(out, visited, r.id());
689
690
691
692
693
694 }
695
696 /***
697 * Helper function for save().
698 */
699 protected int save_rec_original(BufferedWriter out, Map visited, BDD root) throws IOException {
700 if (root.isZero()) {
701 root.free();
702 return 0;
703 }
704 if (root.isOne()) {
705 root.free();
706 return 1;
707 }
708 Integer i = (Integer) visited.get(root);
709 if (i != null) {
710 root.free();
711 return i.intValue();
712 }
713 int v = visited.size() + 2;
714 visited.put(root, new Integer(v));
715
716 BDD l = root.low();
717 int lo = save_rec_original(out, visited, l);
718
719 BDD h = root.high();
720 int hi = save_rec_original(out, visited, h);
721
722 out.write(v + " ");
723 out.write(root.var() + " ");
724 out.write(lo + " ");
725 out.write(hi + "\n");
726
727 return v;
728 }
729
730
731 /***
732 * Helper function for save().
733 */
734 protected int save_rec(BufferedWriter out, BitSet visited, BDD root) throws IOException {
735 if (root.isZero()) {
736 root.free();
737 return 0;
738 }
739 if (root.isOne()) {
740 root.free();
741 return 1;
742 }
743 int i = root.hashCode();
744 if (visited.get(i)) {
745 root.free();
746 return i;
747 }
748 int v = i;
749 visited.set(i);
750
751 BDD h = root.high();
752
753 BDD l = root.low();
754
755 int rootvar = root.var();
756 root.free();
757
758 int lo = save_rec(out, visited, l);
759
760 int hi = save_rec(out, visited, h);
761
762 out.write(i + " ");
763 out.write(rootvar + " ");
764 out.write(lo + " ");
765 out.write(hi + "\n");
766
767 return v;
768 }
769
770
771
772
773
774
775
776 /***** REORDERING ****/
777
778 /***
779 * <p>Convert from a BDD level to a BDD variable.</p>
780 *
781 * <p>Compare to bdd_level2var.</p>
782 */
783 public abstract int level2Var(int level);
784
785 /***
786 * <p>Convert from a BDD variable to a BDD level.</p>
787 *
788 * <p>Compare to bdd_var2level.</p>
789 */
790 public abstract int var2Level(int var);
791
792 /***
793 * No reordering.
794 */
795 public static final ReorderMethod REORDER_NONE = new ReorderMethod(0, "NONE");
796
797 /***
798 * Reordering using a sliding window of 2.
799 */
800 public static final ReorderMethod REORDER_WIN2 = new ReorderMethod(1, "WIN2");
801
802 /***
803 * Reordering using a sliding window of 2, iterating until no further
804 * progress.
805 */
806 public static final ReorderMethod REORDER_WIN2ITE = new ReorderMethod(2, "WIN2ITE");
807
808 /***
809 * Reordering using a sliding window of 3.
810 */
811 public static final ReorderMethod REORDER_WIN3 = new ReorderMethod(5, "WIN3");
812
813 /***
814 * Reordering using a sliding window of 3, iterating until no further
815 * progress.
816 */
817 public static final ReorderMethod REORDER_WIN3ITE = new ReorderMethod(6, "WIN3ITE");
818
819 /***
820 * Reordering where each block is moved through all possible positions. The
821 * best of these is then used as the new position. Potentially a very slow
822 * but good method.
823 */
824 public static final ReorderMethod REORDER_SIFT = new ReorderMethod(3, "SIFT");
825
826 /***
827 * Same as REORDER_SIFT, but the process is repeated until no further
828 * progress is done. Can be extremely slow.
829 */
830 public static final ReorderMethod REORDER_SIFTITE = new ReorderMethod(4, "SIFTITE");
831
832 /***
833 * Selects a random position for each variable. Mostly used for debugging
834 * purposes.
835 */
836 public static final ReorderMethod REORDER_RANDOM = new ReorderMethod(7, "RANDOM");
837
838 /***
839 * Enumeration class for method reordering techniques. Use the static fields
840 * in BDDFactory to access the different reordering techniques.
841 */
842 public static class ReorderMethod {
843 final int id; final String name;
844 private ReorderMethod(int id, String name) {
845 this.id = id;
846 this.name = name;
847 }
848
849
850
851 public String toString() {
852 return name;
853 }
854 }
855
856 /***
857 * <p>Reorder the BDD with the given method.</p>
858 *
859 * <p>Compare to bdd_reorder.</p>
860 */
861 public abstract void reorder(ReorderMethod m);
862
863 /***
864 * <p>Enables automatic reordering. If method is REORDER_NONE then automatic
865 * reordering is disabled.</p>
866 *
867 * <p>Compare to bdd_autoreorder.</p>
868 */
869 public abstract void autoReorder(ReorderMethod method);
870
871 /***
872 * <p>Enables automatic reordering with the given (maximum) number of
873 * reorderings. If method is REORDER_NONE then automatic reordering is
874 * disabled.</p>
875 *
876 * <p>Compare to bdd_autoreorder_times.</p>
877 */
878 public abstract void autoReorder(ReorderMethod method, int max);
879
880 /***
881 * <p>Returns the current reorder method as defined by autoReorder.</p>
882 *
883 * <p>Compare to bdd_getreorder_method.</p>
884 *
885 * @return ReorderMethod
886 */
887 public abstract ReorderMethod getReorderMethod();
888
889 /***
890 * <p>Returns the number of allowed reorderings left. This value can be
891 * defined by autoReorder.</p>
892 *
893 * <p>Compare to bdd_getreorder_times.</p>
894 */
895 public abstract int getReorderTimes();
896
897 /***
898 * <p>Disable automatic reordering until enableReorder is called. Reordering
899 * is enabled by default as soon as any variable blocks have been defined.</p>
900 *
901 * <p>Compare to bdd_disable_reorder.</p>
902 */
903 public abstract void disableReorder();
904
905 /***
906 * <p>Enable automatic reordering after a call to disableReorder.</p>
907 *
908 * <p>Compare to bdd_enable_reorder.</p>
909 */
910 public abstract void enableReorder();
911
912 /***
913 * <p>Enables verbose information about reordering. A value of zero means no
914 * information, one means some information and greater than one means lots
915 * of information.</p>
916 *
917 * @param v the new verbose level
918 * @return the old verbose level
919 */
920 public abstract int reorderVerbose(int v);
921
922 /***
923 * <p>This function sets the current variable order to be the one defined by
924 * neworder. The variable parameter neworder is interpreted as a sequence
925 * of variable indices and the new variable order is exactly this sequence.
926 * The array must contain all the variables defined so far. If, for
927 * instance the current number of variables is 3 and neworder contains
928 * [1; 0; 2] then the new variable order is v1<v0<v2.</p>
929 *
930 * <p>Note that this operation must walk through the node table many times,
931 * and therefore it is much more efficient to call this when the node table
932 * is small.</p>
933 *
934 * @param neworder new variable order
935 */
936 public abstract void setVarOrder(int[] neworder);
937
938 /***
939 * <p>Gets the current variable order.</p>
940 *
941 * @return variable order
942 */
943 public int[] getVarOrder() {
944 int n = varNum();
945 int[] result = new int[n];
946 for (int i = 0; i < n; ++i) {
947 result[i] = level2Var(i);
948 }
949 return result;
950 }
951
952 /***
953 * <p>Make a new BDDPairing object.</p>
954 *
955 * <p>Compare to bdd_newpair.</p>
956 */
957 public abstract BDDPairing makePair();
958
959 /***
960 * Make a new pairing that maps from one variable to another.
961 *
962 * @param oldvar old variable
963 * @param newvar new variable
964 * @return BDD pairing
965 */
966 public BDDPairing makePair(int oldvar, int newvar) {
967 BDDPairing p = makePair();
968 p.set(oldvar, newvar);
969 return p;
970 }
971
972 /***
973 * Make a new pairing that maps from one variable to another BDD.
974 *
975 * @param oldvar old variable
976 * @param newvar new BDD
977 * @return BDD pairing
978 */
979 public BDDPairing makePair(int oldvar, BDD newvar) {
980 BDDPairing p = makePair();
981 p.set(oldvar, newvar);
982 return p;
983 }
984
985 /***
986 * Make a new pairing that maps from one BDD domain to another.
987 *
988 * @param oldvar old BDD domain
989 * @param newvar new BDD domain
990 * @return BDD pairing
991 */
992 public BDDPairing makePair(BDDDomain oldvar, BDDDomain newvar) {
993 BDDPairing p = makePair();
994 p.set(oldvar, newvar);
995 return p;
996 }
997
998 /***
999 * <p>Swap two variables.</p>
1000 *
1001 * <p>Compare to bdd_swapvar.</p>
1002 */
1003 public abstract void swapVar(int v1, int v2);
1004
1005 /***** VARIABLE BLOCKS ****/
1006
1007 /***
1008 * <p>Adds a new variable block for reordering.</p>
1009 *
1010 * <p>Creates a new variable block with the variables in the variable set var.
1011 * The variables in var must be contiguous.</p>
1012 *
1013 * <p>The fixed parameter sets the block to be fixed (no reordering of its
1014 * child blocks is allowed) or free.</p>
1015 *
1016 * <p>Compare to bdd_addvarblock.</p>
1017 */
1018 public void addVarBlock(BDDVarSet var, boolean fixed) {
1019 int[] v = var.toArray();
1020 int first, last;
1021 if (v.length < 1)
1022 throw new BDDException("Invalid parameter for addVarBlock");
1023
1024 first = last = v[0];
1025
1026 for (int n = 1; n < v.length; n++) {
1027 if (v[n] < first)
1028 first = v[n];
1029 if (v[n] > last)
1030 last = v[n];
1031 }
1032
1033 addVarBlock(first, last, fixed);
1034 }
1035
1036
1037 /***
1038 * <p>Adds a new variable block for reordering.</p>
1039 *
1040 * <p>Creates a new variable block with the variables numbered first through
1041 * last, inclusive.</p>
1042 *
1043 * <p>The fixed parameter sets the block to be fixed (no reordering of its
1044 * child blocks is allowed) or free.</p>
1045 *
1046 * <p>Compare to bdd_intaddvarblock.</p>
1047 */
1048 public abstract void addVarBlock(int first, int last, boolean fixed);
1049
1050
1051
1052 /***
1053 * <p>Add a variable block for all variables.</p>
1054 *
1055 * <p>Adds a variable block for all BDD variables declared so far. Each block
1056 * contains one variable only. More variable blocks can be added later with
1057 * the use of addVarBlock -- in this case the tree of variable blocks will
1058 * have the blocks of single variables as the leafs.</p>
1059 *
1060 * <p>Compare to bdd_varblockall.</p>
1061 */
1062 public abstract void varBlockAll();
1063
1064 /***
1065 * <p>Clears all the variable blocks that have been defined by calls to
1066 * addVarBlock.</p>
1067 *
1068 * <p>Compare to bdd_clrvarblocks.</p>
1069 */
1070 public abstract void clearVarBlocks();
1071
1072 /***
1073 * <p>Prints an indented list of the variable blocks.</p>
1074 *
1075 * <p>Compare to bdd_printorder.</p>
1076 */
1077 public abstract void printOrder();
1078
1079
1080
1081 /***** BDD STATS ****/
1082
1083 /***
1084 * Get the BDD library version.
1085 *
1086 * @return version string
1087 */
1088 public abstract String getVersion();
1089
1090 /***
1091 * <p>Counts the number of shared nodes in a collection of BDDs. Counts all
1092 * distinct nodes that are used in the BDDs -- if a node is used in more
1093 * than one BDD then it only counts once.</p>
1094 *
1095 * <p>Compare to bdd_anodecount.</p>
1096 */
1097 public abstract int nodeCount(Collection
1098
1099 /***
1100 * <p>Get the number of allocated nodes. This includes both dead and active
1101 * nodes.</p>
1102 *
1103 * <p>Compare to bdd_getallocnum.</p>
1104 */
1105 public abstract int getNodeTableSize();
1106
1107 /***
1108 * <p>Get the number of active nodes in use. Note that dead nodes that have
1109 * not been reclaimed yet by a garbage collection are counted as active.</p>
1110 *
1111 * <p>Compare to bdd_getnodenum.</p>
1112 */
1113 public abstract int getNodeNum();
1114
1115 /***
1116 * <p>Get the current size of the cache, in entries.</p>
1117 *
1118 * @return size of cache
1119 */
1120 public abstract int getCacheSize();
1121
1122 /***
1123 * <p>Calculate the gain in size after a reordering. The value returned is
1124 * (100*(A-B))/A, where A is previous number of used nodes and B is current
1125 * number of used nodes.</p>
1126 *
1127 * <p>Compare to bdd_reorder_gain.</p>
1128 */
1129 public abstract int reorderGain();
1130
1131 /***
1132 * <p>Print cache statistics.</p>
1133 *
1134 * <p>Compare to bdd_printstat.</p>
1135 */
1136 public abstract void printStat();
1137
1138 /***
1139 * Stores statistics about garbage collections.
1140 *
1141 * @author jwhaley
1142 * @version $Id: BDDFactory.java 476 2007-03-06 06:08:40Z joewhaley $
1143 */
1144 public static class GCStats {
1145 public int nodes;
1146 public int freenodes;
1147 public long time;
1148 public long sumtime;
1149 public int num;
1150
1151 protected GCStats() { }
1152
1153
1154
1155
1156 public String toString() {
1157 StringBuffer sb = new StringBuffer();
1158 sb.append("Garbage collection #");
1159 sb.append(num);
1160 sb.append(": ");
1161 sb.append(nodes);
1162 sb.append(" nodes / ");
1163 sb.append(freenodes);
1164 sb.append(" free");
1165
1166 sb.append(" / ");
1167 sb.append((float) time / (float) 1000);
1168 sb.append("s / ");
1169 sb.append((float) sumtime / (float) 1000);
1170 sb.append("s total");
1171 return sb.toString();
1172 }
1173 }
1174
1175 /***
1176 * Singleton object for GC statistics.
1177 */
1178 protected GCStats gcstats = new GCStats();
1179
1180 /***
1181 * <p>Return the current GC statistics for this BDD factory.</p>
1182 *
1183 * @return GC statistics
1184 */
1185 public GCStats getGCStats() {
1186 return gcstats;
1187 }
1188
1189 /***
1190 * Stores statistics about reordering.
1191 *
1192 * @author jwhaley
1193 * @version $Id: BDDFactory.java 476 2007-03-06 06:08:40Z joewhaley $
1194 */
1195 public static class ReorderStats {
1196
1197 public long time;
1198 public int usednum_before, usednum_after;
1199
1200 protected ReorderStats() { }
1201
1202 public int gain() {
1203 if (usednum_before == 0)
1204 return 0;
1205
1206 return (100 * (usednum_before - usednum_after)) / usednum_before;
1207 }
1208
1209 public String toString() {
1210 StringBuffer sb = new StringBuffer();
1211 sb.append("Went from ");
1212 sb.append(usednum_before);
1213 sb.append(" to ");
1214 sb.append(usednum_after);
1215 sb.append(" nodes, gain = ");
1216 sb.append(gain());
1217 sb.append("% (");
1218 sb.append((float) time / 1000f);
1219 sb.append(" sec)");
1220 return sb.toString();
1221 }
1222 }
1223
1224 /***
1225 * Singleton object for reorder statistics.
1226 */
1227 protected ReorderStats reorderstats = new ReorderStats();
1228
1229 /***
1230 * <p>Return the current reordering statistics for this BDD factory.</p>
1231 *
1232 * @return reorder statistics
1233 */
1234 public ReorderStats getReorderStats() {
1235 return reorderstats;
1236 }
1237
1238 /***
1239 * Stores statistics about the operator cache.
1240 *
1241 * @author jwhaley
1242 * @version $Id: BDDFactory.java 476 2007-03-06 06:08:40Z joewhaley $
1243 */
1244 public static class CacheStats {
1245 public int uniqueAccess;
1246 public int uniqueChain;
1247 public int uniqueHit;
1248 public int uniqueMiss;
1249 public int opHit;
1250 public int opMiss;
1251 public int swapCount;
1252
1253 protected CacheStats() { }
1254
1255 void copyFrom(CacheStats that) {
1256 this.uniqueAccess = that.uniqueAccess;
1257 this.uniqueChain = that.uniqueChain;
1258 this.uniqueHit = that.uniqueHit;
1259 this.uniqueMiss = that.uniqueMiss;
1260 this.opHit = that.opHit;
1261 this.opMiss = that.opMiss;
1262 this.swapCount = that.swapCount;
1263 }
1264
1265
1266
1267
1268 public String toString() {
1269 StringBuffer sb = new StringBuffer();
1270 String newLine = getProperty("line.separator", "\n");
1271 sb.append(newLine);
1272 sb.append("Cache statistics");
1273 sb.append(newLine);
1274 sb.append("----------------");
1275 sb.append(newLine);
1276
1277 sb.append("Unique Access: ");
1278 sb.append(uniqueAccess);
1279 sb.append(newLine);
1280 sb.append("Unique Chain: ");
1281 sb.append(uniqueChain);
1282 sb.append(newLine);
1283 sb.append("=> Ave. chain = ");
1284 if (uniqueAccess > 0)
1285 sb.append(((float) uniqueChain) / ((float) uniqueAccess));
1286 else
1287 sb.append((float)0);
1288 sb.append(newLine);
1289 sb.append("Unique Hit: ");
1290 sb.append(uniqueHit);
1291 sb.append(newLine);
1292 sb.append("Unique Miss: ");
1293 sb.append(uniqueMiss);
1294 sb.append(newLine);
1295 sb.append("=> Hit rate = ");
1296 if (uniqueHit + uniqueMiss > 0)
1297 sb.append(((float) uniqueHit) / ((float) uniqueHit + uniqueMiss));
1298 else
1299 sb.append((float)0);
1300 sb.append(newLine);
1301 sb.append("Operator Hits: ");
1302 sb.append(opHit);
1303 sb.append(newLine);
1304 sb.append("Operator Miss: ");
1305 sb.append(opMiss);
1306 sb.append(newLine);
1307 sb.append("=> Hit rate = ");
1308 if (opHit + opMiss > 0)
1309 sb.append(((float) opHit) / ((float) opHit + opMiss));
1310 else
1311 sb.append((float)0);
1312 sb.append(newLine);
1313 sb.append("Swap count = ");
1314 sb.append(swapCount);
1315 sb.append(newLine);
1316 return sb.toString();
1317 }
1318 }
1319
1320 /***
1321 * Singleton object for cache statistics.
1322 */
1323 protected CacheStats cachestats = new CacheStats();
1324
1325 /***
1326 * <p>Return the current cache statistics for this BDD factory.</p>
1327 *
1328 * @return cache statistics
1329 */
1330 public CacheStats getCacheStats() {
1331 return cachestats;
1332 }
1333
1334
1335
1336
1337
1338
1339 /***** FINITE DOMAINS ****/
1340
1341 protected BDDDomain[] domain;
1342 protected int fdvarnum;
1343 protected int firstbddvar;
1344
1345 /***
1346 * <p>Implementors must implement this factory method to create BDDDomain
1347 * objects of the correct type.</p>
1348 */
1349 protected BDDDomain createDomain(int a, BigInteger b) {
1350 return new BDDDomain(a, b) {
1351 public BDDFactory getFactory() { return BDDFactory.this; }
1352 };
1353 }
1354
1355 /***
1356 * <p>Creates a new finite domain block of the given size. Allocates
1357 * log 2 (|domainSize|) BDD variables for the domain.</p>
1358 */
1359 public BDDDomain extDomain(long domainSize) {
1360 return extDomain(BigInteger.valueOf(domainSize));
1361 }
1362 public BDDDomain extDomain(BigInteger domainSize) {
1363 return extDomain(new BigInteger[] { domainSize })[0];
1364 }
1365
1366 /***
1367 * <p>Extends the set of finite domain blocks with domains of the given sizes.
1368 * Each entry in domainSizes is the size of a new finite domain which later
1369 * on can be used for finite state machine traversal and other operations on
1370 * finite domains. Each domain allocates log 2 (|domainSizes[i]|) BDD
1371 * variables to be used later. The ordering is interleaved for the domains
1372 * defined in each call to extDomain. This means that assuming domain D0
1373 * needs 2 BDD variables x1 and x2 , and another domain D1 needs 4 BDD
1374 * variables y1, y2, y3 and y4, then the order then will be x1, y1, x2, y2,
1375 * y3, y4. The new domains are returned in order. The BDD variables needed
1376 * to encode the domain are created for the purpose and do not interfere
1377 * with the BDD variables already in use.</p>
1378 *
1379 * <p>Compare to fdd_extdomain.</p>
1380 */
1381 public BDDDomain[] extDomain(int[] dom) {
1382 BigInteger[] a = new BigInteger[dom.length];
1383 for (int i = 0; i < a.length; ++i) {
1384 a[i] = BigInteger.valueOf(dom[i]);
1385 }
1386 return extDomain(a);
1387 }
1388 public BDDDomain[] extDomain(long[] dom) {
1389 BigInteger[] a = new BigInteger[dom.length];
1390 for (int i = 0; i < a.length; ++i) {
1391 a[i] = BigInteger.valueOf(dom[i]);
1392 }
1393 return extDomain(a);
1394 }
1395 public BDDDomain[] extDomain(BigInteger[] domainSizes) {
1396 int offset = fdvarnum;
1397 int binoffset;
1398 int extravars = 0;
1399 int n, bn;
1400 boolean more;
1401 int num = domainSizes.length;
1402
1403
1404 if (domain == null)
1405 domain = new BDDDomain[num];
1406 } else
1407 if (fdvarnum + num > domain.length) {
1408 int fdvaralloc = domain.length + Math.max(num, domain.length);
1409 BDDDomain[] d2 = new BDDDomain[fdvaralloc];
1410 System.arraycopy(domain, 0, d2, 0, domain.length);
1411 domain = d2;
1412 }
1413 }
1414
1415
1416 for (n = 0; n < num; n++) {
1417 domain[n + fdvarnum] = createDomain(n + fdvarnum, domainSizes[n]);
1418 extravars += domain[n + fdvarnum].varNum();
1419 }
1420
1421 binoffset = firstbddvar;
1422 int bddvarnum = varNum();
1423 if (firstbddvar + extravars > bddvarnum) {
1424 setVarNum(firstbddvar + extravars);
1425 }
1426
1427
1428 for (bn = 0, more = true; more; bn++) {
1429 more = false;
1430
1431 for (n = 0; n < num; n++) {
1432 if (bn < domain[n + fdvarnum].varNum()) {
1433 more = true;
1434 domain[n + fdvarnum].ivar[bn] = binoffset++;
1435 }
1436 }
1437 }
1438
1439 if (isZDD()) {
1440
1441 for (n = 0; n < fdvarnum; n++) {
1442 domain[n].var.free();
1443 domain[n].var =
1444 makeSet(domain[n].ivar);
1445 }
1446 }
1447 for (n = 0; n < num; n++) {
1448 domain[n + fdvarnum].var =
1449 makeSet(domain[n + fdvarnum].ivar);
1450 }
1451
1452 fdvarnum += num;
1453 firstbddvar += extravars;
1454
1455 BDDDomain[] r = new BDDDomain[num];
1456 System.arraycopy(domain, offset, r, 0, num);
1457 return r;
1458 }
1459
1460 /***
1461 * <p>This function takes two finite domain blocks and merges them
1462 * into a new one, such that the new one is encoded using both sets
1463 * of BDD variables.</p>
1464 *
1465 * <p>Compare to fdd_overlapdomain.</p>
1466 */
1467 public BDDDomain overlapDomain(BDDDomain d1, BDDDomain d2) {
1468 BDDDomain d;
1469 int n;
1470
1471 int fdvaralloc = domain.length;
1472 if (fdvarnum + 1 > fdvaralloc) {
1473 fdvaralloc += fdvaralloc;
1474 BDDDomain[] domain2 = new BDDDomain[fdvaralloc];
1475 System.arraycopy(domain, 0, domain2, 0, domain.length);
1476 domain = domain2;
1477 }
1478
1479 d = domain[fdvarnum];
1480 d.realsize = d1.realsize.multiply(d2.realsize);
1481 d.ivar = new int[d1.varNum() + d2.varNum()];
1482
1483 for (n = 0; n < d1.varNum(); n++)
1484 d.ivar[n] = d1.ivar[n];
1485 for (n = 0; n < d2.varNum(); n++)
1486 d.ivar[d1.varNum() + n] = d2.ivar[n];
1487
1488 d.var = makeSet(d.ivar);
1489
1490
1491 fdvarnum++;
1492 return d;
1493 }
1494
1495 /***
1496 * <p>Returns a BDD defining all the variable sets used to define the variable
1497 * blocks in the given array.</p>
1498 *
1499 * <p>Compare to fdd_makeset.</p>
1500 */
1501 public BDDVarSet makeSet(BDDDomain[] v) {
1502 BDDVarSet res = emptySet();
1503 int n;
1504
1505 for (n = 0; n < v.length; n++) {
1506 res.unionWith(v[n].set());
1507 }
1508
1509 return res;
1510 }
1511
1512 /***
1513 * <p>Clear all allocated finite domain blocks that were defined by extDomain()
1514 * or overlapDomain().</p>
1515 *
1516 * <p>Compare to fdd_clearall.</p>
1517 */
1518 public void clearAllDomains() {
1519 domain = null;
1520 fdvarnum = 0;
1521 firstbddvar = 0;
1522 }
1523
1524 /***
1525 * <p>Returns the number of finite domain blocks defined by calls to
1526 * extDomain().</p>
1527 *
1528 * <p>Compare to fdd_domainnum.</p>
1529 */
1530 public int numberOfDomains() {
1531 return fdvarnum;
1532 }
1533
1534 /***
1535 * <p>Returns the ith finite domain block, as defined by calls to
1536 * extDomain().</p>
1537 */
1538 public BDDDomain getDomain(int i) {
1539 if (i < 0 || i >= fdvarnum)
1540 throw new IndexOutOfBoundsException();
1541 return domain[i];
1542 }
1543
1544
1545
1546 /***
1547 * <p>Creates a variable ordering from a string. The resulting order
1548 * can be passed into <tt>setVarOrder()</tt>. Example: in the order
1549 * "A_BxC_DxExF", the bits for A are first, followed by the bits for
1550 * B and C interleaved, followed by the bits for D, E, and F
1551 * interleaved.</p>
1552 *
1553 * <p>Obviously, domain names cannot contain the 'x' or '_'
1554 * characters.</p>
1555 *
1556 * @param reverseLocal whether to reverse the bits of each domain
1557 * @param ordering string representation of ordering
1558 * @return int[] of ordering
1559 * @see net.sf.javabdd.BDDFactory#setVarOrder(int[])
1560 */
1561 public int[] makeVarOrdering(boolean reverseLocal, String ordering) {
1562
1563 int varnum = varNum();
1564
1565 int nDomains = numberOfDomains();
1566 int[][] localOrders = new int[nDomains][];
1567 for (int i=0; i<localOrders.length; ++i) {
1568 localOrders[i] = new int[getDomain(i).varNum()];
1569 }
1570
1571 for (int i=0; i<nDomains; ++i) {
1572 BDDDomain d = getDomain(i);
1573 int nVars = d.varNum();
1574 for (int j=0; j<nVars; ++j) {
1575 if (reverseLocal) {
1576 localOrders[i][j] = nVars - j - 1;
1577 } else {
1578 localOrders[i][j] = j;
1579 }
1580 }
1581 }
1582
1583 BDDDomain[] doms = new BDDDomain[nDomains];
1584
1585 int[] varorder = new int[varnum];
1586
1587
1588 StringTokenizer st = new StringTokenizer(ordering, "x_", true);
1589 int numberOfDomains = 0, bitIndex = 0;
1590 boolean[] done = new boolean[nDomains];
1591 for (int i=0; ; ++i) {
1592 String s = st.nextToken();
1593 BDDDomain d;
1594 for (int j=0; ; ++j) {
1595 if (j == numberOfDomains())
1596 throw new BDDException("bad domain: "+s);
1597 d = getDomain(j);
1598 if (s.equals(d.getName())) break;
1599 }
1600 if (done[d.getIndex()])
1601 throw new BDDException("duplicate domain: "+s);
1602 done[d.getIndex()] = true;
1603 doms[i] = d;
1604 if (st.hasMoreTokens()) {
1605 s = st.nextToken();
1606 if (s.equals("x")) {
1607 ++numberOfDomains;
1608 continue;
1609 }
1610 }
1611 bitIndex = fillInVarIndices(doms, i-numberOfDomains, numberOfDomains+1,
1612 localOrders, bitIndex, varorder);
1613 if (!st.hasMoreTokens()) {
1614 break;
1615 }
1616 if (s.equals("_"))
1617 numberOfDomains = 0;
1618 else
1619 throw new BDDException("bad token: "+s);
1620 }
1621
1622 for (int i=0; i<doms.length; ++i) {
1623 if (!done[i]) {
1624 throw new BDDException("missing domain #"+i+": "+getDomain(i));
1625 }
1626 }
1627
1628 while (bitIndex < varorder.length) {
1629 varorder[bitIndex] = bitIndex;
1630 ++bitIndex;
1631 }
1632
1633 int[] test = new int[varorder.length];
1634 System.arraycopy(varorder, 0, test, 0, varorder.length);
1635 Arrays.sort(test);
1636 for (int i=0; i<test.length; ++i) {
1637 if (test[i] != i)
1638 throw new BDDException(test[i]+" != "+i);
1639 }
1640
1641 return varorder;
1642 }
1643
1644 /***
1645 * Helper function for makeVarOrder().
1646 */
1647 static int fillInVarIndices(
1648 BDDDomain[] doms, int domainIndex, int numDomains,
1649 int[][] localOrders, int bitIndex, int[] varorder) {
1650
1651 int maxBits = 0;
1652 for (int i=0; i<numDomains; ++i) {
1653 BDDDomain d = doms[domainIndex+i];
1654 maxBits = Math.max(maxBits, d.varNum());
1655 }
1656
1657 for (int bitNumber=0; bitNumber<maxBits; ++bitNumber) {
1658 for (int i=0; i<numDomains; ++i) {
1659 BDDDomain d = doms[domainIndex+i];
1660 if (bitNumber < d.varNum()) {
1661 int di = d.getIndex();
1662 int local = localOrders[di][bitNumber];
1663 if (local >= d.vars().length) {
1664 System.out.println("bug!");
1665 }
1666 if (bitIndex >= varorder.length) {
1667 System.out.println("bug2!");
1668 }
1669 varorder[bitIndex++] = d.vars()[local];
1670 }
1671 }
1672 }
1673 return bitIndex;
1674 }
1675
1676
1677
1678 /***** BIT VECTORS ****/
1679
1680 /***
1681 * <p>Implementors must implement this factory method to create BDDBitVector
1682 * objects of the correct type.</p>
1683 */
1684 protected BDDBitVector createBitVector(int a) {
1685 return new BDDBitVector(a) {
1686 public BDDFactory getFactory() { return BDDFactory.this; }
1687 };
1688 }
1689
1690 /***
1691 * <p>Build a bit vector that is constant true or constant false.</p>
1692 *
1693 * <p>Compare to bvec_true, bvec_false.</p>
1694 */
1695 public BDDBitVector buildVector(int bitnum, boolean b) {
1696 BDDBitVector v = createBitVector(bitnum);
1697 v.initialize(b);
1698 return v;
1699 }
1700
1701 /***
1702 * <p>Build a bit vector that corresponds to a constant value.</p>
1703 *
1704 * <p>Compare to bvec_con.</p>
1705 */
1706 public BDDBitVector constantVector(int bitnum, long val) {
1707 BDDBitVector v = createBitVector(bitnum);
1708 v.initialize(val);
1709 return v;
1710 }
1711 public BDDBitVector constantVector(int bitnum, BigInteger val) {
1712 BDDBitVector v = createBitVector(bitnum);
1713 v.initialize(val);
1714 return v;
1715 }
1716
1717 /***
1718 * <p>Build a bit vector using variables offset, offset+step,
1719 * offset+2*step, ... , offset+(bitnum-1)*step.</p>
1720 *
1721 * <p>Compare to bvec_var.</p>
1722 */
1723 public BDDBitVector buildVector(int bitnum, int offset, int step) {
1724 BDDBitVector v = createBitVector(bitnum);
1725 v.initialize(offset, step);
1726 return v;
1727 }
1728
1729 /***
1730 * <p>Build a bit vector using variables from the given BDD domain.</p>
1731 *
1732 * <p>Compare to bvec_varfdd.</p>
1733 */
1734 public BDDBitVector buildVector(BDDDomain d) {
1735 BDDBitVector v = createBitVector(d.varNum());
1736 v.initialize(d);
1737 return v;
1738 }
1739
1740 /***
1741 * <p>Build a bit vector using the given variables.</p>
1742 *
1743 * <p>compare to bvec_varvec.</p>
1744 */
1745 public BDDBitVector buildVector(int[] var) {
1746 BDDBitVector v = createBitVector(var.length);
1747 v.initialize(var);
1748 return v;
1749 }
1750
1751
1752
1753 /***** CALLBACKS ****/
1754
1755 protected List gc_callbacks, reorder_callbacks, resize_callbacks;
1756
1757 /***
1758 * <p>Register a callback that is called when garbage collection is about
1759 * to occur.</p>
1760 *
1761 * @param o base object
1762 * @param m method
1763 */
1764 public void registerGCCallback(Object o, Method m) {
1765 if (gc_callbacks == null) gc_callbacks = new LinkedList();
1766 registerCallback(gc_callbacks, o, m);
1767 }
1768
1769 /***
1770 * <p>Unregister a garbage collection callback that was previously
1771 * registered.</p>
1772 *
1773 * @param o base object
1774 * @param m method
1775 */
1776 public void unregisterGCCallback(Object o, Method m) {
1777 if (gc_callbacks == null) throw new BDDException();
1778 if (!unregisterCallback(gc_callbacks, o, m))
1779 throw new BDDException();
1780 }
1781
1782 /***
1783 * <p>Register a callback that is called when reordering is about
1784 * to occur.</p>
1785 *
1786 * @param o base object
1787 * @param m method
1788 */
1789 public void registerReorderCallback(Object o, Method m) {
1790 if (reorder_callbacks == null) reorder_callbacks = new LinkedList();
1791 registerCallback(reorder_callbacks, o, m);
1792 }
1793
1794 /***
1795 * <p>Unregister a reorder callback that was previously
1796 * registered.</p>
1797 *
1798 * @param o base object
1799 * @param m method
1800 */
1801 public void unregisterReorderCallback(Object o, Method m) {
1802 if (reorder_callbacks == null) throw new BDDException();
1803 if (!unregisterCallback(reorder_callbacks, o, m))
1804 throw new BDDException();
1805 }
1806
1807 /***
1808 * <p>Register a callback that is called when node table resizing is about
1809 * to occur.</p>
1810 *
1811 * @param o base object
1812 * @param m method
1813 */
1814 public void registerResizeCallback(Object o, Method m) {
1815 if (resize_callbacks == null) resize_callbacks = new LinkedList();
1816 registerCallback(resize_callbacks, o, m);
1817 }
1818
1819 /***
1820 * <p>Unregister a reorder callback that was previously
1821 * registered.</p>
1822 *
1823 * @param o base object
1824 * @param m method
1825 */
1826 public void unregisterResizeCallback(Object o, Method m) {
1827 if (resize_callbacks == null) throw new BDDException();
1828 if (!unregisterCallback(resize_callbacks, o, m))
1829 throw new BDDException();
1830 }
1831
1832 protected void gbc_handler(boolean pre, GCStats s) {
1833 if (gc_callbacks == null) {
1834 bdd_default_gbchandler(pre, s);
1835 } else {
1836 doCallbacks(gc_callbacks, new Integer(pre?1:0), s);
1837 }
1838 }
1839
1840 protected static void bdd_default_gbchandler(boolean pre, GCStats s) {
1841 if (pre) {
1842 if (s.freenodes != 0)
1843 System.err.println("Starting GC cycle #"+(s.num+1)+
1844 ": "+s.nodes+" nodes / "+s.freenodes+" free");
1845 } else {
1846 System.err.println(s.toString());
1847 }
1848 }
1849
1850 void reorder_handler(boolean b, ReorderStats s) {
1851 if (b) {
1852 s.usednum_before = getNodeNum();
1853 s.time = System.currentTimeMillis();
1854 } else {
1855 s.time = System.currentTimeMillis() - s.time;
1856 s.usednum_after = getNodeNum();
1857 }
1858 if (reorder_callbacks == null) {
1859 bdd_default_reohandler(b, s);
1860 } else {
1861 doCallbacks(reorder_callbacks, new Boolean(b), s);
1862 }
1863 }
1864
1865 protected void bdd_default_reohandler(boolean prestate, ReorderStats s) {
1866 int verbose = 1;
1867 if (verbose > 0) {
1868 if (prestate) {
1869 System.out.println("Start reordering");
1870 } else {
1871 System.out.println("End reordering. "+s);
1872 }
1873 }
1874 }
1875
1876 protected void resize_handler(int oldsize, int newsize) {
1877 if (resize_callbacks == null) {
1878 bdd_default_reshandler(oldsize, newsize);
1879 } else {
1880 doCallbacks(resize_callbacks, new Integer(oldsize), new Integer(newsize));
1881 }
1882 }
1883
1884 protected static void bdd_default_reshandler(int oldsize, int newsize) {
1885 int verbose = 1;
1886 if (verbose > 0) {
1887 System.out.println("Resizing node table from "+oldsize+" to "+newsize);
1888 }
1889 }
1890
1891 protected void registerCallback(List callbacks, Object o, Method m) {
1892 if (!Modifier.isPublic(m.getModifiers()) && !m.isAccessible()) {
1893 throw new BDDException("Callback method not accessible");
1894 }
1895 if (!Modifier.isStatic(m.getModifiers())) {
1896 if (o == null) {
1897 throw new BDDException("Base object for callback method is null");
1898 }
1899 if (!m.getDeclaringClass().isAssignableFrom(o.getClass())) {
1900 throw new BDDException("Base object for callback method is the wrong type");
1901 }
1902 }
1903 if (false) {
1904 Class[] params = m.getParameterTypes();
1905 if (params.length != 1 || params[0] != int.class) {
1906 throw new BDDException("Wrong signature for callback");
1907 }
1908 }
1909 callbacks.add(new Object[] { o, m });
1910 }
1911
1912 protected boolean unregisterCallback(List callbacks, Object o, Method m) {
1913 if (callbacks != null) {
1914 for (Iterator i = callbacks.iterator(); i.hasNext(); ) {
1915 Object[] cb = (Object[]) i.next();
1916 if (o == cb[0] && m.equals(cb[1])) {
1917 i.remove();
1918 return true;
1919 }
1920 }
1921 }
1922 return false;
1923 }
1924
1925 protected void doCallbacks(List callbacks, Object arg1, Object arg2) {
1926 if (callbacks != null) {
1927 for (Iterator i = callbacks.iterator(); i.hasNext(); ) {
1928 Object[] cb = (Object[]) i.next();
1929 Object o = cb[0];
1930 Method m = (Method) cb[1];
1931 try {
1932 switch (m.getParameterTypes().length) {
1933 case 0:
1934 m.invoke(o, new Object[] { } );
1935 break;
1936 case 1:
1937 m.invoke(o, new Object[] { arg1 } );
1938 break;
1939 case 2:
1940 m.invoke(o, new Object[] { arg1, arg2 } );
1941 break;
1942 default:
1943 throw new BDDException("Wrong number of arguments for "+m);
1944 }
1945 } catch (IllegalArgumentException e) {
1946 e.printStackTrace();
1947 } catch (IllegalAccessException e) {
1948 e.printStackTrace();
1949 } catch (InvocationTargetException e) {
1950 if (e.getTargetException() instanceof RuntimeException)
1951 throw (RuntimeException) e.getTargetException();
1952 if (e.getTargetException() instanceof Error)
1953 throw (Error) e.getTargetException();
1954 e.printStackTrace();
1955 }
1956 }
1957 }
1958 }
1959
1960 }