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.BoolVar;
008import solver.variables.EventType;
009import solver.variables.IntVar;
010import util.ESat;
011
012/**
013 * The first n booleans are the true, the rest are false.
014 *
015 * @author jimmy
016 */
017public class PropSelectN extends Propagator<IntVar> {
018
019    private final BoolVar[] bools;
020    private final IntVar n;
021
022    public PropSelectN(BoolVar[] bools, IntVar n) {
023        super(buildArray(bools, n), PropagatorPriority.BINARY, true);
024        this.bools = bools;
025        this.n = n;
026    }
027
028    private static IntVar[] buildArray(BoolVar[] bools, IntVar n) {
029        IntVar[] init = new IntVar[bools.length + 1];
030        System.arraycopy(bools, 0, init, 0, bools.length);
031        init[bools.length] = n;
032        return init;
033    }
034
035    private boolean isBoolsVar(int varIdx) {
036        return varIdx < bools.length;
037    }
038
039    private boolean isNVar(int varIdx) {
040        return varIdx == bools.length;
041    }
042
043    @Override
044    public int getPropagationConditions(int vIdx) {
045        if (isBoolsVar(vIdx)) {
046            return EventType.INSTANTIATE.mask;
047        }
048        assert isNVar(vIdx);
049        return EventType.DECUPP.mask + EventType.INCLOW.mask + EventType.INSTANTIATE.mask;
050    }
051
052    @Override
053    public void propagate(int evtmask) throws ContradictionException {
054        // Prune n
055        for (int i = n.getLB(); i < n.getUB(); i++) {
056            if (bools[i].instantiated()) {
057                if (bools[i].getValue() == 0) {
058                    n.updateUpperBound(i, aCause);
059                    break;
060                }
061            }
062        }
063        for (int i = n.getUB() - 1; i >= n.getLB(); i--) {
064            if (bools[i].instantiated()) {
065                if (bools[i].getValue() == 1) {
066                    n.updateLowerBound(i + 1, aCause);
067                }
068            }
069        }
070        // Pick bool
071        for (int i = 0; i < n.getLB(); i++) {
072            bools[i].setToTrue(aCause);
073        }
074        for (int i = n.getUB(); i < bools.length; i++) {
075            bools[i].setToFalse(aCause);
076        }
077    }
078
079    @Override
080    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
081        if (isBoolsVar(idxVarInProp)) {
082            assert bools[idxVarInProp].instantiated();
083            if (bools[idxVarInProp].getValue() == 0) {
084                for (int i = idxVarInProp + 1; i < bools.length; i++) {
085                    bools[i].setToFalse(aCause);
086                }
087                if (n.updateUpperBound(idxVarInProp, aCause) && n.getUB() < idxVarInProp) {
088                    for (int i = n.getUB(); i <= idxVarInProp; i++) {
089                        bools[i].setToFalse(aCause);
090                    }
091                }
092            } else {
093                for (int i = 0; i < idxVarInProp; i++) {
094                    bools[i].setToTrue(aCause);
095                }
096                if (n.updateLowerBound(idxVarInProp + 1, aCause) && n.getLB() > idxVarInProp + 1) {
097                    for (int i = idxVarInProp; i < n.getLB(); i++) {
098                        bools[i].setToTrue(aCause);
099                    }
100                }
101            }
102        } else {
103            assert isNVar(idxVarInProp);
104            if (EventType.isInclow(mask) || EventType.isInstantiate(mask)) {
105                for (int i = 0; i < n.getLB(); i++) {
106                    bools[i].setToTrue(aCause);
107                }
108            }
109            if (EventType.isDecupp(mask) || EventType.isInstantiate(mask)) {
110                for (int i = n.getUB(); i < bools.length; i++) {
111                    bools[i].setToFalse(aCause);
112                }
113            }
114        }
115    }
116
117    @Override
118    public ESat isEntailed() {
119        boolean allInstantiated = true;
120        for (int i = 0; i < bools.length; i++) {
121            if (bools[i].instantiated()) {
122                if (bools[i].getValue() == 0 && i < n.getLB()) {
123                    return ESat.FALSE;
124                }
125                if (bools[i].getValue() == 1 && i >= n.getUB()) {
126                    return ESat.FALSE;
127                }
128            } else {
129                allInstantiated = false;
130            }
131        }
132        return allInstantiated && n.instantiated() ? ESat.TRUE : ESat.UNDEFINED;
133    }
134
135    @Override
136    public String toString() {
137        return "selectN(" + Arrays.toString(bools) + ", " + n + ")";
138    }
139}