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 PropJoinInjectiveRelationCard extends Propagator<Variable> {
018
019    private final SetVar take;
020    private final IntVar takeCard;
021    private final IntVar[] childrenCards;
022    private final IntVar toCard;
023
024    public PropJoinInjectiveRelationCard(SetVar take, IntVar takeCard, IntVar[] childrenCards, IntVar toCard) {
025        super(buildArray(take, takeCard, toCard, childrenCards), PropagatorPriority.LINEAR, false);
026        this.take = take;
027        this.takeCard = takeCard;
028        this.childrenCards = childrenCards;
029        this.toCard = toCard;
030    }
031
032    private static Variable[] buildArray(SetVar take, IntVar takeCard, IntVar toCard, IntVar[] childrenCards) {
033        Variable[] array = new Variable[childrenCards.length + 3];
034        array[0] = take;
035        array[1] = takeCard;
036        array[2] = toCard;
037        System.arraycopy(childrenCards, 0, array, 3, childrenCards.length);
038        return array;
039    }
040
041    private boolean isTakeVar(int idx) {
042        return idx == 0;
043    }
044
045    private boolean isTakeCardVar(int idx) {
046        return idx == 1;
047    }
048
049    private boolean isToCardVar(int idx) {
050        return idx == 2;
051    }
052
053    private boolean isChildCardVar(int idx) {
054        return idx >= 3;
055    }
056
057    private int getChildCardVarIndex(int idx) {
058        assert isChildCardVar(idx);
059        return idx - 3;
060    }
061
062    @Override
063    public boolean advise(int idxVarInProp, int mask) {
064        if (isChildCardVar(idxVarInProp)) {
065            return take.envelopeContains(getChildCardVarIndex(idxVarInProp));
066        }
067        return super.advise(idxVarInProp, mask);
068    }
069
070    @Override
071    public int getPropagationConditions(int vIdx) {
072        if (isTakeVar(vIdx)) {
073            return EventType.ADD_TO_KER.mask + EventType.REMOVE_FROM_ENVELOPE.mask;
074        }
075        assert isTakeCardVar(vIdx) || isToCardVar(vIdx) || isChildCardVar(vIdx);
076        return EventType.BOUND.mask + EventType.INSTANTIATE.mask;
077    }
078
079    @Override
080    public void propagate(int evtmask) throws ContradictionException {
081        int minCard = 0;
082        int maxCard = 0;
083        for (int i = take.getEnvelopeFirst(); i != SetVar.END; i = take.getEnvelopeNext()) {
084            IntVar childCard = childrenCards[i];
085            if (take.kernelContains(i)) {
086                minCard += childCard.getLB();
087            }
088            maxCard += childCard.getUB();
089        }
090        boolean changed;
091        do {
092            changed = false;
093            toCard.updateLowerBound(minCard, aCause);
094            toCard.updateUpperBound(maxCard, aCause);
095
096            int lb = toCard.getLB();
097            int ub = toCard.getUB();
098
099            int minCardInc = 0;
100            int maxCardDec = 0;
101
102            for (int i = take.getEnvelopeFirst(); i != SetVar.END; i = take.getEnvelopeNext()) {
103                if (!take.kernelContains(i)) {
104                    IntVar childCard = childrenCards[i];
105                    if (maxCard - childCard.getUB() < lb) {
106                        take.addToKernel(i, aCause);
107                        minCardInc += childCard.getLB();
108                        changed = true;
109                    } else if (minCard + childCard.getLB() > ub) {
110                        take.removeFromEnvelope(i, aCause);
111                        maxCardDec += childCard.getUB();
112                        changed = true;
113                    }
114                }
115            }
116            minCard += minCardInc;
117            maxCard -= maxCardDec;
118        } while (changed);
119
120        int lb = toCard.getLB();
121        int ub = toCard.getUB();
122        int[] envLbs = new int[take.getEnvelopeSize() - take.getKernelSize()];
123        int[] envUbs = new int[envLbs.length];
124        int kerMinCard = 0;
125        int kerMaxCard = 0;
126        int env = 0;
127        for (int i = take.getEnvelopeFirst(); i != SetVar.END; i = take.getEnvelopeNext()) {
128            if (take.kernelContains(i)) {
129                kerMinCard += childrenCards[i].getLB();
130                kerMaxCard += childrenCards[i].getUB();
131            } else {
132                envLbs[env] = childrenCards[i].getLB();
133                envUbs[env] = childrenCards[i].getUB();
134                env++;
135            }
136        }
137        Arrays.sort(envLbs);
138        Arrays.sort(envUbs);
139        int i;
140        for (i = 0; i < envLbs.length && (kerMinCard < ub || envLbs[i] == 0); i++) {
141            kerMinCard += envLbs[i];
142        }
143        takeCard.updateUpperBound(i + take.getKernelSize(), aCause);
144        for (i = envUbs.length - 1; i >= 0 && kerMaxCard < lb; i--) {
145            kerMaxCard += envUbs[i];
146        }
147        takeCard.updateLowerBound(envUbs.length - 1 - i + take.getKernelSize(), aCause);
148    }
149
150    @Override
151    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
152        forcePropagate(EventType.FULL_PROPAGATION);
153    }
154
155    @Override
156    public ESat isEntailed() {
157        boolean completelyInstantiated = take.instantiated() && takeCard.instantiated() && toCard.instantiated();
158        int minCard = 0;
159        int maxCard = 0;
160        for (int i = take.getEnvelopeFirst(); i != SetVar.END; i = take.getEnvelopeNext()) {
161            if (i >= 0 && i < childrenCards.length) {
162                IntVar childCard = childrenCards[i];
163                completelyInstantiated = completelyInstantiated && childCard.instantiated();
164                if (take.kernelContains(i)) {
165                    minCard += childCard.getLB();
166                }
167                maxCard += childCard.getUB();
168            }
169        }
170
171        if (toCard.getUB() < minCard) {
172            return ESat.FALSE;
173        }
174        if (toCard.getLB() > maxCard) {
175            return ESat.FALSE;
176        }
177
178        return completelyInstantiated ? ESat.TRUE : ESat.UNDEFINED;
179    }
180
181    @Override
182    public String toString() {
183        return "joinInjectiveRelationCard(" + take + ", " + takeCard + ", " + Arrays.toString(childrenCards) + ", " + toCard + ")";
184    }
185}