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 solver.variables.delta.IIntDeltaMonitor;
010import util.ESat;
011import util.procedure.IntProcedure;
012
013/**
014 * (reify = reifyC) <=> (x = y)
015 *
016 * @author jimmy
017 */
018public class PropReifyEqualXY extends Propagator<IntVar> {
019
020    private final BoolVar reify;
021    private final int reifyC;
022    private final IntVar x, y;
023    private final IIntDeltaMonitor xD, yD;
024
025    public PropReifyEqualXY(BoolVar reify, boolean reifyC, IntVar x, IntVar y) {
026        super(new IntVar[]{reify, x, y}, PropagatorPriority.BINARY, true);
027        this.reify = reify;
028        this.reifyC = reifyC ? 1 : 0;
029        this.x = x;
030        this.xD = x.monitorDelta(aCause);
031        this.y = y;
032        this.yD = y.monitorDelta(aCause);
033    }
034
035    private boolean isReifyVar(int idx) {
036        return idx == 0;
037    }
038
039    private boolean isXVar(int idx) {
040        return idx == 1;
041    }
042
043    private boolean isYVar(int idx) {
044        return idx == 2;
045    }
046
047    @Override
048    public int getPropagationConditions(int vIdx) {
049        return EventType.INT_ALL_MASK();
050    }
051    private final IntProcedure pruneXOnYRem = new IntProcedure() {
052        @Override
053        public void execute(int i) throws ContradictionException {
054            x.removeValue(i, aCause);
055        }
056    };
057    private final IntProcedure pruneYOnXRem = new IntProcedure() {
058        @Override
059        public void execute(int i) throws ContradictionException {
060            y.removeValue(i, aCause);
061        }
062    };
063
064    private void propagateReifyVar() throws ContradictionException {
065        assert reify.instantiated();
066        if (reify.getValue() == reifyC) {
067            PropUtil.domSubsetDom(x, y, aCause);
068            PropUtil.domSubsetDom(y, x, aCause);
069            if (x.instantiated()) {
070                assert y.instantiated();
071                setPassive();
072            }
073        } else {
074            if (x.instantiated()) {
075                y.removeValue(x.getValue(), aCause);
076                setPassive();
077            } else if (y.instantiated()) {
078                x.removeValue(y.getValue(), aCause);
079                setPassive();
080            }
081        }
082    }
083
084    private void propagateXVar() throws ContradictionException {
085        if (x.instantiated()) {
086            if (reify.instantiated()) {
087                if (reify.getValue() == reifyC) {
088                    y.instantiateTo(x.getValue(), aCause);
089                } else {
090                    y.removeValue(x.getValue(), aCause);
091                }
092                setPassive();
093            } else if (y.contains(x.getValue())) {
094                if (y.instantiated()) {
095                    reify.instantiateTo(reifyC, aCause);
096                    setPassive();
097                }
098            } else {
099                reify.instantiateTo(1 - reifyC, aCause);
100                setPassive();
101            }
102        } else if (reify.instantiatedTo(reifyC)) {
103            xD.freeze();
104            xD.forEach(pruneYOnXRem, EventType.REMOVE);
105            xD.unfreeze();
106        }
107    }
108
109    private void propagateYVar() throws ContradictionException {
110        if (y.instantiated()) {
111            if (reify.instantiated()) {
112                if (reify.getValue() == reifyC) {
113                    x.instantiateTo(y.getValue(), aCause);
114                } else {
115                    x.removeValue(y.getValue(), aCause);
116                }
117                setPassive();
118            } else if (x.contains(y.getValue())) {
119                if (x.instantiated()) {
120                    reify.instantiateTo(reifyC, aCause);
121                    setPassive();
122                }
123            } else {
124                reify.instantiateTo(1 - reifyC, aCause);
125                setPassive();
126            }
127        } else if (reify.instantiatedTo(reifyC)) {
128            yD.freeze();
129            yD.forEach(pruneXOnYRem, EventType.REMOVE);
130            yD.unfreeze();
131        }
132    }
133
134    private void propagateXYVar() throws ContradictionException {
135        if (!PropUtil.isDomIntersectDom(x, y)) {
136            reify.instantiateTo(1 - reifyC, aCause);
137            setPassive();
138        }
139    }
140
141    @Override
142    public void propagate(int evtmask) throws ContradictionException {
143        if (reify.instantiated()) {
144            propagateReifyVar();
145        } else {
146            propagateXVar();
147            if (!isPassive()) {
148                propagateYVar();
149            }
150            if (!isPassive()) {
151                propagateXYVar();
152            }
153        }
154    }
155
156    @Override
157    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
158        if (isReifyVar(idxVarInProp)) {
159            propagateReifyVar();
160        } else if (isXVar(idxVarInProp)) {
161            propagateXVar();
162            if (!isPassive()) {
163                propagateXYVar();
164            }
165        } else {
166            assert isYVar(idxVarInProp);
167            propagateYVar();
168            if (!isPassive()) {
169                propagateXYVar();
170            }
171        }
172    }
173
174    @Override
175    public ESat isEntailed() {
176        if (reify.instantiated()) {
177            if (!PropUtil.isDomIntersectDom(x, y)) {
178                return reify.getValue() == reifyC ? ESat.FALSE : ESat.TRUE;
179            }
180            if (x.instantiated() && y.instantiated()) {
181                return reify.getValue() == reifyC ? ESat.TRUE : ESat.FALSE;
182            }
183        }
184        return ESat.UNDEFINED;
185    }
186
187    @Override
188    public String toString() {
189        return (reifyC == 1 ? reify : "!" + reify) + " <=> (" + x + " = " + y + ")";
190    }
191}