//
// An example of using LCF.not
//
// How many dominos are there where 
//  - first dot v1 is not(v1<2 or v1>4)
//
// NOTE: ¬(A v B) = ¬A & ¬B
//

import org.chocosolver.solver.Solver;
import org.chocosolver.solver.variables.*;
import org.chocosolver.solver.constraints.*;
import org.chocosolver.solver.search.strategy.*;
import org.chocosolver.solver.trace.Chatterbox;
import org.chocosolver.solver.exception.ContradictionException;


public class NOT {

    public static void main(String args[]) throws ContradictionException {
      Solver solver = new Solver("using LCF.not");
      IntVar v1 = VF.enumerated("v1",0,6,solver); // NOTE: enumerated
      IntVar v2 = VF.enumerated("v2",0,6,solver);
      Constraint c1 = ICF.arithm(v1,"<",2);
      Constraint c2 = ICF.arithm(v1,">",4);
      solver.post(LCF.not(LCF.or(new Constraint[]{c1,c2})));
      solver.post(ICF.arithm(v1,"<=",v2));
      solver.propagate();
      System.out.println(v1);
      System.out.println(v2);
      solver.set(ISF.lexico_LB(new IntVar[]{v1,v2})); // Variable ordering
      // find all solutions
      if (solver.findSolution()) {
	  do {System.out.println("["+v1.getValue() +" : "+ v2.getValue() +"]");}
	  while (solver.nextSolution());
      }
    }
}