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