001: package mlsub.typing.lowlevel;
002:
003: /**
004: * A DomainVector maintains an upper approximation of the set of solutions of
005: * a constraint. What is handled dynamically : constraints between rigid and
006: * soft variables. Constraints between soft variables are handled in gfp().
007: *
008: * RMK: only garbage indexes can have null domains
009: *
010: * @version $OrigRevision: 1.9 $, $OrigDate: 1999/10/03 17:37:05 $
011: * @author Alexandre Frey
012: **/
013: final class DomainVector extends java.util.ArrayList {
014: int offset; // offset
015: int width; // size of domains
016:
017: public DomainVector(DomainVector old) {
018: super (old.size());
019: this .offset = old.offset;
020: this .width = old.width;
021: for (int i = 0; i < old.size(); i++) {
022: Domain d = ((Domain) old.get(i));
023: if (d != null)
024: add(new Domain(d));
025: else
026: add(null);
027: }
028: }
029:
030: public DomainVector(int offset, int width) {
031: this .offset = offset;
032: this .width = width;
033: }
034:
035: public DomainVector(int offset, int width, int n) {
036: super (n);
037: //if (width > 0) {
038: for (int i = 0; i < n; i++) {
039: add(new Domain(width));
040: }
041: //}
042: this .offset = offset;
043: this .width = width;
044: }
045:
046: public Domain getDomain(int x) {
047: return (Domain) get(x - offset);
048: }
049:
050: void truncate(int x) {
051: removeRange(x, size());
052: }
053:
054: private boolean isValidSoft(int x) {
055: return x >= offset && x - offset < size()
056: && getDomain(x) != null;
057: }
058:
059: private boolean isGarbage(int x) {
060: return x >= offset && x - offset < size()
061: && getDomain(x) == null;
062: }
063:
064: public void clear(int x) {
065: set(x - offset, null);
066: }
067:
068: public void reduce(int x, boolean unit, BitVector domain)
069: throws LowlevelUnsatisfiable {
070: S.assume(S.a && isValidSoft(x));
071: Domain d = getDomain(x);
072: d.reduce(unit, domain);
073: }
074:
075: public void exclude(int x, BitVector domain)
076: throws LowlevelUnsatisfiable {
077: S.assume(S.a && isValidSoft(x));
078: Domain d = getDomain(x);
079: d.exclude(domain);
080: }
081:
082: public void merge(int src, int dest) throws LowlevelUnsatisfiable {
083: S.assume(S.a && isValidSoft(src));
084: Domain srcDomain = getDomain(src);
085: if (dest >= offset) {
086: // don't forget unit !
087: reduce(dest, srcDomain.containsUnit(), srcDomain);
088: } else {
089: // dest is rigid
090: S.assume(S.a && srcDomain.get(dest), src + " merged with "
091: + dest);
092: }
093: clear(src);
094: }
095:
096: public void exclude(int value) throws LowlevelUnsatisfiable {
097: for (int i = 0; i < size(); i++) {
098: Domain d = (Domain) get(i);
099: if (d != null) {
100: d.exclude(value);
101: }
102: }
103: }
104:
105: public void move(int src, int dest) {
106: S.assume(S.a && isValidSoft(src));
107: S.assume(S.a && isGarbage(dest));
108: set(dest - offset, getDomain(src));
109: clear(src);
110: }
111:
112: public void extend() {
113: // if (width > 0) {
114: add(new Domain(width));
115: //} else {
116: //addElement(null);
117: //}
118: }
119:
120: /***********************************************************************
121: * Fix-point computations
122: ***********************************************************************/
123: private boolean gfpSweep(BitMatrix R, BitMatrix C, int[] strategy,
124: int dS, int direction) throws LowlevelUnsatisfiable {
125: boolean changed = false;
126: BitVector ideal = new BitVector(width);
127: boolean idealContainsUnit = false;
128: int length = strategy.length;
129: for (int s = (dS > 0 ? 0 : length - 1); s >= 0 && s < length; s += dS) {
130: int x = strategy[s];
131: Domain dx = getDomain(x);
132: if (dx != null) {
133: // XXX: already tested ??
134: if (dx.isEmpty()) {
135: throw LowlevelUnsatisfiable.instance;
136: }
137: if (dx.needPropagation(direction)) {
138: changed = true;
139: // compute the ideal of dx
140: // the ideal may contain unit !
141: ideal.clearAll();
142: idealContainsUnit = dx.containsUnit();
143: ideal.addProduct(R, dx);
144:
145: // and intersect the domain of all element j above x with ideal
146: for (int j = offset; j < offset + size(); j++) {
147: Domain dj = getDomain(j);
148: if (dj != null && C.get(x, j)) {
149: if (K0.debugK0) {
150: S.dbg
151: .println("Reducing domain of "
152: + j);
153: S.dbg.println("from " + dj);
154: S.dbg.println("with ideal of " + x
155: + ": " + ideal);
156: }
157: dj.reduce(idealContainsUnit, ideal);
158: // XXX: not necessary to test emptyness ??
159: }
160: // emptyness of dj will normally be tested later on
161: // XXX: this comment correct ?
162: }
163: }
164: }
165: }
166: return changed;
167: }
168:
169: /**
170: * Reduce this domain vector to the greatest fixed-point of a constraint.
171: * @param R constraint on the rigid constants (in [0, width[)
172: * @param Rt its transpose
173: * @param C constraint on [0, offset + size()[
174: * @param Ct its tranpose
175: * @param strategy an iteration strategy: topological sort of C
176: **/
177: public void gfp(BitMatrix R, BitMatrix Rt, BitMatrix C,
178: BitMatrix Ct, int[] strategy) throws LowlevelUnsatisfiable {
179: boolean changed;
180: do {
181: changed = gfpSweep(R, C, strategy, +1, Domain.UP);
182: changed = gfpSweep(Rt, Ct, strategy, -1, Domain.DOWN)
183: || changed;
184: } while (changed);
185: }
186:
187: void initGfpCardinals() {
188: for (int i = 0; i < size(); i++) {
189: Domain d = (Domain) get(i);
190: if (d != null) {
191: d.initGfpCardinals();
192: }
193: }
194: }
195:
196: /**
197: * Choose a non-null, non-singleton, domain and return its index. Return -1
198: * if all the domains are instantiated.
199: **/
200: public int chooseDomain() {
201: return chooseDomain(null);
202: }
203:
204: /**
205: * ditto but choose a domain whose index i is in set
206: **/
207: public int chooseDomain(BitVector set) {
208: /*
209: * Choose the domain of least cardinal (first-fail heuristic)
210: */
211: int leastCard = Integer.MAX_VALUE;
212: int least = Integer.MIN_VALUE;
213: for (int i = 0; i < size(); i++) {
214: if (set == null || set.get(i + offset)) {
215: Domain d = (Domain) get(i);
216: if (d != null) {
217: int card = d.cardinal();
218: if (card < leastCard && card > 1) {
219: least = i + offset;
220: leastCard = card;
221: }
222: }
223: }
224: }
225: return least;
226: }
227:
228: // toString is final in class java.util.Vector...
229: public String dump() {
230: Separator sep = new Separator(", ");
231: StringBuffer sb = new StringBuffer();
232: for (int i = 0; i < size(); i++) {
233: if (get(i) != null) {
234: sb.append(sep).append("D(").append(i + offset).append(
235: ") = ").append(get(i));
236: }
237: }
238: return sb.toString();
239: }
240: }
|