Source code: mlsub/typing/lowlevel/Satisfier.java
1 package mlsub.typing.lowlevel;
2
3 /**
4 * A repository for static methods used during satisfiability test
5 *
6 * @author Alexandre Frey
7 * @version $Revision: 1.1 $, $Date: 2000/06/14 13:32:55 $
8 **/
9 final class Satisfier {
10 // not instantiable
11 private Satisfier() {}
12
13 static int[] compileStrategy(BitMatrix C, BitMatrix Ct, int m, int n) {
14 int[] strategy = new int[n - m];
15 C.topologicalSort(m, strategy);
16 return strategy;
17 }
18
19 private static boolean satisfiable = false;
20 private static class Satisfiable extends Exception {}
21
22 private static void enumerate(int[] strategy, DomainVector domains,
23 BitMatrix C, BitMatrix Ct,
24 BitMatrix R, BitMatrix Rt,
25 int m, int n,
26 BitVector observers,
27 LowlevelSolutionHandler handler)
28 throws LowlevelUnsatisfiable, Satisfiable {
29 domains.gfp(R, Rt, C, Ct, strategy);
30 boolean isObserver = true;
31 // try first the observers
32 int x = domains.chooseDomain(observers);
33 if (x < 0) {
34 isObserver = false;
35 // no more uninstantiated observers
36 x = domains.chooseDomain();
37 if (x < 0) {
38 // no more domains at all, the constraint has been satisfied
39 handler.handle(domains);
40
41 // backtrack
42 throw new Satisfiable();
43 }
44 }
45 Domain dx = (Domain)domains.getDomain(x).clone();
46 for (int a = dx.getLowestSetBit();
47 a >= 0;
48 a = dx.getNextBit(a)) {
49 DomainVector domainsCopy = (DomainVector)domains.clone();
50 try {
51 domainsCopy.getDomain(x).instantiate(a);
52 enumerate(strategy, domainsCopy, C, Ct, R, Rt, m, n,
53 observers, handler);
54 }
55 catch (LowlevelUnsatisfiable e) {
56 // try another value
57 }
58 catch (Satisfiable e) {
59 if (!isObserver) {
60 // ok, we found a solution and reported it
61 // no need to try another value for the non-observer x
62 throw e;
63 } else {
64 // try another value for the observer
65 }
66 }
67 }
68 throw new LowlevelUnsatisfiable();
69 }
70
71 private static void enumerate(int[] strategy, DomainVector domains,
72 BitMatrix C, BitMatrix Ct,
73 BitMatrix R, BitMatrix Rt,
74 int m, int n,
75 LowlevelSolutionHandler handler)
76 throws LowlevelUnsatisfiable, Satisfiable {
77 domains.gfp(R, Rt, C, Ct, strategy);
78
79 int x = domains.chooseDomain();
80 if (x < 0) {
81 // no more domains to be instantiated: a solution has been found
82 satisfiable = true;
83 if (handler == null) {
84 throw new Satisfiable();
85 }
86 handler.handle(domains);
87 throw new LowlevelUnsatisfiable();
88 }
89 Domain dx = (Domain)domains.getDomain(x).clone();
90 // iterate through the elements of dx
91 for (int a = dx.getLowestSetBit();
92 a >= 0;
93 a = dx.getNextBit(a)) {
94 DomainVector domainsCopy = (DomainVector)domains.clone();
95 try {
96 domainsCopy.getDomain(x).instantiate(a);
97 enumerate(strategy, domainsCopy, C, Ct, R, Rt, m, n, handler);
98
99 // XXX: reachable ?
100 throw new Satisfiable();
101 }
102 catch (LowlevelUnsatisfiable _) {
103 // try another value
104 }
105 }
106 throw new LowlevelUnsatisfiable();
107 }
108
109 static void enumerateSolutions(int[] strategy, DomainVector domains,
110 BitMatrix C, BitMatrix Ct,
111 BitMatrix R, BitMatrix Rt,
112 int m, int n,
113 LowlevelSolutionHandler handler)
114 throws LowlevelUnsatisfiable {
115 try {
116 satisfiable = false;
117 domains.initGfpCardinals();
118 enumerate(strategy, domains, C, Ct, R, Rt, m, n, handler);
119 }
120 catch (Satisfiable e) {}
121 catch (LowlevelUnsatisfiable e) {
122 if (!satisfiable) {
123 throw e;
124 } else {
125 /* the exception was thrown to request for more solutions
126 * but there aren't any more
127 */
128 }
129 }
130 }
131
132 static void enumerateSolutions(int[] strategy, DomainVector domains,
133 BitMatrix C, BitMatrix Ct,
134 BitMatrix R, BitMatrix Rt,
135 int m, int n,
136 BitVector observers,
137 LowlevelSolutionHandler handler) {
138 try {
139 domains.initGfpCardinals();
140 enumerate(strategy, domains, C, Ct, R, Rt, m, n, observers, handler);
141 }
142 catch (Satisfiable e) {}
143 catch (LowlevelUnsatisfiable e) {}
144 }
145
146 static void satisfy(int[] strategy, DomainVector domains,
147 BitMatrix C, BitMatrix Ct,
148 BitMatrix R, BitMatrix Rt,
149 int m, int n)
150 throws LowlevelUnsatisfiable {
151 try {
152 domains.initGfpCardinals();
153 enumerate(strategy, domains, C, Ct, R, Rt, m, n, null);
154 }
155 catch (Satisfiable e) {}
156 }
157 }