001package org.clafer.choco.constraint.propagator;
002
003import java.util.Arrays;
004import memory.IStateInt;
005import solver.constraints.Propagator;
006import solver.constraints.PropagatorPriority;
007import solver.exception.ContradictionException;
008import solver.variables.EventType;
009import solver.variables.IntVar;
010import util.ESat;
011
012/**
013 * Enforce no cycles.
014 *
015 * @author jimmy
016 */
017public class PropAcyclic extends Propagator<IntVar> {
018
019    private final IStateInt[] leaders;
020
021    /**
022     * Enforce no cycles. {@code edges[i] = j} implies that there is a directed
023     * edge from node i to node j. {@code edges[i] = edges.length} implies that
024     * there are no direct edges from node i.
025     *
026     * @param edges the edges
027     */
028    public PropAcyclic(IntVar[] edges) {
029        super(edges, PropagatorPriority.TERNARY, true);
030        this.leaders = new IStateInt[edges.length];
031        for (int i = 0; i < this.leaders.length; i++) {
032            this.leaders[i] = environment.makeInt(i);
033        }
034    }
035
036    @Override
037    protected int getPropagationConditions(int vIdx) {
038        return EventType.INSTANTIATE.mask;
039    }
040
041    private int getLeader(int node) {
042        int leader = leaders[node].get();
043        if (leader == node) {
044            return node;
045        }
046        // Find the real leader.
047        int realLeader = getLeader(leader);
048        // Remember the real leader.
049        if (realLeader != leader) {
050            leaders[node].set(realLeader);
051        }
052        return leader;
053    }
054
055    @Override
056    public void propagate(int evtmask) throws ContradictionException {
057        for (int i = 0; i < vars.length; i++) {
058            vars[i].removeValue(i, aCause);
059            vars[i].updateLowerBound(0, aCause);
060            vars[i].updateUpperBound(vars.length, aCause);
061        }
062        for (int i = 0; i < vars.length; i++) {
063            if (vars[i].instantiated()) {
064                follow(i, vars[i].getValue());
065            }
066        }
067    }
068
069    private void follow(int follower, int leader) throws ContradictionException {
070        assert vars[follower].instantiated();
071        if (leader == vars.length) {
072            return;
073        }
074        int realLeader = getLeader(leader);
075        if (realLeader == follower) {
076            contradiction(vars[follower], "Cycle");
077        }
078        boolean changed = false;
079        for (int i = 0; i < vars.length; i++) {
080            if (getLeader(i) == follower) {
081                assert vars[i].instantiated();
082                leaders[i].set(realLeader);
083                changed |= vars[realLeader].removeValue(i, aCause);
084            }
085        }
086        leaders[follower].set(realLeader);
087        if (changed && vars[realLeader].instantiated()) {
088            follow(realLeader, vars[realLeader].getValue());
089        }
090    }
091
092    @Override
093    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
094        follow(idxVarInProp, vars[idxVarInProp].getValue());
095    }
096
097    @Override
098    public ESat isEntailed() {
099        // Hopefully escape analysis will make these boolean arrays cheap.
100        boolean[] visited = new boolean[vars.length];
101        boolean[] localVisited = new boolean[vars.length];
102        boolean allInstantiated = true;
103        for (int i = 0; i < vars.length; i++) {
104            if (visited[i]) {
105                continue;
106            }
107            if (vars[i].instantiated()) {
108                Arrays.fill(localVisited, false);
109                int cur = i;
110                do {
111                    if (localVisited[cur]) {
112                        // Cycle
113                        return ESat.FALSE;
114                    }
115                    visited[cur] = localVisited[cur] = true;
116                    cur = vars[cur].getValue();
117                    if (cur < 0 || cur > vars.length) {
118                        return ESat.FALSE;
119                    }
120                } while (cur != vars.length && vars[cur].instantiated());
121            } else {
122                allInstantiated = false;
123            }
124        }
125        return allInstantiated ? ESat.TRUE : ESat.UNDEFINED;
126    }
127
128    @Override
129    public String toString() {
130        return "acyclic(" + Arrays.toString(vars) + ")";
131    }
132}