001: package mlsub.typing.lowlevel;
002:
003: /**
004: * A repository for static methods used during satisfiability test
005: *
006: * @author Alexandre Frey
007: * @version $Revision: 1.5 $, $Date: 2005/04/01 12:12:05 $
008: **/
009: final class Satisfier {
010: // not instantiable
011: private Satisfier() {
012: }
013:
014: static int[] compileStrategy(BitMatrix C, BitMatrix Ct, int m, int n) {
015: int[] strategy = new int[n - m];
016: C.topologicalSort(m, strategy);
017: return strategy;
018: }
019:
020: private static boolean satisfiable = false;
021:
022: private static class Satisfiable extends Exception {
023: }
024:
025: private static Satisfiable sat = new Satisfiable();
026:
027: private static void enumerate(int[] strategy, DomainVector domains,
028: BitMatrix C, BitMatrix Ct, BitMatrix R, BitMatrix Rt,
029: int m, int n, BitVector observers,
030: LowlevelSolutionHandler handler)
031: throws LowlevelUnsatisfiable, Satisfiable {
032: domains.gfp(R, Rt, C, Ct, strategy);
033: boolean isObserver = true;
034: // try first the observers
035: int x = domains.chooseDomain(observers);
036: if (x < 0) {
037: isObserver = false;
038: // no more uninstantiated observers
039: x = domains.chooseDomain();
040: if (x < 0) {
041: // no more domains at all, the constraint has been satisfied
042: handler.handle(domains);
043:
044: // backtrack
045: throw sat;
046: }
047: }
048: Domain dx = new Domain(domains.getDomain(x));
049: for (int a = dx.getLowestSetBit(); a >= 0; a = dx.getNextBit(a)) {
050: DomainVector domainsCopy = new DomainVector(domains);
051: try {
052: domainsCopy.getDomain(x).instantiate(a);
053: enumerate(strategy, domainsCopy, C, Ct, R, Rt, m, n,
054: observers, handler);
055: } catch (LowlevelUnsatisfiable e) {
056: // try another value
057: } catch (Satisfiable e) {
058: if (!isObserver) {
059: // ok, we found a solution and reported it
060: // no need to try another value for the non-observer x
061: throw e;
062: } else {
063: // try another value for the observer
064: }
065: }
066: }
067: throw LowlevelUnsatisfiable.instance;
068: }
069:
070: private static void enumerate(int[] strategy, DomainVector domains,
071: BitMatrix C, BitMatrix Ct, BitMatrix R, BitMatrix Rt,
072: int m, int n, LowlevelSolutionHandler handler)
073: throws LowlevelUnsatisfiable, Satisfiable {
074: domains.gfp(R, Rt, C, Ct, strategy);
075:
076: int x = domains.chooseDomain();
077: if (x < 0) {
078: // no more domains to be instantiated: a solution has been found
079: satisfiable = true;
080: if (handler == null) {
081: throw sat;
082: }
083: handler.handle(domains);
084: throw LowlevelUnsatisfiable.instance;
085: }
086: Domain dx = new Domain(domains.getDomain(x));
087: // iterate through the elements of dx
088: for (int a = dx.getLowestSetBit(); a >= 0; a = dx.getNextBit(a)) {
089: DomainVector domainsCopy = new DomainVector(domains);
090: try {
091: domainsCopy.getDomain(x).instantiate(a);
092: enumerate(strategy, domainsCopy, C, Ct, R, Rt, m, n,
093: handler);
094:
095: // XXX: reachable ?
096: throw sat;
097: } catch (LowlevelUnsatisfiable _) {
098: // try another value
099: }
100: }
101: throw LowlevelUnsatisfiable.instance;
102: }
103:
104: static void enumerateSolutions(int[] strategy,
105: DomainVector domains, BitMatrix C, BitMatrix Ct,
106: BitMatrix R, BitMatrix Rt, int m, int n,
107: LowlevelSolutionHandler handler)
108: throws LowlevelUnsatisfiable {
109: try {
110: satisfiable = false;
111: domains.initGfpCardinals();
112: enumerate(strategy, domains, C, Ct, R, Rt, m, n, handler);
113: } catch (Satisfiable e) {
114: } catch (LowlevelUnsatisfiable e) {
115: if (!satisfiable) {
116: throw e;
117: } else {
118: /* the exception was thrown to request for more solutions
119: * but there aren't any more
120: */
121: }
122: }
123: }
124:
125: static void enumerateSolutions(int[] strategy,
126: DomainVector domains, BitMatrix C, BitMatrix Ct,
127: BitMatrix R, BitMatrix Rt, int m, int n,
128: BitVector observers, LowlevelSolutionHandler handler) {
129: try {
130: domains.initGfpCardinals();
131: enumerate(strategy, domains, C, Ct, R, Rt, m, n, observers,
132: handler);
133: } catch (Satisfiable e) {
134: } catch (LowlevelUnsatisfiable e) {
135: }
136: }
137:
138: static void satisfy(int[] strategy, DomainVector domains,
139: BitMatrix C, BitMatrix Ct, BitMatrix R, BitMatrix Rt,
140: int m, int n) throws LowlevelUnsatisfiable {
141: try {
142: domains.initGfpCardinals();
143: enumerate(strategy, domains, C, Ct, R, Rt, m, n, null);
144: } catch (Satisfiable e) {
145: }
146: }
147: }
|