//
// Maths challenge 2004-2005 J5
// 
//
// My bank card has a 4 digit pin, abcd. I use the following facts to help me
// remember it:
//
// - no two digits are the same
// - the 2-digit number cd is 3 times the 2-digit number ab
// - the 2-digit number da is 2 times the 2-digit number bc
//
// What are the values of a, b, c, and d?
//

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.model.variables.integer.IntegerExpressionVariable;
import choco.kernel.model.variables.integer.IntegerVariable;

import choco.kernel.solver.ContradictionException;

public class MathChallenge {

  
  public static void main(String[] args) throws ContradictionException {
      Model m = new CPModel();   
  
      /*
     IntegerVariable a  = makeIntVar("a",0,9,"cp:enum");
     IntegerVariable b  = makeIntVar("b",0,9,"cp:enum");
     IntegerVariable c  = makeIntVar("c",0,9,"cp:enum");
     IntegerVariable d  = makeIntVar("d",0,9,"cp:enum");
      */

     IntegerVariable a  = makeIntVar("a",0,9,"cp:bound");
     IntegerVariable b  = makeIntVar("b",0,9,"cp:bound");
     IntegerVariable c  = makeIntVar("c",0,9,"cp:bound");
     IntegerVariable d  = makeIntVar("d",0,9,"cp:bound");
    
 
     m.addConstraint(allDifferent(new IntegerVariable[]{a,b,c,d}));

     IntegerVariable ab = makeIntVar("ab",0,99);
     IntegerVariable bc = makeIntVar("bc",0,99);
     IntegerVariable cd = makeIntVar("cd",0,99);
     IntegerVariable da = makeIntVar("da",0,99);

     m.addConstraint(eq(ab,plus(mult(10,a),b))); // ab = 10 * a + b
     m.addConstraint(eq(bc,plus(mult(10,b),c))); // bc = 10 * b + c
     m.addConstraint(eq(cd,plus(mult(10,c),d))); // cd = 10 * c + d
     m.addConstraint(eq(da,plus(mult(10,d),a))); // da = 10 * d + a

     m.addConstraint(eq(mult(3,ab),cd));         // 3 * ab = cd
     m.addConstraint(eq(mult(2,bc),da));         // 2 * bc = da

     
     Solver s = new CPSolver();
     s.read(m);
     //System.out.println(s.solve(true) +" solutions: "+ s.getNbSolutions());
     s.propagate();
     //s.printRuntimeStatistics();  // LOOK! I spelt it right and that was wrong :(
     //s.printRuntimeSatistics();     // French :)

     System.out.println(s.getVar(a).pretty());
     System.out.println(s.getVar(b).pretty());
     System.out.println(s.getVar(c).pretty());
     System.out.println(s.getVar(d).pretty());
     System.out.println(s.getVar(ab).pretty());
     System.out.println(s.getVar(bc).pretty());
     System.out.println(s.getVar(cd).pretty());
     System.out.println(s.getVar(da).pretty());
  }
}

//
// (unique) solution should be that abcd = 2163
//
// (1) How do I know it is a unique solution?
// (2) How much search effort was involved?
// (3) have we yet looked at propagate? i.e. is propagate enough?
//