001package org.clafer.choco.constraint.propagator;
002
003import solver.constraints.Propagator;
004import solver.constraints.PropagatorPriority;
005import solver.exception.ContradictionException;
006import solver.variables.EventType;
007import solver.variables.SetVar;
008import solver.variables.delta.monitor.SetDeltaMonitor;
009import util.ESat;
010import util.procedure.IntProcedure;
011
012/**
013 * More efficient than the provided PropAllDiff. Idempotent unlike the
014 * PropAllDiff.
015 *
016 * @author jimmy
017 */
018public class PropSetNotEqual extends Propagator<SetVar> {
019
020    private final SetVar s1, s2;
021    private SetDeltaMonitor s1D, s2D;
022
023    public PropSetNotEqual(SetVar s1, SetVar s2) {
024        super(new SetVar[]{s1, s2}, PropagatorPriority.LINEAR, true);
025        this.s1 = s1;
026        this.s1D = s1.monitorDelta(aCause);
027        this.s2 = s2;
028        this.s2D = s2.monitorDelta(aCause);
029    }
030
031    private boolean isS1Var(int idx) {
032        return idx == 0;
033    }
034
035    private boolean isS2Var(int idx) {
036        return idx == 1;
037    }
038
039    @Override
040    public int getPropagationConditions(int vIdx) {
041        return EventType.ADD_TO_KER.mask + EventType.REMOVE_FROM_ENVELOPE.mask;
042    }
043
044    private void checkNotSame() throws ContradictionException {
045        if (s1.instantiated() && s2.instantiated()) {
046            if (s1.getKernelSize() == s2.getKernelSize()) {
047                int i = s1.getKernelFirst();
048                int j = s2.getKernelFirst();
049                while (i != SetVar.END) {
050                    assert j != SetVar.END;
051                    if (i != j) {
052                        return;
053                    }
054                    i = s1.getKernelNext();
055                    j = s2.getKernelNext();
056                }
057                assert j == SetVar.END;
058                contradiction(s1, "Same");
059            }
060        }
061    }
062
063    @Override
064    public void propagate(int evtmask) throws ContradictionException {
065        for (int i = s1.getKernelFirst(); i != SetVar.END; i = s1.getKernelNext()) {
066            if (!s2.envelopeContains(i)) {
067                setPassive();
068                return;
069            }
070        }
071        for (int i = s2.getKernelFirst(); i != SetVar.END; i = s2.getKernelNext()) {
072            if (!s1.envelopeContains(i)) {
073                setPassive();
074                return;
075            }
076        }
077        checkNotSame();
078    }
079
080    @Override
081    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
082        if (isS1Var(idxVarInProp)) {
083            s1D.freeze();
084            s1D.forEach(onS1Env, EventType.REMOVE_FROM_ENVELOPE);
085            s1D.forEach(onS1Ker, EventType.ADD_TO_KER);
086            s1D.unfreeze();
087        } else {
088            assert isS2Var(idxVarInProp);
089            s2D.freeze();
090            s2D.forEach(onS2Env, EventType.REMOVE_FROM_ENVELOPE);
091            s2D.forEach(onS2Ker, EventType.ADD_TO_KER);
092            s2D.unfreeze();
093        }
094        checkNotSame();
095    }
096    private final IntProcedure onS1Env = new IntProcedure() {
097        @Override
098        public void execute(int s1Env) throws ContradictionException {
099            if (isActive() && s2.kernelContains(s1Env)) {
100                setPassive();
101            }
102        }
103    };
104    private final IntProcedure onS1Ker = new IntProcedure() {
105        @Override
106        public void execute(int s1Ker) throws ContradictionException {
107            if (isActive() && !s2.envelopeContains(s1Ker)) {
108                setPassive();
109            }
110        }
111    };
112    private final IntProcedure onS2Env = new IntProcedure() {
113        @Override
114        public void execute(int s2Env) throws ContradictionException {
115            if (isActive() && s1.kernelContains(s2Env)) {
116                setPassive();
117            }
118        }
119    };
120    private final IntProcedure onS2Ker = new IntProcedure() {
121        @Override
122        public void execute(int s2Ker) throws ContradictionException {
123            if (isActive() && !s1.envelopeContains(s2Ker)) {
124                setPassive();
125            }
126        }
127    };
128
129    @Override
130    public ESat isEntailed() {
131        if (!PropUtil.isKerSubsetEnv(s1, s2) || !PropUtil.isKerSubsetEnv(s2, s1)) {
132            return ESat.TRUE;
133        }
134        return s1.instantiated() && s2.instantiated() ? ESat.FALSE : ESat.UNDEFINED;
135    }
136
137    @Override
138    public String toString() {
139        return s1 + " != " + s2;
140    }
141}