import choco.Problem;
import choco.integer.constraints.AbstractLargeIntConstraint;
import choco.integer.*;
import choco.ContradictionException;
import choco.mem.StoredBitSet;
import choco.mem.StoredInt;
import choco.mem.Environment;
import choco.Solver;

//
// Subtour Elimination Constraint
// see "Solving Small TSPs with Constraints" by Caseau & Laburthe
//

public class SubtourElimination extends AbstractLargeIntConstraint {  

    private StoredInt[] start;   // the start of a chain
    private StoredInt[] end;     // the end of a chain
    private StoredInt[] length;  // the length of the chain
    private int n;

    public SubtourElimination(Problem pb,IntDomainVar[] S) {
	super(S);
	n             = S.length;
	problem       = pb;
	Environment e = pb.getEnvironment();
	start         = new StoredInt[n];
	end           = new StoredInt[n];
	length        = new StoredInt[n];
	for (int i=0;i<n;i++){
	    start[i]  = new StoredInt(e,i);
	    end[i]    = new StoredInt(e,i);
	    length[i] = new StoredInt(e,0);
	}
    }
    //
    // Note: we assume all variables in S are allDifferent
    //

    public boolean isSatisfied(){
	// System.out.println("isSatisfied()");
	return true;
    }
    
    public void awake() throws ContradictionException {
	// System.out.println("awake()");
    }

    public void propagate() throws ContradictionException {
	// System.out.println("propagate()");
    }

    public void awakeOnInf(int idx) throws ContradictionException {
    // System.out.println("awakeOnInf(" + idx + ")");
    }

    public void awakeOnSup(int idx) throws ContradictionException {
     // System.out.println("awakeOnSup(" + idx + ")");
    }

    public void awakeOnRem(int idx,int x) throws ContradictionException {
	// System.out.println("awakeOnRem(" + idx + "," + x + ")");
    }

    public void awakeOnInst(int idx) throws ContradictionException {
	// System.out.println("awakeOnInst(" + idx + "," + vars[idx].getVal() + ")");
	int i   = idx,
	    j   = vars[i].getVal(), // city_j comes immediately after city_i
	    s_i = start[i].get(),
	    e_j = end[j].get();	    
	length[e_j].add(length[i].get() + 1);
	start[e_j].set(s_i);	
	end[s_i].set(e_j);
	if (length[e_j].get() < n-1)
	    vars[e_j].remVal(s_i);
    }

    public static void main(String[] args) throws choco.ContradictionException {

	Problem pb          = new Problem();
	int n               = Integer.parseInt(args[0]);     // length of sequence
	IntDomainVar[] next = new IntDomainVar[n];
	for (int i=0;i<n;i++){
	    next[i] = pb.makeEnumIntVar("n_" + i,0,n-1);
	    //next[i].remVal(i);
	}
	pb.post(pb.allDifferent(next));
	pb.post(new SubtourElimination(pb,next));


	pb.solve(true);

	/*
	if (pb.solve().booleanValue()){
	  for (int i=0;i<n;i++)
	      System.out.print("(" + i + "," + next[i].getVal() + ") ");
	  System.out.println();
	  while (pb.nextSolution().booleanValue()){
	      for (int i=0;i<n;i++)
		  System.out.print("(" + i + "," + next[i].getVal() + ") ");
	  System.out.println();
	  }
	}
	*/

      Solver s = pb.getSolver();
      System.out.println("feasible: " + pb.isFeasible());
      System.out.println("nbSol: " + s.getNbSolutions());
    }
}