001package org.clafer.choco.constraint.propagator;
002
003import solver.constraints.Propagator;
004import solver.constraints.PropagatorPriority;
005import solver.exception.ContradictionException;
006import solver.variables.BoolVar;
007import solver.variables.EventType;
008import solver.variables.IntVar;
009import util.ESat;
010
011/**
012 * (reify = reifyC) <=> (x = c)
013 *
014 * @author jimmy
015 */
016public class PropReifyEqualXC extends Propagator<IntVar> {
017
018    private final BoolVar reify;
019    private final int reifyC;
020    private final IntVar x;
021    private final int c;
022
023    public PropReifyEqualXC(BoolVar reify, boolean reifyC, IntVar x, int c) {
024        super(new IntVar[]{reify, x}, PropagatorPriority.UNARY, true);
025        this.reify = reify;
026        this.reifyC = reifyC ? 1 : 0;
027        this.x = x;
028        this.c = c;
029    }
030
031    private boolean isReifyVar(int idx) {
032        return idx == 0;
033    }
034
035    private boolean isXVar(int idx) {
036        return idx == 1;
037    }
038
039    @Override
040    public int getPropagationConditions(int vIdx) {
041        return EventType.INT_ALL_MASK();
042    }
043
044    private void propagateReifyVar() throws ContradictionException {
045        assert reify.instantiated();
046        if (reify.getValue() == reifyC) {
047            x.instantiateTo(c, aCause);
048        } else {
049            x.removeValue(c, aCause);
050        }
051        setPassive();
052    }
053
054    private void propagateXVar() throws ContradictionException {
055        if (x.contains(c)) {
056            if (x.instantiated()) {
057                reify.instantiateTo(reifyC, aCause);
058                setPassive();
059            }
060        } else {
061            reify.instantiateTo(1 - reifyC, aCause);
062            setPassive();
063        }
064    }
065
066    @Override
067    public void propagate(int evtmask) throws ContradictionException {
068        if (reify.instantiated()) {
069            propagateReifyVar();
070        } else {
071            propagateXVar();
072        }
073    }
074
075    @Override
076    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
077        if (isReifyVar(idxVarInProp)) {
078            propagateReifyVar();
079        } else {
080            assert isXVar(idxVarInProp);
081            propagateXVar();
082        }
083    }
084
085    @Override
086    public ESat isEntailed() {
087        if (reify.instantiated()) {
088            if (!x.contains(c)) {
089                return reify.getValue() == reifyC ? ESat.FALSE : ESat.TRUE;
090            }
091            if (x.instantiated()) {
092                return reify.getValue() == reifyC ? ESat.TRUE : ESat.FALSE;
093            }
094        }
095        return ESat.UNDEFINED;
096    }
097
098    @Override
099    public String toString() {
100        return (reifyC == 1 ? reify : "!" + reify) + " <=> (" + x + " = " + c + ")";
101    }
102}