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.SetVar;
010import solver.variables.delta.monitor.SetDeltaMonitor;
011import util.ESat;
012import util.procedure.IntProcedure;
013
014/**
015 *
016 * @author jimmy
017 */
018public class PropSetNotEqualC extends Propagator<SetVar> {
019
020    private final SetVar s;
021    private SetDeltaMonitor sD;
022    private final int[] c;
023
024    public PropSetNotEqualC(SetVar s, int[] c) {
025        super(new SetVar[]{s}, PropagatorPriority.LINEAR, true);
026        this.s = s;
027        this.sD = s.monitorDelta(aCause);
028        this.c = c;
029    }
030
031    @Override
032    public int getPropagationConditions(int vIdx) {
033        return EventType.ADD_TO_KER.mask + EventType.REMOVE_FROM_ENVELOPE.mask;
034    }
035
036    private void checkNotSame() throws ContradictionException {
037        if (s.instantiated()) {
038            if (s.getKernelSize() == c.length) {
039                int i = s.getKernelFirst();
040                int j = 0;
041                while (i != SetVar.END) {
042                    if (i != c[j]) {
043                        return;
044                    }
045                    i = s.getKernelNext();
046                    j++;
047                }
048                assert j == c.length;
049                contradiction(s, "Same");
050            }
051        }
052    }
053
054    @Override
055    public void propagate(int evtmask) throws ContradictionException {
056        for (int i = s.getKernelFirst(); i != SetVar.END; i = s.getKernelNext()) {
057            if (!Util.in(i, c)) {
058                setPassive();
059                return;
060            }
061        }
062        for (int i : c) {
063            if (!s.envelopeContains(i)) {
064                setPassive();
065                return;
066            }
067        }
068        checkNotSame();
069    }
070
071    @Override
072    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
073        sD.freeze();
074        sD.forEach(onS1Env, EventType.REMOVE_FROM_ENVELOPE);
075        sD.forEach(onS1Ker, EventType.ADD_TO_KER);
076        sD.unfreeze();
077        checkNotSame();
078    }
079    private final IntProcedure onS1Env = new IntProcedure() {
080        @Override
081        public void execute(int s1Env) throws ContradictionException {
082            if (isActive() && Util.in(s1Env, c)) {
083                setPassive();
084            }
085        }
086    };
087    private final IntProcedure onS1Ker = new IntProcedure() {
088        @Override
089        public void execute(int s1Ker) throws ContradictionException {
090            if (isActive() && !Util.in(s1Ker, c)) {
091                setPassive();
092            }
093        }
094    };
095
096    private static boolean isEnvSubsetOf(SetVar s, int[] c) {
097        for (int i = s.getKernelFirst(); i != SetVar.END; i = s.getKernelNext()) {
098            if (!Util.in(i, c)) {
099                return false;
100            }
101        }
102        return true;
103    }
104
105    private static boolean isSubsetEnv(int[] c, SetVar s) {
106        for (int i : c) {
107            if (!s.envelopeContains(i)) {
108                return false;
109            }
110        }
111        return true;
112    }
113
114    @Override
115    public ESat isEntailed() {
116        if (!isEnvSubsetOf(s, c) || !isSubsetEnv(c, s)) {
117            return ESat.TRUE;
118        }
119        return s.instantiated() ? ESat.FALSE : ESat.UNDEFINED;
120    }
121
122    @Override
123    public String toString() {
124        return s + " != " + Arrays.toString(c);
125    }
126}