import choco.ContradictionException;
import choco.integer.IntDomainVar;
import choco.integer.IntVar;
import choco.integer.constraints.AbstractLargeIntConstraint;
import choco.mem.StoredBitSet;
import choco.mem.StoredInt;

/**
 * <code>LeximinConstraint</code> is a constraint that ensures
 * the leximin ordering over two vectors.
 *
 * @author <a href="mailto:sylvain.bouveret@cert.fr">Sylvain Bouveret</a>
 * @version 1.0
 */

public class LeximinConstraint extends AbstractLargeIntConstraint {

    private StoredInt alpha, beta;
    private StoredInt gamma, delta;
    private StoredBitSet epsilon;
    /*
      epsilon is a set of additional flags useful for the gac() algorithm :
      - epsilon[0] = true iff occx[alpha] = occy[alpha] - 1
      - epsilon[1] = true iff occx[alpha] = occy[alpha] + 1
      - epsilon[2] = true iff occx[beta] = occy[beta] - 1
      - epsilon[3] = true iff occx[beta] = occy[beta] + 1
    */
    //private StoredInt[] occx, occy;
    private StoredInt[] floorx, ceily;
    private StoredInt[] sortedFloorx, sortedCeily;
    private int maximum;
    private int minimum;
    private int n;

    public boolean verbose = false;

    /**
     * Creates a new <code>LeximinConstraint</code> instance.
     *
     * @param x the first array of integer variables
     * @param y the second array of integer variables
     */
    public LeximinConstraint (IntVar[] x, IntVar[] y) {
	super(LeximinConstraint.mergeIntVarArrays(x, y));
	if (x.length != y.length || x.length == 0 || y.length == 0) {
	    throw new Error("LeximinConstraint Error: the two vectors "
			    +"must be of the same (non zero) size");
	}
	this.n = x.length;

	super.problem = x[0].getProblem();

	this.alpha = new StoredInt(super.problem.getEnvironment());
	this.beta = new StoredInt(super.problem.getEnvironment());
	this.gamma = new StoredInt(super.problem.getEnvironment());
	this.delta = new StoredInt(super.problem.getEnvironment());
	this.epsilon = new StoredBitSet(super.problem.getEnvironment(), 4);

	this.generateVectors();
    }

    /**
     * A utility class that merges two <code>IntVar</code>
     * arrays into an <code>IntDomainVar</code> one.
     *
     * @param firstArray an <code>IntVar</code> array
     * @param secondArray an <code>IntVar</code> array
     * @return the <code>IntDomainVar</code> array built from the parameters
     */
    private static IntDomainVar[] mergeIntVarArrays (IntVar[] firstArray, IntVar[] secondArray) {
	IntDomainVar[] newArray = new IntDomainVar[firstArray.length + secondArray.length];
	for (int i = 0; i < firstArray.length; i++)
	    newArray[i] = (IntDomainVar) firstArray[i];
	for (int i = 0; i < secondArray.length; i++)
	    newArray[i + firstArray.length] = (IntDomainVar) secondArray[i];
	return (newArray);
    }

    /**
     * This methods builds the vectors used by the gac algorithm.
     *
     */
    private void generateVectors() {
	this.floorx = new StoredInt[n];
	this.ceily = new StoredInt[n];
	this.sortedFloorx = new StoredInt[n];
	this.sortedCeily = new StoredInt[n];
	int minimumX = Integer.MAX_VALUE;
	int minimumY = Integer.MAX_VALUE;
	int maximumX = 0;
	int maximumY = 0;
	for (int i = 0; i < n; i++) {
	    this.sortedFloorx[i] = new StoredInt(this.problem.getEnvironment(), super.vars[i].getInf());
	    this.floorx[i] = new StoredInt(this.problem.getEnvironment(), super.vars[i].getInf());
	    minimumX = minimumX > this.sortedFloorx[i].get() ? this.sortedFloorx[i].get() : minimumX;
	    maximumX = maximumX < this.sortedFloorx[i].get() ? this.sortedFloorx[i].get() : maximumX;
	    this.sortedCeily[i] = new StoredInt(this.problem.getEnvironment(), super.vars[n + i].getSup());
	    this.ceily[i] = new StoredInt(this.problem.getEnvironment(), super.vars[n + i].getSup());
	    minimumY = minimumY > this.sortedCeily[i].get() ? this.sortedCeily[i].get() : minimumY;
	    maximumY = maximumY < this.sortedCeily[i].get() ? this.sortedCeily[i].get() : maximumY;
	}
	this.minimum = minimumX < minimumY ? minimumX : minimumY;
	this.maximum = maximumX > maximumY ? maximumX : maximumY;

	java.util.Arrays.sort(this.sortedFloorx, this.new SIComparator());
	java.util.Arrays.sort(this.sortedCeily, this.new SIComparator());
    }

    /**
     * This methods updates the vectors used by the gac algorithm.
     *
     */
    private void updateVectors(int idx) {
	int oldValue, newValue, i;
	if (idx < this.n) {
	    oldValue = this.floorx[idx].get();
	    newValue = super.vars[idx].getInf();
	    this.floorx[idx].set(newValue);
	    for (i = 0; this.sortedFloorx[i].get() < oldValue; i++);
	    int j;
	    for (j = i + 1; (j < this.n) && (this.sortedFloorx[j].get() < newValue); j++) {
		this.sortedFloorx[j - 1].set(this.sortedFloorx[j].get());
	    }
	    this.sortedFloorx[j - 1].set(newValue);
	}
	else {
	    oldValue = this.ceily[idx - n].get();
	    newValue = super.vars[idx].getSup();
	    this.ceily[idx - n].set(newValue);
	    for (i = this.n - 1; this.sortedCeily[i].get() > oldValue; i--);
	    int j;
	    for (j = i - 1; (j >= 0) && (this.sortedCeily[j].get() > newValue); j--) {
		this.sortedCeily[j + 1].set(this.sortedCeily[j].get());
	    }
	    this.sortedCeily[j + 1].set(newValue);
	}
    }

    /**
     * The <code>setPointersAndFlags</code> method sets the values
     * &alpha;, &beta;, &gamma; and &delta;, used by the algorithm.
     *
     * @param l the minimum value of all the variables
     * @param u the maximum value of all the variables
     * @exception ContradictionException if the problem instance is inconsistant
     */
    public void setPointersAndFlags() throws ContradictionException {
	int l = this.minimum;
	int u = this.maximum;
	int currentX = 0;
	int currentY = 0;
	int currentOccX = 0;
	int currentOccY = 0;
	this.gamma.set(0);
	this.delta.set(0);
	this.alpha.set(l-1);
	for (int i = 0; i < 4; i++) {
	    this.epsilon.set(i, false);
	}
	if (verbose) {
	    System.out.println("l = " + l + " / u = " + u);
	}
	while (this.alpha.get() <= u && currentOccX == currentOccY) {
	    this.alpha.set(this.alpha.get() + 1); // Increase alpha by one.
	    currentOccX = 0;
	    while (currentX < this.sortedFloorx.length && this.sortedFloorx[currentX].get() == this.alpha.get()) {
		currentOccX++;
		currentX++;
	    } // Read sortedFloorx array in order to compute occX
	    currentOccY = 0;
	    while (currentY < this.sortedCeily.length && this.sortedCeily[currentY].get() == this.alpha.get()) {
		currentOccY++;
		currentY++;
	    } // Read sortedCeily array in order to compute occY
	    if (verbose) {
		System.out.println("cX = " + currentX + " / cOX = " + currentOccX);
		System.out.println("cY = " + currentY + " / cOY = " + currentOccY);
	    }
	}

	if (this.alpha.get() <= u && currentOccX < currentOccY) {
	    throw new ContradictionException(super.problem);
	}
	if (this.alpha.get() == u + 1) {
	    //this.alpha.set(Integer.MAX_VALUE);
	    //this.beta.set(Integer.MAX_VALUE);
	    throw new ContradictionException(super.problem); // For ensuring strict inequality
	}
	else {
	    if (currentOccX == currentOccY - 1) {
		this.epsilon.set(0, true);
	    }
	    if (currentOccX == currentOccY + 1) {
		this.epsilon.set(1, true);
	    }
	    this.beta.set(this.alpha.get());
	    this.gamma.set(1);
	    currentOccX = 0;
	    currentOccY = 0;
	    while (this.beta.get() <= u && currentOccX >= currentOccY) {
		if (currentOccX > currentOccY) {
		    this.gamma.set(0);
		}
		this.beta.set(this.beta.get() + 1);
		currentOccX = 0;
		while (currentX < this.sortedFloorx.length && this.sortedFloorx[currentX].get() == this.beta.get()) {
		    currentOccX++;
		    currentX++;
		} // Read sortedFloorx array in order to compute occX
		currentOccY = 0;
		while (currentY < this.sortedCeily.length && this.sortedCeily[currentY].get() == this.beta.get()) {
		    currentOccY++;
		    currentY++;
		} // Read sortedCeily array in order to compute occY
	    }
	    if (this.beta.get() == u + 1) {
		this.beta.set(Integer.MAX_VALUE);
		this.gamma.set(0);
	    }
	    if (currentOccX == currentOccY - 1) {
		this.epsilon.set(2, true);
	    }
	    if (currentOccX == currentOccY + 1) {
		this.epsilon.set(3, true);
	    }
	    if (this.beta.get() < u) {
		int i = this.beta.get();
		currentOccX = 0;
		currentOccY = 0;
		while (i <= u && currentOccX == currentOccY) {
		    i++;
		    currentOccX = 0;
		    while (currentX < this.sortedFloorx.length && this.sortedFloorx[currentX].get() == i) {
			currentOccX++;
			currentX++;
		    } // Read sortedFloorx array in order to compute occX
		    currentOccY = 0;
		    while (currentY < this.sortedCeily.length && this.sortedCeily[currentY].get() == i) {
			currentOccY++;
			currentY++;
		    } // Read sortedCeily array in order to compute occY
		}
		if (i <= u && currentOccX < currentOccY) {
		    this.delta.set(1);
		}
	    }
	}
    }


    /**
     * The <code>setPointersAndFlags</code> method updates the values
     * &alpha;, &beta;, &gamma; and &delta;, used by the algorithm,
     * when the domain of a variable has changed.
     *
     * @param idx the index of the variable whose domain has changed
     * @param inf a <code>boolean</code> value indicating whether the change
     * occured with the lower bound (<code>true</code>) or with thee upper bound
     * (<code>false</code>).
     * @exception ContradictionException if the problem instance is inconsistant
     */
    public void updatePointersAndFlags(int idx, boolean inf) throws ContradictionException {
	/* TODO : for optimizing the constraint update ? */
    }


    /**
     * The <code>gac</code> method ("gac" for Generalized Arc Consistency)
     * checks for a support for each value of the variables, and removes
     * a value if it has no support.
     *
     * @exception ContradictionException if a variable has an empty domain.
     */
    private void gac() throws ContradictionException {
	int a, b;
	for (int i = 0; i < n; i++) {
	    // Check support for x
	    if ((a = super.vars[i].getInf()) < (b = super.vars[i].getSup())) {
		if (a < this.alpha.get()) {
		    super.vars[i].instantiate(a, super.cste);
		}
		if (a == this.alpha.get() && this.epsilon.get(1)) {
		    if (b >= this.beta.get() && this.gamma.get() > 0) {
			if (this.epsilon.get(2)) {
			    if (this.delta.get() > 0) {
				//super.vars[i].updateSup(this.beta.get() - 1, super.cste);
				super.vars[i].updateSup(this.beta.get(), cIndices[i]);
			    }
			    else {
				super.vars[i].updateSup(this.beta.get(), cIndices[i]);
			    }
			}
			else {
			    //super.vars[i].updateSup(this.beta.get() - 1, super.cste);
			    super.vars[i].updateSup(this.beta.get(), cIndices[i]);
			}
		    }
		    else {
			super.vars[i].updateSup(this.beta.get(), cIndices[i]);
		    }
		}
	    }

	    // Check support for y
	    if ((a = super.vars[n + i].getInf()) < (b = super.vars[n + i].getSup())) {
		if (b <= this.alpha.get()) {
		    super.vars[n + i].instantiate(b, super.cste);
		}
		if (this.alpha.get() < b &&
		    b < this.beta.get() &&
		    a <= this.alpha.get()) {
		    super.vars[n + i].updateInf(this.alpha.get(), cIndices[n + i]);
		}
		if (b == this.beta.get() && a <= this.alpha.get()) {
		    if (this.epsilon.get(1)) {
			if (this.gamma.get() > 0 &&
			    this.epsilon.get(2) &&
			    this.delta.get() > 0) {
			    //super.vars[n + i].updateInf(this.alpha.get() + 1, super.cste);
			    super.vars[n + i].updateInf(this.alpha.get(), cIndices[n + i]);
			}
			else {
			    super.vars[n + i].updateInf(this.alpha.get(), cIndices[n + i]);
			}
		    }
		    else {
			super.vars[n + i].updateInf(this.alpha.get(), cIndices[n + i]);
		    }
		}
		if (b > this.beta.get() && a <= this.alpha.get()) {
		    if (this.epsilon.get(1)) {
			if (this.gamma.get() > 0) {
			    //super.vars[n + i].updateInf(this.alpha.get() + 1, super.cste);
			    super.vars[n + i].updateInf(this.alpha.get(), cIndices[n + i]);
			}
		    }
		    else {
			//super.vars[n + i].updateInf(this.alpha.get() + 1, super.cste);
			super.vars[n + i].updateInf(this.alpha.get(), cIndices[n + i]);
		    }
		}

	    }
	}
    }


    /**
     * This method is invoked during the first propagation.
     *
     * @exception ContradictionException if a variable has an empty domain.
     */
    public void awake() throws ContradictionException
    {
	this.setPointersAndFlags();
	this.gac();
	//propagate();
    }


    /**
     * This methode propagates the constraint events.
     *
     * @exception ContradictionException if a variable has an empty domain.
     */
    public void propagate() throws ContradictionException
    {
	//System.out.println("propagate.");
	//this.generateVectors();
	this.setPointersAndFlags();
	this.gac();
    }


    /** This method is called when a variable has been instanciated
     * @param    idx the index of the instanciated variable.
     **/

    public void awakeOnInst(int idx) throws ContradictionException
    {
	if ((idx < this.n) && (super.vars[idx].getInf() > this.maximum)) {
	    this.maximum = super.vars[idx].getInf();
	}
	if ((idx >= this.n) && (super.vars[idx].getSup() < this.minimum)) {
	    this.minimum = super.vars[idx].getSup();
	}
	this.updateVectors(idx);
	this.setPointersAndFlags();
	this.gac();
	//propagate();
    }

    /** Cette méthode réagit si une variable a vu sa borne inférieure augmenter.
     * @param    idx l'indice de la variable qui a été instanciée.
     **/

    public void awakeOnInf(int idx) throws ContradictionException
    {
	if (idx < this.n) {
	    if (super.vars[idx].getInf() > this.maximum) {
		this.maximum = super.vars[idx].getInf();
	    }
	    this.updateVectors(idx);
	    this.setPointersAndFlags();
	    this.gac();
	    }
	//propagate();
    }

    /** Cette méthode réagit si une variable a vu sa borne supérieure diminuer.
     * @param    idx l'indice de la variable qui a été instanciée.
     **/

    public void awakeOnSup(int idx) throws ContradictionException
    {
	if (idx >= this.n) {
	    if (super.vars[idx].getSup() < this.minimum) {
		this.minimum = super.vars[idx].getSup();
	    }
	    this.updateVectors(idx);
	    this.setPointersAndFlags();
	    this.gac();
	}
	//propagate();
    }


    /** 
     * This method checks if the constraint is satisfied, once the variables have
     * all been satisfied.
     * @return <code>true</code> iff the constraint is satisfied.
     **/
    
    public boolean isSatisfied()
    {
	IntDomainVar[] x = new IntDomainVar[n];
	IntDomainVar[] y = new IntDomainVar[n];
	for (int i = 0; i < n; i++) {
	    x[i] = super.vars[i];
	    y[i] = super.vars[n + i];
	}
	
	java.util.Arrays.sort(x, this.new IDVComparator());
	java.util.Arrays.sort(y, this.new IDVComparator());
	int i;
	for (i = 0; i < n && x[i].getVal() >= y[i].getVal(); i++) {}
	if (i == n) return false;
	return true;
    }


    /**
     * The rather classical <code>toString</code> method...
     *
     * @return a <code>String</code> representing the object.
     */
    
    public String toString()
    {
	return "Leximin ordering constraint.";
    }



    /**
     * Prints some of the useful private fields that are used by the gac 
     * algorithm.
     */
    
    public void printOccVectors() {
	System.out.print("x = [");
	for (int i = 0; i < this.sortedFloorx.length; i++) {
	    System.out.print(" " + super.vars[i].pretty());
	}
	System.out.print(" ]\n");
	System.out.print("y = [");
	for (int i = 0; i < this.sortedCeily.length; i++) {
	    System.out.print(" " + super.vars[n + i].pretty());
	}
	System.out.print(" ]\n");
	System.out.print("sortedFloor(x) = [");
	for (int i = 0; i < this.sortedFloorx.length; i++) {
	    System.out.print(" " + this.sortedFloorx[i].get());
	}
	System.out.print(" ]\n");
	System.out.print("sortedCeil(y) = [");
	for (int i = 0; i < this.sortedCeily.length; i++) {
	    System.out.print(" " + this.sortedCeily[i].get());
	}
	System.out.print(" ]\n");
	System.out.print("floor(x) = [");
	for (int i = 0; i < this.floorx.length; i++) {
	    System.out.print(" " + this.floorx[i].get());
	}
	System.out.print(" ]\n");
	System.out.print("ceil(y) = [");
	for (int i = 0; i < this.ceily.length; i++) {
	    System.out.print(" " + this.ceily[i].get());
	}
	System.out.print(" ]\n");
	System.out.println("alpha = " + this.alpha.get());
	System.out.println("beta = " + this.beta.get());
	System.out.println("gamma = " + this.gamma.get());
	System.out.println("delta = " + this.delta.get());
	System.out.print("epsilon = [");
	for (int i = 0; i < 4; i++) {
	    System.out.print(" " + this.epsilon.get(i));
	    }
	System.out.print(" ]\n");
	
    }


    private class IDVComparator implements java.util.Comparator<IntDomainVar> {
	public int compare(IntDomainVar o1, IntDomainVar o2) throws ClassCastException {
	    return (o1.getVal() > o2.getVal() ? 1 : (o1.getVal() < o2.getVal() ? -1 : 0));
	}
    }

    private class SIComparator implements java.util.Comparator<StoredInt> {
	public int compare(StoredInt o1, StoredInt o2) throws ClassCastException {
	    return (o1.get() > o2.get() ? 1 : (o1.get() < o2.get() ? -1 : 0));
	}
    }

}