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

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;

public class CSP6lite {

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

     Model m = new CPModel();

     IntegerVariable v1  = makeIntVar("v1",1,5);
     IntegerVariable v2  = makeIntVar("v2",1,5);
     IntegerVariable v3  = makeIntVar("v3",1,5);
     IntegerVariable v4  = makeIntVar("v4",1,5);

     m.addConstraint(lt(v1,v2));            // v1 < v2
     m.addConstraint(lt(v4,v3));            // v4 < v3
     m.addConstraint(eq(plus(v4,v2),5));    // v4 + v2 = 5
     m.addConstraint(gt(plus(v2,v3),6));    // v2 + v3 > 6
     m.addConstraint(leq(v1,minus(v4,1)));  // v1 <= v4 - 1

     Solver s = new CPSolver();    
     s.read(m);                   

     s.propagate();

     System.out.println(s.pretty());
  }
}