package org.clafer.choco.constraint.propagator;

import java.util.Arrays;
import org.chocosolver.memory.IStateInt;
import org.chocosolver.memory.IStateIntVector;
import org.chocosolver.solver.constraints.Propagator;
import org.chocosolver.solver.constraints.PropagatorPriority;
import org.chocosolver.solver.exception.ContradictionException;
import org.chocosolver.solver.variables.IntVar;
import org.chocosolver.solver.variables.events.IntEventType;
import org.chocosolver.util.ESat;

/**
 * Enforces no path from one node to another.
 *
 * @author jimmy
 */
public class PropUnreachable extends Propagator<IntVar> {

    private final int from;
    private final int to;
    // The end of the path.
    private final IStateInt position;
    // All the nodes that reach the end node.
    private final IStateIntVector toComponent;

    /**
     * Enforce no path from one node to another. {@code edges[i] = j} implies
     * that there is a directed edge from node i to node j.
     * {@code edges[i] ≥ edges.length} implies that there are no direct edges
     * from node i.
     *
     * @param edges the edges
     * @param from the start node
     * @param to the end node
     */
    public PropUnreachable(IntVar[] edges, int from, int to) {
        super(edges, PropagatorPriority.TERNARY, true);
        if (from < 0 || from >= vars.length) {
            throw new IllegalArgumentException();
        }
        if (to < 0 || to >= vars.length) {
            throw new IllegalArgumentException();
        }
        this.from = from;
        this.to = to;
        this.position = edges[0].getEnvironment().makeInt(from);
        this.toComponent = edges[0].getEnvironment().makeIntVector(1, to);
    }

    @Override
    public int getPropagationConditions(int vIdx) {
        return IntEventType.instantiation();
    }

    @Override
    public void propagate(int evtmask) throws ContradictionException {
        if (from == to) {
            fails();
        }
        vars[from].updateLowerBound(0, this);
        vars[from].removeValue(to, this);
        for (int i = 0; i < vars.length; i++) {
            if (vars[i].isInstantiated() && !isPassive()) {
                follow(i);
            }
        }
    }

    private void remove(IntVar var, IStateIntVector remove) throws ContradictionException {
        int size = remove.size();
        for (int i = 0; i < size; i++) {
            var.removeValue(remove.get(i), this);
        }
    }

    private void follow(int follower) throws ContradictionException {
        assert vars[follower].isInstantiated();
        int leader = vars[follower].getValue();
        if (position.get() == follower) {
            int cur = leader;
            if (cur < 0) {
                fails();
            }
            int i;
            for (i = 0; i < vars.length && cur < vars.length && vars[cur].isInstantiated(); i++) {
                if (toComponent.contains(cur)) {
                    fails();
                }
                cur = vars[cur].getValue();
                if (cur < 0) {
                    fails();
                }
            }
            if (toComponent.contains(cur)) {
                fails();
            }
            if (cur >= vars.length || i == vars.length) {
                setPassive();
            } else {
                vars[cur].updateLowerBound(0, this);
                remove(vars[cur], toComponent);
                position.set(cur);
                if (vars[cur].isInstantiated()) {
                    follow(cur);
                }
            }
        } else if (leader < vars.length && !toComponent.contains(follower) && toComponent.contains(leader)) {
            toComponent.add(follower);
            vars[position.get()].removeValue(follower, this);
            for (int i = 0; i < vars.length; i++) {
                if (vars[i].isInstantiatedTo(follower)) {
                    follow(i);
                }
            }
        }
    }

    @Override
    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
        follow(idxVarInProp);
    }

    @Override
    public ESat isEntailed() {
        // Hopefully escape analysis will make these boolean arrays cheap.
        boolean[] visited = new boolean[vars.length];
        int cur = from;
        while (cur < vars.length && vars[cur].isInstantiated() && !visited[cur]) {
            visited[cur] = true;
            if (cur == to) {
                return ESat.FALSE;
            }
            cur = vars[cur].getValue();
            if (cur < 0) {
                return ESat.FALSE;
            }
        }
        return cur >= vars.length || vars[cur].isInstantiated() ? ESat.TRUE : ESat.UNDEFINED;
    }

    @Override
    public String toString() {
        return "unreachable(from=" + from + ", to=" + to + ", " + Arrays.toString(vars) + ")";
    }
}

@@ -3752,32 +3752,143 @@
 ollower, this);%0A
+            if (vars%5Bposition.get()%5D.isInstantiated()) %7B%0A                follow(position.get());%0A            %7D%0A
             for 
@@ -3906,32 +3906,46 @@
  i %3C vars.length
+ && isActive()
 ; i++) %7B%0A       

Fix unreachable constraint to by idempotent.