Source code: mlsub/typing/lowlevel/K0.java
1 package mlsub.typing.lowlevel;
2
3 import java.util.Vector;
4
5 /**
6 * A lowlevel constraint on integers.
7 *
8 * @version $OrigRevision: 1.22 $, $OrigDate: 1999/10/28 10:56:58 $
9 * @author Alexandre Frey
10 * @author Daniel Bonniot (Abstractable Interfaces, and unlimited backtrack)
11 **/
12 public final class K0 {
13 public static abstract class Callbacks {
14 /**
15 * Called when indexes src and dest have been merged. Only dest remains
16 * valid: src is invalidated
17 **/
18 abstract protected void indexMerged(int src, int dest)
19 throws Unsatisfiable;
20
21 /**
22 * Called when index src has been moved to index dest.
23 **/
24 abstract protected void indexMoved(int src, int dest);
25
26 /**
27 * Called when simplification discards index
28 **/
29 abstract protected void indexDiscarded(int index);
30
31 /*
32 * Pretty printing
33 */
34 protected String getName() {
35 return "<k0>";
36 }
37 protected String indexToString(int x) {
38 return Integer.toString(x);
39 }
40 protected String interfaceToString(int iid) {
41 return Integer.toString(iid);
42 }
43 }
44
45 /***********************************************************************
46 * Debugging
47 ***********************************************************************/
48 public static boolean debugK0 = S.debugK0;
49 private static int IDs = 0;
50 private int ID = IDs++;
51
52 // When a K0 is created it is in a special mode where the initial rigid
53 // context is created. In this mode, one can use methods extend, initialLeq,
54 // minimal, newInterface, subInterface, and initialImplements. Then,
55 // one must call method createInitialContext()
56 //
57 // The constraint is then in normal mode, one can no more use the
58 // above-mentioned methods (except extend),
59 // but must use leq, eq, indexImplements, satisfy,
60 // enumerate, rigidify, mark, backtrack, weakMark, weakBacktrack, getSnap,
61 // startSimplify, stopSimplify, tag, simplify, isLeq,
62 // solveConstructorOverloading, solveInterfaceOverloading
63 //
64 // backtrackMode must be either BACKTRACK_ONCE or BACKTRACK_UNLIMITED
65 // see below the doc of backtrack() and mark()
66 public K0(int backtrackMode, Callbacks callbacks) {
67 this.backtrackMode = backtrackMode;
68 this.callbacks = callbacks;
69 this.R = null;
70 this.Rt = null;
71 this.m = 0;
72 this.C = new BitMatrix();
73 this.Ct = new BitMatrix();
74 this.n = 0;
75 this.minimal = new BitVector();
76 this.garbage = new BitVector();
77 this.posTagged = new BitVector();
78 this.negTagged = new BitVector();
79 this.interfaces = new Vector();
80 if (debugK0) {
81 System.err.println("created K0 #" + ID);
82 }
83 }
84
85 public K0(Callbacks callbacks) {
86 this(BACKTRACK_ONCE, callbacks);
87 }
88
89 private Callbacks callbacks;
90
91 /**
92 * Relation on the rigid indexes
93 **/
94 private BitMatrix R;
95 /**
96 * Transpose of R
97 **/
98 private BitMatrix Rt;
99 /**
100 * Number of rigid indexes. Below m, the relation is closed.
101 **/
102 private int m;
103
104 /**
105 * Number of rigid indexes in the initial rigid context
106 * (m0 <= m)
107 **/
108 private int m0;
109
110 int initialContextSize()
111 {
112 return m0;
113 }
114
115 /**
116 * Returns an index that is guaranteed to be greater than any rigid index
117 * and less or equal to any non-rigid index.
118 **/
119 public int firstNonRigid() {
120 return m;
121 }
122
123 /**
124 * Returns true if x is the index of a rigid variable.
125 * the index is assumed valid
126 **/
127 public boolean isRigid(int x) {
128 return x < m;
129 }
130
131 public boolean hasNoSoft() {
132 return n == m;
133 }
134 /**
135 * C maintains the constraint as it is entered
136 **/
137 private BitMatrix C;
138 /**
139 * Transpose of C
140 **/
141 private BitMatrix Ct;
142 /**
143 * Total number of indexes.
144 * Invariant: m <= n && n == C.size()
145 **/
146 private int n;
147
148 public int size() {
149 return n;
150 }
151
152 /**
153 * Maintains the information "x is minimal" on [0, m0[
154 **/
155 private BitVector minimal;
156 public boolean isMinimal(int x) {
157 return minimal.get(x);
158 }
159 public void minimal(int x) {
160 minimal.set(x);
161 }
162
163 // tells if an index should be collected in the next call to collect()
164 private BitVector garbage;
165
166 public boolean isValidIndex(int x) {
167 return x >= 0 && x < n && !garbage.get(x);
168 }
169
170
171 /***********************************************************************
172 * Pretty printing
173 ***********************************************************************/
174 public String getName() {
175 return callbacks.getName();
176 }
177
178 private String indexToString(int index) {
179 return callbacks.indexToString(index);
180 }
181 String interfaceToString(int iid) {
182 return callbacks.interfaceToString(iid);
183 }
184
185 public String domainsToString() {
186 StringBuffer sb = new StringBuffer();
187 for (int i = m; i < n; i++) {
188 if (isValidIndex(i)) {
189 sb.append("D(").append(indexToString(i)).append(") = ");
190 Domain d = (hasBeenInitialized ? domains.getDomain(i) : null);
191 sb.append(d);
192 sb.append("; ");
193 }
194 }
195 return sb.toString();
196 }
197
198 private BitVector weakComponent(int x0) {
199 S.assume(S.a&& isValidIndex(x0));
200 BitVector component = new BitVector();
201 BitVector toInclude = new BitVector();
202 toInclude.set(x0);
203 while (true) {
204 int x = toInclude.getLowestSetBitNotIn(component);
205 if (x == BitVector.UNDEFINED_INDEX) {
206 break;
207 }
208 if (!garbage.get(x)) {
209 component.set(x);
210 BitVector ux = C.getRow(x);
211 if (ux != null) {
212 toInclude.or(ux);
213 }
214 BitVector lx = Ct.getRow(x);
215 if (lx != null) {
216 toInclude.or(lx);
217 }
218 }
219 }
220 return component;
221 }
222
223 private String ineqToString(int x, int y) {
224 return indexToString(x) + " <: " + indexToString(y);
225 }
226
227 private String componentToString(BitVector component) {
228 StringBuffer sb = new StringBuffer();
229 Separator sep = new Separator(", ");
230 int nvars = 0;
231 for (int x = 0; x < n; x++) {
232 if (component.get(x)) {
233 sb.append(sep).append(indexToString(x));
234 if (isRigid(x)) {
235 sb.append("*");
236 }
237 nvars++;
238 }
239 }
240 if (nvars == 0) {
241 return "";
242 }
243
244 sb.append(" | ");
245 sep.reset();
246
247 // enumerate the (x, y) where x < y and at least one of x or y is >= m0
248 for (int x = 0; x < n; x++) {
249 if (component.get(x)) {
250 for (int y = (x < m0 ? m0 : x+1); y < n; y++) {
251 if (component.get(y)) {
252 if (C.get(y, x)) {
253 sb.append(sep).append(ineqToString(y, x));
254 }
255 if (C.get(x, y)) {
256 sb.append(sep).append(ineqToString(x, y));
257 }
258 }
259 }
260 }
261 }
262
263 for (int x = m0; x < n; x++) {
264 if (component.get(x)) {
265 for (int iid = 0; iid < nInterfaces(); iid++) {
266 if (getInterface(iid).implementors.get(x)) {
267 sb.append(sep)
268 .append(indexToString(x))
269 .append(": ")
270 .append(interfaceToString(iid));
271 }
272 }
273 }
274 }
275 return sb.toString();
276 }
277
278 public String toString() {
279 final StringBuffer sb = new StringBuffer();
280 Separator nl = new Separator("\n");
281
282 BitVector rest = new BitVector(n);
283 rest.fill(n);
284 String restComp = componentToString(rest);
285 if (!restComp.equals("")) {
286 sb.append(nl).append(restComp);
287 }
288 if (sb.length() != 0) {
289 sb.append("\n");
290 }
291 return sb.toString();
292 }
293
294 public String dumpInterfaces() {
295 final StringBuffer sb = new StringBuffer();
296 final Separator sep = new Separator(", ");
297 for (int iid = 0; iid < nInterfaces(); iid++) {
298 sb.append(sep).append(interfaceToString(iid));
299 }
300 sb.append(" | ");
301 sep.reset();
302 for (int iid1 = 0; iid1 < nInterfaces(); iid1++) {
303 for (int iid2 = 0; iid2 < nInterfaces(); iid2++) {
304 if (getInterface(iid2).subInterfaces.get(iid1)) {
305 sb.append(sep)
306 .append(interfaceToString(iid1))
307 .append(" < ")
308 .append(interfaceToString(iid2));
309 }
310 }
311 }
312 sb.append("\n");
313 sep.reset();
314 try{
315 implementsIter
316 (
317 new ImplementsIterator(){
318 public void iter(int x, int iid){
319 sb.append(sep)
320 .append(indexToString(x))
321 .append(" : ")
322 .append(interfaceToString(iid));
323 }
324 }
325 );
326 }
327 catch(Unsatisfiable e){}
328 try{
329 abstractsIter
330 (
331 new AbstractsIterator(){
332 public void iter(int x, int iid){
333 sb.append(sep)
334 .append(indexToString(x))
335 .append(" :: ")
336 .append(interfaceToString(iid));
337 }
338 }
339 );
340 }
341 catch(Unsatisfiable e){}
342 return sb.toString();
343 }
344
345 public String dumpRigid() {
346 StringBuffer sb = new StringBuffer();
347 Separator sep = new Separator(", ");
348 for (int x = 0; x < m; x++) {
349 if (isValidIndex(x)) {
350 sb.append(sep).append(indexToString(x));
351 }
352 }
353 sb.append(" | ");
354 sep.reset();
355 for (int x = 0; x < m; x++) {
356 for (int y = 0; y < m; y++) {
357 if (isValidIndex(x) && isValidIndex(y) && R.get(x, y)) {
358 sb.append(sep)
359 .append(indexToString(x))
360 .append(" < ")
361 .append(indexToString(y));
362 }
363 }
364 }
365 for (int iid = 0; iid < nInterfaces(); iid++) {
366 for (int x = 0; x < m; x++) {
367 if (isValidIndex(x) && getInterface(iid).rigidImplementors.get(x)) {
368 sb.append(sep)
369 .append(indexToString(x))
370 .append(": ")
371 .append(interfaceToString(iid));
372 }
373 }
374 }
375
376 return sb.toString();
377 }
378
379 /***********************************************************************/
380 private void setSize(int n) {
381 S.assume(S.a&& n >= m);
382 this.n = n;
383 C.setSize(n);
384 Ct.setSize(n);
385 if (domains != null) {
386 domains.setSize(n - m);
387 }
388 garbage.truncate(n);
389 posTagged.truncate(n);
390 negTagged.truncate(n);
391 minimal.truncate(n);
392 for (int iid = 0; iid < nInterfaces(); iid++) {
393 getInterface(iid).setIndexSize(n);
394 }
395 }
396
397 // collect and compact indexes in [i, j[
398 // returns the last non garbage index plus one of the compacted matrix
399 private int collect(int i, int j) {
400 while (true) {
401 while (true) {
402 if (i >= j) { return i; }
403 if (garbage.get(i)) { break; }
404 i++;
405 }
406 while (true) {
407 if (i >= j) { return i; }
408 j--;
409 if (!garbage.get(j)) { break; }
410 }
411 indexMove(j, i);
412 i++;
413 }
414 }
415
416 // this operation always succeeds
417 private void collect() {
418 setSize(collect(m, n));
419 }
420
421 // assume src > dest && !garbage.get(src) && garbage.get(dest)
422 private void indexMove(int src, int dest) {
423 domainMove(src, dest);
424 posTagged.bitCopy(src, dest);
425 negTagged.bitCopy(src, dest);
426 for (int iid = 0; iid < nInterfaces(); iid++) {
427 getInterface(iid).indexMove(src, dest);
428 }
429 garbage.set(src);
430 garbage.clear(dest);
431 C.indexMove(src, dest);
432 Ct.indexMove(src, dest);
433
434 // notify the user of K0
435 callbacks.indexMoved(src, dest);
436 }
437
438 // assume src > dest && !garbage.get(src) && !garbage.get(dest)
439 private void indexMerge(int src, int dest) throws Unsatisfiable {
440 domainMerge(src, dest);
441 C.indexMerge(src, dest);
442 Ct.indexMerge(src, dest);
443 for (int iid = 0; iid < nInterfaces(); iid++) {
444 getInterface(iid).indexMerge(src, dest);
445 }
446 garbage.set(src);
447 posTagged.bitMerge(src, dest);
448 negTagged.bitMerge(src, dest);
449 // notify the subclass
450 callbacks.indexMerged(src, dest);
451 }
452
453 /**
454 * Add a new variable to the constraint and returns its index
455 **/
456 public int extend() {
457 C.extend();
458 Ct.extend();
459 garbage.clear(n);
460 if (hasBeenInitialized) {
461 domains.extend();
462 }
463 return n++;
464 }
465
466 // a vector of all the Interfaces in this constraint
467 private Vector interfaces;
468 /**
469 * Returns the number of interfaces. Interfaces are garanteed to be
470 * numbered from 0 to nInterfaces()-1
471 **/
472 public int nInterfaces() {
473 return interfaces.size();
474 }
475
476 // assume 0 <= iid < nInterfaces()
477 Interface getInterface(int iid) {
478 return (Interface)interfaces.elementAt(iid);
479 }
480
481 /***********************************************************************
482 * Construction of the initial rigid context
483 ***********************************************************************/
484 private boolean hasBeenInitialized = false;
485 public boolean hasBeenInitialized() {
486 return hasBeenInitialized;
487 }
488 /**
489 * Add a new interface to the constraint and returns its ID
490 **/
491 public int newInterface() {
492 S.assume(S.a&& !hasBeenInitialized);
493 int iid = nInterfaces();
494 Interface iface = new Interface(this, iid);
495 interfaces.addElement(iface);
496 if (debugK0) {
497 System.err.println("newInterface in #" + ID + " -> " + iid);
498 }
499 return iid;
500 }
501
502 /**
503 * Enter the assertion that interface iid1 is a subinterface of iid2
504 * Assume if1 and if2 are >=0 and < nInterfaces()
505 **/
506 public void subInterface(int iid1, int iid2) {
507 S.assume(S.a&& !hasBeenInitialized);
508 getInterface(iid2).subInterfaces.set(iid1);
509 }
510
511 /**
512 * Enter the initial assertion that x : iid
513 **/
514 public void initialImplements(int x, int iid) {
515 S.assume(S.a&& !hasBeenInitialized);
516 getInterface(iid).implementors.set(x);
517 }
518
519 /**
520 * Enter the initial assertion that x :: iid
521 * This means that no node strictly lesser than x may implement iid
522 **/
523 public void initialAbstracts(int x, int iid) {
524 S.assume(S.a&& !hasBeenInitialized);
525 getInterface(iid).abstractors.set(x);
526 }
527
528 /**
529 * Enter the initial assertion that x <= y
530 **/
531 public void initialLeq(int x, int y) {
532 S.assume(S.a&& !hasBeenInitialized);
533 C.set(x, y);
534 Ct.set(y, x);
535 }
536
537 /***********************************************************************
538 * Initial rigidification
539 ***********************************************************************/
540
541 public void createInitialContext()
542 throws LowlevelUnsatisfiable
543 {
544 S.assume(S.a&& !hasBeenInitialized);
545
546 // put in R and Rt, the constraint saturated under
547 // x < y and y < z => x < z
548 R = (BitMatrix)C.clone();
549 R.closure();
550 Rt = (BitMatrix)Ct.clone();
551 Rt.closure();
552 m0 = m = n;
553
554 // saturate the interface subtyping under
555 // I < J and J < K => I < K
556 closeInterfaceRelation();
557
558 BitVector[] rigidImplementors = closeImplements(R, Rt);
559 for (int iid = 0; iid < nInterfaces(); iid++) {
560 getInterface(iid).rigidImplementors = rigidImplementors[iid];
561 }
562
563 computeInitialArrows();
564
565 if(debugK0)
566 System.err.println("Initial Context (saturated) "+getName()+":\n" +
567 this + "\n" +
568 dumpInterfaces() + "\n");
569
570 domains = new DomainVector(m, m);
571 hasBeenInitialized = true;
572 }
573
574 public void releaseInitialContext()
575 {
576 hasBeenInitialized=false;
577
578 if(m != m0)
579 System.err.println("releaseInitialContext should be called when in first rigid context");
580
581 m0 = m = 0;
582 }
583
584 /***********************************************************************
585 * Constraints
586 ***********************************************************************/
587 /**
588 * Enter the constraint x: iid
589 * Assume x is a valid index and iid is a valid interface id
590 **/
591 public void indexImplements(int x, int iid) throws Unsatisfiable {
592 S.assume(S.a&& hasBeenInitialized);
593 if (LowlevelUnsatisfiable.refinedReports) {
594 try {
595 indexImplements0(x, iid);
596 } catch (LowlevelUnsatisfiable e) {
597 throw refine(e);
598 }
599 } else {
600 indexImplements0(x, iid);
601 }
602 }
603
604 // this method makes no effort to report refined unsatisfiability
605 private void indexImplements0(int x, int iid) throws LowlevelUnsatisfiable {
606 if (debugK0) {
607 System.err.println("#" + ID + " -> " + indexToString(x) + ": " + interfaceToString(iid));
608 }
609 Interface iface = getInterface(iid);
610 if (iface.implementors.get(x)) {
611 // nothing to do !
612 return;
613 }
614 if (isRigid(x)) {
615 if (!iface.rigidImplementors.get(x)) {
616 throw new LowlevelImplementsClash(x, iid);
617 } else {
618 return;
619 }
620 }
621 iface.implementors.set(x);
622 // include unit since unit implements all the interfaces
623 reduceDomain(x, true, iface.rigidImplementors);
624 }
625
626 /**
627 * Enter the constraint x1 = x2
628 * Assume x1 and x2 are valid indexes
629 **/
630 public void eq(int x1, int x2) throws Unsatisfiable {
631 leq(x1, x2);
632 leq(x2, x1);
633 }
634
635 /**
636 * Enter the constraint x1 <= x2.
637 * Assume x1 and x2 are valid indexes.
638 **/
639 public void leq(int x1, int x2) throws Unsatisfiable {
640 S.assume(S.a&& hasBeenInitialized);
641 if (LowlevelUnsatisfiable.refinedReports) {
642 try {
643 leq0(x1, x2);
644 } catch (LowlevelUnsatisfiable e) {
645 throw refine(e);
646 }
647 } else {
648 leq0(x1, x2);
649 }
650 }
651
652 public void enterConstraint(int x1, int v0, int x2) throws Unsatisfiable {
653 if (v0 > 0) {
654 leq(x1, x2);
655 }
656 if (v0 < 0) {
657 leq (x2, x1);
658 }
659 if (v0 == 0) {
660 eq(x1, x2);
661 }
662 }
663
664 // versions that does not make any effort to report precise errors
665 // in case of rigid clash
666 private void leq0(int x1, int x2) throws LowlevelUnsatisfiable {
667 if (debugK0) {
668 System.err.println("#" + ID + " -> " + indexToString(x1) + " <: " + indexToString(x2));
669 }
670 if (x1 == x2) { return; }
671 if (C.get(x1, x2)) { return; }
672 // Modify C and Ct after test for rigid clash
673 // so that the constraint if both x1 and x2 are rigid
674 // makes it unnecessary to mark-backtrack in some cases
675 if (isRigid(x1) && isRigid(x2)) {
676 if (!R.get(x1, x2)) {
677 throw new LowlevelRigidClash(indexToString(x1), indexToString(x2));
678 } else {
679 return;
680 }
681 }
682 C.set(x1, x2);
683 Ct.set(x2, x1);
684 if (isRigid(x1)) {
685 // !isRigid(x2)
686 // exclude unit since unit is not comparable to x1
687 reduceDomain(x2, false, R.getRow(x1));
688 }
689 if (isRigid(x2)) {
690 // !isRigid(x1)
691 // exclude unit
692 reduceDomain(x1, false, Rt.getRow(x2));
693 if (minimal.get(x2)) {
694 // x1 = x2;
695 leq0(x2, x1);
696 }
697 }
698 }
699
700 /***********************************************************************
701 * Better error messages
702 ***********************************************************************/
703 // try to refine the exception e, in case of rigid clashes the constraint is
704 // known to be unsatisfiable at this point NB: this method is only called in
705 // case of unsatisfiability that is to be reported to the user. The
706 // important point is to get a message that is precise enough. There is no
707 // need to optimize this method.
708 private LowlevelUnsatisfiable refine(LowlevelUnsatisfiable e) {
709 if (K0.debugK0) {
710 System.err.println("Trying to refine " + e);
711 System.err.println("The constraint is " + this.toString());
712 System.err.println("The rigid constraint is " + dumpRigid());
713 e.printStackTrace();
714 }
715 if (e instanceof LowlevelRigidClash
716 ||
717 e instanceof LowlevelImplementsClash) {
718 return e;
719 }
720 // close the constraint
721 // it does no harm to modify the constraint since
722 // it will be backtracked to display the error message
723 C.closure();
724 Ct.closure();
725
726 BitVector[] saturatedImplementors = closeImplements(C, Ct);
727 for (int iid = 0; iid < nInterfaces(); iid++) {
728 getInterface(iid).implementors = saturatedImplementors[iid];
729 }
730
731 // then try to find a rigid clash, i.e., a constraint a < b where a is not
732 // a subtype of b in the rigid context
733 int[] rigidClash = C.includedIn(m, R);
734 if (rigidClash != null) {
735 return new LowlevelRigidClash(indexToString(rigidClash[0]),
736 indexToString(rigidClash[1]));
737 }
738
739 // try to refine even better: find if the unsatisfiability
740 // stems from attempt to put a common supertype or subtype
741 // to incompatible rigid types
742 LowlevelIncompatibleClash clash = null;
743 clash
744 = refineIncompatible(C, R,
745 LowlevelIncompatibleClash.NO_COMMON_SUPERTYPE);
746 if (clash != null) {
747 return clash;
748 }
749 clash
750 = refineIncompatible(Ct, Rt,
751 LowlevelIncompatibleClash.NO_COMMON_SUBTYPE);
752 if (clash != null) {
753 return clash;
754 }
755
756 // finally try to find an "implements" clash
757 for (int iid = 0; iid < nInterfaces(); iid++) {
758 Interface iface = getInterface(iid);
759 int x = iface.implementors.getLowestSetBitNotIn(iface.rigidImplementors);
760 if (isValidIndex(x) && isRigid(x)) {
761 // XXX: la condition est bonne ???
762 // we've found an index x such that x: iid in the constraint but not
763 // in the rigid context
764 return new LowlevelImplementsClash(x, iid);
765 }
766 }
767
768 // At this point, we failed to give a better error message
769 // than the original one
770 return e;
771 }
772
773 private LowlevelIncompatibleClash refineIncompatible(BitMatrix C,
774 BitMatrix R,
775 int what) {
776 for (int a = 0; a < m; a++) {
777 for (int b = a + 1; b < m; b++) {
778 if (R.getRow(a).getLowestSetBitAnd(R.getRow(b))
779 == BitVector.UNDEFINED_INDEX) {
780 // R(a) and R(b) do not intersect
781 BitVector Ca = C.getRow(a);
782 if (Ca != null) {
783 BitVector Cb = C.getRow(b);
784 if (Cb != null) {
785 int z = Ca.getLowestSetBitAnd(Cb);
786 if (z != BitVector.UNDEFINED_INDEX) {
787 // here is the culprit !
788 return new LowlevelIncompatibleClash(what, a, b, z);
789 }
790 }
791 }
792 }
793 }
794 }
795 return null;
796 }
797
798 /***********************************************************************
799 * Domains
800 ***********************************************************************/
801 // each soft variable is associated to a domain, i.e., a subset of the rigid
802 // variables plus unit (a special rigid value that implements all the
803 // interfaces). Subtyping constraints between a soft variable and a rigid
804 // one, and "implements" constraints on a soft variable immediately affect
805 // the domain of the soft variable. If a domain becomes empty, the
806 // constraint is unsatisfiable. When method satisfy or enumerate is called,
807 // the domains already hold an initial approximation of the solutions, which
808 // is refined by iteration of the closure operators associated to the
809 // subtyping constraints between soft variables. Then, instantiation and
810 // backtracking are used to find a solution (see Satisfier)
811 private DomainVector domains = null;
812 private void domainMerge(int src, int dest) throws Unsatisfiable {
813 domains.merge(src, dest);
814 }
815 private void domainMove(int src, int dest) {
816 domains.move(src, dest);
817 }
818
819 public void reduceDomain(int x, boolean unit, BitVector set)
820 throws LowlevelUnsatisfiable {
821 S.assume(S.a&& x >= -1);
822 if (x == -1) {
823 if (!unit) {
824 throw new LowlevelUnsatisfiable();
825 }
826 } else if (x < m) {
827 // the domain must contain x itself (we assume here that the relation
828 // is condensed on the rigid variables)
829 if (!set.get(x)) {
830 throw new LowlevelUnsatisfiable();
831 }
832 } else {
833 if(debugK0){
834 System.err.println("Reducing domain of "+indexToString(x));
835 System.err.println("from "+domains.getDomain(x));
836 System.err.println("with "+set);
837 }
838 domains.reduce(x, unit, set);
839 }
840 }
841
842 /***********************************************************************
843 * Constraint preparation
844 ***********************************************************************/
845
846 // The constraint is "prepared" by
847 // 1. saturate it under Min and Abs axioms
848 // 2. condensing equivalent nodes
849
850 /**
851 * Saturate the constraint C, Ct under the axiom:
852 * x <* y and Min(y) => y < x (hence x ~ y)
853 **/
854 private void collapseMinimal() throws Unsatisfiable {
855 for (int y = 0; y < m0; y++) {
856 if (minimal.get(y)) {
857 BitVector uy = R.getRow(y);
858 // breadth-first search of the lower ideal of y
859 _collapsed.clearAll();
860 _toCollapse.clearAll();
861 _toCollapse.set(y);
862 while (true) {
863 int x = _toCollapse.getLowestSetBitNotIn(_collapsed);
864 if (x == BitVector.UNDEFINED_INDEX) {
865 break;
866 }
867 _collapsed.set(x);
868 BitVector lx = Ct.getRow(x);
869 if (lx != null) {
870 _toCollapse.or(lx);
871 }
872 if (x != y && !C.get(y, x)) {
873 // If x is a rigid variable, this is a clash.
874 if (x < m0)
875 throw new LowlevelRigidClash(indexToString(x), indexToString(y));
876 // set y < x
877 C.set(y, x);
878 Ct.set(x, y);
879 // exclude from D(x) all elements outside uy
880 // exclude unit as well
881 reduceDomain(x, false, uy);
882 }
883 }
884 }
885 }
886 }
887 // preallocate these bit-vectors
888 private BitVector _collapsed = new BitVector(256);
889 private BitVector _toCollapse = new BitVector(256);
890
891 /****************************************************************
892 * Algorithms on interfaces
893 ****************************************************************/
894
895 /**
896 * Computes the arrows a ->_i b
897 * for a's that abstract some surinterface of i
898 */
899 private void computeInitialArrows()
900 throws LowlevelUnsatisfiable
901 {
902 for (int iid = 0; iid < nInterfaces(); iid++)
903 {
904 Interface i = getInterface(iid);
905 BitVector abstractors = i.abstractors;
906 BitVector subInterfaces = i.subInterfaces;
907
908 for (int abs = abstractors.getLowestSetBit();
909 abs != BitVector.UNDEFINED_INDEX;
910 abs = abstractors.getNextBit(abs))
911 for (int jid = subInterfaces.getLowestSetBit();
912 jid != BitVector.UNDEFINED_INDEX;
913 jid = subInterfaces.getNextBit(jid))
914 // abs is a constant that abstracts i
915 // and j is a subInterface of i
916 {
917 BitVector labs = Rt.getRow(abs);
918 for (int node = labs.getLowestSetBit();
919 node != BitVector.UNDEFINED_INDEX;
920 node = labs.getNextBit(node))
921 setApproxToMinAbove(node, getInterface(jid), R);
922 }
923 }
924 computeApproxMinimals(0, R);
925 }
926
927 /**
928 Compute arrows for nodes in [min, n[
929 */
930 private void computeApproxMinimals(int min, BitMatrix leq)
931 throws LowlevelUnsatisfiable
932 {
933 for (int node = minimal.getLowestSetBit(min);
934 node != BitVector.UNDEFINED_INDEX;
935 node = minimal.getNextBit(node))
936 for (int iid = 0; iid < nInterfaces(); iid++)
937 setApproxToMinAbove(node, getInterface(iid), leq);
938 }
939
940 /**
941 Finds a minimum rigid node above 'abs' that implements 'j'
942 and set it as the approximation of 'abs' for 'j'.
943 */
944 private void setApproxToMinAbove(int abs, Interface j, BitMatrix leq)
945 throws LowlevelUnsatisfiable
946 {
947 BitVector implementors = j.rigidImplementors;
948
949 boolean toCheck = false;
950 int approx = BitVector.UNDEFINED_INDEX;
951
952 for (int x = implementors.getLowestSetBit();
953 x != BitVector.UNDEFINED_INDEX && x < m0;
954 x = implementors.getNextBit(x))
955 {
956 if (leq.get(abs,x))
957 if (approx==BitVector.UNDEFINED_INDEX || leq.get(x,approx))
958 approx = x;
959 else
960 // optimize ? :
961 // make tocheck an int, -1 at start. first to check-> N, second to check->-2 if not comparable with toCheck, otherwise the smaller
962 // if at then end toCheck == -2, full check. Otherwise just check leq.get(approx, toCheck) !
963 toCheck = true;
964 }
965
966 // verifies it is minimal
967 if(toCheck)
968 for (int x = implementors.getLowestSetBit();
969 x != BitVector.UNDEFINED_INDEX;
970 x = implementors.getNextBit(x))
971 if(leq.get(abs,x) && !leq.get(approx,x))
972 {
973 approx = BitVector.UNDEFINED_INDEX;
974 break;
975 }
976
977 if(debugK0)
978 System.err.println("Initial approximation for " +
979 j + ": " +
980 indexToString(abs) + " -> " +
981 indexToString(approx));
982 j.setApprox(abs,approx);
983 }
984
985 private void computeArrows(BitMatrix leq)
986 throws LowlevelUnsatisfiable
987 {
988 computeApproxMinimals(m, leq);
989
990 for(int iid=0; iid<nInterfaces(); iid++)
991 {
992 Interface i=getInterface(iid);
993 i.setIndexSize(n);
994 BitVector abstractors=i.abstractors;
995 for (int x = abstractors.getLowestSetBit();
996 x != BitVector.UNDEFINED_INDEX;
997 x = abstractors.getNextBit(x))
998 {
999 int approx=i.getApprox(x);
1000 if(approx!=BitVector.UNDEFINED_INDEX)
1001 {
1002 // The approximation for indexes below m is fixed
1003 for(int node=m;node<n;node++)
1004 if(leq.get(node,x))
1005 {
1006 i.setApprox(node,approx);
1007 if(debugK0)
1008 System.err.println("Approximation for "+iid+": "+
1009 indexToString(node)+" -> "
1010 +indexToString(approx));
1011 }
1012 }
1013 }
1014 }
1015 }
1016
1017 /**
1018 * Saturate the constraint under the Abs axiom.
1019 */
1020 private void saturateAbs(BitMatrix leq)
1021 throws Unsatisfiable
1022 {
1023 boolean changed;
1024
1025 do
1026 {
1027 changed=false;
1028 int nInt = nInterfaces();
1029 for(int iid=0; iid<nInt; iid++)
1030 {
1031 Interface i=getInterface(iid);
1032 int n1;
1033 BitVector hasApprox = i.getHasApprox();
1034 for(int node=hasApprox.getLowestSetBit();
1035 node != BitVector.UNDEFINED_INDEX;
1036 node = hasApprox.getNextBit(node))
1037 {
1038 // node ->_i n1
1039 n1=i.getApprox(node);
1040 for(int p = i.implementors.getLowestSetBit();
1041 p != BitVector.UNDEFINED_INDEX;
1042 p = i.implementors.getNextBit(p))
1043 // is implementors OK ?
1044 // or should not we compute rigidImplementors first ?
1045 if(leq.get(node,p) && !leq.get(n1,p))
1046 if(this.isRigid(p))
1047 throw new LowlevelUnsatisfiable
1048 ("saturateAbs: there should be "+
1049 indexToString(n1)+" <: "+
1050 indexToString(p)+
1051 " (node="+indexToString(node)+")\n"+
1052 "interface "+interfaceToString(iid)+"\n"+
1053 this);
1054 else
1055 {
1056 if(debugK0)
1057 System.err.println("Abs rule applied : "+
1058 indexToString(n1)+" < "+indexToString(p)+
1059 " using "+indexToString(node)+
1060 " for interface "+interfaceToString(iid));
1061 C .set(n1,p);
1062 Ct.set(p,n1);
1063 leq.set(n1,p);
1064 changed=true;
1065 }
1066 }
1067 }
1068 if(changed)
1069 leq.closure();
1070 }
1071 while(changed);
1072 }
1073
1074 private void condense()
1075 throws Unsatisfiable
1076 {
1077 BitMatrix T=(BitMatrix)C.clone();
1078 T.closure();
1079 condense(T);
1080 }
1081
1082 /**
1083 * Condense the relation by merging equivalent indexes and collecting the
1084 * garbage nodes.
1085 * T is a closure of C
1086 **/
1087 private void condense(BitMatrix T) throws Unsatisfiable {
1088 // XXX: TODO: verify safety when indexMerged creates new nodes
1089 // XXX: actually, the specification should say that indexMerged
1090 // XXX: cannot access to K0 (neither create new nodes, nor enter new
1091 // XXX: constraints) (see Undispatched.VarK.indexMerged)
1092
1093 // computes the connected components of (C, Ct).
1094 // we computes the transitive closure of C and Ct
1095 // this looks sub-optimal but:
1096 // 1. it's efficient in practice (transitive closure is cheap)
1097 // 2. it allows early test of satisfiability (if C* violates assertions
1098 // on rigid variables
1099 // 3. it is obviously correct (Tarjan algorithm is a mess to debug...)
1100
1101 if (m > 0) {
1102 if (T.includedIn(m, R) != null) {
1103 // T is NOT included in R on [0, m[ x [0, m[
1104 throw new LowlevelUnsatisfiable();// will be refined if necessary
1105 }
1106 }
1107 BitMatrix Tt = (BitMatrix)Ct.clone();
1108 Tt.closure();
1109
1110 if(debugK0){
1111 System.err.println(toString());
1112 System.err.println(domainsToString());
1113 }
1114
1115 for (int i = 0; i < n; i++) {
1116 if (!garbage.get(i)) {
1117 int root = T.getRow(i).getLowestSetBitAnd(Tt.getRow(i));
1118 if (root != i) {
1119 // we've found that root is equivalent to i
1120 // we are going to merge them. However, remember that the domains
1121 // of soft variables are assumed to keep track of all
1122 // the direct constraints relations between soft and rigid variables
1123 // and soft and interfaces.
1124 //
1125 // if root and i are soft, we simply have to merge their domains
1126 // (take the intersection) to account for all direct constraints
1127 //
1128 // if root is rigid and i is soft, then all the soft variables that
1129 // are comparable to i should have their domain restricted
1130 //
1131 // root cannot be soft if i is rigid because root < i
1132 if (isRigid(root) && !isRigid(i)) {
1133 for (int j = m; j < n; j++) {
1134 if (i != j && isValidIndex(j)) {
1135 if (C.get(i, j)) {
1136 // exclude unit since it is not comparable to root
1137 reduceDomain(j, false, R.getRow(root));
1138 }
1139 if (Ct.get(i, j)) {
1140 // ditto
1141 reduceDomain(j, false, Rt.getRow(root));
1142 }
1143 }
1144 }
1145 }
1146 indexMerge(i, root);
1147 }
1148 }
1149 }
1150 collect();
1151 }
1152
1153 private void prepareConstraint() throws Unsatisfiable {
1154 collapseMinimal();
1155 BitMatrix leq = (BitMatrix)C.clone();
1156 leq.closure();
1157 computeArrows(leq);
1158 saturateAbs(leq);
1159 //condense(leq);
1160 }
1161
1162
1163 /***********************************************************************
1164 * Satisfiability
1165 ***********************************************************************/
1166 // enumerate the solutions on rigid variables (constructive witness)
1167 // or throw Unsatisfiable if no solution (right thing to do ???)
1168 // XXX: refine Unsatisfiable ??
1169 public void enumerate(LowlevelSolutionHandler handler)
1170 throws Unsatisfiable {
1171 S.assume(S.a&& hasBeenInitialized);
1172 prepareConstraint();
1173 domains.trimToSize();
1174 if (m == 0 || m == n) {
1175 // the constraint is satisfiable
1176 // if m == 0, all the variables are mapped to unit
1177 // if m == n, there is no variable
1178 // In both cases, there is still exactly one solution.
1179 handler.handle(domains);
1180 } else {
1181 // here goes real satisfiability
1182 int[] strategy = Satisfier.compileStrategy(C, Ct, m, n);
1183 Satisfier.enumerateSolutions(strategy, domains, C, Ct, R, Rt, m, n, handler);
1184 }
1185 }
1186
1187 // XXX: spec ??
1188 public void enumerate(BitVector observers,
1189 LowlevelSolutionHandler handler) {
1190 S.assume(S.a&& hasBeenInitialized);
1191 try {
1192 prepareConstraint();
1193 } catch (Unsatisfiable e) {
1194 // not satisfiable
1195 return;
1196 }
1197 domains.trimToSize();
1198 if (m == 0 || m == n) {
1199 handler.handle(domains);
1200 } else {
1201 int[] strategy = Satisfier.compileStrategy(C, Ct, m, n);
1202 Satisfier.enumerateSolutions(strategy, domains,
1203 C, Ct, R, Rt, m, n,
1204 observers, handler);
1205 }
1206 }
1207
1208 public void satisfy() throws Unsatisfiable {
1209 S.assume(S.a&& hasBeenInitialized);
1210
1211 if (m == 0 || m == n)
1212 return;
1213
1214 try {
1215 prepareConstraint();
1216 rawSatisfy();
1217 } catch (LowlevelUnsatisfiable e) {
1218 if (LowlevelUnsatisfiable.refinedReports) {
1219 throw refine(e);
1220 } else {
1221 throw e;
1222 }
1223 }
1224 }
1225
1226 private void rawSatisfy() throws Unsatisfiable {
1227 domains.trimToSize();
1228 if (0 < m && m < n) {
1229 int[] strategy = Satisfier.compileStrategy(C, Ct, m, n);
1230 Satisfier.satisfy(strategy, domains, C, Ct, R, Rt, m, n);
1231 }
1232 }
1233
1234 /***********************************************************************
1235 * Rigidification
1236 ***********************************************************************/
1237 /**
1238 * Saturate the subtyping between interfaces under :
1239 * I < J and J < K => I < K
1240 **/
1241 private void closeInterfaceRelation() {
1242 // Warshall algorithm
1243 for (int k = 0; k < nInterfaces(); k++) {
1244 Interface K = getInterface(k);
1245 for (int i = 0; i < nInterfaces(); i++) {
1246 Interface I = getInterface(i);
1247 if (I.subInterfaces.get(k)) {
1248 // K < I
1249 // for all J < K, add J < I
1250 I.subInterfaces.or(K.subInterfaces);
1251 }
1252 }
1253 // reflexivity
1254 K.subInterfaces.set(k);
1255 }
1256 }
1257
1258 /**
1259 * Saturate the "implements" constraint under the following axioms:
1260 * x: I and I < J => x: J
1261 * x ~ y and y: I => x: I
1262 *
1263 * Returns an array of BitVector rigidImplementors
1264 * rigidImplementors[iid] is the set of x such that x :* iid
1265 **/
1266 BitVector[] closeImplements(BitMatrix R, BitMatrix Rt) {
1267 BitVector[] rigidImplementors = new BitVector[nInterfaces()];
1268 for (int iid = 0; iid < nInterfaces(); iid++) {
1269 BitVector I_impls = getInterface(iid).implementors;
1270 rigidImplementors[iid] = (BitVector)I_impls.clone();
1271 for (int x = I_impls.getLowestSetBit();
1272 x != BitVector.UNDEFINED_INDEX;
1273 x = I_impls.getNextBit(x)) {
1274 // x: iid
1275 // for all y ~ x, add y: iid
1276 rigidImplementors[iid].orAnd(Rt.getRow(x),R.getRow(x));
1277 }
1278 }
1279 int nInt = nInterfaces();
1280 for (int iid1 = 0; iid1 < nInt; iid1++) {
1281 for (int iid2 = 0; iid2 < nInt; iid2++) {
1282 if (getInterface(iid2).subInterfaces.get(iid1)) {
1283 // I1 < I2
1284 // for all x: I1, add x: I2
1285 rigidImplementors[iid2].or(rigidImplementors[iid1]);
1286 }
1287 }
1288 }
1289 return rigidImplementors;
1290 }
1291
1292
1293 /**
1294 * Rigidify the current constraint
1295 * You must have called satisfy before
1296 **/
1297 public void rigidify() {
1298 S.assume(S.a&& hasBeenInitialized);
1299 R = (BitMatrix)C.clone();
1300 R.closure();
1301 Rt = (BitMatrix)Ct.clone();
1302 Rt.closure();
1303 m = n;
1304 BitVector[] rigidImplementors = closeImplements(R, Rt);
1305 for (int iid = 0; iid < nInterfaces(); iid++) {
1306 getInterface(iid).rigidImplementors = rigidImplementors[iid];
1307 }
1308 domains = new DomainVector(m, m);
1309 }
1310
1311 /***********************************************************************
1312 * Marking / Backtracking
1313 ***********************************************************************/
1314 // There are two modes of backtracking: BACKTRACK_UNLIMITED and
1315 // BACKTRACK_ONCE
1316 //
1317 // 1. BACKTRACK_ONCE: backtrack() may be called to undo all modifications
1318 // made to the constraint since the last call to mark() (time t1). The
1319 // constraint may then be modified and another call to backtrack still
1320 // restores the constraint to the state at time t1. Or the constraint may be
1321 // modified, then mark() called (at time t2). Any subsequent call to
1322 // backtrack restores to t2, unless mark() is called another time. This is
1323 // the default mode adapted to type inference, used by the Jazz compiler.
1324 //
1325 // 2. BACKTRACK_UNLIMITED: calls to mark and backtrack may be nested: a call
1326 // to backtrack undoes all the modification made to this constraint since
1327 // the last call to mark() in the same nested level. It is an error if there
1328 // are more calls to backtrack() than to mark(). This mode is adapted to
1329 // type checking and used by the Nice compiler.
1330 private int backtrackMode;
1331 final public static int BACKTRACK_UNLIMITED=1;
1332 final public static int BACKTRACK_ONCE=2;
1333
1334 private class Backup {
1335 // may be non-null if backtrackMode==BACKTRACK_UNLIMITED
1336 Backup previous;
1337 int savedM;
1338 int savedN;
1339 BitVector savedGarbage;
1340 DomainVector savedDomains;
1341 //BitVector[] savedImplementors;
1342
1343 private Backup() {
1344 if (K0.this.backtrackMode == K0.BACKTRACK_UNLIMITED) {
1345 this.previous = K0.this.backup;
1346 } else {
1347 this.previous = null;
1348 }
1349 this.savedM = K0.this.m;
1350 this.savedN = K0.this.n;
1351
1352 this.savedGarbage = (BitVector)K0.this.garbage.clone();
1353 this.savedDomains = (DomainVector)K0.this.domains.clone();
1354 /*
1355 this.savedImplementors = new BitVector[K0.this.nInterfaces()];
1356 for (int iid = 0; iid < savedImplementors.length; iid++) {
1357 savedImplementors[iid]
1358 = (BitVector)K0.this.getInterface(iid).implementors.clone();
1359 }
1360 */
1361 }
1362 }
1363
1364 private Backup backup = null;
1365
1366 public void mark() {
1367 S.assume(S.a&& hasBeenInitialized);
1368
1369 backup = new Backup();
1370 }
1371
1372 // backtrack to the situation the last time mark() has been called
1373 public void backtrack() {
1374 if (backup == null)
1375 // This can happen for a K0 that has been created on the fly
1376 // at a point where (several) backups existed.
1377 return;
1378
1379 S.assume(S.a&& hasBeenInitialized);
1380
1381 this.m = backup.savedM;
1382 this.R.setSize(m);
1383 this.Rt.setSize(m);
1384
1385 this.n = backup.savedN;
1386 this.C.setSize(n);
1387 this.Ct.setSize(n);
1388
1389 this.garbage = backup.savedGarbage;
1390 this.domains = backup.savedDomains;
1391 this.minimal.truncate(n);
1392
1393 for (int iid = 0; iid < nInterfaces(); iid++) {
1394 Interface I = getInterface(iid);
1395 I.setIndexSize(n);
1396 //I.implementors = backup.savedImplementors[iid];
1397 }
1398
1399 clearTags();
1400 if (backtrackMode == BACKTRACK_UNLIMITED) {
1401 backup = backup.previous;
1402 } else {
1403 backup = null;
1404 mark();
1405 }
1406 if (debugK0) {
1407 System.err.println("backtracked #" + ID);
1408 }
1409 }
1410
1411 /***********************************************************************
1412 * Iterate thru the constraint
1413 ***********************************************************************/
1414 public static final int
1415 ALL = 0,
1416 SIMPLIFIED = 1;
1417
1418 public static abstract class IneqIterator {
1419 public IneqIterator()
1420 { this.range1 = this.range2 = ALL; }
1421 public IneqIterator(int range1, int range2)
1422 { this.range1 = range1; this.range2 = range2; }
1423 int range1, range2;