1
2
3
4 package net.sf.javabdd;
5
6 import java.math.BigInteger;
7 import net.sf.javabdd.BDD.BDDIterator;
8
9 /***
10 * Represents a domain of BDD variables. This is useful for finite state
11 * machines, among other things.
12 *
13 * <p>BDDDomains are called "finite domain blocks" in Section 2.9
14 * of the buddy documentation. A BDDDomain is a block of BDD variables
15 * that can represent integer values as opposed to only true and false.</p>
16 *
17 * <p>Use <tt>BDDFactory.extDomain()</tt> to create one or more domains with
18 * a specified list of sizes.</p>
19 *
20 * @author John Whaley
21 * @version $Id: BDDDomain.java 468 2006-11-29 08:07:13Z joewhaley $
22 * @see net.sf.javabdd.BDDFactory#extDomain(int[])
23 */
24 public abstract class BDDDomain {
25
26
27 protected String name;
28
29 protected int index;
30
31
32 protected BigInteger realsize;
33
34 protected int[] ivar;
35
36 protected BDDVarSet var;
37
38 /***
39 * Default constructor.
40 *
41 * @param index index of this domain
42 * @param range size of this domain
43 */
44 protected BDDDomain(int index, BigInteger range) {
45 BigInteger calcsize = BigInteger.valueOf(2L);
46 if (range.signum() <= 0)
47 throw new BDDException();
48 this.name = Integer.toString(index);
49 this.index = index;
50 this.realsize = range;
51 int binsize = 1;
52 while (calcsize.compareTo(range) < 0) {
53 binsize++;
54 calcsize = calcsize.shiftLeft(1);
55 }
56 this.ivar = new int[binsize];
57 }
58
59 /***
60 * Returns the factory that created this domain.
61 */
62 public abstract BDDFactory getFactory();
63
64 /***
65 * Sets the name of this domain.
66 */
67 public void setName(String name) {
68 this.name = name;
69 }
70
71 /***
72 * Gets the name of this domain.
73 */
74 public String getName() {
75 return name;
76 }
77
78 /***
79 * Returns the index of this domain.
80 */
81 public int getIndex() {
82 return index;
83 }
84
85 /***
86 * <p>Returns what corresponds to a disjunction of all possible values of this
87 * domain. This is more efficient than doing ithVar(0) OR ithVar(1) ...
88 * explicitly for all values in the domain.</p>
89 *
90 * <p>Compare to fdd_domain.</p>
91 */
92 public BDD domain() {
93 BDDFactory factory = getFactory();
94
95
96 BigInteger val = size().subtract(BigInteger.ONE);
97 BDD d = factory.universe();
98 int[] ivar = vars();
99 for (int n = 0; n < this.varNum(); n++) {
100 if (val.testBit(0))
101 d.orWith(factory.nithVar(ivar[n]));
102 else
103 d.andWith(factory.nithVar(ivar[n]));
104 val = val.shiftRight(1);
105 }
106 return d;
107 }
108
109 /***
110 * Returns the size of the domain for this finite domain block.
111 *
112 * Compare to fdd_domainsize.
113 */
114 public BigInteger size() {
115 return this.realsize;
116 }
117
118 public BDD buildAdd(BDDDomain that, long value) {
119 if (this.varNum() != that.varNum())
120 throw new BDDException();
121 return buildAdd(that, this.varNum(), value);
122 }
123 public BDD buildAdd(BDDDomain that, int bits, long value) {
124 if (bits > this.varNum() ||
125 bits > that.varNum())
126 throw new BDDException("Number of bits requested ("+bits+") is larger than domain sizes "+this.varNum()+","+that.varNum());
127
128 BDDFactory bdd = getFactory();
129
130 if (value == 0L) {
131 BDD result = bdd.universe();
132 int n;
133 for (n = 0; n < bits; n++) {
134 BDD b = bdd.ithVar(this.ivar[n]);
135 b.biimpWith(bdd.ithVar(that.ivar[n]));
136 result.andWith(b);
137 }
138 for ( ; n < Math.max(this.varNum(), that.varNum()); n++) {
139 BDD b = (n < this.varNum()) ? bdd.nithVar(this.ivar[n]) : bdd.one();
140 b.andWith((n < that.varNum()) ? bdd.nithVar(that.ivar[n]) : bdd.one());
141 result.andWith(b);
142 }
143 return result;
144 }
145
146 int[] vars = new int[bits];
147 System.arraycopy(this.ivar, 0, vars, 0, vars.length);
148 BDDBitVector y = bdd.buildVector(vars);
149 BDDBitVector v = bdd.constantVector(bits, value);
150 BDDBitVector z = y.add(v);
151
152 int[] thatvars = new int[bits];
153 System.arraycopy(that.ivar, 0, thatvars, 0, thatvars.length);
154 BDDBitVector x = bdd.buildVector(thatvars);
155 BDD result = bdd.one();
156 int n;
157 for (n = 0; n < x.size(); n++) {
158 BDD b = x.bitvec[n].biimp(z.bitvec[n]);
159 result.andWith(b);
160 }
161 for ( ; n < Math.max(this.varNum(), that.varNum()); n++) {
162 BDD b = (n < this.varNum()) ? bdd.nithVar(this.ivar[n]) : bdd.one();
163 b.andWith((n < that.varNum()) ? bdd.nithVar(that.ivar[n]) : bdd.one());
164 result.andWith(b);
165 }
166 x.free(); y.free(); z.free(); v.free();
167 return result;
168 }
169
170 /***
171 * Builds a BDD which is true for all the possible assignments to the
172 * variable blocks that makes the blocks equal.
173 *
174 * Compare to fdd_equals/fdd_equ.
175 *
176 * @param that
177 * @return BDD
178 */
179 public BDD buildEquals(BDDDomain that) {
180 if (!this.size().equals(that.size())) {
181 throw new BDDException("Size of "+this+" != size of that "+that+"( "+this.size()+" vs "+that.size()+")");
182 }
183
184 BDDFactory factory = getFactory();
185 BDD e = factory.universe();
186
187 int[] this_ivar = this.vars();
188 int[] that_ivar = that.vars();
189
190 for (int n = 0; n < this.varNum(); n++) {
191 BDD a = factory.ithVar(this_ivar[n]);
192 BDD b = factory.ithVar(that_ivar[n]);
193 a.biimpWith(b);
194 e.andWith(a);
195 }
196
197 return e;
198 }
199
200 /***
201 * Returns the variable set that contains the variables used to define this
202 * finite domain block.
203 *
204 * Compare to fdd_ithset.
205 *
206 * @return BDDVarSet
207 */
208 public BDDVarSet set() {
209 return var.id();
210 }
211
212 /***
213 * Returns the BDD that defines the given value for this finite domain
214 * block.
215 *
216 * Compare to fdd_ithvar.
217 *
218 * @return BDD
219 */
220 public BDD ithVar(long val) {
221 return ithVar(BigInteger.valueOf(val));
222 }
223 public BDD ithVar(BigInteger val) {
224 if (val.signum() < 0 || val.compareTo(size()) >= 0) {
225 throw new BDDException(val+" is out of range");
226 }
227
228 BDDFactory factory = getFactory();
229 BDD v = factory.universe();
230 int[] ivar = this.vars();
231 for (int n = 0; n < ivar.length; n++) {
232 if (val.testBit(0))
233 v.andWith(factory.ithVar(ivar[n]));
234 else
235 v.andWith(factory.nithVar(ivar[n]));
236 val = val.shiftRight(1);
237 }
238
239 return v;
240 }
241
242 /***
243 * Returns the BDD that defines the given range of values, inclusive,
244 * for this finite domain block.
245 *
246 * @return BDD
247 */
248 public BDD varRange(long lo, long hi) {
249 return varRange(BigInteger.valueOf(lo), BigInteger.valueOf(hi));
250 }
251 public BDD varRange(BigInteger lo, BigInteger hi) {
252 if (lo.signum() < 0 || hi.compareTo(size()) >= 0 || lo.compareTo(hi) > 0) {
253 throw new BDDException("range <"+lo+", "+hi+"> is invalid");
254 }
255
256 BDDFactory factory = getFactory();
257 BDD result = factory.zero();
258 int[] ivar = this.vars();
259 while (lo.compareTo(hi) <= 0) {
260 BDD v = factory.universe();
261 for (int n = ivar.length - 1; ; n--) {
262 if (lo.testBit(n)) {
263 v.andWith(factory.ithVar(ivar[n]));
264 } else {
265 v.andWith(factory.nithVar(ivar[n]));
266 }
267 BigInteger mask = BigInteger.ONE.shiftLeft(n).subtract(BigInteger.ONE);
268 if (!lo.testBit(n) && lo.or(mask).compareTo(hi) <= 0) {
269 lo = lo.or(mask).add(BigInteger.ONE);
270 break;
271 }
272 }
273 result.orWith(v);
274 }
275 return result;
276 }
277
278 /***
279 * Returns the number of BDD variables used for this finite domain block.
280 *
281 * Compare to fdd_varnum.
282 *
283 * @return int
284 */
285 public int varNum() {
286 return this.ivar.length;
287 }
288
289 /***
290 * Returns an integer array containing the indices of the BDD variables used
291 * to define this finite domain.
292 *
293 * Compare to fdd_vars.
294 *
295 * @return int[]
296 */
297 public int[] vars() {
298 return this.ivar;
299 }
300
301 public int ensureCapacity(long range) {
302 return ensureCapacity(BigInteger.valueOf(range));
303 }
304 public int ensureCapacity(BigInteger range) {
305 BigInteger calcsize = BigInteger.valueOf(2L);
306 if (range.signum() < 0)
307 throw new BDDException();
308 if (range.compareTo(realsize) < 0)
309 return ivar.length;
310 this.realsize = range.add(BigInteger.ONE);
311 int binsize = 1;
312 while (calcsize.compareTo(range) <= 0) {
313 binsize++;
314 calcsize = calcsize.shiftLeft(1);
315 }
316 if (ivar.length == binsize) return binsize;
317
318 throw new BDDException("Can't add bits to domains, requested domain "+name+" upper limit "+range);
319 }
320
321
322
323
324 public String toString() {
325 return getName();
326 }
327
328 /***
329 * Convert a BDD that to a list of indices of this domain.
330 * This method assumes that the BDD passed is a disjunction
331 * of ithVar(i_1) to ithVar(i_k). It returns an array
332 * of length 'k' with elements [i_1,...,i_k].
333 * <p>
334 * Be careful when using this method for BDDs with a large number
335 * of entries, as it allocates a BigInteger[] array of dimension k.
336 *
337 * @param bdd bdd that is the disjunction of domain indices
338 * @see #getVarIndices(BDD,int)
339 * @see #ithVar(BigInteger)
340 */
341 public BigInteger[] getVarIndices(BDD bdd) {
342 return getVarIndices(bdd, -1);
343 }
344
345 /***
346 * Convert a BDD that to a list of indices of this domain.
347 * Same as getVarIndices(BDD), except only 'max' indices
348 * are extracted.
349 *
350 * @param bdd bdd that is the disjunction of domain indices
351 * @param max maximum number of entries to be returned
352 *
353 * @see #ithVar(long)
354 */
355 public BigInteger[] getVarIndices(BDD bdd, int max) {
356 BDDVarSet myvarset = set();
357 int n = (int) bdd.satCount(myvarset);
358 if (max != -1 && n > max)
359 n = max;
360 BigInteger[] res = new BigInteger[n];
361 BDDIterator it = bdd.iterator(myvarset);
362 myvarset.free();
363 for (int i = 0; i < n; i++) {
364 res[i] = it.nextValue(this);
365 }
366 return res;
367 }
368 }