1
2
3
4 package net.sf.javabdd;
5
6 /***
7 * Encodes a table of variable pairs. This is used for replacing variables in a
8 * BDD.
9 *
10 * @author John Whaley
11 * @version $Id: BDDPairing.java 282 2004-10-16 02:59:52Z joewhaley $
12 */
13 public abstract class BDDPairing {
14
15 /***
16 * Adds the pair (oldvar, newvar) to this table of pairs. This results in
17 * oldvar being substituted with newvar in a call to BDD.replace().
18 *
19 * Compare to bdd_setpair.
20 */
21 public abstract void set(int oldvar, int newvar);
22
23 /***
24 * Like set(), but with a whole list of pairs.
25 *
26 * Compare to bdd_setpairs.
27 */
28 public void set(int[] oldvar, int[] newvar) {
29 if (oldvar.length != newvar.length)
30 throw new BDDException();
31
32 for (int n = 0; n < oldvar.length; n++)
33 this.set(oldvar[n], newvar[n]);
34 }
35
36 /***
37 * Adds the pair (oldvar, newvar) to this table of pairs. This results in
38 * oldvar being substituted with newvar in a call to bdd.replace(). The
39 * variable oldvar is substituted with the BDD newvar. The possibility to
40 * substitute with any BDD as newvar is utilized in BDD.compose(), whereas
41 * only the topmost variable in the BDD is used in BDD.replace().
42 *
43 * Compare to bdd_setbddpair.
44 */
45 public abstract void set(int oldvar, BDD newvar);
46
47 /***
48 * Like set(), but with a whole list of pairs.
49 *
50 * Compare to bdd_setbddpairs.
51 */
52 public void set(int[] oldvar, BDD[] newvar) {
53 if (oldvar.length != newvar.length)
54 throw new BDDException();
55
56 for (int n = 0; n < newvar.length; n++)
57 this.set(oldvar[n], newvar[n]);
58 }
59
60 /***
61 * Defines each variable in the finite domain block p1 to be paired with the
62 * corresponding variable in p2.
63 *
64 * Compare to fdd_setpair.
65 */
66 public void set(BDDDomain p1, BDDDomain p2) {
67 int[] ivar1 = p1.vars();
68 int[] ivar2 = p2.vars();
69 this.set(ivar1, ivar2);
70 }
71
72 /***
73 * Like set(), but with a whole list of pairs.
74 *
75 * Compare to fdd_setpairs.
76 */
77 public void set(BDDDomain[] p1, BDDDomain[] p2) {
78 if (p1.length != p2.length)
79 throw new BDDException();
80
81 for (int n = 0; n < p1.length; n++)
82 if (p1[n].varNum() != p2[n].varNum())
83 throw new BDDException();
84
85 for (int n = 0; n < p1.length; n++) {
86 this.set(p1[n], p2[n]);
87 }
88 }
89
90 /***
91 * Resets this table of pairs by setting all substitutions to their default
92 * values (that is, no change).
93 *
94 * Compare to bdd_resetpair.
95 */
96 public abstract void reset();
97
98 }