Source code: mlsub/typing/lowlevel/Domain.java
1 package mlsub.typing.lowlevel;
2
3 /**
4 * A "Domain" is a BitVector that holds all the possible values of a variable.
5 *
6 * A value can be any rigid variable or a special constant called "unit" which
7 * implements all the interfaces of the constraint but is comparable with no
8 * rigid variable. This is to handle satisfiability in the absence of any
9 * satisfiability witness For example, the constraint x <= x IS satisfiable
10 * even if there is no rigid variable. In this case, the domain of x is {unit}
11 *
12 * When a domain becomes empty, i.e., when it does not contain any rigid
13 * variable nor unit, it means that the contraint is unsatisfiable.
14 *
15 * @version $Revision: 1.4 $, $Date: 2003/09/06 11:31:10 $
16 * @author Alexandre Frey
17 **/
18 final class Domain extends BitVector {
19 private boolean containsUnit; // true if this domain contains index -1 (or unit)
20
21 final static int UP = 0;
22 final static int DOWN = 1;
23 int cardUp = Integer.MAX_VALUE; // cardinal of the domain the last time
24 // it has been propagated up (including unit)
25 int cardDown = Integer.MAX_VALUE;// and down
26 public Domain(int width) {
27 super(width);
28 fill(width);
29 this.containsUnit = true;
30 this.cardUp = width;
31 this.cardDown = width;
32 }
33
34 // size of this domain (possibly including unit)
35 int cardinal() {
36 if (containsUnit) {
37 return super.bitCount() + 1;
38 } else {
39 return super.bitCount();
40 }
41 }
42
43 public boolean isEmpty() {
44 return !containsUnit && super.isEmpty();
45 }
46
47 public boolean containsUnit() {
48 return containsUnit;
49 }
50
51 public boolean needPropagation(int direction) {
52 int card = cardinal();
53 switch(direction) {
54 case UP:
55 if (card < cardUp) {
56 cardUp = card;
57 return true;
58 }
59 break;
60 case DOWN:
61 if (card < cardDown) {
62 cardDown = card;
63 return true;
64 }
65 break;
66 }
67 return false;
68 }
69
70 void initGfpCardinals() {
71 cardUp = Integer.MAX_VALUE;
72 cardDown = Integer.MAX_VALUE;
73 }
74
75 /**
76 * Constrain this domain to be included in (set, unit)
77 **/
78 public void reduce(boolean unit, BitVector set)
79 throws LowlevelUnsatisfiable {
80 this.and(set);
81 this.containsUnit &= unit;
82 if (this.isEmpty()) {
83 throw new LowlevelUnsatisfiable();
84 }
85 }
86
87 /**
88 * Exclude all the values in set
89 **/
90 public void exclude(BitVector set)
91 throws LowlevelUnsatisfiable {
92 this.andNot(set);
93 if (this.isEmpty()) {
94 throw new LowlevelUnsatisfiable();
95 }
96 }
97
98 void rawExcludeUnit() {
99 this.containsUnit = false;
100 }
101
102 public void excludeUnit() throws LowlevelUnsatisfiable {
103 this.containsUnit = false;
104 if (this.isEmpty()) {
105 throw new LowlevelUnsatisfiable();
106 }
107 }
108
109 /**
110 * Exclude value of this domain
111 * assume value >= -1 (-1 represents unit)
112 **/
113 public void exclude(int value) throws LowlevelUnsatisfiable {
114 if (value == -1) {
115 this.containsUnit = false;
116 } else {
117 super.clear(value);
118 }
119 if (this.isEmpty()) {
120 throw new LowlevelUnsatisfiable();
121 }
122 }
123
124 /**
125 * choose a value in this domain
126 * Returns -1 if the only possible value is unit
127 * @exception LowlevelUnsatisfiable if this.isEmpty()
128 **/
129 public int chooseValue() throws LowlevelUnsatisfiable {
130 return chooseValue(true, null);
131 }
132
133 /**
134 * Choose a value within (unit, set)
135 * @exception LowlevelUnsatisfiable is this contains
136 * no element in (unit, set)
137 **/
138 public int chooseValue(boolean unit, BitVector set)
139 throws LowlevelUnsatisfiable {
140 int res = (set == null ?
141 getLowestSetBit() :
142 getLowestSetBitAnd(set));
143 if (res != BitVector.UNDEFINED_INDEX) {
144 return res;
145 } else {
146 if (unit && containsUnit()) {
147 return -1;
148 } else {
149 throw new LowlevelUnsatisfiable();
150 }
151 }
152 }
153
154 /**
155 * value >= -1 (-1 represents unit)
156 **/
157 public boolean containsValue(int value) {
158 if (value == -1) {
159 return containsUnit;
160 } else {
161 return super.get(value);
162 }
163 }
164
165 /**
166 * Restrict this domain to be exactly {value}
167 * value is required to be >= -1 (-1 represents unit)
168 * @exception LowlevelUnsatisfiable if value is not in the domain
169 **/
170 public void instantiate(int value) throws LowlevelUnsatisfiable {
171 if (!containsValue(value)) {
172 throw new LowlevelUnsatisfiable();
173 }
174 clearAll();
175 this.containsUnit = false;
176 if (value == -1) {
177 this.containsUnit = true;
178 } else {
179 set(value);
180 }
181 }
182
183 /**
184 * Returns true if there is a common value in this and set
185 * i.e., if chooseValue(false, set) will not throw LowlevelUnsatisfiable
186 **/
187 public boolean intersect(BitVector set) {
188 return this.getLowestSetBitAnd(set) != BitVector.UNDEFINED_INDEX;
189 }
190
191 public String toString() {
192 StringBuffer sb = new StringBuffer();
193 sb.append(super.toString());
194 if (containsUnit) {
195 sb.append("+{-1}");
196 }
197 return sb.toString();
198 }
199
200
201 /**
202 * Iteration thru the domain elements
203 **/
204 int getFirstBit() { // unused method ???
205 int result = super.getLowestSetBit();
206 if (result == UNDEFINED_INDEX && containsUnit) {
207 // don't forget unit !
208 result = -1;
209 }
210 return result;
211 }
212 public int getNextBit(int i) {
213 int result;
214 if (i >= 0) {
215 result = super.getNextBit(i);
216 if (result == UNDEFINED_INDEX && containsUnit) {
217 result = -1;
218 }
219 } else {
220 // i is either -1 or UNDEFINED_INDEX
221 result = UNDEFINED_INDEX;
222 }
223 return result;
224 }
225 }