Source code: mlsub/typing/lowlevel/DomainVector.java
1 package mlsub.typing.lowlevel;
2
3 /**
4 * A DomainVector maintains an upper approximation of the set of solutions of
5 * a constraint. What is handled dynamically : constraints between rigid and
6 * soft variables. Constraints between soft variables are handled in gfp().
7 *
8 * RMK: only garbage indexes can have null domains
9 *
10 * @version $OrigRevision: 1.9 $, $OrigDate: 1999/10/03 17:37:05 $
11 * @author Alexandre Frey
12 **/
13 final class DomainVector extends java.util.Vector {
14 int offset; // offset
15 int width; // size of domains
16
17 public DomainVector(int offset, int width) {
18 this.offset = offset;
19 this.width = width;
20 }
21 public DomainVector(int offset, int width, int n) {
22 super(n);
23 setSize(n);
24 //if (width > 0) {
25 for (int i = 0; i < n; i++) {
26 setElementAt(new Domain(width), i);
27 }
28 //}
29 this.offset = offset;
30 this.width = width;
31 }
32 public Domain getDomain(int x) {
33 return (Domain)elementAt(x - offset);
34 }
35
36 private boolean isValidSoft(int x) {
37 return x>=offset && x-offset<size() && getDomain(x)!=null;
38 }
39 private boolean isGarbage(int x) {
40 return x>=offset && x-offset<size() && getDomain(x)==null;
41 }
42
43 public void clear(int x) {
44 setElementAt(null, x - offset);
45 }
46 public void reduce(int x, boolean unit, BitVector domain)
47 throws LowlevelUnsatisfiable {
48 S.assume(S.a&& isValidSoft(x));
49 Domain d = getDomain(x);
50 d.reduce(unit, domain);
51 }
52 public void exclude(int x, BitVector domain)
53 throws LowlevelUnsatisfiable {
54 S.assume(S.a&& isValidSoft(x));
55 Domain d = getDomain(x);
56 d.exclude(domain);
57 }
58
59 public void merge(int src, int dest) throws LowlevelUnsatisfiable {
60 S.assume(S.a&& isValidSoft(src));
61 Domain srcDomain = getDomain(src);
62 if (dest >= offset) {
63 // don't forget unit !
64 reduce(dest, srcDomain.containsUnit(), srcDomain);
65 }
66 else {
67 // dest is rigid
68 S.assume(S.a&& srcDomain.get(dest),src+" merged with "+dest);
69 }
70 clear(src);
71 }
72
73 public void exclude(int value) throws LowlevelUnsatisfiable {
74 for (int i = 0; i < elementCount; i++) {
75 Domain d = (Domain)elementData[i];
76 if (d != null) {
77 d.exclude(value);
78 }
79 }
80 }
81 public void move(int src, int dest) {
82 S.assume(S.a&& isValidSoft(src));
83 S.assume(S.a&& isGarbage(dest));
84 setElementAt(getDomain(src), dest - offset);
85 clear(src);
86 }
87 public void extend() {
88 // if (width > 0) {
89 addElement(new Domain(width));
90 //} else {
91 //addElement(null);
92 //}
93 }
94
95 public Object clone() {
96 DomainVector result = (DomainVector)super.clone();
97 for (int i = 0; i < elementCount; i++) {
98 Domain d = ((Domain)elementData[i]);
99 if (d != null) {
100 result.elementData[i] = (Domain)d.clone();
101 }
102 }
103 return result;
104 }
105
106 /***********************************************************************
107 * Fix-point computations
108 ***********************************************************************/
109 private boolean gfpSweep(BitMatrix R, BitMatrix C,
110 int[] strategy, int dS,
111 int direction)
112 throws LowlevelUnsatisfiable {
113 boolean changed = false;
114 BitVector ideal = new BitVector(width);
115 boolean idealContainsUnit = false;
116 int length = strategy.length;
117 for (int s = (dS > 0 ? 0 : length - 1); s >= 0 && s < length; s += dS) {
118 int x = strategy[s];
119 Domain dx = getDomain(x);
120 if (dx != null) {
121 // XXX: already tested ??
122 if (dx.isEmpty()) {
123 throw new LowlevelUnsatisfiable();
124 }
125 if (dx.needPropagation(direction)) {
126 changed = true;
127 // compute the ideal of dx
128 // the ideal may contain unit !
129 ideal.clearAll();
130 idealContainsUnit = dx.containsUnit();
131 ideal.addProduct(R, dx);
132
133 // and intersect the domain of all element j above x with ideal
134 for (int j = offset; j < offset + elementCount; j++) {
135 Domain dj = getDomain(j);
136 if (dj != null && C.get(x, j)) {
137 if(K0.debugK0){
138 S.dbg.println("Reducing domain of "+j);
139 S.dbg.println("from "+dj);
140 S.dbg.println("with ideal of "+x+": "+ideal);
141 }
142 dj.reduce(idealContainsUnit, ideal);
143 // XXX: not necessary to test emptyness ??
144 }
145 // emptyness of dj will normally be tested later on
146 // XXX: this comment correct ?
147 }
148 }
149 }
150 }
151 return changed;
152 }
153
154 /**
155 * Reduce this domain vector to the greatest fixed-point of a constraint.
156 * @param R constraint on the rigid constants (in [0, width[)
157 * @param Rt its transpose
158 * @param C constraint on [0, offset + size()[
159 * @param Ct its tranpose
160 * @param strategy an iteration strategy: topological sort of C
161 **/
162 public void gfp(BitMatrix R, BitMatrix Rt,
163 BitMatrix C, BitMatrix Ct,
164 int[] strategy)
165 throws LowlevelUnsatisfiable {
166 boolean changed;
167 do {
168 changed = gfpSweep(R, C, strategy, +1, Domain.UP);
169 changed = gfpSweep(Rt, Ct, strategy, -1, Domain.DOWN) || changed;
170 } while (changed);
171 }
172
173 void initGfpCardinals() {
174 for (int i = 0; i < elementCount; i++) {
175 Domain d = (Domain)elementData[i];
176 if (d != null) {
177 d.initGfpCardinals();
178 }
179 }
180 }
181
182 /**
183 * Choose a non-null, non-singleton, domain and return its index. Return -1
184 * if all the domains are instantiated.
185 **/
186 public int chooseDomain() {
187 return chooseDomain(null);
188 }
189
190 /**
191 * ditto but choose a domain whose index i is in set
192 **/
193 public int chooseDomain(BitVector set) {
194 /*
195 * Choose the domain of least cardinal (first-fail heuristic)
196 */
197 int leastCard = Integer.MAX_VALUE;
198 int least = Integer.MIN_VALUE;
199 for (int i = 0; i < elementCount; i++) {
200 if (set == null || set.get(i + offset)) {
201 Domain d = (Domain)elementAt(i);
202 if (d != null){
203 int card = d.cardinal();
204 if (card < leastCard && card > 1) {
205 least = i + offset;
206 leastCard = card;
207 }
208 }
209 }
210 }
211 return least;
212 }
213
214
215 // toString is final in class java.util.Vector...
216 public String dump() {
217 Separator sep = new Separator(", ");
218 StringBuffer sb = new StringBuffer();
219 for (int i = 0; i < elementCount; i++) {
220 if (elementData[i] != null) {
221 sb.append(sep)
222 .append("D(")
223 .append(i + offset)
224 .append(") = ")
225 .append(elementData[i]);
226 }
227 }
228 return sb.toString();
229 }
230 }
231