0001: package mlsub.typing.lowlevel;
0002:
0003: import java.util.ArrayList;
0004:
0005: /**
0006: * A lowlevel constraint on integers.
0007: *
0008: * @version $OrigRevision: 1.22 $, $OrigDate: 1999/10/28 10:56:58 $
0009: * @author Alexandre Frey
0010: * @author Daniel Bonniot (Abstractable Interfaces, and unlimited backtrack)
0011: **/
0012: public final class K0 {
0013: public static abstract class Callbacks {
0014: /**
0015: * Called when indexes src and dest have been merged. Only dest remains
0016: * valid: src is invalidated
0017: **/
0018: abstract protected void indexMerged(int src, int dest)
0019: throws Unsatisfiable;
0020:
0021: /**
0022: * Called when index src has been moved to index dest.
0023: **/
0024: abstract protected void indexMoved(int src, int dest);
0025:
0026: /**
0027: * Called when simplification discards index
0028: **/
0029: abstract protected void indexDiscarded(int index);
0030:
0031: /*
0032: * Pretty printing
0033: */
0034: protected String getName() {
0035: return "<k0>";
0036: }
0037:
0038: protected String indexToString(int x) {
0039: return Integer.toString(x);
0040: }
0041:
0042: protected String interfaceToString(int iid) {
0043: return Integer.toString(iid);
0044: }
0045: }
0046:
0047: /***********************************************************************
0048: * Debugging
0049: ***********************************************************************/
0050: public static boolean debugK0 = bossa.util.Debug.K0;
0051: private static int IDs = 0;
0052: private int ID = IDs++;
0053:
0054: // When a K0 is created it is in a special mode where the initial rigid
0055: // context is created. In this mode, one can use methods extend, initialLeq,
0056: // minimal, newInterface, subInterface, and initialImplements. Then,
0057: // one must call method createInitialContext()
0058: //
0059: // The constraint is then in normal mode, one can no more use the
0060: // above-mentioned methods (except extend),
0061: // but must use leq, eq, indexImplements, satisfy,
0062: // enumerate, rigidify, mark, backtrack, weakMark, weakBacktrack, getSnap,
0063: // startSimplify, stopSimplify, tag, simplify, isLeq,
0064: // solveConstructorOverloading, solveInterfaceOverloading
0065: //
0066: // backtrackMode must be either BACKTRACK_ONCE or BACKTRACK_UNLIMITED
0067: // see below the doc of backtrack() and mark()
0068: public K0(int backtrackMode, Callbacks callbacks) {
0069: this .backtrackMode = backtrackMode;
0070: this .callbacks = callbacks;
0071: this .R = null;
0072: this .Rt = null;
0073: this .m = 0;
0074: this .C = new BitMatrix();
0075: this .Ct = new BitMatrix();
0076: this .n = 0;
0077: this .minimal = new BitVector();
0078: this .garbage = new BitVector();
0079: this .posTagged = new BitVector();
0080: this .negTagged = new BitVector();
0081: this .interfaces = new ArrayList();
0082: if (debugK0) {
0083: System.err.println("created K0 #" + ID);
0084: }
0085: }
0086:
0087: public K0(Callbacks callbacks) {
0088: this (BACKTRACK_ONCE, callbacks);
0089: }
0090:
0091: private Callbacks callbacks;
0092:
0093: /**
0094: * Relation on the rigid indexes
0095: **/
0096: private BitMatrix R;
0097: /**
0098: * Transpose of R
0099: **/
0100: private BitMatrix Rt;
0101: /**
0102: * Number of rigid indexes. Below m, the relation is closed.
0103: **/
0104: private int m;
0105:
0106: /**
0107: * Number of rigid indexes in the initial rigid context
0108: * (m0 <= m)
0109: **/
0110: private int m0;
0111:
0112: int initialContextSize() {
0113: return m0;
0114: }
0115:
0116: /**
0117: * Returns an index that is guaranteed to be greater than any rigid index
0118: * and less or equal to any non-rigid index.
0119: **/
0120: public int firstNonRigid() {
0121: return m;
0122: }
0123:
0124: /**
0125: * Returns true if x is the index of a rigid variable.
0126: * the index is assumed valid
0127: **/
0128: public boolean isRigid(int x) {
0129: return x < m;
0130: }
0131:
0132: public boolean hasNoSoft() {
0133: return n == m;
0134: }
0135:
0136: /**
0137: * C maintains the constraint as it is entered
0138: **/
0139: private BitMatrix C;
0140: /**
0141: * Transpose of C
0142: **/
0143: private BitMatrix Ct;
0144: /**
0145: * Total number of indexes.
0146: * Invariant: m <= n && n == C.size()
0147: **/
0148: private int n;
0149:
0150: public int size() {
0151: return n;
0152: }
0153:
0154: /**
0155: * Maintains the information "x is minimal" on [0, m0[
0156: **/
0157: private BitVector minimal;
0158:
0159: public boolean isMinimal(int x) {
0160: return minimal.get(x);
0161: }
0162:
0163: public void minimal(int x) {
0164: minimal.set(x);
0165: }
0166:
0167: // tells if an index should be collected in the next call to collect()
0168: private BitVector garbage;
0169:
0170: public boolean isValidIndex(int x) {
0171: return x >= 0 && x < n && !garbage.get(x);
0172: }
0173:
0174: void discard(int x) {
0175: garbage.set(x);
0176: }
0177:
0178: /***********************************************************************
0179: * Pretty printing
0180: ***********************************************************************/
0181: public String getName() {
0182: return callbacks.getName();
0183: }
0184:
0185: private String indexToString(int index) {
0186: return callbacks.indexToString(index);
0187: }
0188:
0189: String interfaceToString(int iid) {
0190: return callbacks.interfaceToString(iid);
0191: }
0192:
0193: public String domainsToString() {
0194: StringBuffer sb = new StringBuffer();
0195: for (int i = m; i < n; i++) {
0196: if (isValidIndex(i)) {
0197: sb.append("D(").append(indexToString(i)).append(") = ");
0198: Domain d = (hasBeenInitialized ? domains.getDomain(i)
0199: : null);
0200: sb.append(d);
0201: sb.append("; ");
0202: }
0203: }
0204: return sb.toString();
0205: }
0206:
0207: private BitVector weakComponent(int x0) {
0208: S.assume(S.a && isValidIndex(x0));
0209: BitVector component = new BitVector();
0210: BitVector toInclude = new BitVector();
0211: toInclude.set(x0);
0212: while (true) {
0213: int x = toInclude.getLowestSetBitNotIn(component);
0214: if (x == BitVector.UNDEFINED_INDEX) {
0215: break;
0216: }
0217: if (!garbage.get(x)) {
0218: component.set(x);
0219: BitVector ux = C.getRow(x);
0220: if (ux != null) {
0221: toInclude.or(ux);
0222: }
0223: BitVector lx = Ct.getRow(x);
0224: if (lx != null) {
0225: toInclude.or(lx);
0226: }
0227: }
0228: }
0229: return component;
0230: }
0231:
0232: private String ineqToString(int x, int y) {
0233: return indexToString(x) + " <: " + indexToString(y);
0234: }
0235:
0236: private String componentToString(BitVector component) {
0237: StringBuffer sb = new StringBuffer();
0238: Separator sep = new Separator(", ");
0239: int nvars = 0;
0240: for (int x = 0; x < n; x++) {
0241: if (component.get(x)) {
0242: sb.append(sep).append(indexToString(x));
0243: if (isRigid(x)) {
0244: sb.append("*");
0245: }
0246: nvars++;
0247: }
0248: }
0249: if (nvars == 0) {
0250: return "";
0251: }
0252:
0253: sb.append(" | ");
0254: sep.reset();
0255:
0256: // enumerate the (x, y) where x < y and at least one of x or y is >= m0
0257: for (int x = 0; x < n; x++) {
0258: if (component.get(x)) {
0259: for (int y = (x < m0 ? m0 : x + 1); y < n; y++) {
0260: if (component.get(y)) {
0261: if (C.get(y, x)) {
0262: sb.append(sep).append(ineqToString(y, x));
0263: }
0264: if (C.get(x, y)) {
0265: sb.append(sep).append(ineqToString(x, y));
0266: }
0267: }
0268: }
0269: }
0270: }
0271:
0272: for (int x = m0; x < n; x++) {
0273: if (component.get(x)) {
0274: for (int iid = 0; iid < nInterfaces(); iid++) {
0275: if (getInterface(iid).implementors.get(x)) {
0276: sb.append(sep).append(indexToString(x)).append(
0277: ": ").append(interfaceToString(iid));
0278: }
0279: }
0280: }
0281: }
0282: return sb.toString();
0283: }
0284:
0285: public String toString() {
0286: final StringBuffer sb = new StringBuffer();
0287: Separator nl = new Separator("\n");
0288:
0289: BitVector rest = new BitVector(n);
0290: rest.fill(n);
0291: String restComp = componentToString(rest);
0292: if (!restComp.equals("")) {
0293: sb.append(nl).append(restComp);
0294: }
0295: if (sb.length() != 0) {
0296: sb.append("\n");
0297: }
0298: return sb.toString();
0299: }
0300:
0301: public String dumpInterfaces() {
0302: final StringBuffer sb = new StringBuffer();
0303: final Separator sep = new Separator(", ");
0304: for (int iid = 0; iid < nInterfaces(); iid++) {
0305: sb.append(sep).append(interfaceToString(iid));
0306: }
0307: sb.append(" | ");
0308: sep.reset();
0309: for (int iid1 = 0; iid1 < nInterfaces(); iid1++) {
0310: for (int iid2 = 0; iid2 < nInterfaces(); iid2++) {
0311: if (getInterface(iid2).subInterfaces.get(iid1)) {
0312: sb.append(sep).append(interfaceToString(iid1))
0313: .append(" < ").append(
0314: interfaceToString(iid2));
0315: }
0316: }
0317: }
0318: sb.append("\n");
0319: sep.reset();
0320: try {
0321: implements Iter(new ImplementsIterator() {
0322: public void iter(int x, int iid) {
0323: sb.append(sep).append(indexToString(x)).append(
0324: " : ").append(interfaceToString(iid));
0325: }
0326: });
0327: } catch (Unsatisfiable e) {
0328: }
0329: try {
0330: abstractsIter(new AbstractsIterator() {
0331: public void iter(int x, int iid) {
0332: sb.append(sep).append(indexToString(x)).append(
0333: " :: ").append(interfaceToString(iid));
0334: }
0335: });
0336: } catch (Unsatisfiable e) {
0337: }
0338: return sb.toString();
0339: }
0340:
0341: public String dumpRigid() {
0342: StringBuffer sb = new StringBuffer();
0343: Separator sep = new Separator(", ");
0344: for (int x = 0; x < m; x++) {
0345: if (isValidIndex(x)) {
0346: sb.append(sep).append(indexToString(x));
0347: }
0348: }
0349: sb.append(" | ");
0350: sep.reset();
0351: for (int x = 0; x < m; x++) {
0352: for (int y = 0; y < m; y++) {
0353: if (isValidIndex(x) && isValidIndex(y) && R.get(x, y)) {
0354: sb.append(sep).append(indexToString(x)).append(
0355: " < ").append(indexToString(y));
0356: }
0357: }
0358: }
0359: for (int iid = 0; iid < nInterfaces(); iid++) {
0360: for (int x = 0; x < m; x++) {
0361: if (isValidIndex(x)
0362: && getInterface(iid).rigidImplementors.get(x)) {
0363: sb.append(sep).append(indexToString(x))
0364: .append(": ")
0365: .append(interfaceToString(iid));
0366: }
0367: }
0368: }
0369:
0370: return sb.toString();
0371: }
0372:
0373: /***********************************************************************/
0374: private void setSize(int n) {
0375: S.assume(S.a && n >= m);
0376: this .n = n;
0377: C.setSize(n);
0378: Ct.setSize(n);
0379: if (domains != null) {
0380: domains.truncate(n - m);
0381: }
0382: garbage.truncate(n);
0383: posTagged.truncate(n);
0384: negTagged.truncate(n);
0385: minimal.truncate(n);
0386: for (int iid = 0; iid < nInterfaces(); iid++) {
0387: getInterface(iid).setIndexSize(n);
0388: }
0389: }
0390:
0391: // collect and compact indexes in [i, j[
0392: // returns the last non garbage index plus one of the compacted matrix
0393: private int collect(int i, int j) {
0394: while (true) {
0395: while (true) {
0396: if (i >= j) {
0397: return i;
0398: }
0399: if (garbage.get(i)) {
0400: break;
0401: }
0402: i++;
0403: }
0404: while (true) {
0405: if (i >= j) {
0406: return i;
0407: }
0408: j--;
0409: if (!garbage.get(j)) {
0410: break;
0411: }
0412: }
0413: indexMove(j, i);
0414: i++;
0415: }
0416: }
0417:
0418: // this operation always succeeds
0419: private void collect() {
0420: setSize(collect(m, n));
0421: }
0422:
0423: // assume src > dest && !garbage.get(src) && garbage.get(dest)
0424: private void indexMove(int src, int dest) {
0425: domainMove(src, dest);
0426: posTagged.bitCopy(src, dest);
0427: negTagged.bitCopy(src, dest);
0428: for (int iid = 0; iid < nInterfaces(); iid++) {
0429: getInterface(iid).indexMove(src, dest);
0430: }
0431: garbage.set(src);
0432: garbage.clear(dest);
0433: C.indexMove(src, dest);
0434: Ct.indexMove(src, dest);
0435:
0436: // notify the user of K0
0437: callbacks.indexMoved(src, dest);
0438: }
0439:
0440: // assume src > dest && !garbage.get(src) && !garbage.get(dest)
0441: private void indexMerge(int src, int dest) throws Unsatisfiable {
0442: domainMerge(src, dest);
0443: C.indexMerge(src, dest);
0444: Ct.indexMerge(src, dest);
0445: for (int iid = 0; iid < nInterfaces(); iid++) {
0446: getInterface(iid).indexMerge(src, dest);
0447: }
0448: garbage.set(src);
0449: posTagged.bitMerge(src, dest);
0450: negTagged.bitMerge(src, dest);
0451: // notify the subclass
0452: callbacks.indexMerged(src, dest);
0453: }
0454:
0455: /**
0456: * Add a new variable to the constraint and returns its index
0457: **/
0458: public int extend() {
0459: C.extend();
0460: Ct.extend();
0461: garbage.clear(n);
0462: if (hasBeenInitialized) {
0463: domains.extend();
0464: }
0465: return n++;
0466: }
0467:
0468: // a vector of all the Interfaces in this constraint
0469: private ArrayList interfaces;
0470:
0471: /**
0472: * Returns the number of interfaces. Interfaces are garanteed to be
0473: * numbered from 0 to nInterfaces()-1
0474: **/
0475: public int nInterfaces() {
0476: return interfaces.size();
0477: }
0478:
0479: // assume 0 <= iid < nInterfaces()
0480: Interface getInterface(int iid) {
0481: return (Interface) interfaces.get(iid);
0482: }
0483:
0484: /***********************************************************************
0485: * Construction of the initial rigid context
0486: ***********************************************************************/
0487: private boolean hasBeenInitialized = false;
0488:
0489: public boolean hasBeenInitialized() {
0490: return hasBeenInitialized;
0491: }
0492:
0493: /**
0494: * Add a new interface to the constraint and returns its ID
0495: **/
0496: public int newInterface() {
0497: S.assume(S.a && !hasBeenInitialized);
0498: int iid = nInterfaces();
0499: Interface iface = new Interface(this , iid);
0500: interfaces.add(iface);
0501: if (debugK0) {
0502: System.err.println("newInterface in #" + ID + " -> " + iid);
0503: }
0504: return iid;
0505: }
0506:
0507: /**
0508: * Enter the assertion that interface iid1 is a subinterface of iid2
0509: * Assume if1 and if2 are >=0 and < nInterfaces()
0510: **/
0511: public void subInterface(int iid1, int iid2) {
0512: S.assume(S.a && !hasBeenInitialized);
0513: getInterface(iid2).subInterfaces.set(iid1);
0514: }
0515:
0516: /**
0517: * Enter the initial assertion that x : iid
0518: **/
0519: public void initialImplements(int x, int iid) {
0520: S.assume(S.a && !hasBeenInitialized);
0521: getInterface(iid).implementors.set(x);
0522: }
0523:
0524: /**
0525: * Enter the initial assertion that x :: iid
0526: * This means that no node strictly lesser than x may implement iid
0527: **/
0528: public void initialAbstracts(int x, int iid) {
0529: S.assume(S.a && !hasBeenInitialized);
0530: getInterface(iid).abstractors.set(x);
0531: }
0532:
0533: /**
0534: * Enter the initial assertion that x <= y
0535: **/
0536: public void initialLeq(int x, int y) {
0537: S.assume(S.a && !hasBeenInitialized);
0538: C.set(x, y);
0539: Ct.set(y, x);
0540: }
0541:
0542: /***********************************************************************
0543: * Initial rigidification
0544: ***********************************************************************/
0545:
0546: public void createInitialContext() throws LowlevelUnsatisfiable {
0547: S.assume(S.a && !hasBeenInitialized);
0548:
0549: // put in R and Rt, the constraint saturated under
0550: // x < y and y < z => x < z
0551: R = new BitMatrix(C);
0552: R.closure();
0553: Rt = new BitMatrix(Ct);
0554: Rt.closure();
0555: m0 = m = n;
0556:
0557: // saturate the interface subtyping under
0558: // I < J and J < K => I < K
0559: closeInterfaceRelation();
0560:
0561: BitVector[] rigidImplementors = closeImplements(R, Rt);
0562: for (int iid = 0; iid < nInterfaces(); iid++) {
0563: getInterface(iid).rigidImplementors = rigidImplementors[iid];
0564: }
0565:
0566: computeInitialArrows();
0567:
0568: if (debugK0)
0569: System.err.println("Initial Context (saturated) "
0570: + getName() + ":\n" + this + "\n"
0571: + dumpInterfaces() + "\n");
0572:
0573: domains = new DomainVector(m, m);
0574: hasBeenInitialized = true;
0575: }
0576:
0577: public void releaseInitialContext() {
0578: hasBeenInitialized = false;
0579:
0580: if (m != m0)
0581: System.err
0582: .println("releaseInitialContext should be called when in first rigid context");
0583:
0584: m0 = m = 0;
0585: }
0586:
0587: /***********************************************************************
0588: * Constraints
0589: ***********************************************************************/
0590: /**
0591: * Enter the constraint x: iid
0592: * Assume x is a valid index and iid is a valid interface id
0593: **/
0594: public void indexImplements(int x, int iid) throws Unsatisfiable {
0595: usingInterfaces = true;
0596: S.assume(S.a && hasBeenInitialized);
0597: if (LowlevelUnsatisfiable.refinedReports) {
0598: try {
0599: indexImplements0(x, iid);
0600: } catch (LowlevelUnsatisfiable e) {
0601: throw refine(e);
0602: }
0603: } else {
0604: indexImplements0(x, iid);
0605: }
0606: }
0607:
0608: // this method makes no effort to report refined unsatisfiability
0609: private void indexImplements0(int x, int iid)
0610: throws LowlevelUnsatisfiable {
0611: if (debugK0) {
0612: System.err.println("#" + ID + " -> " + indexToString(x)
0613: + ": " + interfaceToString(iid));
0614: }
0615: Interface iface = getInterface(iid);
0616: if (iface.implementors.get(x)) {
0617: // nothing to do !
0618: return;
0619: }
0620: if (isRigid(x)) {
0621: if (!iface.rigidImplementors.get(x)) {
0622: throw new LowlevelImplementsClash(x, iid);
0623: } else {
0624: return;
0625: }
0626: }
0627: iface.implementors.set(x);
0628: // include unit since unit implements all the interfaces
0629: reduceDomain(x, true, iface.rigidImplementors);
0630: }
0631:
0632: /**
0633: * Enter the constraint x1 = x2
0634: * Assume x1 and x2 are valid indexes
0635: **/
0636: public void eq(int x1, int x2) throws Unsatisfiable {
0637: leq(x1, x2);
0638: leq(x2, x1);
0639: }
0640:
0641: /**
0642: * Enter the constraint x1 <= x2.
0643: * Assume x1 and x2 are valid indexes.
0644: **/
0645: public void leq(int x1, int x2) throws Unsatisfiable {
0646: S.assume(S.a && hasBeenInitialized);
0647: if (LowlevelUnsatisfiable.refinedReports) {
0648: try {
0649: leq0(x1, x2);
0650: } catch (LowlevelUnsatisfiable e) {
0651: throw refine(e);
0652: }
0653: } else {
0654: leq0(x1, x2);
0655: }
0656: }
0657:
0658: public void enterConstraint(int x1, int v0, int x2)
0659: throws Unsatisfiable {
0660: if (v0 > 0) {
0661: leq(x1, x2);
0662: }
0663: if (v0 < 0) {
0664: leq(x2, x1);
0665: }
0666: if (v0 == 0) {
0667: eq(x1, x2);
0668: }
0669: }
0670:
0671: // versions that does not make any effort to report precise errors
0672: // in case of rigid clash
0673: private void leq0(int x1, int x2) throws LowlevelUnsatisfiable {
0674: if (debugK0) {
0675: System.err.println("#" + ID + " -> " + indexToString(x1)
0676: + " <: " + indexToString(x2));
0677: }
0678: if (x1 == x2) {
0679: return;
0680: }
0681: if (C.get(x1, x2)) {
0682: return;
0683: }
0684: // Modify C and Ct after test for rigid clash
0685: // so that the constraint if both x1 and x2 are rigid
0686: // makes it unnecessary to mark-backtrack in some cases
0687: if (isRigid(x1) && isRigid(x2)) {
0688: if (!R.get(x1, x2)) {
0689: if (debugK0)
0690: throw new LowlevelRigidClash(indexToString(x1),
0691: indexToString(x2));
0692: else
0693: throw LowlevelUnsatisfiable.instance;
0694: } else {
0695: return;
0696: }
0697: }
0698: C.set(x1, x2);
0699: Ct.set(x2, x1);
0700: if (isRigid(x1)) {
0701: // !isRigid(x2)
0702: // exclude unit since unit is not comparable to x1
0703: reduceDomain(x2, false, R.getRow(x1));
0704: }
0705: if (isRigid(x2)) {
0706: // !isRigid(x1)
0707: // exclude unit
0708: reduceDomain(x1, false, Rt.getRow(x2));
0709: if (minimal.get(x2)) {
0710: // x1 = x2;
0711: leq0(x2, x1);
0712: }
0713: }
0714: }
0715:
0716: /***********************************************************************
0717: * Better error messages
0718: ***********************************************************************/
0719: // try to refine the exception e, in case of rigid clashes the constraint is
0720: // known to be unsatisfiable at this point NB: this method is only called in
0721: // case of unsatisfiability that is to be reported to the user. The
0722: // important point is to get a message that is precise enough. There is no
0723: // need to optimize this method.
0724: private LowlevelUnsatisfiable refine(LowlevelUnsatisfiable e) {
0725: if (K0.debugK0) {
0726: System.err.println("Trying to refine " + e);
0727: System.err.println("The constraint is " + this .toString());
0728: System.err
0729: .println("The rigid constraint is " + dumpRigid());
0730: e.printStackTrace();
0731: }
0732: if (e instanceof LowlevelRigidClash
0733: || e instanceof LowlevelImplementsClash) {
0734: return e;
0735: }
0736: // close the constraint
0737: // it does no harm to modify the constraint since
0738: // it will be backtracked to display the error message
0739: C.closure();
0740: Ct.closure();
0741:
0742: BitVector[] saturatedImplementors = closeImplements(C, Ct);
0743: for (int iid = 0; iid < nInterfaces(); iid++) {
0744: getInterface(iid).implementors = saturatedImplementors[iid];
0745: }
0746:
0747: // then try to find a rigid clash, i.e., a constraint a < b where a is not
0748: // a subtype of b in the rigid context
0749: int[] rigidClash = C.includedIn(m, R);
0750: if (rigidClash != null) {
0751: return new LowlevelRigidClash(indexToString(rigidClash[0]),
0752: indexToString(rigidClash[1]));
0753: }
0754:
0755: // try to refine even better: find if the unsatisfiability
0756: // stems from attempt to put a common supertype or subtype
0757: // to incompatible rigid types
0758: LowlevelIncompatibleClash clash = null;
0759: clash = refineIncompatible(C, R,
0760: LowlevelIncompatibleClash.NO_COMMON_SUPERTYPE);
0761: if (clash != null) {
0762: return clash;
0763: }
0764: clash = refineIncompatible(Ct, Rt,
0765: LowlevelIncompatibleClash.NO_COMMON_SUBTYPE);
0766: if (clash != null) {
0767: return clash;
0768: }
0769:
0770: // finally try to find an "implements" clash
0771: for (int iid = 0; iid < nInterfaces(); iid++) {
0772: Interface iface = getInterface(iid);
0773: int x = iface.implementors
0774: .getLowestSetBitNotIn(iface.rigidImplementors);
0775: if (isValidIndex(x) && isRigid(x)) {
0776: // XXX: la condition est bonne ???
0777: // we've found an index x such that x: iid in the constraint but not
0778: // in the rigid context
0779: return new LowlevelImplementsClash(x, iid);
0780: }
0781: }
0782:
0783: // At this point, we failed to give a better error message
0784: // than the original one
0785: return e;
0786: }
0787:
0788: private LowlevelIncompatibleClash refineIncompatible(BitMatrix C,
0789: BitMatrix R, int what) {
0790: for (int a = 0; a < m; a++) {
0791: for (int b = a + 1; b < m; b++) {
0792: if (R.getRow(a).getLowestSetBitAnd(R.getRow(b)) == BitVector.UNDEFINED_INDEX) {
0793: // R(a) and R(b) do not intersect
0794: BitVector Ca = C.getRow(a);
0795: if (Ca != null) {
0796: BitVector Cb = C.getRow(b);
0797: if (Cb != null) {
0798: int z = Ca.getLowestSetBitAnd(Cb);
0799: if (z != BitVector.UNDEFINED_INDEX) {
0800: // here is the culprit !
0801: return new LowlevelIncompatibleClash(
0802: what, a, b, z);
0803: }
0804: }
0805: }
0806: }
0807: }
0808: }
0809: return null;
0810: }
0811:
0812: /***********************************************************************
0813: * Domains
0814: ***********************************************************************/
0815: // each soft variable is associated to a domain, i.e., a subset of the rigid
0816: // variables plus unit (a special rigid value that implements all the
0817: // interfaces). Subtyping constraints between a soft variable and a rigid
0818: // one, and "implements" constraints on a soft variable immediately affect
0819: // the domain of the soft variable. If a domain becomes empty, the
0820: // constraint is unsatisfiable. When method satisfy or enumerate is called,
0821: // the domains already hold an initial approximation of the solutions, which
0822: // is refined by iteration of the closure operators associated to the
0823: // subtyping constraints between soft variables. Then, instantiation and
0824: // backtracking are used to find a solution (see Satisfier)
0825: private DomainVector domains = null;
0826:
0827: private void domainMerge(int src, int dest) throws Unsatisfiable {
0828: domains.merge(src, dest);
0829: }
0830:
0831: private void domainMove(int src, int dest) {
0832: domains.move(src, dest);
0833: }
0834:
0835: public void reduceDomain(int x, boolean unit, BitVector set)
0836: throws LowlevelUnsatisfiable {
0837: S.assume(S.a && x >= -1);
0838: if (x == -1) {
0839: if (!unit) {
0840: throw LowlevelUnsatisfiable.instance;
0841: }
0842: } else if (x < m) {
0843: // the domain must contain x itself (we assume here that the relation
0844: // is condensed on the rigid variables)
0845: if (!set.get(x)) {
0846: throw LowlevelUnsatisfiable.instance;
0847: }
0848: } else {
0849: if (debugK0) {
0850: System.err.println("Reducing domain of "
0851: + indexToString(x));
0852: System.err.println("from " + domains.getDomain(x));
0853: System.err.println("with " + set);
0854: }
0855: domains.reduce(x, unit, set);
0856: }
0857: }
0858:
0859: /***********************************************************************
0860: * Constraint preparation
0861: ***********************************************************************/
0862:
0863: // The constraint is "prepared" by
0864: // 1. saturate it under Min and Abs axioms
0865: // 2. condensing equivalent nodes
0866: /**
0867: * Saturate the constraint C, Ct under the axiom:
0868: * x <* y and Min(y) => y < x (hence x ~ y)
0869: **/
0870: private void collapseMinimal() throws Unsatisfiable {
0871: for (int y = 0; y < m0; y++) {
0872: if (minimal.get(y)) {
0873: BitVector uy = R.getRow(y);
0874: // breadth-first search of the lower ideal of y
0875: _collapsed.clearAll();
0876: _toCollapse.clearAll();
0877: _toCollapse.set(y);
0878: while (true) {
0879: int x = _toCollapse
0880: .getLowestSetBitNotIn(_collapsed);
0881: if (x == BitVector.UNDEFINED_INDEX) {
0882: break;
0883: }
0884: _collapsed.set(x);
0885: BitVector lx = Ct.getRow(x);
0886: if (lx != null) {
0887: _toCollapse.or(lx);
0888: }
0889: if (x != y && !C.get(y, x)) {
0890: // If x is a rigid variable, this is a clash.
0891: if (x < m0)
0892: throw new LowlevelRigidClash(
0893: indexToString(x), indexToString(y));
0894: // set y < x
0895: C.set(y, x);
0896: Ct.set(x, y);
0897: // exclude from D(x) all elements outside uy
0898: // exclude unit as well
0899: reduceDomain(x, false, uy);
0900: }
0901: }
0902: }
0903: }
0904: }
0905:
0906: // preallocate these bit-vectors
0907: private BitVector _collapsed = new BitVector(256);
0908: private BitVector _toCollapse = new BitVector(256);
0909:
0910: /****************************************************************
0911: * Algorithms on interfaces
0912: ****************************************************************/
0913:
0914: /**
0915: * Computes the arrows a ->_i b
0916: * for a's that abstract some surinterface of i
0917: */
0918: private void computeInitialArrows() throws LowlevelUnsatisfiable {
0919: for (int iid = 0; iid < nInterfaces(); iid++) {
0920: Interface i = getInterface(iid);
0921: BitVector abstractors = i.abstractors;
0922: BitVector subInterfaces = i.subInterfaces;
0923:
0924: for (int abs = abstractors.getLowestSetBit(); abs != BitVector.UNDEFINED_INDEX; abs = abstractors
0925: .getNextBit(abs))
0926: for (int jid = subInterfaces.getLowestSetBit(); jid != BitVector.UNDEFINED_INDEX; jid = subInterfaces
0927: .getNextBit(jid))
0928: // abs is a constant that abstracts i
0929: // and j is a subInterface of i
0930: {
0931: BitVector labs = Rt.getRow(abs);
0932: for (int node = labs.getLowestSetBit(); node != BitVector.UNDEFINED_INDEX; node = labs
0933: .getNextBit(node))
0934: setApproxToMinAbove(node, getInterface(jid), R);
0935: }
0936: }
0937: computeApproxMinimals(0, R);
0938: }
0939:
0940: /**
0941: Compute arrows for nodes in [min, n[
0942: */
0943: private void computeApproxMinimals(int min, BitMatrix leq)
0944: throws LowlevelUnsatisfiable {
0945: for (int node = minimal.getLowestSetBit(min); node != BitVector.UNDEFINED_INDEX; node = minimal
0946: .getNextBit(node))
0947: for (int iid = 0; iid < nInterfaces(); iid++)
0948: setApproxToMinAbove(node, getInterface(iid), leq);
0949: }
0950:
0951: /**
0952: Finds a minimum rigid node above 'abs' that implements 'j'
0953: and set it as the approximation of 'abs' for 'j'.
0954: */
0955: private void setApproxToMinAbove(int abs, Interface j, BitMatrix leq)
0956: throws LowlevelUnsatisfiable {
0957: BitVector implementors = j.rigidImplementors;
0958:
0959: boolean toCheck = false;
0960: int approx = BitVector.UNDEFINED_INDEX;
0961:
0962: for (int x = implementors.getLowestSetBit(); x != BitVector.UNDEFINED_INDEX
0963: && x < m0; x = implementors.getNextBit(x)) {
0964: if (leq.get(abs, x))
0965: if (approx == BitVector.UNDEFINED_INDEX
0966: || leq.get(x, approx))
0967: approx = x;
0968: else
0969: // optimize ? :
0970: // make tocheck an int, -1 at start. first to check-> N, second to check->-2 if not comparable with toCheck, otherwise the smaller
0971: // if at then end toCheck == -2, full check. Otherwise just check leq.get(approx, toCheck) !
0972: toCheck = true;
0973: }
0974:
0975: // verifies it is minimal
0976: if (toCheck)
0977: for (int x = implementors.getLowestSetBit(); x != BitVector.UNDEFINED_INDEX; x = implementors
0978: .getNextBit(x))
0979: if (leq.get(abs, x) && !leq.get(approx, x)) {
0980: approx = BitVector.UNDEFINED_INDEX;
0981: break;
0982: }
0983:
0984: if (debugK0)
0985: System.err.println("Initial approximation for " + j + ": "
0986: + indexToString(abs) + " -> "
0987: + indexToString(approx));
0988: j.setApprox(abs, approx);
0989: }
0990:
0991: private void computeArrows(BitMatrix leq)
0992: throws LowlevelUnsatisfiable {
0993: computeApproxMinimals(m, leq);
0994:
0995: for (int iid = 0; iid < nInterfaces(); iid++) {
0996: Interface i = getInterface(iid);
0997: i.setIndexSize(n);
0998: BitVector abstractors = i.abstractors;
0999: for (int x = abstractors.getLowestSetBit(); x != BitVector.UNDEFINED_INDEX; x = abstractors
1000: .getNextBit(x)) {
1001: int approx = i.getApprox(x);
1002: if (approx != BitVector.UNDEFINED_INDEX) {
1003: // The approximation for indexes below m is fixed
1004: for (int node = m; node < n; node++)
1005: if (leq.get(node, x)) {
1006: i.setApprox(node, approx);
1007: if (debugK0)
1008: System.err.println("Approximation for "
1009: + iid + ": "
1010: + indexToString(node) + " -> "
1011: + indexToString(approx));
1012: }
1013: }
1014: }
1015: }
1016: }
1017:
1018: /**
1019: * Saturate the constraint under the Abs axiom.
1020: */
1021: private void saturateAbs(BitMatrix leq) throws Unsatisfiable {
1022: boolean changed;
1023:
1024: do {
1025: changed = false;
1026: int nInt = nInterfaces();
1027: for (int iid = 0; iid < nInt; iid++) {
1028: Interface i = getInterface(iid);
1029: int n1;
1030: BitVector hasApprox = i.getHasApprox();
1031: for (int node = hasApprox.getLowestSetBit(); node != BitVector.UNDEFINED_INDEX; node = hasApprox
1032: .getNextBit(node)) {
1033: // node ->_i n1
1034: n1 = i.getApprox(node);
1035: for (int p = i.implementors.getLowestSetBit(); p != BitVector.UNDEFINED_INDEX; p = i.implementors
1036: .getNextBit(p))
1037: // is implementors OK ?
1038: // or should not we compute rigidImplementors first ?
1039: if (leq.get(node, p) && !leq.get(n1, p))
1040: if (this .isRigid(p))
1041: throw new LowlevelUnsatisfiable(
1042: "saturateAbs: there should be "
1043: + indexToString(n1)
1044: + " <: "
1045: + indexToString(p)
1046: + " (node="
1047: + indexToString(node)
1048: + ")\n"
1049: + "interface "
1050: + interfaceToString(iid)
1051: + "\n" + this );
1052: else {
1053: if (debugK0)
1054: System.err
1055: .println("Abs rule applied : "
1056: + indexToString(n1)
1057: + " < "
1058: + indexToString(p)
1059: + " using "
1060: + indexToString(node)
1061: + " for interface "
1062: + interfaceToString(iid));
1063: C.set(n1, p);
1064: Ct.set(p, n1);
1065: leq.set(n1, p);
1066: changed = true;
1067: }
1068: }
1069: }
1070: if (changed)
1071: leq.closure();
1072: } while (changed);
1073: }
1074:
1075: private void condense() throws Unsatisfiable {
1076: BitMatrix T = new BitMatrix(C);
1077: T.closure();
1078: condense(T);
1079: }
1080:
1081: /**
1082: * Condense the relation by merging equivalent indexes and collecting the
1083: * garbage nodes.
1084: * T is a closure of C
1085: **/
1086: private void condense(BitMatrix T) throws Unsatisfiable {
1087: // XXX: TODO: verify safety when indexMerged creates new nodes
1088: // XXX: actually, the specification should say that indexMerged
1089: // XXX: cannot access to K0 (neither create new nodes, nor enter new
1090: // XXX: constraints) (see Undispatched.VarK.indexMerged)
1091:
1092: // computes the connected components of (C, Ct).
1093: // we computes the transitive closure of C and Ct
1094: // this looks sub-optimal but:
1095: // 1. it's efficient in practice (transitive closure is cheap)
1096: // 2. it allows early test of satisfiability (if C* violates assertions
1097: // on rigid variables
1098: // 3. it is obviously correct (Tarjan algorithm is a mess to debug...)
1099:
1100: if (m > 0) {
1101: if (T.includedIn(m, R) != null) {
1102: // T is NOT included in R on [0, m[ x [0, m[
1103: throw LowlevelUnsatisfiable.instance; // will be refined if necessary
1104: }
1105: }
1106: BitMatrix Tt = new BitMatrix(Ct);
1107: Tt.closure();
1108:
1109: if (debugK0) {
1110: System.err.println(toString());
1111: System.err.println(domainsToString());
1112: }
1113:
1114: for (int i = 0; i < n; i++) {
1115: if (!garbage.get(i)) {
1116: int root = T.getRow(i).getLowestSetBitAnd(Tt.getRow(i));
1117: if (root != i) {
1118: // we've found that root is equivalent to i
1119: // we are going to merge them. However, remember that the domains
1120: // of soft variables are assumed to keep track of all
1121: // the direct constraints relations between soft and rigid variables
1122: // and soft and interfaces.
1123: //
1124: // if root and i are soft, we simply have to merge their domains
1125: // (take the intersection) to account for all direct constraints
1126: //
1127: // if root is rigid and i is soft, then all the soft variables that
1128: // are comparable to i should have their domain restricted
1129: //
1130: // root cannot be soft if i is rigid because root < i
1131: if (isRigid(root) && !isRigid(i)) {
1132: for (int j = m; j < n; j++) {
1133: if (i != j && isValidIndex(j)) {
1134: if (C.get(i, j)) {
1135: // exclude unit since it is not comparable to root
1136: reduceDomain(j, false, R
1137: .getRow(root));
1138: }
1139: if (Ct.get(i, j)) {
1140: // ditto
1141: reduceDomain(j, false, Rt
1142: .getRow(root));
1143: }
1144: }
1145: }
1146: }
1147: indexMerge(i, root);
1148: }
1149: }
1150: }
1151: collect();
1152: }
1153:
1154: private boolean usingInterfaces = false;
1155:
1156: private void prepareConstraint() throws Unsatisfiable {
1157: collapseMinimal();
1158: if (usingInterfaces) {
1159: BitMatrix leq = new BitMatrix(C);
1160: leq.closure();
1161: computeArrows(leq);
1162: saturateAbs(leq);
1163: //condense(leq);
1164: usingInterfaces = false;
1165: }
1166: }
1167:
1168: /***********************************************************************
1169: * Satisfiability
1170: ***********************************************************************/
1171: // enumerate the solutions on rigid variables (constructive witness)
1172: // or throw Unsatisfiable if no solution (right thing to do ???)
1173: // XXX: refine Unsatisfiable ??
1174: public void enumerate(LowlevelSolutionHandler handler)
1175: throws Unsatisfiable {
1176: S.assume(S.a && hasBeenInitialized);
1177: prepareConstraint();
1178: domains.trimToSize();
1179: if (m == 0 || m == n) {
1180: // the constraint is satisfiable
1181: // if m == 0, all the variables are mapped to unit
1182: // if m == n, there is no variable
1183: // In both cases, there is still exactly one solution.
1184: handler.handle(domains);
1185: } else {
1186: // here goes real satisfiability
1187: int[] strategy = Satisfier.compileStrategy(C, Ct, m, n);
1188: Satisfier.enumerateSolutions(strategy, domains, C, Ct, R,
1189: Rt, m, n, handler);
1190: }
1191: }
1192:
1193: // XXX: spec ??
1194: public void enumerate(BitVector observers,
1195: LowlevelSolutionHandler handler) {
1196: S.assume(S.a && hasBeenInitialized);
1197: try {
1198: prepareConstraint();
1199: } catch (Unsatisfiable e) {
1200: // not satisfiable
1201: return;
1202: }
1203: domains.trimToSize();
1204: if (m == 0 || m == n) {
1205: handler.handle(domains);
1206: } else {
1207: int[] strategy = Satisfier.compileStrategy(C, Ct, m, n);
1208: Satisfier.enumerateSolutions(strategy, domains, C, Ct, R,
1209: Rt, m, n, observers, handler);
1210: }
1211: }
1212:
1213: public void satisfy() throws Unsatisfiable {
1214: S.assume(S.a && hasBeenInitialized);
1215:
1216: if (m == 0 || m == n)
1217: return;
1218:
1219: try {
1220: prepareConstraint();
1221: rawSatisfy();
1222: } catch (LowlevelUnsatisfiable e) {
1223: if (LowlevelUnsatisfiable.refinedReports) {
1224: throw refine(e);
1225: } else {
1226: throw e;
1227: }
1228: }
1229: }
1230:
1231: private void rawSatisfy() throws Unsatisfiable {
1232: domains.trimToSize();
1233: if (0 < m && m < n) {
1234: int[] strategy = Satisfier.compileStrategy(C, Ct, m, n);
1235: Satisfier.satisfy(strategy, domains, C, Ct, R, Rt, m, n);
1236: }
1237: }
1238:
1239: /***********************************************************************
1240: * Rigidification
1241: ***********************************************************************/
1242: /**
1243: * Saturate the subtyping between interfaces under :
1244: * I < J and J < K => I < K
1245: **/
1246: private void closeInterfaceRelation() {
1247: // Warshall algorithm
1248: for (int k = 0; k < nInterfaces(); k++) {
1249: Interface K = getInterface(k);
1250: for (int i = 0; i < nInterfaces(); i++) {
1251: Interface I = getInterface(i);
1252: if (I.subInterfaces.get(k)) {
1253: // K < I
1254: // for all J < K, add J < I
1255: I.subInterfaces.or(K.subInterfaces);
1256: }
1257: }
1258: // reflexivity
1259: K.subInterfaces.set(k);
1260: }
1261: }
1262:
1263: /**
1264: * Saturate the "implements" constraint under the following axioms:
1265: * x: I and I < J => x: J
1266: * x ~ y and y: I => x: I
1267: *
1268: * Returns an array of BitVector rigidImplementors
1269: * rigidImplementors[iid] is the set of x such that x :* iid
1270: **/
1271: BitVector[] closeImplements(BitMatrix R, BitMatrix Rt) {
1272: BitVector[] rigidImplementors = new BitVector[nInterfaces()];
1273: for (int iid = 0; iid < nInterfaces(); iid++) {
1274: BitVector I_impls = getInterface(iid).implementors;
1275: rigidImplementors[iid] = new BitVector(I_impls);
1276: for (int x = I_impls.getLowestSetBit(); x != BitVector.UNDEFINED_INDEX; x = I_impls
1277: .getNextBit(x)) {
1278: // x: iid
1279: // for all y ~ x, add y: iid
1280: rigidImplementors[iid].orAnd(Rt.getRow(x), R.getRow(x));
1281: }
1282: }
1283: int nInt = nInterfaces();
1284: for (int iid1 = 0; iid1 < nInt; iid1++) {
1285: for (int iid2 = 0; iid2 < nInt; iid2++) {
1286: if (getInterface(iid2).subInterfaces.get(iid1)) {
1287: // I1 < I2
1288: // for all x: I1, add x: I2
1289: rigidImplementors[iid2].or(rigidImplementors[iid1]);
1290: }
1291: }
1292: }
1293: return rigidImplementors;
1294: }
1295:
1296: /**
1297: * Rigidify the current constraint
1298: * You must have called satisfy before
1299: **/
1300: public void rigidify() {
1301: S.assume(S.a && hasBeenInitialized);
1302: R = new BitMatrix(C);
1303: R.closure();
1304: Rt = new BitMatrix(Ct);
1305: Rt.closure();
1306: m = n;
1307: BitVector[] rigidImplementors = closeImplements(R, Rt);
1308: for (int iid = 0; iid < nInterfaces(); iid++) {
1309: getInterface(iid).rigidImplementors = rigidImplementors[iid];
1310: }
1311: domains = new DomainVector(m, m);
1312: }
1313:
1314: /***********************************************************************
1315: * Marking / Backtracking
1316: ***********************************************************************/
1317: // There are two modes of backtracking: BACKTRACK_UNLIMITED and
1318: // BACKTRACK_ONCE
1319: //
1320: // 1. BACKTRACK_ONCE: backtrack() may be called to undo all modifications
1321: // made to the constraint since the last call to mark() (time t1). The
1322: // constraint may then be modified and another call to backtrack still
1323: // restores the constraint to the state at time t1. Or the constraint may be
1324: // modified, then mark() called (at time t2). Any subsequent call to
1325: // backtrack restores to t2, unless mark() is called another time. This is
1326: // the default mode adapted to type inference, used by the Jazz compiler.
1327: //
1328: // 2. BACKTRACK_UNLIMITED: calls to mark and backtrack may be nested: a call
1329: // to backtrack undoes all the modification made to this constraint since
1330: // the last call to mark() in the same nested level. It is an error if there
1331: // are more calls to backtrack() than to mark(). This mode is adapted to
1332: // type checking and used by the Nice compiler.
1333: private int backtrackMode;
1334: final public static int BACKTRACK_UNLIMITED = 1;
1335: final public static int BACKTRACK_ONCE = 2;
1336:
1337: private class Backup {
1338: // may be non-null if backtrackMode==BACKTRACK_UNLIMITED
1339: Backup previous;
1340: int savedM;
1341: BitMatrix savedC;
1342: BitVector savedGarbage;
1343: DomainVector savedDomains;
1344:
1345: //BitVector[] savedImplementors;
1346:
1347: private Backup() {
1348: if (K0.this .backtrackMode == K0.BACKTRACK_UNLIMITED) {
1349: this .previous = K0.this .backup;
1350: } else {
1351: this .previous = null;
1352: }
1353: this .savedM = K0.this .m;
1354:
1355: // We only need to save C if there are soft variables, since
1356: // others can't be modified anyway.
1357: if (K0.this .m != K0.this .n)
1358: this .savedC = new BitMatrix(K0.this .C);
1359:
1360: this .savedGarbage = new BitVector(K0.this .garbage);
1361: this .savedDomains = new DomainVector(K0.this .domains);
1362: /*
1363: this.savedImplementors = new BitVector[K0.this.nInterfaces()];
1364: for (int iid = 0; iid < savedImplementors.length; iid++) {
1365: savedImplementors[iid]
1366: = (BitVector)K0.this.getInterface(iid).implementors.clone();
1367: }
1368: */
1369: }
1370: }
1371:
1372: private Backup backup = null;
1373:
1374: public void mark() {
1375: S.assume(S.a && hasBeenInitialized);
1376:
1377: backup = new Backup();
1378: }
1379:
1380: // backtrack to the situation the last time mark() has been called
1381: public void backtrack(boolean ignore) {
1382: if (backup == null)
1383: // This can happen for a K0 that has been created on the fly
1384: // at a point where (several) backups existed.
1385: return;
1386:
1387: if (ignore) {
1388: backup = backup.previous;
1389: return;
1390: }
1391:
1392: S.assume(S.a && hasBeenInitialized);
1393:
1394: this .m = backup.savedM;
1395: this .R.setSize(m);
1396: this .Rt.setSize(m);
1397:
1398: if (backup.savedC != null) {
1399: this .C = backup.savedC;
1400: this .Ct = backup.savedC.transpose();
1401: this .n = backup.savedC.size();
1402: } else {
1403: this .n = backup.savedM;
1404: this .C.setSize(n);
1405: this .Ct.setSize(n);
1406: }
1407:
1408: this .garbage = backup.savedGarbage;
1409: this .domains = backup.savedDomains;
1410: this .minimal.truncate(n);
1411:
1412: for (int iid = 0; iid < nInterfaces(); iid++) {
1413: Interface I = getInterface(iid);
1414: I.setIndexSize(n);
1415: //I.implementors = backup.savedImplementors[iid];
1416: }
1417:
1418: clearTags();
1419: if (backtrackMode == BACKTRACK_UNLIMITED) {
1420: backup = backup.previous;
1421: } else {
1422: backup = null;
1423: mark();
1424: }
1425: if (debugK0) {
1426: System.err.println("backtracked #" + ID);
1427: }
1428: }
1429:
1430: /***********************************************************************
1431: * Iterate thru the constraint
1432: ***********************************************************************/
1433: public static final int ALL = 0, SIMPLIFIED = 1;
1434:
1435: public static abstract class IneqIterator {
1436: public IneqIterator() {
1437: this .range1 = this .range2 = ALL;
1438: }
1439:
1440: public IneqIterator(int range1, int range2) {
1441: this .range1 = range1;
1442: this .range2 = range2;
1443: }
1444:
1445: int range1, range2;
1446:
1447: abstract protected void iter(int x1, int x2)
1448: throws Unsatisfiable;
1449: }
1450:
1451: public void ineqIter(IneqIterator iterator) throws Unsatisfiable {
1452: int from1, from2, to1 = n, to2 = n;
1453: if (iterator.range1 == SIMPLIFIED)
1454: from1 = weakMarkedSize;
1455: else
1456: from1 = 0;
1457: if (iterator.range2 == SIMPLIFIED)
1458: from2 = weakMarkedSize;
1459: else
1460: from2 = 0;
1461: boolean[] notgarb = new boolean[n];
1462: for (int i = 0; i < n; i++)
1463: notgarb[i] = !garbage.get(i);
1464:
1465: for (int i = from1; i < to1; i++) {
1466: if (notgarb[i]) {
1467: for (int j = C.getNextSetInRow(i, from2 - 1); j != BitVector.UNDEFINED_INDEX; j = C
1468: .getNextSetInRow(i, j)) {
1469: if (notgarb[j]) {
1470: iterator.iter(i, j);
1471: }
1472: }
1473: }
1474: }
1475: }
1476:
1477: public static abstract class IndexIterator {
1478: abstract protected void iter(int x);
1479: }
1480:
1481: public void indexIter(IndexIterator iterator) {
1482: for (int i = 0; i < n; i++) {
1483: if (!garbage.get(i)) {
1484: iterator.iter(i);
1485: }
1486: }
1487: }
1488:
1489: public static abstract class ImplementsIterator {
1490: abstract protected void iter(int x, int iid)
1491: throws Unsatisfiable;
1492: }
1493:
1494: public void implements Iter(ImplementsIterator iterator)
1495: throws Unsatisfiable {
1496: for (int iid = 0; iid < nInterfaces(); iid++) {
1497: BitVector implementors = getInterface(iid).implementors;
1498: for (int x = implementors.getLowestSetBit(); x != BitVector.UNDEFINED_INDEX; x = implementors
1499: .getNextBit(x)) {
1500: if (!garbage.get(x)) {
1501: iterator.iter(x, iid);
1502: }
1503: }
1504: }
1505: }
1506:
1507: public static abstract class AbstractsIterator {
1508: abstract protected void iter(int x, int iid)
1509: throws Unsatisfiable;
1510: }
1511:
1512: public void abstractsIter(AbstractsIterator iterator)
1513: throws Unsatisfiable {
1514: for (int iid = 0; iid < nInterfaces(); iid++) {
1515: BitVector abstractors = getInterface(iid).abstractors;
1516: for (int x = abstractors.getLowestSetBit(); x != BitVector.UNDEFINED_INDEX; x = abstractors
1517: .getNextBit(x)) {
1518: if (!garbage.get(x)) {
1519: iterator.iter(x, iid);
1520: }
1521: }
1522: }
1523: }
1524:
1525: static abstract public class IndexSelector {
1526: abstract protected boolean select(int index);
1527: }
1528:
1529: /***********************************************************************
1530: * Weak marking / Backtracking (only keeps track of the sizes)
1531: * NB: calls to mark/backtrack and weakMark/weakBacktrack mustn't
1532: * be interleaved
1533: ***********************************************************************/
1534: // is it really useful ? we'd better do a robust optimized version of
1535: // mark/backtrack that is lazy to avoid unnecessary copies...
1536: private int weakMarkedSize = -1;
1537: private int weakMarkedM = -1;
1538:
1539: public void weakMark() {
1540: S.assume(S.a && weakMarkedSize == -1);
1541: weakMarkedSize = n;
1542: weakMarkedM = m;
1543: if (debugK0) {
1544: System.err.println("weakMark'ed");
1545: }
1546: }
1547:
1548: public void weakBacktrack() {
1549: S.assume(S.a && weakMarkedSize >= 0);
1550: R.setSize(weakMarkedM);
1551: Rt.setSize(weakMarkedM);
1552: for (int iid = 0; iid < nInterfaces(); iid++) {
1553: getInterface(iid).rigidImplementors.truncate(weakMarkedM);
1554: }
1555: int nMin = weakMarkedSize;
1556: int nMax = n;
1557: setSize(weakMarkedSize);
1558: weakMarkedSize = -1;
1559: weakMarkedM = -1;
1560: /*
1561: Alex did that, but it is not done for real backtracks.
1562: It is not convenient for simplification (and a waste of time).
1563:
1564: for (int i = nMin; i < nMax; i++) {
1565: callbacks.indexDiscarded(i);
1566: }
1567: */
1568: if (debugK0) {
1569: System.err.println("weakBacktrack'ed");
1570: }
1571: }
1572:
1573: int weakMarkedSize() {
1574: return weakMarkedSize;
1575: }
1576:
1577: /***********************************************************************
1578: * Simplification
1579: ***********************************************************************/
1580: // XXX: should be entirely worked out...
1581: // XXX: comment utiliser mark/backtrack avec recopie lazy ??
1582: // the size of the constraint when startSimplify() has been called
1583: public void startSimplify() {
1584: S.assume(S.a && hasBeenInitialized);
1585: weakMark();
1586:
1587: // necessary ?
1588: posTagged.fill(n);
1589: negTagged.fill(n);
1590: }
1591:
1592: public void stopSimplify() {
1593: S.assume(S.a && hasBeenInitialized);
1594: weakBacktrack();
1595: }
1596:
1597: BitVector negTagged;
1598: BitVector posTagged;
1599:
1600: public boolean posTagged(int i) {
1601: return posTagged.get(i);
1602: }
1603:
1604: public boolean negTagged(int i) {
1605: return negTagged.get(i);
1606: }
1607:
1608: public void clearTags() {
1609: posTagged.clearAll();
1610: negTagged.clearAll();
1611: }
1612:
1613: public void tag(int i, int variance) {
1614: if (variance >= 0) {
1615: posTagged.set(i);
1616: }
1617: if (variance <= 0) {
1618: negTagged.set(i);
1619: }
1620: }
1621:
1622: // simplify all the variables introduced since last weakMark()
1623: public void simplify() {
1624: S.assume(S.a && hasBeenInitialized);
1625:
1626: if (weakMarkedSize >= 0) {
1627: if (weakMarkedSize == n) {
1628: return;
1629: }
1630: if (S.debugSimpl) {
1631: System.err.println("SIMPL: start simplification");
1632: }
1633: BitVector simplified = new BitVector(n);
1634: simplified.fill(n);
1635: simplified.fillNot(weakMarkedSize);
1636: (new Simplifier(simplified)).simplify();
1637: } else {
1638: throw S.panic();
1639: }
1640: }
1641:
1642: public void simplify(IndexSelector selector) {
1643: S.assume(S.a && hasBeenInitialized);
1644: BitVector simplified = new BitVector(n);
1645: boolean empty = true;
1646: for (int i = 0; i < n; i++) {
1647: if (selector.select(i)) {
1648: simplified.set(i);
1649: empty = false;
1650: }
1651: }
1652: if (!empty) {
1653: (new Simplifier(simplified)).simplify();
1654: }
1655: }
1656:
1657: public boolean isBeingSimplified(int i) {
1658: return i >= weakMarkedSize;
1659: }
1660:
1661: private final class Simplifier {
1662: Simplifier(BitVector simplified) {
1663: this .simplified = simplified;
1664: this .initN = simplified.getLowestSetBit();
1665: R = new BitMatrix(C);
1666: R.closure();
1667: Rt = new BitMatrix(Ct);
1668: Rt.closure();
1669:
1670: implementors = closeImplements(R, Rt);
1671:
1672: Sdomains = new DomainVector(initN, n, n - initN);
1673: for (int i = initN; i < n; i++) {
1674: if (!simplified.get(i)) {
1675: Sdomains.clear(i);
1676: }
1677: }
1678: }
1679:
1680: int initN; // don't simplify below this index
1681: BitVector simplified; // the vector of indexes being simplified
1682:
1683: // closed constraint
1684: BitMatrix R;
1685: BitMatrix Rt;
1686: BitVector[] implementors;
1687:
1688: DomainVector Sdomains;
1689:
1690: private void computeInitialDomains() {
1691: if (S.debugSimpl) {
1692: System.err.println("SIMPL: computing initial domains");
1693: }
1694: //
1695: // Compute the initial value of D(x) for all simplified variable x
1696: //
1697: for (int x = initN; x < n; x++) {
1698: Domain dx = Sdomains.getDomain(x);
1699: if (dx != null) {
1700: // now, we know that simplified.get(x) is true
1701:
1702: // can't simplify rigid variable of the initial context
1703: S.assume(S.a && x >= m0);
1704: BitVector ux = R.getRow(x);
1705: if (ux != null) {
1706: for (int x0 = ux.getLowestSetBit(); x0 != BitVector.UNDEFINED_INDEX; x0 = ux
1707: .getNextBit(x0)) {
1708: if (!simplified.get(x0)) {
1709: // we have x <C x0
1710: // sigma(x0) = x0 for all auto-solution
1711: // do D(x) = D(x) \inter \Lower{x0}
1712: dx.and(Rt.getRow(x0));
1713: // and exclude unit since unit is not comparable to x0
1714: dx.rawExcludeUnit();
1715: }
1716: }
1717: }
1718: BitVector lx = Rt.getRow(x);
1719: if (lx != null) {
1720: for (int x0 = lx.getLowestSetBit(); x0 != BitVector.UNDEFINED_INDEX; x0 = lx
1721: .getNextBit(x0)) {
1722: if (!simplified.get(x0)) {
1723: // x0 <C x
1724: // do D(x) = D(x) \inter \Upper{x0}
1725: dx.and(R.getRow(x0));
1726: dx.rawExcludeUnit();
1727: }
1728: }
1729: }
1730: for (int iid = 0; iid < nInterfaces(); iid++) {
1731: if (implementors[iid].get(x)) {
1732: // we have x: I
1733: // ("implements" relation has been saturated)
1734: dx.and(implementors[iid]);
1735: // don't exclude unit !!
1736: }
1737: }
1738:
1739: if (posTagged(x)) {
1740: // We must have sigma(x) <= x
1741: // Do D(x) = D(x) \inter \Lower{x}
1742: dx.and(Rt.getRow(x));
1743: dx.rawExcludeUnit();
1744: }
1745: if (negTagged(x)) {
1746: // We must have sigma(x) >= x
1747: dx.and(R.getRow(x));
1748: dx.rawExcludeUnit();
1749: }
1750: }
1751: }
1752: if (S.debugSimpl) {
1753: System.err.println("SIMPL: initial domains are : "
1754: + domainsToString());
1755: }
1756: }
1757:
1758: /**
1759: * Fills (solution, nker) with a solution of C w.r.t R.
1760: * After the call, for initN <= x < n, solution[x - initN] = sigma(x)
1761: * and sigma(x) \in domains(x).
1762: **/
1763: private void findSolution(int[] strategy, final int[] solution)
1764: throws LowlevelUnsatisfiable {
1765: final RuntimeException abort = new RuntimeException();
1766: try {
1767: Satisfier.enumerateSolutions(strategy, Sdomains, C, Ct,
1768: R, Rt, initN, n, new LowlevelSolutionHandler() {
1769: protected void handle() {
1770: for (int x = initN; x < n; x++) {
1771: if (Sdomains.getDomain(x) != null) {
1772: solution[x - initN] = getSolutionOf(x);
1773: } else {
1774: solution[x - initN] = x;
1775: }
1776: }
1777: throw abort;
1778: }
1779: });
1780: } catch (RuntimeException e) {
1781: if (e != abort) {
1782: throw e;
1783: }
1784: }
1785: }
1786:
1787: private class Normal extends Exception {
1788: }
1789:
1790: /**
1791: * Fills solution with a non-surjective solution or throws Normal.
1792: * Starts to exclude elements downwards from excludedA.
1793: *
1794: * @exception Normal if the constraint is in normal form
1795: **/
1796: private int findNonSurjective(int excludedA, int[] strategy,
1797: int[] solution) throws Normal {
1798: while (excludedA >= initN) {
1799: if (!garbage.get(excludedA)
1800: && simplified.get(excludedA)) {
1801: int x;
1802: DomainVector savedDomains = new DomainVector(
1803: Sdomains);
1804: try {
1805: if (S.debugSimpl) {
1806: System.err.println("Try excluding "
1807: + excludedA);
1808: }
1809: Sdomains.exclude(excludedA);
1810: if (S.debugSimpl) {
1811: System.err.println("Satisfying with "
1812: + Sdomains.dump());
1813: }
1814: findSolution(strategy, solution);
1815: return excludedA;
1816: } catch (LowlevelUnsatisfiable e) {
1817: if (S.debugSimpl) {
1818: System.err.println("Failed");
1819: }
1820: // try another value
1821: } finally {
1822: Sdomains = savedDomains;
1823: }
1824: }
1825: excludedA--;
1826: }
1827: throw new Normal();
1828: }
1829:
1830: /**
1831: * assume solution contains a solution of C |= C.
1832: * Do one stroke of simplification on x.
1833: **/
1834: private void simplifyIndex(int x, int[] solution, int[] nker) {
1835: if (S.debugSimpl) {
1836: System.err.println("x = " + x + " nker[x - initN] = "
1837: + nker[x - initN] + " garbage.get(x) = "
1838: + garbage.get(x));
1839: }
1840: while (x >= initN && simplified.get(x)
1841: && nker[x - initN] == 0) {
1842: // OK, x is not in the codomain of sigma, we can eliminate it
1843:
1844: if (S.debugSimpl) {
1845: System.err.println("Eliminate " + x);
1846: }
1847: try {
1848: //
1849: // Propagate the constraints in (C, Ct) that go through x
1850: //
1851: // XXX: is it inconvenient that it can modify the context ?
1852: // XXX: normally not: it only adds consequences of the context...
1853: for (int y = 0; y < n; y++) {
1854: if (!garbage.get(y)) {
1855: if (x != y && C.get(y, x)) {
1856: // y < x
1857: // for each x < z, add y < z
1858: BitVector ux = C.getRow(x);
1859: if (ux != null) {
1860: // C.getRow(y) is necessarily non-null since C.get(y, x) is
1861: // true
1862: C.getRow(y).or(ux);
1863: }
1864: }
1865: if (x != y && Ct.get(y, x)) {
1866: // x < y
1867: // add z < y for each z < x
1868: BitVector lx = Ct.getRow(x);
1869: if (lx != null) {
1870: // Ct.getRow(y) is necessarily non-null because Ct.get(y, x)
1871: // is true
1872: Ct.getRow(y).or(lx);
1873: }
1874: }
1875: }
1876: }
1877:
1878: // should clear C Ct ?
1879: Sdomains.clear(x);
1880: Sdomains.exclude(x);
1881: domains.clear(x); // Added by Daniel
1882: simplified.clear(x);
1883: garbage.set(x);
1884: int sx = solution[x - initN];
1885: if (sx >= initN) {
1886: nker[sx - initN]--;
1887: }
1888: if (posTagged(x) || negTagged(x)) {
1889: // sx can't be -1 because unit is not comparable with x
1890: S.assume(S.a && sx >= 0);
1891: // discard x by merging with sx
1892: if (S.debugSimpl) {
1893: System.err.println("Merge " + x + " and "
1894: + sx);
1895: }
1896: if (simplified.get(sx)) {
1897: if (posTagged(x) && !posTagged(sx)) {
1898: // we now have found that sx is tagged +
1899: // exclude unit, not comparable to sx
1900: Sdomains.reduce(sx, false, Rt
1901: .getRow(sx));
1902: posTagged.set(sx);
1903: }
1904: if (negTagged(x) && !negTagged(sx)) {
1905: Sdomains
1906: .reduce(sx, false, R.getRow(sx));
1907: negTagged.set(sx);
1908: }
1909: }
1910: callbacks.indexMerged(x, sx);
1911: } else {
1912: // just discard x
1913: callbacks.indexDiscarded(x);
1914: }
1915: // iterate sigma until its codomain is stable
1916: x = sx;
1917: } catch (Unsatisfiable e) {
1918: throw S.panic();
1919: }
1920: }
1921: }
1922:
1923: private void simplifyOnce(int[] solution) {
1924: int[] nker = new int[n - initN];
1925: for (int x = initN; x < n; x++) {
1926: if (!garbage.get(x)) {
1927: int sx = solution[x - initN];
1928: if (sx >= initN) {
1929: nker[sx - initN]++;
1930: }
1931: }
1932: }
1933: for (int x = initN; x < n; x++) {
1934: simplifyIndex(x, solution, nker);
1935: }
1936: }
1937:
1938: String indexToString(int index) {
1939: return K0.this .indexToString(index)
1940: + (posTagged(index) ? "+" : "")
1941: + (negTagged(index) ? "-" : "");
1942: }
1943:
1944: private void reduce(BitMatrix C, BitMatrix R, BitMatrix Rt) {
1945: BitVector garbage = K0.this .garbage;
1946: if (S.debugSimpl) {
1947: System.err.println("reduce C = " + C + ", R = " + R
1948: + ", garbage = " + garbage);
1949: }
1950: for (int k = 0; k < n; k++) {
1951: if (!garbage.get(k)) {
1952: C.clear(k, k);
1953: // uk is necessarily non-null (at least k <* k)
1954: BitVector uk = R.getRow(k);
1955: BitVector lk = Rt.getRow(k);
1956: for (int j = lk.getLowestSetBit(); j != BitVector.UNDEFINED_INDEX; j = lk
1957: .getNextBit(j)) {
1958: if (!garbage.get(j) && !uk.get(j)) {
1959: // j <* k and not k <* j
1960: BitVector uj = C.getRow(j);
1961: if (uj != null) {
1962: if (simplified.get(j)) {
1963: // delete all j < l when k <* l but not l <* k
1964: uj.andNotOr(uk, lk);
1965: } else {
1966: // same but only if l is simplified
1967: uj.andNotAndOr(simplified, uk, lk);
1968: }
1969: }
1970: }
1971: }
1972: }
1973: }
1974: if (S.debugSimpl) {
1975: System.err.println("reduced C = " + C + ", R = " + R
1976: + ", garbage = " + garbage);
1977: }
1978: }
1979:
1980: // transitive reduction of the relation x: I
1981: private void reduceImplements() {
1982: for (int iid = 0; iid < nInterfaces(); iid++) {
1983: Interface I = getInterface(iid);
1984: BitVector lI = implementors[iid];
1985: BitVector Iimplementors = I.implementors;
1986: for (int k = lI.getLowestSetBit(); k != BitVector.UNDEFINED_INDEX; k = lI
1987: .getNextBit(k)) {
1988: if (!garbage.get(k)) {
1989: // k:* I
1990: // for all j in simplified, delete j: I if j <* k strictly
1991: Iimplementors.andNotAndOr(simplified, // leave the bits outside simplified unchanged
1992: Rt.getRow(k), // if j <* k
1993: R.getRow(k)); // and !(k <* j), then delete j: I
1994: }
1995: }
1996: }
1997: for (int iid2 = 0; iid2 < nInterfaces(); iid2++) {
1998: Interface I2 = getInterface(iid2);
1999: BitVector I2sub = I2.subInterfaces;
2000: BitVector I2implementors = I2.implementors;
2001: for (int iid1 = I2sub.getLowestSetBit(); iid1 != BitVector.UNDEFINED_INDEX; iid1 = I2sub
2002: .getNextBit(iid1)) {
2003: Interface I1 = getInterface(iid1);
2004: if (!I1.subInterfaces.get(iid2)) {
2005: // I1 <* I2 strictly
2006: // delete all j: I2 when j:* I1 and j is simplified
2007: I2implementors.andNotAnd(implementors[iid1],
2008: simplified);
2009: }
2010: }
2011: }
2012: }
2013:
2014: /**
2015: * Transitive reduction.
2016: **/
2017: void reduce() {
2018: if (S.debugSimpl) {
2019: System.err
2020: .println("starting reduction: K = " + K0.this );
2021: }
2022: reduce(C, R, Rt);
2023: reduce(Ct, Rt, R);
2024: reduceImplements();
2025: if (S.debugSimpl) {
2026: System.err
2027: .println("finished reduction: K = " + K0.this );
2028: }
2029: }
2030:
2031: void simplify() {
2032: if (initN < 0) {
2033: // no index to simplify
2034: return;
2035: }
2036: computeInitialDomains();
2037: try {
2038: int[] solution = new int[n - initN];
2039: int[] strategy = Satisfier.compileStrategy(C, Ct,
2040: initN, n);
2041: int excludedA = n - 1;
2042: while (true) {
2043: if (n - garbage.bitCount() == 1) {
2044: // only one variable (including rigid ones)
2045: int x = garbage.getLowestClearedBit();
2046: if (simplified.get(x) && !posTagged(x)
2047: && !negTagged(x)) {
2048: // It is not even tagged
2049: // eliminate it and make the constraint empty
2050: setSize(0);
2051: callbacks.indexDiscarded(x);
2052: return;
2053: } else {
2054: // keep it, but the constraint is now in normal form...
2055: if (x != 0) {
2056: indexMove(x, 0);
2057: }
2058: setSize(1);
2059: C.clear(0, 0);
2060: Ct.clear(0, 0);
2061: return;
2062: }
2063: }
2064: if (S.debugSimpl) {
2065: System.err.println("Try to simplify "
2066: + K0.this .toString());
2067: System.err.println("with domains "
2068: + Sdomains.dump());
2069: }
2070: excludedA = findNonSurjective(excludedA, strategy,
2071: solution);
2072: if (S.debugSimpl) {
2073: System.err.print(" sigma = {");
2074: Separator sep = new Separator(", ");
2075: for (int x = initN; x < n; x++) {
2076: if (Sdomains.getDomain(x) != null) {
2077: System.err.print(sep);
2078: System.err.print(indexToString(x));
2079: System.err.print(" -> ");
2080: int sx = solution[x - initN];
2081: if (sx == -1) {
2082: System.err.print("unit");
2083: } else {
2084: System.err.print(indexToString(sx));
2085: }
2086: }
2087: }
2088: System.err.println("}");
2089: }
2090: simplifyOnce(solution);
2091: }
2092: } catch (Normal e) {
2093: reduce();
2094: collect();
2095: }
2096: }
2097: } // end of inner class Simplify
2098:
2099: public void deleteAllSoft() {
2100: S.assume(S.a && hasBeenInitialized);
2101: setSize(m);
2102: n = m;
2103: }
2104:
2105: /**
2106: * Assume i1 and i2 are rigid
2107: **/
2108: public boolean isLeq(int i1, int i2) {
2109: return R.get(i1, i2);
2110: }
2111:
2112: /**
2113: * Test if a constraint i1 <: i2 was explicitely entered.
2114: **/
2115: public boolean wasEntered(int i1, int i2) {
2116: return C.get(i1, i2);
2117: }
2118:
2119: /***********************************************************************
2120: * Overloading resolution
2121: ***********************************************************************/
2122: private final static int OVERLOADING_CONSTRUCTOR = 0;
2123: private final static int OVERLOADING_INTERFACE = 1;
2124:
2125: /**
2126: * Assume this constraint has just been satisfied possibilities contains
2127: * indexes of rigid variables (if what == OVERLOADING_CONSTRUCTOR) or
2128: * interfaces (if what == OVERLOADING_INTERFACE). For each index k in
2129: * possibilities, try to enter constraint x <= k or x: k and delete k from
2130: * possibilities if this makes the constraint unsatisfiable
2131: **/
2132: private void solveOverloading(int what, int x,
2133: BitVector possibilities) {
2134: S.assume(S.a && hasBeenInitialized);
2135: S.assume(S.a && isValidIndex(x));
2136: if (isRigid(x)) {
2137: if (what == OVERLOADING_CONSTRUCTOR) {
2138: // R.getRow(x) is Up(x)
2139: possibilities.and(R.getRow(x));
2140: } else {
2141: for (int iid = possibilities.getLowestSetBit(); iid != BitVector.UNDEFINED_INDEX; iid = possibilities
2142: .getNextBit(iid)) {
2143: if (!getInterface(iid).rigidImplementors.get(x)) {
2144: possibilities.clear(iid);
2145: }
2146: }
2147: }
2148: } else {
2149: // x is soft
2150: for (int x0 = possibilities.getLowestSetBit(); x0 != BitVector.UNDEFINED_INDEX; x0 = possibilities
2151: .getNextBit(x0)) {
2152: // try simple things first
2153: if (what == OVERLOADING_CONSTRUCTOR
2154: && !domains.getDomain(x).intersect(
2155: Rt.getRow(x0))) {
2156: possibilities.clear(x0);
2157: } else if (what == OVERLOADING_INTERFACE
2158: && !domains.getDomain(x).containsUnit()
2159: && !domains.getDomain(x).intersect(
2160: getInterface(x0).rigidImplementors)) {
2161: possibilities.clear(x0);
2162: } else {
2163: // try to really satisfy
2164: Backup savedBackup = backup;
2165: mark();
2166: try {
2167: if (what == OVERLOADING_CONSTRUCTOR) {
2168: leq0(x, x0);
2169: } else {
2170: indexImplements0(x, x0);
2171: }
2172: rawSatisfy();
2173: } catch (Unsatisfiable e) {
2174: possibilities.clear(x0);
2175: } finally {
2176: backtrack(false);
2177: backup = savedBackup;
2178: }
2179: }
2180: }
2181: }
2182: }
2183:
2184: public void solveConstructorOverloading(int x,
2185: BitVector possibilities) {
2186: solveOverloading(OVERLOADING_CONSTRUCTOR, x, possibilities);
2187: }
2188:
2189: public void solveInterfaceOverloading(int x, BitVector possibilities) {
2190: solveOverloading(OVERLOADING_INTERFACE, x, possibilities);
2191: }
2192: }
|