001: package mlsub.typing.lowlevel;
002:
003: /**
004: * A "Domain" is a BitVector that holds all the possible values of a variable.
005: *
006: * A value can be any rigid variable or a special constant called "unit" which
007: * implements all the interfaces of the constraint but is comparable with no
008: * rigid variable. This is to handle satisfiability in the absence of any
009: * satisfiability witness For example, the constraint x <= x IS satisfiable
010: * even if there is no rigid variable. In this case, the domain of x is {unit}
011: *
012: * When a domain becomes empty, i.e., when it does not contain any rigid
013: * variable nor unit, it means that the contraint is unsatisfiable.
014: *
015: * @version $Revision: 1.7 $, $Date: 2005/03/30 23:08:16 $
016: * @author Alexandre Frey
017: **/
018: final class Domain extends BitVector {
019: private boolean containsUnit; // true if this domain contains index -1 (or unit)
020:
021: final static int UP = 0;
022: final static int DOWN = 1;
023: int cardUp = Integer.MAX_VALUE; // cardinal of the domain the last time
024: // it has been propagated up (including unit)
025: int cardDown = Integer.MAX_VALUE;// and down
026:
027: public Domain(int width) {
028: super (width);
029: fill(width);
030: this .containsUnit = true;
031: this .cardUp = width;
032: this .cardDown = width;
033: }
034:
035: /**
036: * Creates a copy of a Domain.
037: **/
038: public Domain(Domain old) {
039: super (old);
040: this .containsUnit = old.containsUnit;
041: this .cardUp = old.cardUp;
042: this .cardDown = old.cardDown;
043: }
044:
045: // size of this domain (possibly including unit)
046: int cardinal() {
047: if (containsUnit) {
048: return super .bitCount() + 1;
049: } else {
050: return super .bitCount();
051: }
052: }
053:
054: public boolean isEmpty() {
055: return !containsUnit && super .isEmpty();
056: }
057:
058: public boolean containsUnit() {
059: return containsUnit;
060: }
061:
062: public boolean needPropagation(int direction) {
063: int card = cardinal();
064: switch (direction) {
065: case UP:
066: if (card < cardUp) {
067: cardUp = card;
068: return true;
069: }
070: break;
071: case DOWN:
072: if (card < cardDown) {
073: cardDown = card;
074: return true;
075: }
076: break;
077: }
078: return false;
079: }
080:
081: void initGfpCardinals() {
082: cardUp = Integer.MAX_VALUE;
083: cardDown = Integer.MAX_VALUE;
084: }
085:
086: /**
087: * Constrain this domain to be included in (set, unit)
088: **/
089: public void reduce(boolean unit, BitVector set)
090: throws LowlevelUnsatisfiable {
091: this .and(set);
092: this .containsUnit &= unit;
093: if (this .isEmpty()) {
094: throw LowlevelUnsatisfiable.instance;
095: }
096: }
097:
098: /**
099: * Exclude all the values in set
100: **/
101: public void exclude(BitVector set) throws LowlevelUnsatisfiable {
102: this .andNot(set);
103: if (this .isEmpty()) {
104: throw LowlevelUnsatisfiable.instance;
105: }
106: }
107:
108: void rawExcludeUnit() {
109: this .containsUnit = false;
110: }
111:
112: public void excludeUnit() throws LowlevelUnsatisfiable {
113: this .containsUnit = false;
114: if (this .isEmpty()) {
115: throw LowlevelUnsatisfiable.instance;
116: }
117: }
118:
119: /**
120: * Exclude value of this domain
121: * assume value >= -1 (-1 represents unit)
122: **/
123: public void exclude(int value) throws LowlevelUnsatisfiable {
124: if (value == -1) {
125: this .containsUnit = false;
126: } else {
127: super .clear(value);
128: }
129: if (this .isEmpty()) {
130: throw LowlevelUnsatisfiable.instance;
131: }
132: }
133:
134: /**
135: * choose a value in this domain
136: * Returns -1 if the only possible value is unit
137: * @exception LowlevelUnsatisfiable if this.isEmpty()
138: **/
139: public int chooseValue() throws LowlevelUnsatisfiable {
140: return chooseValue(true, null);
141: }
142:
143: /**
144: * Choose a value within (unit, set)
145: * @exception LowlevelUnsatisfiable is this contains
146: * no element in (unit, set)
147: **/
148: public int chooseValue(boolean unit, BitVector set)
149: throws LowlevelUnsatisfiable {
150: int res = (set == null ? getLowestSetBit()
151: : getLowestSetBitAnd(set));
152: if (res != BitVector.UNDEFINED_INDEX) {
153: return res;
154: } else {
155: if (unit && containsUnit()) {
156: return -1;
157: } else {
158: throw LowlevelUnsatisfiable.instance;
159: }
160: }
161: }
162:
163: /**
164: * value >= -1 (-1 represents unit)
165: **/
166: public boolean containsValue(int value) {
167: if (value == -1) {
168: return containsUnit;
169: } else {
170: return super .get(value);
171: }
172: }
173:
174: /**
175: * Restrict this domain to be exactly {value}
176: * value is required to be >= -1 (-1 represents unit)
177: * @exception LowlevelUnsatisfiable if value is not in the domain
178: **/
179: public void instantiate(int value) throws LowlevelUnsatisfiable {
180: if (!containsValue(value)) {
181: throw LowlevelUnsatisfiable.instance;
182: }
183: clearAll();
184: this .containsUnit = false;
185: if (value == -1) {
186: this .containsUnit = true;
187: } else {
188: set(value);
189: }
190: }
191:
192: /**
193: * Returns true if there is a common value in this and set
194: * i.e., if chooseValue(false, set) will not throw LowlevelUnsatisfiable
195: **/
196: public boolean intersect(BitVector set) {
197: return this .getLowestSetBitAnd(set) != BitVector.UNDEFINED_INDEX;
198: }
199:
200: public String toString() {
201: StringBuffer sb = new StringBuffer();
202: sb.append(super .toString());
203: if (containsUnit) {
204: sb.append("+{-1}");
205: }
206: return sb.toString();
207: }
208:
209: /**
210: * Iteration thru the domain elements
211: **/
212: int getFirstBit() { // unused method ???
213: int result = super .getLowestSetBit();
214: if (result == UNDEFINED_INDEX && containsUnit) {
215: // don't forget unit !
216: result = -1;
217: }
218: return result;
219: }
220:
221: public int getNextBit(int i) {
222: int result;
223: if (i >= 0) {
224: result = super .getNextBit(i);
225: if (result == UNDEFINED_INDEX && containsUnit) {
226: result = -1;
227: }
228: } else {
229: // i is either -1 or UNDEFINED_INDEX
230: result = UNDEFINED_INDEX;
231: }
232: return result;
233: }
234:
235: }
|