import choco.Problem;
import choco.ContradictionException;
import choco.integer.*;


public class MyProblem extends Problem {
    int[] inst;
    long nodes;
    long time;
    long nodeLimit;
    int status;

    public MyProblem() {
	super();
	nodes      = 0;
	time       = 0;
	nodeLimit  = -1;
        status     = 0; 
    }

    private boolean isConsistent(DecisionVar[] v,int i,int x) throws ContradictionException {
	//System.out.println("isConsistent(" + v[i] + "," + i + "," + x + ")");
	nodes++;
	boolean consistent = true;
	inst[i] = x;
	try{v[i].setVal(x);super.propagate();}
	catch (ContradictionException e) {consistent = false;}
	return consistent;
    }
    //
    // test if the problem can be made AC when v takes value x
    //

    public long getNodes(){return nodes;}
    public long getTime(){return time;}
    public int getStatus(){return status;}
    public void setNodeLimit(long nodeLimit){this.nodeLimit = nodeLimit;}

    private int getPotentialDiscrepancies(DecisionVar[] v,int n,int i){
	int pd = 0;
	for (int j=i;j<n;j++) pd = pd + (v[j].getDomainSize()-1);
	return pd;
    }
    //
    // how many potential discrepancies can be taken at depth i, depth i+1, 
    // and so on to depth n-1?
    //

    public boolean lds(DecisionVar[] v,int kMax,boolean lateDiscrepancies) throws ContradictionException {
	int n = v.length;
	inst  = new int[n];
	nodes = 0;
	time  = System.currentTimeMillis();
	boolean consistent = true;
	worldPush();
	try{super.propagate();}
	catch (ContradictionException e) {consistent = false;}
	if (consistent){
	    consistent = false;
	    for (int k=0;k<=kMax && !consistent && status == 0;k++){
		worldPush();
		try {consistent = ldsProbe(v,n,k,0,lateDiscrepancies);}
		catch (Exception e) {status = 1;}
		worldPop();
	    }
	}
	worldPop();
	if (consistent && status == 0)
	    for (int i=0;i<n;i++) v[i].setVal(inst[i]);
	time = System.currentTimeMillis() - time;
	return (consistent && status == 0);
    }

    private boolean ldsProbe(DecisionVar[] v,int n,int k,int i,boolean lateDiscrepancies) throws Exception, ContradictionException {
	//System.out.println("ldsProbe(" + k + "," + i + ")");
	if (nodeLimit>0 && nodes>nodeLimit) throw new Exception();
	if (i==n) return true;   // all vars instantiated
	DecVarEnumeration dve = new DecVarEnumeration(v[i]);
	boolean result = false;
	int m  = v[i].getDomainSize();
	int x  = dve.getNextValue(); 
	int y  = -999;
	int pd = getPotentialDiscrepancies(v,n,i+1);
	if (lateDiscrepancies && k<=pd && !result){
	    worldPush();
	    result = isConsistent(v,i,x) && ldsProbe(v,n,k,i+1,lateDiscrepancies);
	    worldPop();
	}
	for (int j=1;j<m && j<=k && !result;j++){
	    y = dve.getNextValue();
	    worldPush();
	    if (isConsistent(v,i,y)) result = ldsProbe(v,n,k-j,i+1,lateDiscrepancies);
	    worldPop();
	}
	if (!lateDiscrepancies && k<=pd && !result){
	    worldPush();
	    result = isConsistent(v,i,x) && ldsProbe(v,n,k,i+1,lateDiscrepancies);
	    worldPop();
	}
	return result;
    }

    public boolean bt(DecisionVar[] v) throws ContradictionException {
	int n = v.length;
	inst  = new int[n];
	nodes = 0;
	time  = System.currentTimeMillis();
	boolean consistent = true;
	worldPush();
	try{super.propagate();}
	catch (ContradictionException e) {consistent = false;}
        try{consistent = consistent && bt(v,n,0);}
	catch (Exception e) {status = 1;}
	worldPop();
	if (consistent && status==0)
	    for (int i=0;i<n;i++) v[i].setVal(inst[i]);
	time = System.currentTimeMillis() - time;
	return (consistent && status == 0);
    }

    private boolean bt(DecisionVar[] v,int n,int i) throws Exception, ContradictionException {
	if (nodeLimit>0 && nodes>nodeLimit) throw new Exception();
	if (i==n) return true;   // all vars instantiated
	//System.out.println("bt(" + v[i] + ")");
	DecVarEnumeration dve = new DecVarEnumeration(v[i]);
	boolean result = false;
	int m = v[i].getDomainSize();
	int x = -999; 
	for (int j=0;j<m && !result;j++){
	    x = dve.getNextValue();
	    worldPush();
	    if (isConsistent(v,i,x)) result = bt(v,n,i+1);
	    worldPop();
	}
	return result;
    }
}