//
// csp6
// from AR33, figure 18, page 35
//

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

public class CSP6 {

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

     Problem pb = new Problem();

     System.out.println("// problem, no variables, no constraints //");
     System.out.println(pb.pretty());

     IntDomainVar v1  = pb.makeEnumIntVar("v1",1,5);
     IntDomainVar v2  = pb.makeEnumIntVar("v2",1,5);
     IntDomainVar v3  = pb.makeEnumIntVar("v3",1,5);
     IntDomainVar v4  = pb.makeEnumIntVar("v4",1,5);

     System.out.println("// problem, four variables, no constraints //");
     System.out.println(pb.pretty());
 
     pb.post(pb.lt(v1,v2));               // v1 < v2
     pb.post(pb.lt(v4,v3));               // v4 < v3
     pb.post(pb.eq(pb.plus(v4,v2),5));    // v4 + v2 = 5
     pb.post(pb.gt(pb.plus(v2,v3),6));    // v2 + v3 > 6
     pb.post(pb.leq(v1,pb.minus(v4,1)));  // v1 <= v4 - 1

     System.out.println("// problem, four variables, five constraints, not AC //");
     System.out.println(pb.pretty());

     pb.propagate();

     System.out.println("// problem, four variables, five constraints, AC //");
     System.out.println(pb.pretty());


     System.out.println("// solutions, if any //");
     if (pb.solve().booleanValue()){
	 System.out.println("v1 = " + v1.getVal() + "  v2 = " + v2.getVal() + 
			    "  v3 = " + v3.getVal() + "  v4 = " + v4.getVal());
	while (pb.nextSolution().booleanValue()) 
	    System.out.println("v1 = " + v1.getVal() + "  v2 = " + v2.getVal() + 
			    "  v3 = " + v3.getVal() + "  v4 = " + v4.getVal());
     }
     	
     /*
     Solver s = pb.getSolver();
     pb.solve(true);
     System.out.println("feasible: " + pb.isFeasible());
     System.out.println("nbSol: " + s.getNbSolutions());
     */
  }
}