%
% Implementation of the global constraint circuit in Minizinc
%
% Cf http://www.emn.fr/x-info/sdemasse/gccat/sec4.46.html
%
% This Minizinc program is written by Hakan Kjellerstrand and is commented in 
% Constraint Programming: Minizinc, Gecode/flatzinc och ECLiPSe/minizinc
% http://www.hakank.org/webblogg/archives/001209.html
%
% Model created by Hakan Kjellerstrand, hakank@bonetmail.com
% See also my MiniZinc page: http://www.hakank.org/minizinc
 

include "globals.mzn";
int: n = 120;
array[1..n] of var 1..n: x;


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

%
% This variant uses an extra array (z) for the orbit of x[1].
%
% The constraint is that z[i] must not be 1 until i = n and then
% must be 1.
predicate circuit(array[int] of var int: x) =
  let { int: n = length(x),
        array[1..n] of var 1..n: z}
  in
   all_different(x) /\
   all_different(z) /\

   % put the orbit of x[1] in in z[1..n]
   % 
   z[1] = x[1] /\ 
   forall(i in 2..n) (
      z[i] = x[z[i-1]]
   )
   /\ % may not be 1 for i < n
   forall(i in 1..n-1) (
      z[i] != 1
   )
   /\  % when i = n it must be 1
   z[n] = 1
;


constraint
  circuit(x)
;
output [
      show(x)
%       "z: ", show(z), "\n"
];