001package org.clafer.choco.constraint.propagator;
002
003import org.clafer.common.Check;
004import solver.constraints.Propagator;
005import solver.constraints.PropagatorPriority;
006import solver.exception.ContradictionException;
007import solver.variables.EventType;
008import solver.variables.SetVar;
009import solver.variables.delta.monitor.SetDeltaMonitor;
010import util.ESat;
011import util.procedure.IntProcedure;
012
013/**
014 *
015 * @author jimmy
016 */
017public class PropSetDifference extends Propagator<SetVar> {
018
019    private final SetVar minuend, subtrahend, difference;
020    private final SetDeltaMonitor minuendD, subtrahendD, differenceD;
021
022    public PropSetDifference(SetVar minuend, SetVar subtrahend, SetVar difference) {
023        super(new SetVar[]{minuend, subtrahend, difference}, PropagatorPriority.LINEAR, true);
024        this.minuend = Check.notNull(minuend);
025        this.subtrahend = Check.notNull(subtrahend);
026        this.difference = Check.notNull(difference);
027        this.minuendD = minuend.monitorDelta(aCause);
028        this.subtrahendD = subtrahend.monitorDelta(aCause);
029        this.differenceD = difference.monitorDelta(aCause);
030    }
031
032    @Override
033    public int getPropagationConditions(int vIdx) {
034        return EventType.ADD_TO_KER.mask + EventType.REMOVE_FROM_ENVELOPE.mask;
035    }
036
037    @Override
038    public void propagate(int evtmask) throws ContradictionException {
039        for (int i = minuend.getEnvelopeFirst(); i != SetVar.END; i = minuend.getEnvelopeNext()) {
040            if (!subtrahend.envelopeContains(i) && !minuend.envelopeContains(i)) {
041                minuend.removeFromEnvelope(i, aCause);
042            }
043        }
044        for (int i = difference.getKernelFirst(); i != SetVar.END; i = difference.getKernelNext()) {
045            minuend.addToKernel(i, aCause);
046            subtrahend.removeFromEnvelope(i, aCause);
047        }
048
049        PropUtil.envSubsetEnv(difference, minuend, aCause);
050        for (int i = subtrahend.getKernelFirst(); i != SetVar.END; i = subtrahend.getKernelNext()) {
051            difference.removeFromEnvelope(i, aCause);
052        }
053        for (int i = minuend.getKernelFirst(); i != SetVar.END; i = minuend.getKernelNext()) {
054            if (!subtrahend.envelopeContains(i)) {
055                difference.addToKernel(i, aCause);
056            }
057        }
058    }
059
060    @Override
061    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
062        switch (idxVarInProp) {
063            case 0:
064                // minuend
065                minuendD.freeze();
066                minuendD.forEach(pruneDifferenceOnMinuendEnv, EventType.REMOVE_FROM_ENVELOPE);
067                minuendD.forEach(pickDifferenceOnMinuendKer, EventType.ADD_TO_KER);
068                minuendD.unfreeze();
069                break;
070            case 1:
071                // subtrahend
072                subtrahendD.freeze();
073                subtrahendD.forEach(pickMinuendPickDiffrenceOnSubtrahendEnv, EventType.REMOVE_FROM_ENVELOPE);
074                subtrahendD.forEach(pruneDifferenceOnSubtrahendKer, EventType.ADD_TO_KER);
075                subtrahendD.unfreeze();
076                break;
077            case 2:
078                // difference
079                differenceD.freeze();
080                differenceD.forEach(pruneMinuendOnDifferenceEnv, EventType.REMOVE_FROM_ENVELOPE);
081                differenceD.forEach(pickMinuendPruneSubtrahendOnDifferenceKer, EventType.ADD_TO_KER);
082                differenceD.unfreeze();
083                break;
084        }
085    }
086    private final IntProcedure pruneDifferenceOnMinuendEnv = new IntProcedure() {
087        @Override
088        public void execute(int minuendEnv) throws ContradictionException {
089            difference.removeFromEnvelope(minuendEnv, aCause);
090        }
091    };
092    private final IntProcedure pickDifferenceOnMinuendKer = new IntProcedure() {
093        @Override
094        public void execute(int minuendKer) throws ContradictionException {
095            if (!subtrahend.envelopeContains(minuendKer)) {
096                difference.addToKernel(minuendKer, aCause);
097            }
098        }
099    };
100    private final IntProcedure pickMinuendPickDiffrenceOnSubtrahendEnv = new IntProcedure() {
101        @Override
102        public void execute(int subtrahendEnv) throws ContradictionException {
103            if (minuend.kernelContains(subtrahendEnv)) {
104                difference.addToKernel(subtrahendEnv, aCause);
105            } else if (difference.kernelContains(subtrahendEnv)) {
106                minuend.addToKernel(subtrahendEnv, aCause);
107            }
108        }
109    };
110    private final IntProcedure pruneDifferenceOnSubtrahendKer = new IntProcedure() {
111        @Override
112        public void execute(int subtrahendKer) throws ContradictionException {
113            difference.removeFromEnvelope(subtrahendKer, aCause);
114        }
115    };
116    private final IntProcedure pruneMinuendOnDifferenceEnv = new IntProcedure() {
117        @Override
118        public void execute(int differenceEnv) throws ContradictionException {
119            if (!subtrahend.envelopeContains(differenceEnv)) {
120                minuend.removeFromEnvelope(differenceEnv, aCause);
121            }
122        }
123    };
124    private final IntProcedure pickMinuendPruneSubtrahendOnDifferenceKer = new IntProcedure() {
125        @Override
126        public void execute(int differenceKer) throws ContradictionException {
127            minuend.addToKernel(differenceKer, aCause);
128            subtrahend.removeFromEnvelope(differenceKer, aCause);
129        }
130    };
131
132    @Override
133    public ESat isEntailed() {
134        for (int i = minuend.getKernelFirst(); i != SetVar.END; i = minuend.getKernelNext()) {
135            if (!subtrahend.envelopeContains(i) && !difference.envelopeContains(i)) {
136                return ESat.FALSE;
137            }
138        }
139        for (int i = difference.getKernelFirst(); i != SetVar.END; i = difference.getKernelNext()) {
140            if (!minuend.envelopeContains(i) || subtrahend.kernelContains(i)) {
141                return ESat.FALSE;
142            }
143        }
144        return isCompletelyInstantiated() ? ESat.TRUE : ESat.UNDEFINED;
145    }
146
147    @Override
148    public String toString() {
149        return minuend + " - " + subtrahend + " = " + difference;
150    }
151}