Source code

001package org.clafer.choco.constraint.propagator;
002
003import java.util.Arrays;
004import solver.constraints.Propagator;
005import solver.constraints.PropagatorPriority;
006import solver.exception.ContradictionException;
007import solver.variables.EventType;
008import solver.variables.IntVar;
009import util.ESat;
010
011/**
012 * strings[i] &lt; strings[j] iff ints[i] &lt;= ints[j] strings[i] = strings[j]
013 * iff ints[i] = ints[j]
014 *
015 * 0 &lt; ints[i] &lt; |{ints}|
016 *
017 * @author jimmy
018 */
019public class PropLexChainChannel extends Propagator<IntVar> {
020
021    private final IntVar[][] strings;
022    private final IntVar[] ints;
023
024    public PropLexChainChannel(IntVar[][] strings, IntVar[] ints) {
025        super(buildArray(strings, ints), PropagatorPriority.CUBIC, false);
026        this.strings = strings;
027        this.ints = ints;
028    }
029
030    private static IntVar[] buildArray(IntVar[][] strings, IntVar[] ints) {
031        if (strings.length != ints.length) {
032            throw new IllegalArgumentException();
033        }
034        IntVar[] array = new IntVar[strings.length * strings[0].length + ints.length];
035        System.arraycopy(ints, 0, array, 0, ints.length);
036        int i = ints.length;
037        for (IntVar[] string : strings) {
038            System.arraycopy(string, 0, array, i, string.length);
039            i += string.length;
040        }
041        assert i == array.length;
042        return array;
043    }
044
045    @Override
046    public int getPropagationConditions(int vIdx) {
047        return EventType.BOUND.mask + EventType.INSTANTIATE.mask;
048    }
049
050    private static Ordering compareString(IntVar[] a, IntVar[] b) {
051        return compareString(a, b, 0);
052    }
053
054    private static Ordering compareString(IntVar[] a, IntVar[] b, int index) {
055        if (index == a.length) {
056            return a.length == b.length ? Ordering.EQ : Ordering.LT;
057        }
058        if (index == b.length) {
059            assert a.length != b.length;
060            return Ordering.GT;
061        }
062        Ordering ord = compare(a[index], b[index]);
063        switch (ord) {
064            case EQ:
065                return compareString(a, b, index + 1);
066            case LE:
067                switch (compareString(a, b, index + 1)) {
068                    case LT:
069                        return Ordering.LT;
070                    case LE:
071                    case EQ:
072                        return Ordering.LE;
073                    default:
074                        return Ordering.UNKNOWN;
075                }
076            case GE:
077                switch (compareString(a, b, index + 1)) {
078                    case GT:
079                        return Ordering.GT;
080                    case GE:
081                    case EQ:
082                        return Ordering.GE;
083                    default:
084                        return Ordering.UNKNOWN;
085                }
086            default:
087                return ord;
088        }
089    }
090
091    private static Ordering compare(IntVar a, IntVar b) {
092        int aLb = a.getLB();
093        int aUb = a.getUB();
094        int bLb = b.getLB();
095        int bUb = b.getUB();
096        if (aLb == bUb && aUb == bLb) {
097            return Ordering.EQ;
098        }
099        if (aLb > bUb) {
100            return Ordering.GT;
101        }
102        if (aLb >= bUb) {
103            return Ordering.GE;
104        }
105        if (aUb < bLb) {
106            return Ordering.LT;
107        }
108        if (aUb <= bLb) {
109            return Ordering.LE;
110        }
111        return Ordering.UNKNOWN;
112    }
113
114    private boolean equalString(IntVar[] a, IntVar[] b) throws ContradictionException {
115        boolean changed = false;
116        for (int i = 0; i < a.length; i++) {
117            changed |= equal(a[i], b[i]);
118        }
119        return changed;
120    }
121
122    private boolean equal(IntVar a, IntVar b) throws ContradictionException {
123        // Don't use short-circuit or
124        return a.updateLowerBound(b.getLB(), aCause)
125                | a.updateUpperBound(b.getUB(), aCause)
126                | b.updateLowerBound(a.getLB(), aCause)
127                | b.updateUpperBound(a.getUB(), aCause);
128    }
129
130    private boolean lessThanString(IntVar[] a, IntVar[] b) throws ContradictionException {
131        return lessThanString(a, b, 0);
132    }
133
134    private boolean lessThanString(IntVar[] a, IntVar[] b, int index) throws ContradictionException {
135        if (index == a.length) {
136            if (index == b.length) {
137                contradiction(a[0], "a = b");
138            }
139            return false;
140        }
141        if (index == b.length) {
142            assert a.length != b.length;
143            contradiction(a[index], "a > b");
144        }
145        switch (compare(a[index], b[index])) {
146            case EQ:
147                return lessThanString(a, b, index + 1);
148            case LT:
149                return false;
150            case GT:
151                contradiction(a[index], "a > b");
152                return true;
153            case LE:
154            case GE:
155            case UNKNOWN:
156                switch (compareString(a, b, index + 1)) {
157                    case EQ:
158                    case GT:
159                    case GE:
160                        return lessThan(a[index], b[index]);
161                    case LT:
162                    case LE:
163                    case UNKNOWN:
164                        return lessThanEqual(a[index], b[index]);
165                    default:
166                        throw new IllegalStateException();
167                }
168            default:
169                throw new IllegalStateException();
170        }
171    }
172
173    private boolean lessThan(IntVar a, IntVar b) throws ContradictionException {
174        // Don't use short-circuit or
175        return a.updateUpperBound(b.getUB() - 1, aCause)
176                | b.updateLowerBound(a.getLB() + 1, aCause);
177    }
178
179    private boolean lessThanEqualString(IntVar[] a, IntVar[] b) throws ContradictionException {
180        return lessThanEqualString(a, b, 0);
181    }
182
183    private boolean lessThanEqualString(IntVar[] a, IntVar[] b, int index) throws ContradictionException {
184        if (index == a.length) {
185            return false;
186        }
187        if (index == b.length) {
188            assert a.length != b.length;
189            contradiction(a[index], "a > b");
190        }
191        switch (compare(a[index], b[index])) {
192            case EQ:
193                return lessThanEqualString(a, b, index + 1);
194            case LT:
195                return false;
196            case GT:
197                contradiction(a[index], "a > b");
198                return true;
199            case LE:
200            case GE:
201            case UNKNOWN:
202                switch (compareString(a, b, index + 1)) {
203                    case EQ:
204                    case LT:
205                    case LE:
206                    case GE:
207                    case UNKNOWN:
208                        return lessThanEqual(a[index], b[index]);
209                    case GT:
210                        return lessThan(a[index], b[index]);
211                    default:
212                        throw new IllegalStateException();
213                }
214            default:
215                throw new IllegalStateException();
216        }
217    }
218
219    private boolean lessThanEqual(IntVar a, IntVar b) throws ContradictionException {
220        // Don't use short-circuit or
221        return a.updateUpperBound(b.getUB(), aCause)
222                | b.updateLowerBound(a.getLB(), aCause);
223    }
224
225    private boolean propagateSmallest(boolean[] notSmallest, boolean notSmaller[], boolean[] lessThanEqual, int smallest) throws ContradictionException {
226        boolean changed = false;
227        boolean stop = true;
228        boolean lessThanEqualStop = false;
229        boolean[] notNextSmallest = new boolean[strings.length];
230        for (int i = 0; i < notSmallest.length; i++) {
231            if (!notSmallest[i]) {
232                notSmaller[i] = false;
233                stop = false;
234                lessThanEqualStop |= lessThanEqual[i];
235                changed |= ints[i].instantiateTo(smallest, aCause);
236            }
237            notNextSmallest[i] = !notSmaller[i];
238        }
239        if (stop || lessThanEqualStop) {
240            return changed;
241        }
242        for (int i = 0; i < strings.length; i++) {
243            if (notSmaller[i]) {
244                for (int j = i + 1; j < strings.length; j++) {
245                    if (notSmaller[j]) {
246                        Ordering ord = compareString(strings[i], strings[j]);
247                        switch (ord) {
248                            case LE:
249                                lessThanEqual[i] = true;
250                            // fallthrough
251                            case LT:
252                                notNextSmallest[j] = true;
253                                break;
254                            case GE:
255                                lessThanEqual[j] = true;
256                            // fallthrough
257                            case GT:
258                                notNextSmallest[i] = true;
259                                break;
260                            case UNKNOWN:
261                                notNextSmallest[i] = true;
262                                notNextSmallest[j] = true;
263                                break;
264                        }
265                    }
266                }
267            }
268        }
269        changed |= propagateSmallest(notNextSmallest, notSmaller, lessThanEqual, smallest + 1);
270        return changed;
271    }
272
273    // Idempotent.
274    private boolean propagateStrings() throws ContradictionException {
275        int eqs = 0;
276        boolean[] notSmallest = new boolean[strings.length];
277        boolean[] lessThanEqual = new boolean[strings.length];
278        boolean changed = false;
279        for (int i = 0; i < strings.length; i++) {
280            boolean equivalenceClass = false;
281            for (int j = i + 1; j < strings.length; j++) {
282                Ordering ord = compareString(strings[i], strings[j]);
283                switch (ord) {
284                    case EQ:
285                        changed |= equal(ints[i], ints[j]);
286                        equivalenceClass = true;
287                        break;
288                    case LE:
289                        changed |= lessThanEqual(ints[i], ints[j]);
290                        lessThanEqual[i] = true;
291                        notSmallest[j] = true;
292                        break;
293                    case LT:
294                        changed |= lessThan(ints[i], ints[j]);
295                        notSmallest[j] = true;
296                        break;
297                    case GE:
298                        changed |= lessThanEqual(ints[j], ints[i]);
299                        lessThanEqual[j] = true;
300                        notSmallest[i] = true;
301                        break;
302                    case GT:
303                        changed |= lessThan(ints[j], ints[i]);
304                        notSmallest[i] = true;
305                        break;
306                    case UNKNOWN:
307                        notSmallest[i] = true;
308                        notSmallest[j] = true;
309                        break;
310                }
311            }
312            if (equivalenceClass) {
313                eqs++;
314            }
315        }
316        changed |= propagateSmallest(notSmallest, notSmallest, lessThanEqual, 0);
317        for (int i = 0; i < ints.length; i++) {
318            changed |= ints[i].updateUpperBound(ints.length - 1 - eqs, aCause);
319        }
320        return changed;
321    }
322
323    // Idempotent.
324    private boolean propagateInts() throws ContradictionException {
325        boolean changed = false;
326        boolean repeat;
327        do {
328            repeat = false;
329            for (int i = 0; i < ints.length; i++) {
330                for (int j = i + 1; j < ints.length; j++) {
331                    switch (compare(ints[i], ints[j])) {
332                        case EQ:
333                            repeat |= equalString(strings[i], strings[j]);
334                            break;
335                        case LT:
336                            repeat |= lessThanString(strings[i], strings[j]);
337                            break;
338                        case LE:
339                            repeat |= lessThanEqualString(strings[i], strings[j]);
340                            break;
341                        case GT:
342                            repeat |= lessThanString(strings[j], strings[i]);
343                            break;
344                        case GE:
345                            repeat |= lessThanEqualString(strings[j], strings[i]);
346                            break;
347                    }
348                }
349            }
350            changed |= repeat;
351        } while (repeat);
352        return changed;
353    }
354
355    @Override
356    public void propagate(int evtmask) throws ContradictionException {
357        propagateStrings();
358        while (propagateInts() && propagateStrings());
359    }
360
361    @Override
362    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
363        forcePropagate(EventType.FULL_PROPAGATION);
364    }
365
366    @Override
367    public ESat isEntailed() {
368        boolean[] values = new boolean[ints.length];
369        for (int i = 0; i < strings.length; i++) {
370            for (int j = i + 1; j < strings.length; j++) {
371                Ordering intOrdering = compare(ints[i], ints[j]);
372                Ordering ord = compareString(strings[i], strings[j]);
373                if (intOrdering.contradicts(ord)) {
374                    return ESat.FALSE;
375                }
376            }
377            if (ints[i].instantiated()) {
378                int value = ints[i].getValue();
379                if (value < 0 || value >= values.length) {
380                    return ESat.FALSE;
381                }
382                values[value] = true;
383            }
384        }
385        if (isCompletelyInstantiated()) {
386            int i = 0;
387            while (i < values.length && values[i]) {
388                i++;
389            }
390            for (; i < values.length; i++) {
391                if (values[i]) {
392                    return ESat.FALSE;
393                }
394            }
395            return ESat.TRUE;
396        }
397        return ESat.UNDEFINED;
398    }
399
400    @Override
401    public String toString() {
402        return "lexChainChannel(" + Arrays.deepToString(strings) + ", " + Arrays.toString(ints) + ")";
403    }
404
405    private static enum Ordering {
406
407        EQ,
408        LT,
409        LE,
410        GT,
411        GE,
412        UNKNOWN;
413
414        boolean contradicts(Ordering ord) {
415            switch (this) {
416                case EQ:
417                    return LT.equals(ord) || GT.equals(ord);
418                case LT:
419                    return EQ.equals(ord) || GE.equals(ord) || GT.equals(ord);
420                case LE:
421                    return GT.equals(ord);
422                case GT:
423                    return EQ.equals(ord) || LE.equals(ord) || LT.equals(ord);
424                case GE:
425                    return LT.equals(ord);
426                case UNKNOWN:
427                    return false;
428                default:
429                    throw new IllegalStateException();
430            }
431        }
432    }
433}