%
% Implementation of the global constraint cycle in Minizinc
%
% This Minizinc program is written by Hakan Kjellerstrand, hakank@bonetmail.com,
% and is commented in the (swedish) blog post
% Constraint Programming: Minizinc, Gecode/flatzinc och ECLiPSe/minizinc
% http://www.hakank.org/webblogg/archives/001209.html
%
% See also my MiniZinc page: http://www.hakank.org/minizinc
%

include "globals.mzn";

solve :: int_search(x, "first_fail", "indomain", "complete") satisfy;
% solve satisfy;

int: n = 6;
array[1..n] of var 1..n: x;
%array[1..n, 1..n] of var 1..n: y;
% array[1..n, 1..n] of var 1..n: y_transposed;


var int: num_cycles;


%
% This is quite complicated, but probably simpler to implement than using sets.
% The principle is simple:
% - create a cycle matrix from the permutation
% - create first fix position per column
% - count number of position (global_cardinality)
% - sum over that amount (gcc[i] / i)
%
predicate cycle(var int: nc, array[int] of var int: x) = 
 let {
    int: n = length(x),
    array[1..n] of var 1..n: ff_pos,
    array[1..n] of var 0..n: gcc_card,
    array[1..n, 1..n] of var 1..n: y
 } 
 in
 cycle_matrix(x,y)
 /\
 forall(i,j in 1..n) (
   let {
       % note: it is the _column_ j we are interested in, not the row i,
       % hence the construct index[j,i] 
        array[1..n] of var 1..n: tmp = [ y[j,i] | j in 1..n]
    } 
    in
    first_fixed(tmp, i, ff_pos[i])
  )
  /\ 
  global_cardinality(ff_pos, gcc_card)
  /\
  num_cycles = sum(i in 1..n) (
                  gcc_card[i] div i
               )            
;


% find first fixed position in an array
predicate first_fixed(array[int] of var int: x, var int: v, var int: ix) =
   let {
       int: n = length(x)
   }
   in
   forall(i in 1..n) (
       % 1) ix must be i
       % 2) and the must be not other i before this position
       ix = i <-> (x[i] = v /\
                   forall(j in 1..i-1) (
                       x[j] != v
                   )
                  )
  )
;

predicate cycle_matrix(array[int] of var int: x, array[int,int] of var int: m) =
  let { 
     int: n = length(x) 
  } 
  in
  all_different(x) /\  
  % copy array x to first line in matrix
  forall(j in 1..n) (
     m[1,j] = x[j]
  ) /\
  % create the rotations in the following rows
  % note that the values is from x (first row in m)
   forall(i in 2..n, j in 1..n) (
      m[i,j] = m[i-1,m[1,j]]
  ) 
;


constraint
  all_different(x) /\
  cycle(num_cycles, x)
  % some constraints...
   /\ num_cycles >= 0
   /\ num_cycles = 4

;


output [
   "x: ", show(x), " num_cycles: ", show(num_cycles) ++ "\n"
]