package org.clafer.choco.constraint.propagator;

import java.util.Arrays;
import org.clafer.common.Util;
import solver.constraints.Propagator;
import solver.constraints.PropagatorPriority;
import solver.exception.ContradictionException;
import solver.variables.IntVar;
import solver.variables.events.IntEventType;
import util.ESat;

/**
 *
 * @author jimmy
 */
public class PropLength extends Propagator<IntVar> {

    private final IntVar[] chars;

    private final IntVar length;

    public PropLength(IntVar[] chars, IntVar length) {
        super(Util.cons(length, chars), PropagatorPriority.LINEAR, true);
        this.chars = chars;
        this.length = length;
    }

    private boolean isLengthVar(int idx) {
        return idx == 0;
    }

    private boolean isCharVar(int idx) {
        return idx > 0;
    }

    private int getCharVarIndex(int idx) {
        return idx - 1;
    }

    @Override
    protected int getPropagationConditions(int vIdx) {
        if (isLengthVar(vIdx)) {
            return IntEventType.boundAndInst();
        }
        assert isCharVar(vIdx);
        return IntEventType.all();
    }

    @Override
    public void propagate(int evtmask) throws ContradictionException {
        length.updateLowerBound(0, aCause);
        length.updateUpperBound(chars.length, aCause);
        for (int i = chars.length - 1; i >= 0; i--) {
            onCharRemove(i);
        }
        for (int i = 0; i < chars.length; i++) {
            onCharInstantiate(i);
        }
        onLengthLB();
        onLengthUB();
    }

    @Override
    public void propagate(int idxVarInProp, int mask) throws ContradictionException {
        if (isLengthVar(idxVarInProp)) {
            if (IntEventType.isInclow(mask)) {
                onLengthLB();
            }
            if (IntEventType.isDecupp(mask)) {
                onLengthUB();
            }
        } else {
            assert isCharVar(idxVarInProp);
            int id = getCharVarIndex(idxVarInProp);
            if (onCharRemove(id)) {
                onLengthLB();
            }
            if (onCharInstantiate(id)) {
                onLengthUB();
            }
        }
    }

    private void onLengthLB() throws ContradictionException {
        for (int i = 0; i < length.getLB(); i++) {
            chars[i].removeValue(0, aCause);
        }
    }

    private void onLengthUB() throws ContradictionException {
        for (int i = length.getUB(); i < chars.length; i++) {
            chars[i].instantiateTo(0, aCause);
        }
    }

    private boolean onCharRemove(int i) throws ContradictionException {
        return !chars[i].contains(0)
                && length.updateLowerBound(i + 1, aCause);
    }

    private boolean onCharInstantiate(int i) throws ContradictionException {
        return chars[i].isInstantiatedTo(0)
                && length.updateUpperBound(i, aCause);
    }

    @Override
    public ESat isEntailed() {
        if (length.getLB() > chars.length || length.getUB() < 0) {
            return ESat.FALSE;
        }
        for (int i = 0; i < length.getLB(); i++) {
            if (chars[i].isInstantiatedTo(0)) {
                return ESat.FALSE;
            }
        }
        for (int i = length.getUB(); i < chars.length; i++) {
            if (!chars[i].contains(0)) {
                return ESat.FALSE;
            }
        }
        return isCompletelyInstantiated() ? ESat.TRUE : ESat.UNDEFINED;
    }

    @Override
    public String toString() {
        return "length(" + Arrays.toString(chars) + ", " + length + ")";
    }
}

@@ -442,17 +442,16 @@
  chars;%0A
-%0A
     priv
@@ -474,16 +474,50 @@
  length;
+%0A    private final int terminator;
 %0A%0A    pu
@@ -561,24 +561,134 @@
 r length) %7B%0A
+        this(chars, length, 0);%0A    %7D%0A%0A    public PropLength(IntVar%5B%5D chars, IntVar length, int terminator) %7B%0A
         supe
@@ -773,24 +773,24 @@
 rs = chars;%0A
-
         this
@@ -803,24 +803,62 @@
 h = length;%0A
+        this.terminator = terminator;%0A
     %7D%0A%0A    p
@@ -2492,17 +2492,26 @@
 veValue(
-0
+terminator
 , aCause
@@ -2689,17 +2689,26 @@
 tiateTo(
-0
+terminator
 , aCause
@@ -2833,17 +2833,26 @@
 ontains(
-0
+terminator
 )%0A      
@@ -3029,17 +3029,26 @@
 iatedTo(
-0
+terminator
 )%0A      
@@ -3349,17 +3349,26 @@
 iatedTo(
-0
+terminator
 )) %7B%0A   
@@ -3520,17 +3520,26 @@
 ontains(
-0
+terminator
 )) %7B%0A   

Generalize length constraint to use any constant terminator.