/*

  Global constraint alldifferent_except_0 in Comet.


  From Global Constraint Catalog
  http://www.emn.fr/x-info/sdemasse/gccat/Calldifferent_except_0.html
  """
  Enforce all variables of the collection VARIABLES to take distinct values, 
  except those variables that are assigned to 0.
  """


  This Comet model was created by Hakan Kjellerstrand (hakank@bonetmail.com)
  Also, see my Comet page: http://www.hakank.org/comet 

 */

import cotfd;
// import cotls;
// import cotln;
int t0 = System.getCPUTime();

int n=10;
range Digits = 0..9;

Solver<CP> m();
var<CP>{int} x[i in 1..n](m, 0..n);

//
// alldifferent except 0
//
function void alldifferent_except_0(Solver<CP> m, var<CP>{int}[] x) {
  int n = x.getSize();
  forall(i in 1..n, j in i+1..n) {
    m.post(
           x[i] > 0 && x[j] > 0 => 
           x[i] != x[j]
           
           );
  }
}


//
// x should be in increasing order
//
function void increasing(Solver<CP> m, var<CP>{int}[] x) {
  forall(i in 2..x.getSize()) 
    m.post(x[i-1] <= x[i]);

}

Integer num_solutions(0);

exploreall<m> {

  alldifferent_except_0(m, x);
  increasing(m, x);

  // exactly 3 0's
  m.post(sum(i in 1..n) (x[i] ==0)  == 3);

} using {
      

  label(m);

  num_solutions := num_solutions + 1;
      
  cout << "x: " << x << endl;

}

cout << "\nnum_solutions: " << num_solutions << endl;
    
int t1 = System.getCPUTime();
cout << "time:      " << (t1-t0) << endl;
cout << "#choices = " << m.getNChoice() << endl;
cout << "#fail    = " << m.getNFail() << endl;
cout << "#propag  = " << m.getNPropag() << endl;