001package org.clafer.choco.constraint.propagator;
002
003import java.util.Arrays;
004import org.clafer.common.Util;
005import solver.constraints.Propagator;
006import solver.constraints.PropagatorPriority;
007import solver.exception.ContradictionException;
008import solver.variables.EventType;
009import solver.variables.IntVar;
010import util.ESat;
011
012/**
013 *
014 * @author jimmy
015 */
016public class PropSetUnionCard extends Propagator<IntVar> {
017
018    private final IntVar[] setCards;
019    private final IntVar unionCard;
020
021    private static PropagatorPriority computePriority(int nbvars) {
022        switch (nbvars) {
023            case 1:
024                return PropagatorPriority.UNARY;
025            case 2:
026                return PropagatorPriority.BINARY;
027            case 3:
028                return PropagatorPriority.TERNARY;
029            default:
030                return PropagatorPriority.LINEAR;
031        }
032    }
033
034    public PropSetUnionCard(IntVar[] setCards, IntVar unionCard) {
035        super(Util.snoc(setCards, unionCard), computePriority(setCards.length), false);
036        this.setCards = setCards;
037        this.unionCard = unionCard;
038    }
039
040    private boolean isSetCardVar(int idx) {
041        return idx < setCards.length;
042    }
043
044    private int getSetCardVarIndex(int idx) {
045        return idx;
046    }
047
048    private boolean isUnionCardVar(int idx) {
049        return idx == setCards.length;
050    }
051
052    @Override
053    protected int getPropagationConditions(int vIdx) {
054        return EventType.BOUND.mask + EventType.INSTANTIATE.mask;
055    }
056
057    @Override
058    public void propagate(int evtmask) throws ContradictionException {
059        boolean changed;
060        do {
061            changed = false;
062            int min = 0;
063            int max = 0;
064            for (IntVar setCard : setCards) {
065                min = Math.max(min, setCard.getLB());
066                max += setCard.getUB();
067            }
068            unionCard.updateLowerBound(min, aCause);
069            unionCard.updateUpperBound(max, aCause);
070            int lb = unionCard.getLB();
071            int ub = unionCard.getUB();
072
073            for (IntVar setCard : setCards) {
074                changed |= setCard.updateUpperBound(ub, aCause);
075                changed |= setCard.updateLowerBound(lb - max + setCard.getUB(), aCause);
076            }
077        } while (changed);
078    }
079
080    @Override
081    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
082        forcePropagate(EventType.FULL_PROPAGATION);
083    }
084
085    @Override
086    public ESat isEntailed() {
087        int min = 0;
088        int max = 0;
089        for (IntVar setCard : setCards) {
090            min = Math.max(min, setCard.getLB());
091            max += setCard.getUB();
092        }
093        if (min > unionCard.getUB() || max < unionCard.getLB()) {
094            return ESat.FALSE;
095        }
096        return isCompletelyInstantiated() ? ESat.TRUE : ESat.UNDEFINED;
097    }
098
099    @Override
100    public String toString() {
101        return "unionCard(" + Arrays.toString(setCards) + ", " + unionCard + ")";
102    }
103}