1
2
3
4 package net.sf.javabdd;
5
6 import java.util.Arrays;
7 import java.util.HashMap;
8 import java.util.Iterator;
9 import java.util.LinkedList;
10 import java.util.NoSuchElementException;
11 import java.io.PrintStream;
12 import java.math.BigInteger;
13
14 /***
15 * <p>Binary Decision Diagrams (BDDs) are used for efficient computation of many
16 * common problems. This is done by giving a compact representation and a set of
17 * efficient operations on boolean functions f: {0,1}^n --> {0,1}.</p>
18 *
19 * <p>Use an implementation of BDDFactory to create BDD objects.</p>
20 *
21 * @see net.sf.javabdd.BDDFactory
22 * @see net.sf.javabdd.BDDDomain#set()
23 *
24 * @author John Whaley
25 * @version $Id: BDD.java 472 2006-12-03 10:32:26Z joewhaley $
26 */
27 public abstract class BDD {
28
29 /***
30 * <p>Returns the factory that created this BDD.</p>
31 *
32 * @return factory that created this BDD
33 */
34 public abstract BDDFactory getFactory();
35
36 /***
37 * <p>Returns true if this BDD is the zero (false) BDD.</p>
38 *
39 * @return true if this BDD is the zero (false) BDD
40 */
41 public abstract boolean isZero();
42
43 /***
44 * <p>Returns true if this BDD is the one (true) BDD.</p>
45 *
46 * @return true if this BDD is the one (true) BDD
47 */
48 public abstract boolean isOne();
49
50 /***
51 * <p>Returns true if this BDD is the universe BDD.
52 * The universal BDD differs from the one BDD in ZDD mode.</p>
53 *
54 * @return true if this BDD is the universe BDD
55 */
56 public boolean isUniverse() { return isOne(); }
57
58 /***
59 * <p>Converts this BDD to a new BDDVarSet.</p>
60 *
61 * <p>This BDD must be a boolean function that represents the all-true minterm
62 * of the BDD variables of interest.</p>
63 *
64 * @return the contents of this BDD as a new BDDVarSet
65 */
66 public BDDVarSet toVarSet() {
67 return new BDDVarSet.DefaultImpl(id());
68 }
69
70 /***
71 * <p>Gets the variable labeling the BDD.</p>
72 *
73 * <p>Compare to bdd_var.</p>
74 *
75 * @return the index of the variable labeling the BDD
76 */
77 public abstract int var();
78
79 /***
80 * <p>Gets the level of this BDD.</p>
81 *
82 * <p>Compare to LEVEL() macro.</p>
83 *
84 * @return the level of this BDD
85 */
86 public int level() {
87 if (isZero() || isOne()) return getFactory().varNum();
88 return getFactory().var2Level(var());
89 }
90
91 /***
92 * <p>Gets the true branch of this BDD.</p>
93 *
94 * <p>Compare to bdd_high.</p>
95 *
96 * @return true branch of this BDD
97 */
98 public abstract BDD high();
99
100 /***
101 * <p>Gets the false branch of this BDD.</p>
102 *
103 * <p>Compare to bdd_low.</p>
104 *
105 * @return false branch of this BDD
106 */
107 public abstract BDD low();
108
109 /***
110 * <p>Identity function. Returns a copy of this BDD. Use as the argument to
111 * the "xxxWith" style operators when you do not want to have the argument
112 * consumed.</p>
113 *
114 * <p>Compare to bdd_addref.</p>
115 *
116 * @return copy of this BDD
117 */
118 public abstract BDD id();
119
120 /***
121 * <p>Negates this BDD by exchanging all references to the zero-terminal with
122 * references to the one-terminal and vice-versa.</p>
123 *
124 * <p>Compare to bdd_not.</p>
125 *
126 * @return the negated BDD
127 */
128 public abstract BDD not();
129
130 /***
131 * <p>Returns the logical 'and' of two BDDs. This is a shortcut for calling
132 * "apply" with the "and" operator.</p>
133 *
134 * <p>Compare to bdd_and.</p>
135 *
136 * @param that BDD to 'and' with
137 * @return the logical 'and' of two BDDs
138 */
139 public BDD and(BDD that) {
140 return this.apply(that, BDDFactory.and);
141 }
142
143 /***
144 * <p>Makes this BDD be the logical 'and' of two BDDs. The "that" BDD is
145 * consumed, and can no longer be used. This is a shortcut for calling
146 * "applyWith" with the "and" operator.</p>
147 *
148 * <p>Compare to bdd_and and bdd_delref.</p>
149 *
150 * @param that the BDD to 'and' with
151 */
152 public BDD andWith(BDD that) {
153 return this.applyWith(that, BDDFactory.and);
154 }
155
156 /***
157 * <p>Returns the logical 'or' of two BDDs. This is a shortcut for calling
158 * "apply" with the "or" operator.</p>
159 *
160 * <p>Compare to bdd_or.</p>
161 *
162 * @param that the BDD to 'or' with
163 * @return the logical 'or' of two BDDs
164 */
165 public BDD or(BDD that) {
166 return this.apply(that, BDDFactory.or);
167 }
168
169 /***
170 * <p>Makes this BDD be the logical 'or' of two BDDs. The "that" BDD is
171 * consumed, and can no longer be used. This is a shortcut for calling
172 * "applyWith" with the "or" operator.</p>
173 *
174 * <p>Compare to bdd_or and bdd_delref.</p>
175 *
176 * @param that the BDD to 'or' with
177 */
178 public BDD orWith(BDD that) {
179 return this.applyWith(that, BDDFactory.or);
180 }
181
182 /***
183 * <p>Returns the logical 'xor' of two BDDs. This is a shortcut for calling
184 * "apply" with the "xor" operator.</p>
185 *
186 * <p>Compare to bdd_xor.</p>
187 *
188 * @param that the BDD to 'xor' with
189 * @return the logical 'xor' of two BDDs
190 */
191 public BDD xor(BDD that) {
192 return this.apply(that, BDDFactory.xor);
193 }
194
195 /***
196 * <p>Makes this BDD be the logical 'xor' of two BDDs. The "that" BDD is
197 * consumed, and can no longer be used. This is a shortcut for calling
198 * "applyWith" with the "xor" operator.</p>
199 *
200 * <p>Compare to bdd_xor and bdd_delref.</p>
201 *
202 * @param that the BDD to 'xor' with
203 */
204 public BDD xorWith(BDD that) {
205 return this.applyWith(that, BDDFactory.xor);
206 }
207
208 /***
209 * <p>Returns the logical 'implication' of two BDDs. This is a shortcut for
210 * calling "apply" with the "imp" operator.</p>
211 *
212 * <p>Compare to bdd_imp.</p>
213 *
214 * @param that the BDD to 'implication' with
215 * @return the logical 'implication' of two BDDs
216 */
217 public BDD imp(BDD that) {
218 return this.apply(that, BDDFactory.imp);
219 }
220
221 /***
222 * <p>Makes this BDD be the logical 'implication' of two BDDs. The "that" BDD
223 * is consumed, and can no longer be used. This is a shortcut for calling
224 * "applyWith" with the "imp" operator.</p>
225 *
226 * <p>Compare to bdd_imp and bdd_delref.</p>
227 *
228 * @param that the BDD to 'implication' with
229 */
230 public BDD impWith(BDD that) {
231 return this.applyWith(that, BDDFactory.imp);
232 }
233
234 /***
235 * <p>Returns the logical 'bi-implication' of two BDDs. This is a shortcut for
236 * calling "apply" with the "biimp" operator.</p>
237 *
238 * <p>Compare to bdd_biimp.</p>
239 *
240 * @param that the BDD to 'bi-implication' with
241 * @return the logical 'bi-implication' of two BDDs
242 */
243 public BDD biimp(BDD that) {
244 return this.apply(that, BDDFactory.biimp);
245 }
246
247 /***
248 * <p>Makes this BDD be the logical 'bi-implication' of two BDDs. The "that"
249 * BDD is consumed, and can no longer be used. This is a shortcut for
250 * calling "applyWith" with the "biimp" operator.</p>
251 *
252 * <p>Compare to bdd_biimp and bdd_delref.</p>
253 *
254 * @param that the BDD to 'bi-implication' with
255 */
256 public BDD biimpWith(BDD that) {
257 return this.applyWith(that, BDDFactory.biimp);
258 }
259
260 /***
261 * <p>if-then-else operator.</p>
262 *
263 * <p>Compare to bdd_ite.</p>
264 *
265 * @param thenBDD the 'then' BDD
266 * @param elseBDD the 'else' BDD
267 * @return the result of the if-then-else operator on the three BDDs
268 */
269 public abstract BDD ite(BDD thenBDD, BDD elseBDD);
270
271 /***
272 * <p>Relational product. Calculates the relational product of the two BDDs as
273 * this AND that with the variables in var quantified out afterwards.
274 * Identical to applyEx(that, and, var).</p>
275 *
276 * <p>Compare to bdd_relprod.</p>
277 *
278 * @param that the BDD to 'and' with
279 * @param var the BDDVarSet to existentially quantify with
280 * @return the result of the relational product
281 * @see net.sf.javabdd.BDDDomain#set()
282 */
283 public BDD relprod(BDD that, BDDVarSet var) {
284 return applyEx(that, BDDFactory.and, var);
285 }
286
287 /***
288 * <p>Functional composition. Substitutes the variable var with the BDD that
289 * in this BDD: result = f[g/var].</p>
290 *
291 * <p>Compare to bdd_compose.</p>
292 *
293 * @param g the function to use to replace
294 * @param var the variable number to replace
295 * @return the result of the functional composition
296 */
297 public abstract BDD compose(BDD g, int var);
298
299 /***
300 * <p>Simultaneous functional composition. Uses the pairs of variables and
301 * BDDs in pair to make the simultaneous substitution: f [g1/V1, ... gn/Vn].
302 * In this way one or more BDDs may be substituted in one step. The BDDs in
303 * pair may depend on the variables they are substituting. BDD.compose()
304 * may be used instead of BDD.replace() but is not as efficient when gi is a
305 * single variable, the same applies to BDD.restrict(). Note that
306 * simultaneous substitution is not necessarily the same as repeated
307 * substitution.</p>
308 *
309 * <p>Compare to bdd_veccompose.</p>
310 *
311 * @param pair the pairing of variables to functions
312 * @return BDD the result of the simultaneous functional composition
313 */
314 public abstract BDD veccompose(BDDPairing pair);
315
316 /***
317 * <p>Generalized cofactor. Computes the generalized cofactor of this BDD with
318 * respect to the given BDD.</p>
319 *
320 * <p>Compare to bdd_constrain.</p>
321 *
322 * @param that the BDD with which to compute the generalized cofactor
323 * @return the result of the generalized cofactor
324 */
325 public abstract BDD constrain(BDD that);
326
327 /***
328 * <p>Existential quantification of variables. Removes all occurrences of this
329 * BDD in variables in the set var by existential quantification.</p>
330 *
331 * <p>Compare to bdd_exist.</p>
332 *
333 * @param var BDDVarSet containing the variables to be existentially quantified
334 * @return the result of the existential quantification
335 * @see net.sf.javabdd.BDDDomain#set()
336 */
337 public abstract BDD exist(BDDVarSet var);
338
339 /***
340 * <p>Universal quantification of variables. Removes all occurrences of this
341 * BDD in variables in the set var by universal quantification.</p>
342 *
343 * <p>Compare to bdd_forall.</p>
344 *
345 * @param var BDDVarSet containing the variables to be universally quantified
346 * @return the result of the universal quantification
347 * @see net.sf.javabdd.BDDDomain#set()
348 */
349 public abstract BDD forAll(BDDVarSet var);
350
351 /***
352 * <p>Unique quantification of variables. This type of quantification uses a
353 * XOR operator instead of an OR operator as in the existential
354 * quantification.</p>
355 *
356 * <p>Compare to bdd_unique.</p>
357 *
358 * @param var BDDVarSet containing the variables to be uniquely quantified
359 * @return the result of the unique quantification
360 * @see net.sf.javabdd.BDDDomain#set()
361 */
362 public abstract BDD unique(BDDVarSet var);
363
364 /***
365 * <p>Restrict a set of variables to constant values. Restricts the variables
366 * in this BDD to constant true if they are included in their positive form
367 * in var, and constant false if they are included in their negative form.</p>
368 *
369 * <p><i>Note that this is quite different than Coudert and Madre's restrict
370 * function.</i></p>
371 *
372 * <p>Compare to bdd_restrict.</p>
373 *
374 * @param var BDD containing the variables to be restricted
375 * @return the result of the restrict operation
376 * @see net.sf.javabdd.BDD#simplify(BDD)
377 */
378 public abstract BDD restrict(BDD var);
379
380 /***
381 * <p>Mutates this BDD to restrict a set of variables to constant values.
382 * Restricts the variables in this BDD to constant true if they are included
383 * in their positive form in var, and constant false if they are included in
384 * their negative form. The "that" BDD is consumed, and can no longer be used.</p>
385 *
386 * <p><i>Note that this is quite different than Coudert and Madre's restrict
387 * function.</i></p>
388 *
389 * <p>Compare to bdd_restrict and bdd_delref.</p>
390 *
391 * @param var BDD containing the variables to be restricted
392 * @see net.sf.javabdd.BDDDomain#set()
393 */
394 public abstract BDD restrictWith(BDD var);
395
396 /***
397 * <p>Coudert and Madre's restrict function. Tries to simplify the BDD f by
398 * restricting it to the domain covered by d. No checks are done to see if
399 * the result is actually smaller than the input. This can be done by the
400 * user with a call to nodeCount().</p>
401 *
402 * <p>Compare to bdd_simplify.</p>
403 *
404 * @param d BDDVarSet containing the variables in the domain
405 * @return the result of the simplify operation
406 */
407 public abstract BDD simplify(BDDVarSet d);
408
409 /***
410 * <p>Returns the variable support of this BDD. The support is all the
411 * variables that this BDD depends on.</p>
412 *
413 * <p>Compare to bdd_support.</p>
414 *
415 * @return the variable support of this BDD
416 */
417 public abstract BDDVarSet support();
418
419 /***
420 * <p>Returns the result of applying the binary operator <tt>opr</tt> to the
421 * two BDDs.</p>
422 *
423 * <p>Compare to bdd_apply.</p>
424 *
425 * @param that the BDD to apply the operator on
426 * @param opr the operator to apply
427 * @return the result of applying the operator
428 */
429 public abstract BDD apply(BDD that, BDDFactory.BDDOp opr);
430
431 /***
432 * <p>Makes this BDD be the result of the binary operator <tt>opr</tt> of two
433 * BDDs. The "that" BDD is consumed, and can no longer be used. Attempting
434 * to use the passed in BDD again will result in an exception being thrown.</p>
435 *
436 * <p>Compare to bdd_apply and bdd_delref.</p>
437 *
438 * @param that the BDD to apply the operator on
439 * @param opr the operator to apply
440 */
441 public abstract BDD applyWith(BDD that, BDDFactory.BDDOp opr);
442
443 /***
444 * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs a
445 * universal quantification of the variables from the variable set
446 * <tt>var</tt>.</p>
447 *
448 * <p>Compare to bdd_appall.</p>
449 *
450 * @param that the BDD to apply the operator on
451 * @param opr the operator to apply
452 * @param var BDDVarSet containing the variables to quantify
453 * @return the result
454 * @see net.sf.javabdd.BDDDomain#set()
455 */
456 public abstract BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var);
457
458 /***
459 * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs
460 * an existential quantification of the variables from the variable set
461 * <tt>var</tt>.</p>
462 *
463 * <p>Compare to bdd_appex.</p>
464 *
465 * @param that the BDD to apply the operator on
466 * @param opr the operator to apply
467 * @param var BDDVarSet containing the variables to quantify
468 * @return the result
469 * @see net.sf.javabdd.BDDDomain#set()
470 */
471 public abstract BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var);
472
473 /***
474 * <p>Applies the binary operator <tt>opr</tt> to two BDDs and then performs
475 * a unique quantification of the variables from the variable set
476 * <tt>var</tt>.</p>
477 *
478 * <p>Compare to bdd_appuni.</p>
479 *
480 * @param that the BDD to apply the operator on
481 * @param opr the operator to apply
482 * @param var BDDVarSet containing the variables to quantify
483 * @return the result
484 * @see net.sf.javabdd.BDDDomain#set()
485 */
486 public abstract BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var);
487
488 /***
489 * <p>Finds one satisfying variable assignment. Finds a BDD with at most one
490 * variable at each level. The new BDD implies this BDD and is not false
491 * unless this BDD is false.</p>
492 *
493 * <p>Compare to bdd_satone.</p>
494 *
495 * @return one satisfying variable assignment
496 */
497 public abstract BDD satOne();
498
499 /***
500 * <p>Finds one satisfying variable assignment. Finds a BDD with exactly one
501 * variable at all levels. The new BDD implies this BDD and is not false
502 * unless this BDD is false.</p>
503 *
504 * <p>Compare to bdd_fullsatone.</p>
505 *
506 * @return one satisfying variable assignment
507 */
508 public abstract BDD fullSatOne();
509
510 /***
511 * <p>Finds one satisfying variable assignment. Finds a minterm in this BDD.
512 * The <tt>var</tt> argument is a set of variables that must be mentioned in
513 * the result. The polarity of these variables in the result - in case they
514 * are undefined in this BDD - are defined by the <tt>pol</tt> parameter.
515 * If <tt>pol</tt> is false, then all variables will be in negative form.
516 * Otherwise they will be in positive form.</p>
517 *
518 * <p>Compare to bdd_satoneset.</p>
519 *
520 * @param var BDDVarSet containing the set of variables that must be mentioned in the result
521 * @param pol the polarity of the result
522 * @return one satisfying variable assignment
523 * @see net.sf.javabdd.BDDDomain#set()
524 */
525 public abstract BDD satOne(BDDVarSet var, boolean pol);
526
527 /***
528 * <p>Finds all satisfying variable assignments.</p>
529 *
530 * <p>Compare to bdd_allsat.</p>
531 *
532 * @return all satisfying variable assignments
533 */
534 public AllSatIterator allsat() {
535 return new AllSatIterator(this);
536 }
537
538 /***
539 * Iterator that returns all satisfying assignments as byte arrays.
540 * In the byte arrays, -1 means dont-care, 0 means 0, and 1 means 1.
541 */
542 public static class AllSatIterator implements Iterator {
543
544 protected final BDDFactory f;
545 protected LinkedList loStack, hiStack;
546 protected byte[] allsatProfile;
547 protected final boolean useLevel;
548
549 protected AllSatIterator(BDDFactory factory, boolean level) {
550 f = factory;
551 useLevel = level;
552 }
553
554 /***
555 * Constructs a satisfying-assignment iterator on the given BDD.
556 * next() returns a byte array indexed by BDD variable number.
557 *
558 * @param r BDD to iterate over
559 */
560 public AllSatIterator(BDD r) {
561 this(r, false);
562 }
563
564 /***
565 * Constructs a satisfying-assignment iterator on the given BDD.
566 * If lev is true, next() will returns a byte array indexed by
567 * level. If lev is false, the byte array will be indexed by
568 * BDD variable number.
569 *
570 * @param r BDD to iterate over
571 * @param lev whether to index byte array by level instead of var
572 */
573 public AllSatIterator(BDD r, boolean lev) {
574 f = r.getFactory();
575 useLevel = lev;
576 if (r.isZero()) return;
577 allsatProfile = new byte[f.varNum()];
578 if (!f.isZDD())
579 Arrays.fill(allsatProfile, (byte) -1);
580 loStack = new LinkedList();
581 hiStack = new LinkedList();
582 if (!r.isOne()) {
583 loStack.addLast(r.id());
584 if (!gotoNext()) allsatProfile = null;
585 }
586 }
587
588 private boolean gotoNext() {
589 BDD r;
590 for (;;) {
591 boolean lo_empty = loStack.isEmpty();
592 if (lo_empty) {
593 if (hiStack.isEmpty()) {
594 return false;
595 }
596 r = (BDD) hiStack.removeLast();
597 } else {
598 r = (BDD) loStack.removeLast();
599 }
600 int LEVEL_r = r.level();
601 allsatProfile[useLevel?LEVEL_r:f.level2Var(LEVEL_r)] =
602 lo_empty ? (byte)1 : (byte)0;
603 BDD rn = lo_empty ? r.high() : r.low();
604 int v = rn.isOne()||rn.isZero() ? f.varNum() - 1 : rn.level() - 1;
605 for ( ; v > LEVEL_r; --v) {
606 allsatProfile[useLevel?v:f.level2Var(v)] = f.isZDD()?(byte)0:(byte)-1;
607 }
608 if (!lo_empty) {
609 if (f.isZDD()) {
610
611 BDD rh = r.high();
612 boolean isDontCare = rn.equals(rh);
613 rh.free();
614 if (isDontCare) {
615
616 allsatProfile[useLevel?v:f.level2Var(v)] = -1;
617 r.free();
618 } else {
619 hiStack.addLast(r);
620 }
621 } else {
622
623 hiStack.addLast(r);
624 }
625 } else {
626 r.free();
627 }
628 if (rn.isOne()) {
629 rn.free();
630 return true;
631 }
632 if (rn.isZero()) {
633 rn.free();
634 continue;
635 }
636 loStack.addLast(rn);
637 }
638 }
639
640
641
642
643 public boolean hasNext() {
644 return allsatProfile != null;
645 }
646
647 /***
648 * Return the next satisfying var setting.
649 *
650 * @return byte[]
651 */
652 public byte[] nextSat() {
653 if (allsatProfile == null)
654 throw new NoSuchElementException();
655 byte[] b = new byte[allsatProfile.length];
656 System.arraycopy(allsatProfile, 0, b, 0, b.length);
657 if (!gotoNext()) allsatProfile = null;
658 return b;
659 }
660
661
662
663
664 public Object next() {
665 return nextSat();
666 }
667
668
669
670
671 public void remove() {
672 throw new UnsupportedOperationException();
673 }
674
675 }
676
677 /***
678 * <p>Finds one satisfying assignment of the domain <tt>d</tt> in this BDD
679 * and returns that value.</p>
680 *
681 * <p>Compare to fdd_scanvar.</p>
682 *
683 * @param d domain to scan
684 * @return one satisfying assignment for that domain
685 */
686 public BigInteger scanVar(BDDDomain d) {
687 if (this.isZero())
688 return BigInteger.valueOf(-1);
689 BigInteger[] allvar = this.scanAllVar();
690 BigInteger res = allvar[d.getIndex()];
691 return res;
692 }
693
694 /***
695 * <p>Finds one satisfying assignment in this BDD of all the defined
696 * BDDDomain's. Each value is stored in an array which is returned. The size
697 * of this array is exactly the number of BDDDomain's defined.</p>
698 *
699 * <p>Compare to fdd_scanallvar.</p>
700 *
701 * @return array containing one satisfying assignment of all the defined domains
702 */
703 public BigInteger[] scanAllVar() {
704 int n;
705 boolean[] store;
706 BigInteger[] res;
707
708 if (this.isZero())
709 return null;
710
711 BDDFactory factory = getFactory();
712
713 int bddvarnum = factory.varNum();
714 store = new boolean[bddvarnum];
715
716 BDD p = this.id();
717 while (!p.isOne() && !p.isZero()) {
718 BDD lo = p.low();
719 if (!lo.isZero()) {
720 store[p.var()] = false;
721 BDD p2 = p.low();
722 p.free(); p = p2;
723 } else {
724 store[p.var()] = true;
725 BDD p2 = p.high();
726 p.free(); p = p2;
727 }
728 lo.free();
729 }
730
731 int fdvarnum = factory.numberOfDomains();
732 res = new BigInteger[fdvarnum];
733
734 for (n = 0; n < fdvarnum; n++) {
735 BDDDomain dom = factory.getDomain(n);
736 int[] ivar = dom.vars();
737
738 BigInteger val = BigInteger.ZERO;
739 for (int m = dom.varNum() - 1; m >= 0; m--) {
740 val = val.shiftLeft(1);
741 if (store[ivar[m]])
742 val = val.add(BigInteger.ONE);
743 }
744
745 res[n] = val;
746 }
747
748 return res;
749 }
750
751 /***
752 * Utility function to convert from a BDD varset to an array of levels.
753 *
754 * @param r BDD varset
755 * @return array of levels
756 */
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782 /***
783 * <p>Returns an iteration of the satisfying assignments of this BDD. Returns
784 * an iteration of minterms. The <tt>var</tt> argument is the set of variables
785 * that will be mentioned in the result.</p>
786 *
787 * @param var set of variables to mention in result
788 * @return an iteration of minterms
789 * @see net.sf.javabdd.BDDDomain#set()
790 */
791 public BDDIterator iterator(final BDDVarSet var) {
792 return new BDDIterator(this, var);
793 }
794
795 /***
796 * BDDIterator is used to iterate through the satisfying assignments of a BDD.
797 * It includes the ability to check if bits are dont-cares and skip them.
798 *
799 * @author jwhaley
800 * @version $Id: BDD.java 472 2006-12-03 10:32:26Z joewhaley $
801 */
802 public static class BDDIterator implements Iterator {
803 final BDDFactory f;
804 final AllSatIterator i;
805
806 final BDD initialBDD;
807
808 final int[] v;
809
810 final boolean[] b;
811
812 byte[] a;
813
814 BDD lastReturned;
815
816 /***
817 * Construct a new BDDIterator on the given BDD.
818 * The var argument is the set of variables that will be mentioned in the result.
819 *
820 * @param bdd BDD to iterate over
821 * @param var variable set to mention in result
822 */
823 public BDDIterator(BDD bdd, BDDVarSet var) {
824 initialBDD = bdd;
825 f = bdd.getFactory();
826 i = new AllSatIterator(bdd, true);
827
828 v = var.toLevelArray();
829
830 b = new boolean[v.length];
831 gotoNext();
832 }
833
834 protected void gotoNext() {
835 if (i.hasNext()) {
836 a = (byte[]) i.next();
837 } else {
838 a = null;
839 return;
840 }
841 for (int i = 0; i < v.length; ++i) {
842 int vi = v[i];
843 if (a[vi] == 1) b[i] = true;
844 else b[i] = false;
845 }
846 }
847
848 protected boolean gotoNextA() {
849 for (int i = v.length-1; i >= 0; --i) {
850 int vi = v[i];
851 if (a[vi] != -1) continue;
852 if (b[i] == false) {
853 b[i] = true;
854 return true;
855 }
856 b[i] = false;
857 }
858 return false;
859 }
860
861
862
863
864 public boolean hasNext() {
865 return a != null;
866 }
867
868
869
870
871 public Object next() {
872 return nextBDD();
873 }
874
875 public BigInteger nextValue(BDDDomain dom) {
876 if (a == null) {
877 throw new NoSuchElementException();
878 }
879 lastReturned = null;
880 BigInteger val = BigInteger.ZERO;
881 int[] ivar = dom.vars();
882 for (int m = dom.varNum() - 1; m >= 0; m--) {
883 val = val.shiftLeft(1);
884 int level = f.var2Level(ivar[m]);
885 int k = Arrays.binarySearch(v, level);
886 if (k < 0) {
887 val = null;
888 break;
889 }
890 if (b[k]) {
891 val = val.add(BigInteger.ONE);
892 }
893 }
894 if (!gotoNextA()) {
895 gotoNext();
896 }
897 return val;
898 }
899
900 /***
901 * Return the next tuple of domain values in the iteration.
902 *
903 * @return the next tuple of domain values in the iteration.
904 */
905 public BigInteger[] nextTuple() {
906 if (a == null) {
907 throw new NoSuchElementException();
908 }
909 lastReturned = null;
910 BigInteger[] result = new BigInteger[f.numberOfDomains()];
911 for (int i = 0; i < result.length; ++i) {
912 BDDDomain dom = f.getDomain(i);
913 int[] ivar = dom.vars();
914 BigInteger val = BigInteger.ZERO;
915 for (int m = dom.varNum() - 1; m >= 0; m--) {
916 val = val.shiftLeft(1);
917 int level = f.var2Level(ivar[m]);
918 int k = Arrays.binarySearch(v, level);
919 if (k < 0) {
920 val = null;
921 break;
922 }
923 if (b[k]) {
924 val = val.add(BigInteger.ONE);
925 }
926 }
927 result[i] = val;
928 }
929 if (!gotoNextA()) {
930 gotoNext();
931 }
932 return result;
933 }
934
935 /***
936 * An alternate implementation of nextTuple().
937 * This may be slightly faster than the default if there are many domains.
938 *
939 * @return the next tuple of domain values in the iteration.
940 */
941 public BigInteger[] nextTuple2() {
942 boolean[] store = nextSat();
943 BigInteger[] result = new BigInteger[f.numberOfDomains()];
944 for (int i = 0; i < result.length; ++i) {
945 BDDDomain dom = f.getDomain(i);
946 int[] ivar = dom.vars();
947 BigInteger val = BigInteger.ZERO;
948 for (int m = dom.varNum() - 1; m >= 0; m--) {
949 val = val.shiftLeft(1);
950 if (store[ivar[m]])
951 val = val.add(BigInteger.ONE);
952 }
953 result[i] = val;
954 }
955 return result;
956 }
957
958 /***
959 * Return the next single satisfying assignment in the iteration.
960 *
961 * @return the next single satisfying assignment in the iteration.
962 */
963 public boolean[] nextSat() {
964 if (a == null) {
965 throw new NoSuchElementException();
966 }
967 lastReturned = null;
968 boolean[] result = new boolean[f.varNum()];
969 for (int i = 0; i < b.length; ++i) {
970 result[f.level2Var(v[i])] = b[i];
971 }
972 if (!gotoNextA()) {
973 gotoNext();
974 }
975 return result;
976 }
977
978 /***
979 * Return the next BDD in the iteration.
980 *
981 * @return the next BDD in the iteration
982 */
983 public BDD nextBDD() {
984 if (a == null) {
985 throw new NoSuchElementException();
986 }
987
988 lastReturned = f.universe();
989
990 for (int i = v.length-1; i >= 0; --i) {
991 int li = v[i];
992 int vi = f.level2Var(li);
993 if (b[i] == true) lastReturned.andWith(f.ithVar(vi));
994 else lastReturned.andWith(f.nithVar(vi));
995 }
996 if (!gotoNextA()) {
997 gotoNext();
998 }
999 return lastReturned;
1000 }
1001
1002
1003
1004
1005 public void remove() {
1006 if (lastReturned == null)
1007 throw new IllegalStateException();
1008 initialBDD.applyWith(lastReturned.id(), BDDFactory.diff);
1009 lastReturned = null;
1010 }
1011
1012 /***
1013 * <p>Returns true if the given BDD variable number is a dont-care.
1014 * <tt>var</tt> must be a variable in the iteration set.</p>
1015 *
1016 * @param var variable number to check
1017 * @return if the given variable is a dont-care
1018 */
1019 public boolean isDontCare(int var) {
1020 if (a == null) return false;
1021 int level = f.var2Level(var);
1022 return a[level] == -1;
1023 }
1024
1025 /***
1026 * <p>Returns true if the BDD variables in the given BDD domain are
1027 * all dont-care's.<p>
1028 *
1029 * @param d domain to check
1030 * @return if the variables are all dont-cares
1031 * @throws BDDException if d is not in the iteration set
1032 */
1033 public boolean isDontCare(BDDDomain d) {
1034 if (a == null) return false;
1035 int[] vars = d.vars();
1036 for (int i = 0; i < vars.length; ++i) {
1037 if (!isDontCare(vars[i])) return false;
1038 }
1039 return true;
1040 }
1041
1042 /***
1043 * Fast-forward the iteration such that the given variable number is true.
1044 *
1045 * @param var number of variable
1046 */
1047 public void fastForward(int var) {
1048 if (a == null)
1049 throw new BDDException();
1050 int level = f.var2Level(var);
1051 int i = Arrays.binarySearch(v, level);
1052 if (i < 0 || a[i] != -1)
1053 throw new BDDException();
1054 b[i] = true;
1055 }
1056
1057 /***
1058 * Fast-forward the iteration such that the given set of variables are true.
1059 *
1060 * @param vars set of variable indices
1061 */
1062 public void fastForward(int[] vars) {
1063 for (int i = 0; i < vars.length; ++i) {
1064 fastForward(vars[i]);
1065 }
1066 }
1067
1068 /***
1069 * Assuming <tt>d</tt> is a dont-care, skip to the end of the iteration for
1070 * <tt>d</tt>
1071 *
1072 * @param d BDD domain to fast-forward past
1073 */
1074 public void skipDontCare(BDDDomain d) {
1075 int[] vars = d.vars();
1076 fastForward(vars);
1077 if (!gotoNextA()) {
1078 gotoNext();
1079 }
1080 }
1081 }
1082
1083 /***
1084 * <p>Returns a BDD where all variables are replaced with the variables
1085 * defined by pair. Each entry in pair consists of a old and a new variable.
1086 * Whenever the old variable is found in this BDD then a new node with
1087 * the new variable is inserted instead.</p>
1088 *
1089 * <p>Compare to bdd_replace.</p>
1090 *
1091 * @param pair pairing of variables to the BDDs that replace those variables
1092 * @return result of replace
1093 */
1094 public abstract BDD replace(BDDPairing pair);
1095
1096 /***
1097 * <p>Replaces all variables in this BDD with the variables defined by pair.
1098 * Each entry in pair consists of a old and a new variable. Whenever the
1099 * old variable is found in this BDD then a new node with the new variable
1100 * is inserted instead. Mutates the current BDD.</p>
1101 *
1102 * <p>Compare to bdd_replace and bdd_delref.</p>
1103 *
1104 * @param pair pairing of variables to the BDDs that replace those variables
1105 */
1106 public abstract BDD replaceWith(BDDPairing pair);
1107
1108 /***
1109 * <p>Prints the set of truth assignments specified by this BDD.</p>
1110 *
1111 * <p>Compare to bdd_printset.</p>
1112 */
1113 public void printSet() {
1114 System.out.println(this.toString());
1115 }
1116
1117 /***
1118 * <p>Prints this BDD using a set notation as in printSet() but with the index
1119 * of the finite domain blocks included instead of the BDD variables.</p>
1120 *
1121 * <p>Compare to fdd_printset.</p>
1122 */
1123 public void printSetWithDomains() {
1124 System.out.println(toStringWithDomains());
1125 }
1126
1127 /***
1128 * <p>Prints this BDD in dot graph notation.</p>
1129 *
1130 * <p>Compare to bdd_printdot.</p>
1131 */
1132 public void printDot() {
1133 PrintStream out = System.out;
1134 out.println("digraph G {");
1135 out.println("0 [shape=box, label=\"0\", style=filled, shape=box, height=0.3, width=0.3];");
1136 out.println("1 [shape=box, label=\"1\", style=filled, shape=box, height=0.3, width=0.3];");
1137
1138 boolean[] visited = new boolean[nodeCount()+2];
1139 visited[0] = true; visited[1] = true;
1140 HashMap map = new HashMap();
1141 map.put(getFactory().zero(), new Integer(0));
1142 map.put(getFactory().one(), new Integer(1));
1143 printdot_rec(out, 1, visited, map);
1144
1145 for (Iterator i = map.keySet().iterator(); i.hasNext(); ) {
1146 BDD b = (BDD) i.next();
1147 b.free();
1148 }
1149 out.println("}");
1150 }
1151
1152 protected int printdot_rec(PrintStream out, int current, boolean[] visited, HashMap map) {
1153 Integer ri = ((Integer) map.get(this));
1154 if (ri == null) {
1155 map.put(this.id(), ri = new Integer(++current));
1156 }
1157 int r = ri.intValue();
1158 if (visited[r])
1159 return current;
1160 visited[r] = true;
1161
1162
1163 out.println(r+" [label=\""+this.var()+"\"];");
1164
1165 BDD l = this.low(), h = this.high();
1166 Integer li = (Integer) map.get(l);
1167 if (li == null) {
1168 map.put(l.id(), li = new Integer(++current));
1169 }
1170 int low = li.intValue();
1171 Integer hi = (Integer) map.get(h);
1172 if (hi == null) {
1173 map.put(h.id(), hi = new Integer(++current));
1174 }
1175 int high = hi.intValue();
1176
1177 out.println(r+" -> "+low+" [style=dotted];");
1178 out.println(r+" -> "+high+" [style=filled];");
1179
1180 current = l.printdot_rec(out, current, visited, map);
1181 l.free();
1182 current = h.printdot_rec(out, current, visited, map);
1183 h.free();
1184 return current;
1185 }
1186
1187 /***
1188 * <p>Counts the number of distinct nodes used for this BDD.</p>
1189 *
1190 * <p>Compare to bdd_nodecount.</p>
1191 *
1192 * @return the number of distinct nodes used for this BDD
1193 */
1194 public abstract int nodeCount();
1195
1196 /***
1197 * <p>Counts the number of paths leading to the true terminal.</p>
1198 *
1199 * <p>Compare to bdd_pathcount.</p>
1200 *
1201 * @return the number of paths leading to the true terminal
1202 */
1203 public abstract double pathCount();
1204
1205 /***
1206 * <p>Calculates the number of satisfying variable assignments.</p>
1207 *
1208 * <p>Compare to bdd_satcount.</p>
1209 *
1210 * @return the number of satisfying variable assignments
1211 */
1212 public abstract double satCount();
1213
1214 /***
1215 * <p>Calculates the number of satisfying variable assignments to the variables
1216 * in the given varset. ASSUMES THAT THE BDD DOES NOT HAVE ANY ASSIGNMENTS TO
1217 * VARIABLES THAT ARE NOT IN VARSET. You will need to quantify out the other
1218 * variables first.</p>
1219 *
1220 * <p>Compare to bdd_satcountset.</p>
1221 *
1222 * @return the number of satisfying variable assignments
1223 */
1224 public double satCount(BDDVarSet varset) {
1225 BDDFactory factory = getFactory();
1226
1227 if (varset.isEmpty() || isZero())
1228 return 0.;
1229
1230 double unused = factory.varNum();
1231 unused -= varset.size();
1232 unused = satCount() / Math.pow(2.0, unused);
1233
1234 return unused >= 1.0 ? unused : 1.0;
1235 }
1236
1237 /***
1238 * <p>Calculates the logarithm of the number of satisfying variable assignments.</p>
1239 *
1240 * <p>Compare to bdd_satcount.</p>
1241 *
1242 * @return the logarithm of the number of satisfying variable assignments
1243 */
1244 public double logSatCount() {
1245 return Math.log(satCount());
1246 }
1247
1248 /***
1249 * <p>Calculates the logarithm of the number of satisfying variable assignments to the
1250 * variables in the given varset.</p>
1251 *
1252 * <p>Compare to bdd_satcountset.</p>
1253 *
1254 * @return the logarithm of the number of satisfying variable assignments
1255 */
1256 public double logSatCount(BDDVarSet varset) {
1257 return Math.log(satCount(varset));
1258 }
1259
1260 /***
1261 * <p>Counts the number of times each variable occurs in this BDD. The
1262 * result is stored and returned in an integer array where the i'th
1263 * position stores the number of times the i'th printing variable
1264 * occurred in the BDD.</p>
1265 *
1266 * <p>Compare to bdd_varprofile.</p>
1267 */
1268 public abstract int[] varProfile();
1269
1270 /***
1271 * <p>Returns true if this BDD equals that BDD, false otherwise.</p>
1272 *
1273 * @param that the BDD to compare with
1274 * @return true iff the two BDDs are equal
1275 */
1276 public abstract boolean equals(BDD that);
1277
1278
1279
1280
1281 public boolean equals(Object o) {
1282 if (!(o instanceof BDD)) return false;
1283 return this.equals((BDD) o);
1284 }
1285
1286
1287
1288
1289 public abstract int hashCode();
1290
1291
1292
1293
1294 public String toString() {
1295 BDDFactory f = this.getFactory();
1296 int[] set = new int[f.varNum()];
1297 if (f.isZDD())
1298 Arrays.fill(set, 1);
1299 StringBuffer sb = new StringBuffer();
1300 bdd_printset_rec(f, sb, this, set);
1301 return sb.toString();
1302 }
1303
1304 private static void bdd_printset_rec(BDDFactory f, StringBuffer sb, BDD r, int[] set) {
1305 int n;
1306 boolean first;
1307
1308 if (r.isZero())
1309 return;
1310 else if (r.isOne()) {
1311 sb.append('<');
1312 first = true;
1313
1314 for (n = 0; n < set.length; n++) {
1315 if (set[n] > 0) {
1316 if (!first)
1317 sb.append(", ");
1318 first = false;
1319 sb.append(f.level2Var(n));
1320 sb.append(':');
1321 sb.append((set[n] == 2 ? 1 : 0));
1322 }
1323 }
1324 sb.append('>');
1325 } else {
1326 if (f.isZDD()) {
1327 if (r.low().equals(r.high())) {
1328 set[f.var2Level(r.var())] = 0;
1329 } else {
1330 BDD rl = r.low();
1331 bdd_printset_rec(f, sb, rl, set);
1332 rl.free();
1333
1334 set[f.var2Level(r.var())] = 2;
1335 }
1336 BDD rl = r.high();
1337 bdd_printset_rec(f, sb, rl, set);
1338 rl.free();
1339
1340 set[f.var2Level(r.var())] = 1;
1341 } else {
1342 set[f.var2Level(r.var())] = 1;
1343 BDD rl = r.low();
1344 bdd_printset_rec(f, sb, rl, set);
1345 rl.free();
1346
1347 set[f.var2Level(r.var())] = 2;
1348 BDD rh = r.high();
1349 bdd_printset_rec(f, sb, rh, set);
1350 rh.free();
1351
1352 set[f.var2Level(r.var())] = 0;
1353 }
1354 }
1355 }
1356
1357 /***
1358 * <p>Returns a string representation of this BDD using the defined domains.</p>
1359 *
1360 * @return string representation of this BDD using the defined domains
1361 */
1362 public String toStringWithDomains() {
1363 return toStringWithDomains(BDDToString.INSTANCE);
1364 }
1365
1366 /***
1367 * <p>Returns a string representation of this BDD on the defined domains,
1368 * using the given BDDToString converter.</p>
1369 *
1370 * @see net.sf.javabdd.BDD.BDDToString
1371 *
1372 * @return string representation of this BDD using the given BDDToString converter
1373 */
1374 public String toStringWithDomains(BDDToString ts) {
1375 if (this.isZero()) return "F";
1376 if (this.isOne()) return "T";
1377
1378 BDDFactory bdd = getFactory();
1379 StringBuffer sb = new StringBuffer();
1380 int[] set = new int[bdd.varNum()];
1381 fdd_printset_rec(bdd, sb, ts, this, set);
1382 return sb.toString();
1383 }
1384
1385 private static class OutputBuffer {
1386 BDDToString ts;
1387 StringBuffer sb;
1388 int domain;
1389 BigInteger lastLow;
1390 BigInteger lastHigh;
1391 boolean done;
1392
1393 static final BigInteger MINUS2 = BigInteger.valueOf(-2);
1394
1395 OutputBuffer(BDDToString ts, StringBuffer sb, int domain) {
1396 this.ts = ts;
1397 this.sb = sb;
1398 this.lastHigh = MINUS2;
1399 this.domain = domain;
1400 }
1401
1402 void append(BigInteger low, BigInteger high) {
1403 if (low.equals(lastHigh.add(BigInteger.ONE))) {
1404 lastHigh = high;
1405 } else {
1406 finish();
1407 lastLow = low; lastHigh = high;
1408 }
1409 }
1410
1411 StringBuffer finish() {
1412 if (!lastHigh.equals(MINUS2)) {
1413 if (done) sb.append('/');
1414 if (lastLow.equals(lastHigh))
1415 sb.append(ts.elementName(domain, lastHigh));
1416 else
1417 sb.append(ts.elementNames(domain, lastLow, lastHigh));
1418 lastHigh = MINUS2;
1419 }
1420 done = true;
1421 return sb;
1422 }
1423
1424 void append(BigInteger low) {
1425 append(low, low);
1426 }
1427 }
1428
1429 private static void fdd_printset_helper(OutputBuffer sb,
1430 BigInteger value, int i,
1431 int[] set, int[] var,
1432 int maxSkip) {
1433 if (i == maxSkip) {
1434
1435 BigInteger maxValue = value.or(BigInteger.ONE.shiftLeft(i+1).subtract(BigInteger.ONE));
1436 sb.append(value, maxValue);
1437 return;
1438 }
1439 int val = set[var[i]];
1440 if (val == 0) {
1441 BigInteger temp = value.setBit(i);
1442 fdd_printset_helper(sb, temp, i-1, set, var, maxSkip);
1443 }
1444 fdd_printset_helper(sb, value, i-1, set, var, maxSkip);
1445 }
1446
1447 private static void fdd_printset_rec(BDDFactory bdd, StringBuffer sb, BDDToString ts, BDD r, int[] set) {
1448 int fdvarnum = bdd.numberOfDomains();
1449
1450 int n, m, i;
1451 boolean used = false;
1452 int[] var;
1453 boolean first;
1454
1455 if (r.isZero())
1456 return;
1457 else if (r.isOne()) {
1458 sb.append('<');
1459 first = true;
1460
1461 for (n=0 ; n<fdvarnum ; n++) {
1462 used = false;
1463
1464 BDDDomain domain_n = bdd.getDomain(n);
1465
1466 int[] domain_n_ivar = domain_n.vars();
1467 int domain_n_varnum = domain_n_ivar.length;
1468 for (m=0 ; m<domain_n_varnum ; m++)
1469 if (set[domain_n_ivar[m]] != 0)
1470 used = true;
1471
1472 if (used) {
1473 if (!first)
1474 sb.append(", ");
1475 first = false;
1476 sb.append(domain_n.getName());
1477 sb.append(':');
1478
1479 var = domain_n_ivar;
1480
1481 BigInteger pos = BigInteger.ZERO;
1482 int maxSkip = -1;
1483 boolean hasDontCare = false;
1484 for (i=0; i<domain_n_varnum; ++i) {
1485 int val = set[var[i]];
1486 if (val == 0) {
1487 hasDontCare = true;
1488 if (maxSkip == i-1)
1489 maxSkip = i;
1490 }
1491 }
1492 for (i=domain_n_varnum-1; i>=0; --i) {
1493 pos = pos.shiftLeft(1);
1494 int val = set[var[i]];
1495 if (val == 2) {
1496 pos = pos.setBit(0);
1497 }
1498 }
1499 if (!hasDontCare) {
1500 sb.append(ts.elementName(n, pos));
1501 } else {
1502 OutputBuffer ob = new OutputBuffer(ts, sb, n);
1503 fdd_printset_helper(ob, pos, domain_n_varnum-1,
1504 set, var, maxSkip);
1505 ob.finish();
1506 }
1507 }
1508 }
1509
1510 sb.append('>');
1511 } else {
1512 set[r.var()] = 1;
1513 BDD lo = r.low();
1514 fdd_printset_rec(bdd, sb, ts, lo, set);
1515 lo.free();
1516
1517 set[r.var()] = 2;
1518 BDD hi = r.high();
1519 fdd_printset_rec(bdd, sb, ts, hi, set);
1520 hi.free();
1521
1522 set[r.var()] = 0;
1523 }
1524 }
1525
1526 /***
1527 * <p>BDDToString is used to specify the printing behavior of BDDs with domains.
1528 * Subclass this type and pass it as an argument to toStringWithDomains to
1529 * have the toStringWithDomains function use your domain names and element names,
1530 * instead of just numbers.</p>
1531 */
1532 public static class BDDToString {
1533 /***
1534 * <p>Singleton instance that does the default behavior: domains and
1535 * elements are printed as their numbers.</p>
1536 */
1537 public static final BDDToString INSTANCE = new BDDToString();
1538
1539 /***
1540 * <p>Protected constructor.</p>
1541 */
1542 protected BDDToString() { }
1543
1544 /***
1545 * <p>Given a domain index and an element index, return the element's name.
1546 * Called by the toStringWithDomains() function.</p>
1547 *
1548 * @param i the domain number
1549 * @param j the element number
1550 * @return the string representation of that element
1551 */
1552 public String elementName(int i, BigInteger j) {
1553 return j.toString();
1554 }
1555
1556 /***
1557 * <p>Given a domain index and an inclusive range of element indices,
1558 * return the names of the elements in that range.
1559 * Called by the toStringWithDomains() function.</p>
1560 *
1561 * @param i the domain number
1562 * @param lo the low range of element numbers, inclusive
1563 * @param hi the high range of element numbers, inclusive
1564 * @return the string representation of the elements in the range
1565 */
1566 public String elementNames(int i, BigInteger lo, BigInteger hi) {
1567 return lo.toString()+"-"+hi.toString();
1568 }
1569 }
1570
1571 /***
1572 * <p>Frees this BDD. Further use of this BDD will result in an exception being thrown.</p>
1573 */
1574 public abstract void free();
1575
1576 /***
1577 * <p>Protected constructor.</p>
1578 */
1579 protected BDD() { }
1580
1581 }