001package org.clafer.choco.constraint.propagator;
002
003import org.clafer.common.Util;
004import solver.ICause;
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 * Idempotent version of the one provided by the Choco library.
016 *
017 * @author jimmy
018 */
019public class PropSetUnion extends Propagator<SetVar> {
020
021    private final SetVar[] sets;
022    private final SetDeltaMonitor[] setsD;
023    private final SetVar union;
024    private final SetDeltaMonitor unionD;
025
026    public PropSetUnion(SetVar[] sets, SetVar union) {
027        super(Util.cons(union, sets), PropagatorPriority.LINEAR, true);
028        this.sets = sets;
029        this.setsD = PropUtil.monitorDeltas(sets, aCause);
030        this.union = union;
031        this.unionD = union.monitorDelta(aCause);
032    }
033
034    private boolean isSetVar(int idx) {
035        return idx >= 1;
036    }
037
038    private int getSetVarIndex(int idx) {
039        assert isSetVar(idx);
040        return idx - 1;
041    }
042
043    private boolean isUnionVar(int idx) {
044        return idx == 0;
045    }
046
047    @Override
048    public int getPropagationConditions(int vIdx) {
049        return EventType.ADD_TO_KER.mask + EventType.REMOVE_FROM_ENVELOPE.mask;
050    }
051
052    private void findMate(int unionEnv) throws ContradictionException {
053        boolean inKer = union.kernelContains(unionEnv);
054        int mate = -1;
055        for (int j = 0; j < sets.length; j++) {
056            if (sets[j].envelopeContains(unionEnv)) {
057                // Found a second mate.
058                if (mate != -1 || !inKer) {
059                    mate = -2;
060                    break;
061                }
062                mate = j;
063            }
064        }
065        if (mate == -1) {
066            // No mates.
067            union.removeFromEnvelope(unionEnv, aCause);
068        } else if (mate != -2 && inKer) {
069            // One mate.
070            sets[mate].addToKernel(unionEnv, aCause);
071        }
072    }
073
074    private static boolean isKerSubsetEnvs(SetVar set, SetVar[] envs) {
075        for (int i = set.getKernelFirst(); i != SetVar.END; i = set.getKernelNext()) {
076            if (!PropUtil.envsContain(envs, i)) {
077                return false;
078            }
079        }
080        return true;
081    }
082
083    private static void envSubsetEnvs(SetVar set, SetVar[] envs, ICause propagator) throws ContradictionException {
084        for (int i = set.getEnvelopeFirst(); i != SetVar.END; i = set.getEnvelopeNext()) {
085            if (!PropUtil.envsContain(envs, i)) {
086                set.removeFromEnvelope(i, propagator);
087            }
088        }
089    }
090
091    @Override
092    public void propagate(int evtmask) throws ContradictionException {
093        for (SetVar set : sets) {
094            PropUtil.envSubsetEnv(set, union, aCause);
095            PropUtil.kerSubsetKer(set, union, aCause);
096        }
097        envSubsetEnvs(union, sets, aCause);
098        for (int i = union.getEnvelopeFirst(); i != SetVar.END; i = union.getEnvelopeNext()) {
099            findMate(i);
100        }
101    }
102
103    @Override
104    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
105        if (isSetVar(idxVarInProp)) {
106            int id = getSetVarIndex(idxVarInProp);
107            setsD[id].freeze();
108            setsD[id].forEach(pruneUnionOnSetEnv, EventType.REMOVE_FROM_ENVELOPE);
109            setsD[id].forEach(pickUnionOnSetKer, EventType.ADD_TO_KER);
110            setsD[id].unfreeze();
111        } else {
112            assert isUnionVar(idxVarInProp);
113            unionD.freeze();
114            unionD.forEach(pruneSetOnUnionEnv, EventType.REMOVE_FROM_ENVELOPE);
115            unionD.forEach(pickSetOnUnionKer, EventType.ADD_TO_KER);
116            unionD.unfreeze();
117        }
118    }
119    private final IntProcedure pruneUnionOnSetEnv = new IntProcedure() {
120        @Override
121        public void execute(int setEnv) throws ContradictionException {
122            findMate(setEnv);
123        }
124    };
125    private final IntProcedure pickUnionOnSetKer = new IntProcedure() {
126        @Override
127        public void execute(int setKer) throws ContradictionException {
128            union.addToKernel(setKer, aCause);
129        }
130    };
131    private final IntProcedure pruneSetOnUnionEnv = new IntProcedure() {
132        @Override
133        public void execute(int unionEnv) throws ContradictionException {
134            for (SetVar set : sets) {
135                set.removeFromEnvelope(unionEnv, aCause);
136            }
137        }
138    };
139    private final IntProcedure pickSetOnUnionKer = new IntProcedure() {
140        @Override
141        public void execute(int unionKer) throws ContradictionException {
142            findMate(unionKer);
143        }
144    };
145
146    @Override
147    public ESat isEntailed() {
148        boolean allInstantiated = true;
149        for (SetVar set : sets) {
150            if (!PropUtil.isKerSubsetEnv(set, union)) {
151                return ESat.FALSE;
152            }
153            allInstantiated = allInstantiated && set.instantiated();
154        }
155        if (!isKerSubsetEnvs(union, sets)) {
156            return ESat.FALSE;
157        }
158        allInstantiated = allInstantiated && union.instantiated();
159        return allInstantiated ? ESat.TRUE : ESat.UNDEFINED;
160    }
161
162    @Override
163    public String toString() {
164        return Util.intercalate(" ∪ ", sets) + " = " + union;
165    }
166}