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; 
    }

    public String toString(){
	String s = "MyProblem: \n";
	s = s +"nodeLimit: " + nodeLimit;
	return s;
    }

    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 void setNodeLimit(long nodeLimit){this.nodeLimit = nodeLimit;}
    public int getStatus(){return status;}
    // status = 0 <-> search terminated with soln or proof of no soln
    // status = 1 <-> search node limit exceeded

    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;} // {e.printStackTrace();System.out.println("blip");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 {
	//if (i<n) System.out.println("ldsProbe(" + k + "," + i + ") " + v[i]);
	if (nodeLimit>0 && nodes>nodeLimit){throw new Exception();}
	if (i==n) return true;   // all vars instantiated
	//selectVar(v,i,n); // dvo as per Martello, Alg 595
	//DecVarEnumeration dve = new DecVarEnumeration(v,i);
	StaticDecVarEnumeration dve = new StaticDecVarEnumeration(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();
	}

	/*
	for (int j=m-1;j>=0 && !result;j--){
	    y = dve.getNextValueInReverse();
	    if (j<=k){
		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] + ")");
	//selectVar(v,i,n); // dvo as per Martello, Alg 595
	//DecVarEnumeration dve = new DecVarEnumeration(v,i);
	StaticDecVarEnumeration dve = new StaticDecVarEnumeration(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;
    }

   
    public void selectVar(DecisionVar[] v,int i,int n){
	DecisionVar temp;
	for (int j=i+1;j<n;j++){
	    if (H0(v[i]) < H0(v[j]) || H0(v[i]) == H0(v[j]) && H1(v[i]) > H1(v[j])){
		temp = v[i];
		v[i] = v[j];
		v[j] = temp;
	    }
	}
    }


    
    public int H0(DecisionVar v){return v.getInDegree();}
    //
    // Select vertex easiest to get to,
    // i.e. select vertex mith maximum in-degree
    // Consistent with Martello, Algorithm 595, ACM 9(1) 1983
    //

    public int H1(DecisionVar v){return v.getOutDegree();}
    //
    // tie breaker (see H0 above)
    // select variable with minimu out-degree (hardest to get out of)
    //
}