001: package mlsub.typing.lowlevel;
002:
003: import java.util.ArrayList;
004:
005: /**
006: A square matrix of bits, used to represent a relation between integers.
007:
008: @version $Revision: 1.11 $, $Date: 2005/03/30 23:07:58 $
009: @author Alexandre Frey
010: @author Daniel Bonniot (Optimization for sparse and reflexives matrices)
011: **/
012: final public class BitMatrix {
013: /**
014: * a vector of BitVectors. rows.get(i) is the ith line of
015: * the matrix.
016: **/
017: private BitVector[] rows;
018: private int size;
019:
020: // A BitVector instance can be saved if the only bit set is the one
021: // on the diagonal, which is usual here.
022: private boolean reflexive;
023:
024: /**
025: * Constructs an empty matrix
026: **/
027: public BitMatrix() {
028: this (10);
029: }
030:
031: private BitMatrix(int rowCapacity) {
032: if (rowCapacity == 0)
033: rowCapacity = 5;
034: rows = new BitVector[rowCapacity];
035: }
036:
037: /**
038: * Creates a copy of a matrix
039: **/
040: public BitMatrix(BitMatrix old) {
041: BitVector[] oldRows = old.rows;
042: BitVector[] newRows = new BitVector[oldRows.length];
043: for (int i = old.size - 1; i >= 0; i--) {
044: BitVector row = oldRows[i];
045: if (row != null && !row.isEmpty())
046: newRows[i] = new BitVector(row);
047: }
048:
049: this .rows = newRows;
050: this .size = old.size;
051: this .reflexive = old.reflexive;
052: }
053:
054: /**
055: * Returns the number of rows and columns of this matrix
056: **/
057: public int size() {
058: return size;
059: }
060:
061: /**
062: * Set the size of the matrix. If the new size is greater than the current
063: * size, new empty rows and columns are added. If the new size is less than
064: * the current size, all rows and columns at index greater than newSize are
065: * discarded.
066: **/
067: public void setSize(int newSize) {
068: if (newSize < size) {
069: // clear the columns beyond newSize, so that subsequent calls to extend()
070: // or setSize will find them empty.
071: for (int i = 0; i < newSize; i++) {
072: BitVector row = rows[i];
073: if (row != null) {
074: row.truncate(newSize);
075: }
076: }
077: for (int i = size; i > newSize;)
078: rows[--i] = null;
079: } else {
080: if (rows.length < newSize) {
081: BitVector[] newRows = new BitVector[rows.length * 2];
082: System.arraycopy(rows, 0, newRows, 0, rows.length);
083: rows = newRows;
084: }
085: }
086: size = newSize;
087: }
088:
089: /**
090: * Grow the matrix by one column and one row, initially empty. Returns the
091: * index of the new row.
092: **/
093: public int extend() {
094: setSize(size + 1);
095: return size - 1;
096: }
097:
098: /**
099: To be able to return a correct row for reflexive matrices
100: without allocating a new one, we share the short ones
101: with only one bit set.
102: */
103: private static BitVector[] reflexiveRow = new BitVector[256];
104:
105: /**
106: * Get ith row. May return null if it is empty or if row is beyond size()
107: *
108: * <p>If the matrix is reflexive, the row MUST NOT be modified by the caller.
109: **/
110: final BitVector getRow(int i) {
111: if (i < size) {
112: if (reflexive && rows[i] == null) {
113: if (i >= reflexiveRow.length || reflexiveRow[i] == null) {
114: BitVector res = new BitVector(i + 1);
115: res.set(i);
116: if (i < reflexiveRow.length)
117: reflexiveRow[i] = res;
118: return res;
119: }
120:
121: return reflexiveRow[i];
122: } else {
123: if (reflexive)
124: rows[i].set(i);
125: return rows[i];
126: }
127: } else {
128: return null;
129: }
130: }
131:
132: /**
133: * get element at position (i, j), i.e., returns the value of i < j.
134: * Assume i and j are valid indexes
135: **/
136: final public boolean get(int i, int j) {
137: if (i == j && reflexive)
138: return true;
139:
140: BitVector row = rows[i];
141: return row != null && row.get(j);
142: }
143:
144: /**
145: * get index next set bit greater than j in row i.
146: * Assume i and j are valid indexes.
147: **/
148: final public int getNextSetInRow(int i, int j) {
149: BitVector row = rows[i];
150: if (reflexive) {
151: if (row == null) {
152: if (i > j)
153: return i;
154: return BitVector.UNDEFINED_INDEX;
155: }
156: int k = row.getNextBit(j);
157: if ((i > j) && ((k < 0) || (k > i)))
158: return i;
159: return k;
160: }
161: if (row == null)
162: return BitVector.UNDEFINED_INDEX;
163: return row.getNextBit(j);
164: }
165:
166: /**
167: * Set element at position (i, j) to true. Assume i and j are valid indexes.
168: **/
169: public void set(int i, int j) {
170: if (i == j && reflexive)
171: return;
172:
173: BitVector row = rows[i];
174: if (row == null) {
175: row = new BitVector(size);
176: rows[i] = row;
177: }
178: row.set(j);
179: }
180:
181: /**
182: * Set element at position (i, j) to false. Assume i and j are valid indexes.
183: **/
184: public void clear(int i, int j) {
185: if (i == j && reflexive) {
186: // Outch! We have to get back to a non-reflexive representation
187: reflexive = false;
188: for (int k = 0; k < size; k++)
189: if (k != i)
190: set(k, k);
191: }
192:
193: BitVector row = rows[i];
194: if (row != null) {
195: row.clear(j);
196: }
197: }
198:
199: /**
200: * Performs in-place reflexive transitive closure of the relation.
201: **/
202: public void closure() {
203: if (S.debug) {
204: BitMatrix testcopy = new BitMatrix(this );
205: BitMatrix original = new BitMatrix(this );
206: this .closure2();
207: testcopy.closure1();
208: boolean equal = true;
209: for (int i = 0; i < size; i++)
210: if (!((this .getRow(i) == testcopy.getRow(i)) || (this
211: .getRow(i).equals(testcopy.getRow(i)))))
212: equal = false;
213: if (!equal) {
214: Debug
215: .println("Warning new closure method produced incorrect results.");
216: Debug.println("orginal matrix:");
217: Debug.println(original.toString());
218: Debug.println("closure using new method:");
219: Debug.println(this .toString());
220: Debug.println("closure using standard method:");
221: Debug.println(testcopy.toString());
222: }
223:
224: } else if (size < 16)
225: closure1();
226: else
227: closure2();
228: }
229:
230: private void closure1() {
231: // Warshall algorithm
232: int size = this .size;
233: for (int k = 0; k < size; k++) {
234: BitVector row_k = rows[k];
235: if (row_k != null) {
236: for (int i = 0; i < size; i++) {
237: BitVector row_i = rows[i];
238: if (row_i != null && row_i.get(k)) { // i < k
239: /* for all j such that k < j, add i < j */
240: row_i.or(row_k);
241: }
242: }
243: }
244: }
245: //for (int i = 0; i < size; i++) set(i, i);
246: reflexive = true;
247: }
248:
249: /**
250: This algorithm is O(n*m) (m = average number bits set per row) when there
251: are no cylcic relations in the a matrix, while closure1 is O(n2).
252: This algorithm has a much larger overhead so for small matrices
253: the old one still faster.
254: */
255: private void closure2() {
256: int size = this .size;
257: boolean[] done = new boolean[size];
258: boolean[] busy = new boolean[size];
259: int[] index = new int[size];
260: int[] bitpos = new int[size];
261: int ndone = 0;
262: while (ndone < size) {
263: if ((rows[ndone] != null) && !done[ndone]) {
264: int stackpos = 0;
265: index[0] = ndone;
266: bitpos[0] = 0;
267: busy[ndone] = true;
268: BitVector current = rows[ndone];
269: while (stackpos >= 0) {
270: if (bitpos[stackpos] < 0) {
271: if (stackpos > 0) {
272: rows[index[stackpos - 1]]
273: .or(rows[index[stackpos]]);
274: current = rows[index[stackpos - 1]];
275: }
276: done[index[stackpos]] = true;
277: busy[index[stackpos--]] = false;
278: } else {
279: int nextbitpos = current
280: .getLowestSetBit(bitpos[stackpos]);
281: if (nextbitpos < 0 || nextbitpos >= size)
282: bitpos[stackpos] = -1;
283: else {
284: bitpos[stackpos] = nextbitpos + 1;
285: if (rows[nextbitpos] != null) {
286: if (done[nextbitpos]) {
287: rows[index[stackpos]]
288: .or(rows[nextbitpos]);
289: } else {
290: if (!busy[nextbitpos]) {
291: busy[nextbitpos] = true;
292: index[++stackpos] = nextbitpos;
293: bitpos[stackpos] = 0;
294: current = rows[index[stackpos]];
295: } else {
296: if (index[stackpos] != nextbitpos) {
297: int tempsp = stackpos - 1;
298: BitVector cyclicmask = new BitVector(
299: size);
300: do {
301: bitpos[tempsp] = -1;
302: rows[index[stackpos]]
303: .or(rows[index[tempsp]]);
304: cyclicmask
305: .set(index[tempsp]);
306: } while (index[tempsp--] != nextbitpos);
307: current = new BitVector(
308: current);
309: current.andNot(cyclicmask);
310: bitpos[stackpos] = 0;
311: }
312: }
313: }
314: }
315: }
316: }
317: }
318: }
319: ndone++;
320: }
321: reflexive = true;
322: }
323:
324: /**
325: * Returns a newly-allocated BitMatrix initialized with the transpose
326: * of this BitMatrix
327: **/
328: public BitMatrix transpose() {
329: BitMatrix m = new BitMatrix(size);
330: m.setSize(size);
331: for (int i = 0; i < size; i++) {
332: BitVector row = rows[i];
333: if (row != null) {
334: for (int j = row.getLowestSetBit(); j >= 0; j = row
335: .getLowestSetBit(j + 1))
336: m.set(j, i);
337: }
338: }
339: m.reflexive = reflexive;
340: return m;
341: }
342:
343: public String toString() {
344: StringBuffer sb = new StringBuffer("{");
345:
346: boolean needSeparator = false;
347:
348: for (int row = 0; row < size; row++)
349: for (int col = 0; col < size; col++)
350: if (get(row, col)) {
351: if (needSeparator) {
352: sb.append(", ");
353: } else {
354: needSeparator = true;
355: }
356: sb.append("(").append(row).append(",").append(col)
357: .append(")");
358: }
359: return sb.append("}").toString();
360: }
361:
362: public boolean equals(Object obj) {
363: if (this == obj)
364: return true;
365:
366: if (obj == null || !(obj instanceof BitMatrix))
367: return false;
368:
369: BitMatrix that = (BitMatrix) obj;
370:
371: for (int row = 0; row < size; row++)
372: for (int col = 0; col < size; col++)
373: if (get(row, col) != that.get(row, col))
374: return false;
375:
376: return true;
377: }
378:
379: /**
380: * Fills the array S with a topological sort of the relation on [m, size()[
381: * described by this matrix. Assume that S is large enough to hold size() -
382: * m integers. Assume 0 <= m <= this.size().
383: *
384: * <p>After a call to topologicalSort() and if the relation is a DAG, for
385: * all i, j such that this.get(i, j) is true, i appears before j in S
386: **/
387: public void topologicalSort(int m, int[] S) {
388: // The algorithm should be modified to handle reflexive case.
389: // Easy way out: insert the reflexive points.
390: // However I'm not sure this case ever happens anyway:
391: // topologicalSort is only used in Satisfier on C which is not reflexive
392:
393: int n = size;
394: int[] sortStack = new int[n - m];
395: int sp = -1; // index in sortStack
396: int s = n - m; // index in S
397: BitVector touched = new BitVector(n);
398: touched.fill(m);
399: for (int i = m; i < n; i++) {
400: if (!touched.get(i)) {
401: touched.set(i);
402: sortStack[++sp] = i;
403: loop: while (sp >= 0) {
404: int j = sortStack[sp];
405: BitVector row_j = getRow(j);
406: if (row_j != null) {
407: int succ = row_j.getLowestSetBitNotIn(touched);
408: if (succ >= 0) {
409: // do the successor first
410: touched.set(succ);
411: sortStack[++sp] = succ;
412: continue loop;
413: }
414: }
415: // no untouched successor found
416: sp--; // pop j
417: S[--s] = j; // push it on the sort array
418: }
419: }
420: }
421: }
422:
423: /**
424: * Tests if this bit matrix is included in M on the first n columns and
425: * lines. Assume m <= this.size() and m <= M.size(). If there exists (i, j)
426: * < (m, m) such that this.get(i, j) but !M.get(i, j), return an array a
427: * such that a[0] = i and a[1] = j. Otherwise, return null.
428: **/
429: public int[] includedIn(int m, BitMatrix M) {
430: if (this == M) {
431: return null;
432: } else {
433: for (int i = 0; i < m; i++) {
434: BitVector row1 = this .getRow(i);
435: if (row1 != null) {
436: int j;
437: BitVector row2 = M.getRow(i);
438: if (row2 != null) {
439: j = row1.getLowestSetBitNotIn(row2);
440: } else {
441: j = row1.getLowestSetBit();
442: }
443: if (0 <= j && j < m) {
444: return new int[] { i, j };
445: }
446: }
447: }
448: return null;
449: }
450: }
451:
452: /**
453: Move index src to dest.
454: */
455: public void indexMove(int src, int dest) {
456: rowMove(src, dest);
457: colMove(src, dest);
458: }
459:
460: /**
461: * In-place copy row src to row dest and clear row src. The previous results
462: * of getRow(src) must not be used after this call.
463: **/
464: private void rowMove(int src, int dest) {
465: rows[dest] = getRow(src);
466: rows[src] = null;
467: }
468:
469: /**
470: * copy column src to column dest and clear column src.
471: * Assume src != dest
472: **/
473: private void colMove(int src, int dest) {
474: for (int i = 0; i < size; i++) {
475: BitVector row = getRow(i);
476: if (row != null) {
477: row.bitCopy(src, dest);
478: }
479: }
480: }
481:
482: /**
483: Merge indexes src and dest, put the result in dest.
484: */
485: public void indexMerge(int src, int dest) {
486: rowMerge(src, dest);
487: colMerge(src, dest);
488: }
489:
490: /**
491: * Merge row src and row dest, put the result in row dest.
492: * Assume src != dest. Previous results of getRow(src) must not be used
493: * after this call.
494: **/
495: private void rowMerge(int src, int dest) {
496: BitVector srcRow = getRow(src);
497: if (srcRow != null) {
498: BitVector destRow = getRow(dest);
499: if (destRow == null) {
500: rows[dest] = srcRow;
501: } else {
502: destRow.or(srcRow);
503: }
504: }
505: rows[src] = null;
506: }
507:
508: /**
509: * Merge column src and column dest, put the result in column dest. Assume
510: * src != dest.
511: **/
512: private void colMerge(int src, int dest) {
513: for (int i = 0; i < size; i++) {
514: BitVector row = getRow(i);
515: if (row != null) {
516: row.bitMerge(src, dest);
517: }
518: }
519: }
520:
521: /**
522: * Compute the set of y such that x <* y.
523: **/
524: public BitVector ideal(int x) {
525: BitVector ideal = new BitVector(size);
526: addIdeal(x, ideal);
527: return ideal;
528: }
529:
530: // assume !ideal.get(x)
531: private void addIdeal(int x, BitVector ideal) {
532: ideal.set(x);
533: BitVector xUp = getRow(x);
534: if (xUp != null) {
535: int y;
536: while ((y = xUp.getLowestSetBitNotIn(ideal)) >= 0) {
537: addIdeal(y, ideal);
538: }
539: }
540: }
541: }
|