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 SemiAtLeastConstraint extends AbstractLargeIntConstraint {

    private int x0;
    private int k, n;
    private StoredBitSet isPossible, isSure;
    private StoredInt nbPossible, nbSure;

    public SemiAtLeastConstraint(IntDomainVar[] lvars, int _x0, int _k) {
	super(lvars);
	this.x0 = _x0;
	this.k = _k;
	this.n = lvars.length;
	
	this.problem = lvars[0].getProblem();
	
	Environment envi = lvars[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);
	
    }

    public void awake() throws ContradictionException {
	for (int i = 0; i < this.n; i++) {
	    if (vars[i].getSup() >= this.x0) {
		isPossible.set(i);
		nbPossible.add(1);
	    }
	    if (vars[i].getInf() >= this.x0) {
		isSure.set(i);
		nbSure.add(1);
	    }
	}
	propagate();
    }

    public void propagate() throws ContradictionException {
	for (int j = 0; j < this.n; j++) {
	    if (this.isPossible.get(j)) {
		if (vars[j].getSup() < this.x0) {
		    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(this.x0 ,cIndices[i]);
		}
	    }
	}
    }

    public void awakeOnInf(int idx) throws ContradictionException {
	if (this.isEntailed() != null) {
	    return;
	}
	if (!this.isSure.get(idx) && vars[idx].getInf() >= this.x0) {
	    this.isSure.set(idx);
	    this.nbSure.add(1);
	}
    }

    public void awakeOnSup(int idx) throws ContradictionException {
	if (this.isEntailed() != null) {
	    return;
	}
	/* *******************************
	   Experimental !!
	   ******************************* */
	//if (!this.isPossible.get(idx)) {
	//    return;
	//}
	/* *******************************
	   Experimental (fin) !!
	   ******************************* */
	if (!this.isSure.get(idx) && this.isPossible.get(idx) && super.vars[idx].getSup() < this.x0) {
	    this.isPossible.clear(idx);
	    this.nbPossible.add(-1);
	    this.filter();
	}
    }

    public void awakeOnInst(int idx) throws ContradictionException {
	if (this.isEntailed() != null) {
	    return;
	}
	if (this.isPossible.get(idx) && super.vars[idx].getVal() < this.x0) {
	    this.isPossible.clear(idx);
	    this.nbPossible.add(-1);
	    this.filter();
	}
    }

    public Boolean isEntailed() {
	if (this.nbSure.get() >= this.k) {
	    return Boolean.TRUE;
	}
	if (this.nbPossible.get() < this.k) {
	    return Boolean.FALSE;
	}
	return null;
    }

    public boolean isSatisfied() {
	int inf = 0, sup = 0;
	for (int i = 0; i < this.n; i++) {
	    if (super.vars[i].getVal() >= this.x0) {
		sup++;
	    }
	    else {
		inf++;
	    }
	    if (sup >= this.k) return true;
	    if (inf > this.n - this.k) return false;
	}
	return false;
    }
}