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 solver.variables.SetVar;
010import solver.variables.Variable;
011import util.ESat;
012
013/**
014 *
015 * @author jimmy
016 */
017public class PropSortedSetsCard extends Propagator<Variable> {
018
019    private final SetVar[] sets;
020    private final IntVar[] cards;
021
022    public PropSortedSetsCard(SetVar[] sets, IntVar[] cards) {
023        super(buildArray(sets, cards), PropagatorPriority.QUADRATIC, false);
024        if (sets.length != cards.length) {
025            throw new IllegalArgumentException();
026        }
027        this.sets = sets;
028        this.cards = cards;
029    }
030
031    private static Variable[] buildArray(SetVar[] sets, IntVar[] cards) {
032        Variable[] array = new Variable[sets.length + cards.length];
033        System.arraycopy(sets, 0, array, 0, sets.length);
034        System.arraycopy(cards, 0, array, sets.length, cards.length);
035        return array;
036    }
037
038    private boolean isSetVar(int idx) {
039        return idx < sets.length;
040    }
041
042    private int getSetVarIndex(int idx) {
043        return idx;
044    }
045
046    private boolean isCardVar(int idx) {
047        return idx >= sets.length;
048    }
049
050    private int getCardVarIndex(int idx) {
051        return idx - sets.length;
052    }
053
054    @Override
055    protected int getPropagationConditions(int vIdx) {
056        if (isCardVar(vIdx)) {
057            return EventType.BOUND.mask | EventType.INSTANTIATE.mask;
058        }
059        return EventType.VOID.mask;
060    }
061
062    @Override
063    public void propagate(int evtmask) throws ContradictionException {
064        int low = 0;
065        int high = 0;
066
067        for (int i = 0; i < cards.length; i++) {
068            IntVar card = cards[i];
069            int newLow = low + card.getLB();
070            int newHigh = high + card.getUB();
071            SetVar set = sets[i];
072            for (int j = set.getEnvelopeFirst(); j != SetVar.END; j = set.getEnvelopeNext()) {
073                if (j < low || j >= newHigh) {
074                    set.removeFromEnvelope(j, aCause);
075                }
076            }
077            for (int j = high; j < newLow; j++) {
078                set.addToKernel(j, aCause);
079            }
080            low = newLow;
081            high = newHigh;
082        }
083    }
084
085    @Override
086    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
087        forcePropagate(EventType.FULL_PROPAGATION);
088    }
089
090    @Override
091    public ESat isEntailed() {
092        int low = 0;
093        int high = 0;
094
095        for (int i = 0; i < cards.length; i++) {
096            IntVar card = cards[i];
097            int newLow = low + card.getLB();
098            int newHigh = high + card.getUB();
099            SetVar set = sets[i];
100            for (int j = set.getEnvelopeFirst(); j != SetVar.END; j = set.getEnvelopeNext()) {
101                if (j < low || j >= newHigh) {
102                    if (set.kernelContains(j)) {
103                        return ESat.FALSE;
104                    }
105                }
106            }
107            for (int j = high; j < newLow; j++) {
108                if (!set.envelopeContains(j)) {
109                    return ESat.FALSE;
110                }
111            }
112            low = newLow;
113            high = newHigh;
114        }
115
116        return isCompletelyInstantiated() ? ESat.TRUE : ESat.UNDEFINED;
117    }
118
119    @Override
120    public String toString() {
121        return "sorted(" + Arrays.toString(sets) + " || " + Arrays.toString(cards) + ")";
122    }
123}