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


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

    public MyProblem() {
	super();
	nodes         = 0;
	time          = 0;
	nodeLimit     = -1;
	discrepancies = 0;
        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 int getDiscrepancies(){return discrepancies;}
    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++){
		discrepancies = k;
		worldPush();
		if (lateDiscrepancies) {
		    try {consistent = ldsProbeLate(v,n,k,0);}		
		    catch (Exception e) {status = 1;}
		}
		else {
		    try {consistent = ldsProbeEarly(v,n,k,0);}		
		    catch (Exception e) {status = 1;}
		}
		worldPop();
	    }
	}
	worldPop();
	if (consistent && status == 0)
	    for (int i=0;i<n;i++){v[i].setVal(inst[i]); super.propagate();}
	time = System.currentTimeMillis() - time;
	return (consistent && status == 0);
    }
    //
    // NOTE: assume binary 0/1 domains
    //

    private boolean ldsProbeEarly(DecisionVar[] v,int n,int k,int i) 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
	/*
	if (i==n){
	    for (int j=0;j<n;j++) System.out.print(v[j].getVal());
	    System.out.println();
	    return false;
	}
	*/
	boolean result = false;
	int pd = getPotentialDiscrepancies(v,n,i+1);
	if (k > 0){
	    worldPush();
	    if (isConsistent(v,i,1)) result = ldsProbeEarly(v,n,k-1,i+1);
	    worldPop();
	}
	if (k <= pd && !result){
	    worldPush();
	    if (isConsistent(v,i,0)) result = ldsProbeEarly(v,n,k,i+1);
	    worldPop();
	}
	return result;
    }

    private boolean ldsProbeLate(DecisionVar[] v,int n,int k,int i) 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){
	    for (int j=0;j<n;j++) System.out.print(v[j].getVal());
	    System.out.println();
	    return false;
	}
	*/
	if (i==n) return true;   // all vars instantiated
	boolean result = false;
	int pd = getPotentialDiscrepancies(v,n,i+1);
	if (k <= pd){
	    worldPush();
	    result = isConsistent(v,i,0) && ldsProbeLate(v,n,k,i+1);
	    worldPop();
	}
	if (!result && k > 0){
	    worldPush();
	    if (isConsistent(v,i,1)) result = ldsProbeLate(v,n,k-1,i+1);
	    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]); super.propagate();}
	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] + ")");
	boolean result = false;
	int[]x         = {0,1};
	for (int j=0;j<2 && !result;j++){
	    worldPush();
	    if (isConsistent(v,i,x[j])) result = bt(v,n,i+1);
	    worldPop();
	}
	return result;
    }
}