//
// How many solutions are there to the equation
// x + y + z = 29 where x,y,z in [0..29]
//
// Prove result is correct.
//

import static choco.Choco.*;
import choco.cp.model.CPModel;
import choco.cp.solver.CPSolver;
import choco.kernel.model.Model;
import choco.kernel.solver.Solver;
import choco.kernel.solver.ContradictionException;
import choco.kernel.model.variables.integer.IntegerExpressionVariable;
import choco.kernel.model.variables.integer.IntegerVariable;
import choco.cp.solver.search.integer.varselector.StaticVarOrder;

public class sum29 {

    static void display(int x, int y, int z){
	System.out.println("java Ramsey334_30a "+ x +" "+ y +" "+ z +" > results/"+ x +"-"+ y +"-"+ z +".txt & ");
    }
  
  public static void main(String[] args) {
     Model m = new CPModel();
     int n = 29;

     IntegerVariable[] vars = makeIntVarArray("",3,0,n);

     IntegerVariable x    = makeIntVar("x",0,n);
     IntegerVariable y    = makeIntVar("y",0,n);
     IntegerVariable z    = makeIntVar("z",0,n);

     m.addConstraint(eq(sum(vars),29));
     m.addConstraint(leq(vars[0],vars[1]));

     Solver solver = new CPSolver();     
     solver.read(m);                       
     //s.solve(true);  
     solver.setVarIntSelector(new StaticVarOrder(solver.getVar(vars)));

     if (solver.solve().booleanValue()){
	 display(solver.getVar(vars[0]).getVal(),solver.getVar(vars[1]).getVal(),solver.getVar(vars[2]).getVal());
	 while (solver.nextSolution().booleanValue()) 
	     display(solver.getVar(vars[0]).getVal(),solver.getVar(vars[1]).getVal(),solver.getVar(vars[2]).getVal());
     }

     //System.out.println("feasible: " + solver.isFeasible());
     //System.out.println("nbSol: " + solver.getNbSolutions());
  }
}