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


public class AtLeastConstraint extends AbstractLargeIntConstraint {
	
	private int k, n;
	private StoredBitSet isPossible, isSure;
	private StoredInt nbPossible, nbSure;
	private StoredInt[] sups;//, invSups;
	
	public AtLeastConstraint(IntDomainVar[] lvars, IntDomainVar x, int _k) {
		super(AtLeastConstraint.mergeIntVarArrays(lvars, x));
		this.k = _k;
		this.n = lvars.length;
		
		this.problem = lvars[0].getProblem();
		this.initStructures();
	}
	
	private void initStructures() {
		Environment envi = super.vars[0].getProblem().getEnvironment();
		this.isPossible = new StoredBitSet(envi, this.n);
		this.nbPossible = new StoredInt(envi, 0);
		this.isSure = new StoredBitSet(envi, this.n);
		this.nbSure = new StoredInt(envi, 0);
		this.sups = new StoredInt[this.n];
		//this.invSups = new StoredInt[this.n];
		for (int i = 0; i < this.n; i++) {
			this.sups[i] = new StoredInt(envi, i);
			//this.invSups[i] = new StoredInt(envi, i);
		}			

		for (int i = 0; i < this.n; i++) {
			if (vars[i].getSup() >= super.vars[this.n].getInf()) {
				this.isPossible.set(i);
				this.nbPossible.add(1);
			}
			if (vars[i].getInf() >= super.vars[this.n].getSup()) {
				this.isSure.set(i);
				this.nbSure.add(1);
			}
		}
		this.quickSort(0, this.n - 1);
	}
	
	private static IntDomainVar[] mergeIntVarArrays (IntDomainVar[] firstArray, IntDomainVar var) {
		IntDomainVar[] newArray = new IntDomainVar[firstArray.length + 1];
		for (int i = 0; i < firstArray.length; i++)
			newArray[i] = firstArray[i];
		newArray[firstArray.length] = var;
		return (newArray);
	}
	
	private void insertionSort()
	{
		int i, j, index;
		
		for (i = 1; i < this.n; i++) {
			index = this.sups[i].get();
			for (j = i; (j > 0) && (super.vars[this.sups[j-1].get()].getSup() > super.vars[index].getSup()); j--) {
				this.sups[j].set(this.sups[j-1].get());
				//this.invSups[this.sups[j].get()].set(j);
			}
			this.sups[j].set(index);
			//this.invSups[this.sups[j].get()].set(j);
		}
	}
	
	@SuppressWarnings("unused")
	private void updateSupPlace(int idx) {
		int i;
		for (i = this.n - 1; i >= 0 && this.sups[i].get() != idx; i--) {}
		for (; i > 0 && this.vars[this.sups[i].get()].getSup() > this.vars[idx].getSup(); i--) {
			this.sups[i].set(this.sups[i - 1].get());
		}
		this.sups[i].set(idx);
	}
	
	private void quickSort (int p, int r) {
		int q;
		if (p < r) {
			q = this.partition(p, r);
			this.quickSort(p, q - 1);
			this.quickSort(q + 1, r);
		}
	}
	
	private int partition (int p, int r) {
		int x = super.vars[this.sups[r].get()].getSup();
		int i = p - 1;
		for (int j = p; j < r; j++) {
			if (super.vars[this.sups[j].get()].getSup() <= x) {
				i++;
				this.permute(i, j);
			}
		}
		this.permute(i + 1, r);
		return (i + 1);
	}
	
	private void permute (int i, int j) {
		int tmp = this.sups[i].get();
		this.sups[i].set(this.sups[j].get());
		this.sups[j].set(tmp);
		//this.invSups[this.sups[i].get()].set(i);
		//this.invSups[this.sups[j].get()].set(j);
	}
	
	
	public void awake() throws ContradictionException {
		propagate();
	}
	
	public void propagate() throws ContradictionException {
		for (int j = 0; j < this.n; j++) {
			if (this.isPossible.get(j)) {
				if (super.vars[j].getSup() < super.vars[this.n].getInf()) {
					isPossible.clear(j);
					nbPossible.add(-1);
				}
			}
		}
		filter();
	}
	
	public void filter() throws ContradictionException {
		if (this.nbPossible.get() < this.k) {
			throw new ContradictionException(this);
		}
		if (this.nbPossible.get() == this.k) {
			for (int i = 0 ; i < this.n ; i ++ ) {
				if (isPossible.get(i)) {
					vars[i].updateInf(super.vars[this.n].getInf() ,cIndices[i]);
				}
			}
		}
		this.insertionSort();
		if (super.vars[this.n].getSup() > super.vars[this.sups[this.n - this.k].get()].getSup()) {
			super.vars[this.n].updateSup(super.vars[this.sups[this.n - this.k].get()].getSup(), cIndices[this.n]);
		}
	}
	
	public void awakeOnInf(int idx) throws ContradictionException
	{
		if (this.isEntailed() != null) {
			return;
		}
		if (idx == this.n) {
			this.propagate();
		}
		else {
			if (!this.isSure.get(idx) && vars[idx].getInf() >= super.vars[this.n].getSup()) {
				this.isSure.set(idx);
				this.nbSure.add(1);
			}
		}
	}
	
	public void awakeOnSup(int idx) throws ContradictionException {
		if (this.isEntailed() != null) {
			return;
		}
		if (idx != this.n) {
			/* *******************************
			 Experimental !!
			 ******************************* */
			//if (!this.isPossible.get(idx)) {
			//	return;
			//}
			/* *******************************
			 Experimental (fin) !!
			 ******************************* */
			//this.printSups();
			//this.quickSort(0, this.n - 1);
			this.insertionSort();
			//this.updateSupPlace(idx);
			//this.printSups();
			if (!this.isSure.get(idx) && this.isPossible.get(idx) && super.vars[idx].getSup() < super.vars[this.n].getInf()) {
				this.isPossible.clear(idx);
				this.nbPossible.add(-1);
				this.filter();
			}
			super.vars[this.n].updateSup(super.vars[this.sups[this.n - this.k].get()].getSup(), cIndices[this.n]);
		}
		else {
			for (int i = 0; i < this.n; i++) {
				if (!this.isSure.get(i) && vars[i].getInf() >= super.vars[this.n].getSup()) {
					this.isSure.set(i);
					this.nbSure.add(1);
				}
			}
		}
	}
	
	public void awakeOnInst(int idx) throws ContradictionException {
		this.awakeOnSup(idx);
		this.awakeOnInf(idx);
	}
	
	
	public boolean isSatisfied() {
		int inf = 0, sup = 0;
		for (int i = 0; i < this.n; i++) {
			if (super.vars[i].getVal() >= super.vars[n].getVal()) {
				sup++;
			}
			else {
				inf++;
			}
			if (sup >= this.k) return true;
			if (inf > this.n - this.k) return false;
		}
		return false;
	}
	
	public Boolean isEntailed() {
		if (this.nbSure.get() >= this.k) {
			return Boolean.TRUE;
		}
		if (this.nbPossible.get() < this.k) {
			return Boolean.FALSE;
		}
		return null;
	}
	
	public void printPossibles() {
		System.out.print("possibles = [");
		for (int i = 0; i < this.n; i++) {
			System.out.print(" " + (this.isPossible.get(i) ? "1" : "0"));
		}
		System.out.println(" ]");
	}
	
	public void printSups() {
		System.out.print("indices = [");
		for (int i = 0; i < this.n; i++) {
			System.out.print(" " + this.sups[i].get());
		}
		System.out.print(" ], sups = [");
		for (int i = 0; i < this.n; i++) {
			System.out.print(" " + this.vars[this.sups[i].get()].getSup());
		}
		System.out.println(" ] ; var[n] = [" + this.vars[n].getInf() + "," + this.vars[n].getSup() + "]");
		/*System.out.print("invSups = [");
		 for (int i = 0; i < this.n; i++) {
		 System.out.print(" " + this.invSups[i].get());
		 }
		 System.out.println(" ]");*/
		try {
			new java.io.BufferedReader(new java.io.InputStreamReader(System.in)).readLine();
		} catch(java.io.IOException e) {}
	}
	
	@SuppressWarnings("unused")
	private void checkOrder() {
		int[] tmp = new int[this.n];
		
		for (int i = 0; i < this.n; i++) {
			tmp[i] = this.sups[i].get();
		}
		
		this.quickSort(0, this.n - 1);
		
		for (int i = 0; i < this.n; i++) {
			if (tmp[i] != this.sups[i].get()) {
				throw new Error();
			}
		}
	}
	
	public void setK(int _k) throws ContradictionException {
		this.k = _k;
		this.initStructures();
		//this.propagate();
	}
	
}