//
// biconditional
// part 4.
//
// x=2 <-> z=2
// y=2 <-> z=2
// x=2
//
// Q: will y now be 2?
//
// Is this the same as:  x=2 && y=2 <-> z=2 ?
//                       x=2 || y=2 <-> z=2 ?
//                       (x=2 <-> z=2) &&( y=2 <-> z=2) ?
//
// How else could we express A <-> B ?
//

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.IntegerVariable;
import choco.kernel.solver.ContradictionException;
import choco.kernel.model.constraints.Constraint;


public class Prop6 {

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

    Model m = new CPModel();
    
    // EDIT
    // m.setDefaultExpressionDecomposition(true);

    IntegerVariable x = makeIntVar("x",0,4,"cp:enum");
    IntegerVariable y = makeIntVar("y",0,4,"cp:enum");
    IntegerVariable z = makeIntVar("z",0,4,"cp:enum");

    m.addConstraint(ifOnlyIf(eq(x,2),eq(z,2)));
    m.addConstraint(ifOnlyIf(eq(y,2),eq(z,2)));
    m.addConstraint(eq(x,2));

    // EDIT:
    // m.addConstraint(ifOnlyIf(and(eq(x,2),eq(y,2)),eq(z,2)));

    Solver s = new CPSolver();
    s.read(m);
    s.propagate();
    System.out.println(s.getVar(x).pretty());
    System.out.println(s.getVar(y).pretty());
    System.out.println(s.getVar(z).pretty());
    //
    // NOTE: what value does y now have?
    //
  }
}