Source code

001package org.clafer.choco.constraint.propagator;
002
003import gnu.trove.iterator.TIntIntIterator;
004import gnu.trove.map.hash.TIntIntHashMap;
005import java.util.Arrays;
006import solver.constraints.Propagator;
007import solver.constraints.PropagatorPriority;
008import solver.exception.ContradictionException;
009import solver.variables.EventType;
010import solver.variables.IntVar;
011import solver.variables.SetVar;
012import solver.variables.Variable;
013import util.ESat;
014
015/**
016 *
017 * @author jimmy
018 */
019public class PropJoinFunctionCard extends Propagator<Variable> {
020
021    private final SetVar take;
022    private final IntVar takeCard;
023    private final IntVar[] refs;
024    private final IntVar toCard;
025    private final Integer globalCardinality;
026
027    public PropJoinFunctionCard(SetVar take, IntVar takeCard, IntVar[] refs, IntVar toCard, Integer globalCardinality) {
028        super(buildArray(take, takeCard, toCard, refs), PropagatorPriority.LINEAR, false);
029        this.take = take;
030        this.takeCard = takeCard;
031        this.refs = refs;
032        this.toCard = toCard;
033        this.globalCardinality = globalCardinality;
034    }
035
036    private static Variable[] buildArray(SetVar take, IntVar takeCard, IntVar toCard, IntVar[] refs) {
037        Variable[] array = new Variable[refs.length + 3];
038        array[0] = take;
039        array[1] = takeCard;
040        array[2] = toCard;
041        System.arraycopy(refs, 0, array, 3, refs.length);
042        return array;
043    }
044
045    private boolean isTakeVar(int idx) {
046        return idx == 0;
047    }
048
049    private boolean isTakeCardVar(int idx) {
050        return idx == 1;
051    }
052
053    private boolean isToCardVar(int idx) {
054        return idx == 2;
055    }
056
057    private boolean isRefVar(int idx) {
058        return idx >= 3;
059    }
060
061    private int getRefVarIndex(int idx) {
062        assert isRefVar(idx);
063        return idx - 3;
064    }
065
066    public boolean hasGlobalCardinality() {
067        return globalCardinality != null;
068    }
069
070    public int getGlobalCardinality() {
071        assert hasGlobalCardinality();
072        return globalCardinality.intValue();
073    }
074
075    @Override
076    public boolean advise(int idxVarInProp, int mask) {
077        if (isRefVar(idxVarInProp)) {
078            return take.envelopeContains(getRefVarIndex(idxVarInProp));
079        }
080        return super.advise(idxVarInProp, mask);
081    }
082
083    @Override
084    public int getPropagationConditions(int vIdx) {
085        if (isTakeVar(vIdx)) {
086            return EventType.ADD_TO_KER.mask + EventType.REMOVE_FROM_ENVELOPE.mask;
087        }
088        if (isRefVar(vIdx)) {
089            return EventType.INSTANTIATE.mask;
090        }
091        assert isTakeCardVar(vIdx) || isToCardVar(vIdx);
092        return EventType.BOUND.mask + EventType.INSTANTIATE.mask;
093    }
094
095    private int countAdditionalSameRefsAllowed(TIntIntHashMap map) {
096        assert hasGlobalCardinality();
097        int gc = getGlobalCardinality();
098
099        int allowed = 0;
100
101        if (gc != 1) {
102            TIntIntIterator iter = map.iterator();
103            for (int i = map.size(); i-- > 0;) {
104                iter.advance();
105                assert iter.value() > 0;
106                assert iter.value() <= gc;
107                allowed += gc - iter.value();
108            }
109            assert !iter.hasNext();
110        }
111
112        return allowed;
113    }
114
115    private TIntIntHashMap countRefs() {
116        TIntIntHashMap map = new TIntIntHashMap(take.getKernelSize());
117        for (int i = take.getKernelFirst(); i != SetVar.END; i = take.getKernelNext()) {
118            IntVar ref = refs[i];
119            if (ref.instantiated()) {
120                map.adjustOrPutValue(ref.getValue(), 1, 1);
121            }
122        }
123        return map;
124    }
125
126    private TIntIntHashMap constrainGlobalCardinality() throws ContradictionException {
127        assert hasGlobalCardinality();
128        int[] ker = PropUtil.iterateKer(take);
129        TIntIntHashMap map = new TIntIntHashMap(ker.length);
130        for (int i = 0; i < ker.length; i++) {
131            constrainGlobalCardinality(ker, i, i, map);
132        }
133        return map;
134    }
135
136    private void constrainGlobalCardinality(int[] ker, int index, int explored, TIntIntHashMap map) throws ContradictionException {
137        assert hasGlobalCardinality();
138        assert index <= explored;
139        assert explored < ker.length;
140
141        IntVar a = refs[ker[index]];
142        if (a.instantiated()) {
143            int value = a.getValue();
144            int count = map.adjustOrPutValue(value, 1, 1);
145            int gc = getGlobalCardinality();
146
147            if (count == gc) {
148                for (int j = 0; j < explored; j++) {
149                    IntVar b = refs[ker[j]];
150                    if (!b.instantiatedTo(value) && b.removeValue(value, aCause)) {
151                        constrainGlobalCardinality(ker, j, explored, map);
152                    }
153                }
154                for (int j = explored + 1; j < ker.length; j++) {
155                    refs[ker[j]].removeValue(value, aCause);
156                }
157            } else if (count > gc) {
158                contradiction(a, "Above global cardinality");
159            }
160        }
161    }
162
163    private static int divRoundUp(int a, int b) {
164        assert a >= 0;
165        assert b > 0;
166
167        return (a + b - 1) / b;
168    }
169
170    @Override
171    public void propagate(int evtmask) throws ContradictionException {
172        takeCard.updateLowerBound(take.getKernelSize(), aCause);
173        takeCard.updateUpperBound(take.getEnvelopeSize(), aCause);
174        boolean changed;
175        do {
176            changed = false;
177            TIntIntHashMap map = hasGlobalCardinality() ? constrainGlobalCardinality() : countRefs();
178            int instCard = map.size();
179            int kerSize = take.getKernelSize();
180
181            int minUninstantiated;
182            int maxUninstantiated;
183            int minCard;
184            int maxCard;
185            boolean cardChanged;
186            do {
187                cardChanged = false;
188//                minUninstantiated = Math.max(0, takeCard.getLB() - kerSize);
189//                maxUninstantiated = Math.max(0, takeCard.getUB() - kerSize);
190                int kerUninstantiated = 0;
191                for (int i = take.getEnvelopeFirst(); i != SetVar.END; i = take.getEnvelopeNext()) {
192                    if (!refs[i].instantiated()) {
193                        if (take.kernelContains(i)) {
194                            kerUninstantiated++;
195                        }
196                    }
197                }
198                assert takeCard.getLB() >= kerSize;
199                minUninstantiated = takeCard.getLB() - kerSize + kerUninstantiated;
200                maxUninstantiated = takeCard.getUB() - kerSize + kerUninstantiated;
201                minCard = instCard
202                        + (hasGlobalCardinality()
203                        ? divRoundUp(Math.max(0, minUninstantiated - countAdditionalSameRefsAllowed(map)), getGlobalCardinality())
204                        : 0);
205                maxCard = instCard + maxUninstantiated;
206
207                toCard.updateLowerBound(minCard, aCause);
208                toCard.updateUpperBound(maxCard, aCause);
209
210                if (hasGlobalCardinality()) {
211                    cardChanged |= takeCard.updateUpperBound(toCard.getUB() * getGlobalCardinality(), aCause);
212                }
213                cardChanged |= takeCard.updateLowerBound(toCard.getLB(), aCause);
214            } while (cardChanged);
215
216
217            if (maxUninstantiated != 0) {
218                if (instCard == toCard.getUB()) {
219                    // The rest must be duplicates.
220                    for (int i = take.getKernelFirst(); i != SetVar.END; i = take.getKernelNext()) {
221                        IntVar ref = refs[i];
222                        assert !ref.instantiated() || map.contains(ref.getValue());
223                        if (!ref.instantiated()) {
224                            changed |= PropUtil.domSubsetSet(ref, map.keySet(), aCause) && ref.instantiated();
225                        }
226                    }
227                }
228                if (maxCard == toCard.getLB()) {
229                    // No more duplicate values.
230                    for (int i = take.getKernelFirst(); i != SetVar.END; i = take.getKernelNext()) {
231                        IntVar ref = refs[i];
232                        if (!ref.instantiated()) {
233                            TIntIntIterator iter = map.iterator();
234                            for (int j = map.size(); j-- > 0;) {
235                                iter.advance();
236                                changed |= ref.removeValue(iter.key(), aCause) && ref.instantiated();
237                            }
238                            assert !iter.hasNext();
239                        }
240                    }
241                }
242            }
243        } while (changed);
244    }
245
246    @Override
247    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
248        forcePropagate(EventType.FULL_PROPAGATION);
249    }
250
251    @Override
252    public ESat isEntailed() {
253        TIntIntHashMap map = new TIntIntHashMap();
254        int gc = hasGlobalCardinality() ? getGlobalCardinality() : Integer.MAX_VALUE;
255        for (int i = take.getKernelFirst(); i != SetVar.END; i = take.getKernelNext()) {
256            IntVar ref = refs[i];
257            if (ref.instantiated()) {
258                if (map.adjustOrPutValue(ref.getValue(), 1, 1) > gc) {
259                    return ESat.FALSE;
260                }
261            }
262        }
263
264        boolean completelyInstantiated = take.instantiated() && takeCard.instantiated() && toCard.instantiated();
265        int instCard = map.size();
266        int minUninstantiated = Math.max(0, takeCard.getLB() - take.getKernelSize());
267        int maxUninstantiated = Math.max(0, takeCard.getUB() - take.getKernelSize());
268        for (int i = take.getEnvelopeFirst(); i != SetVar.END; i = take.getEnvelopeNext()) {
269            if (i >= 0 && i < refs.length && !refs[i].instantiated()) {
270                completelyInstantiated = false;
271                if (take.kernelContains(i)) {
272                    minUninstantiated++;
273                }
274                maxUninstantiated++;
275            }
276        }
277        int minCard = instCard
278                + (hasGlobalCardinality()
279                ? divRoundUp(Math.max(0, minUninstantiated - countAdditionalSameRefsAllowed(map)), getGlobalCardinality())
280                : 0);
281        int maxCard = instCard + maxUninstantiated;
282
283        if (toCard.getUB() < minCard) {
284            return ESat.FALSE;
285        }
286        if (toCard.getLB() > maxCard) {
287            return ESat.FALSE;
288        }
289
290        return completelyInstantiated ? ESat.TRUE : ESat.UNDEFINED;
291    }
292
293    @Override
294    public String toString() {
295        return "joinFunctionCard(" + take + ", " + takeCard + ", " + Arrays.toString(refs) + ", " + toCard + ", " + globalCardinality + ")";
296    }
297}