% 
% Message sending puzzle in MiniZinc.
% 
% Problem from http://www.anselm.edu/homepage/mmalita/logic/message.txt
% """
% Email is out of order at St. Mary's College and the teacher wants 
% to tell Robert something urgent.
% The teacher meets Craig and asks him to tell Robert she wants to speak 
% with him. 
% Craig says that if he meets Robert its OK, but else he will send the message 
% to everyone he meets and the message will go further.
% Each student tells each student he meets that the teacher waits for Robert
% in her office.
% The students meet each other (we don't know in what order):
% 1) Craig meets John and Jason
% 2) Jason meets Kiki and Adam and David
% 3) Adam meets Scott and Jeremy
% 4) Jeremy meets John and Scott
% 5) Kiki meets Chris
% 6) Chris meets David and Adam
% 7) David meets Robert
%
% Do you think the teacher will wait for ever in her office?
% Display all the possible paths from Craig to Robert.
%
% """
% 

% Cf the model all_paths_graph.mzn which also contains then length 
% of the paths, and makes it possible to search for a shortest path.

% 
% This MiniZinc model was created by Hakan Kjellerstrand, hakank@bonetmail.com
% See also my MiniZinc page: http://www.hakank.org/minizinc
%

% include "globals.mzn"; 

int: n = 10;
set of int: N = 1..n;
int: num_edges = 13;

int: Adam = 1;
int: Chris = 2;
int: Craig = 3;
int: David = 4;
int: Jason = 5;
int: Jeremy = 6;
int: John = 7;
int: Kiki = 8;
int: Robert = 9;
int: Scott = 10;

array[N] of var 0..n: x :: is_output; % 0 is no edge
array[1..num_edges, 1..2] of N: graph;

predicate all_different_except_0(array[int] of var int: x) =
  let {
      int: n = length(x)
   }
   in
   forall(i,j in 1..n where i != j) (
        (x[i] > 0 /\ x[j] > 0) -> x[i] != x[j]
   )
;


%
% y is the last element which is > 0. All elements after y is 0
%
predicate last_not_0(array[int] of var int: x, var int: y) =
   exists(i in N) (
      x[i] = y
      /\ % all elements in x after y are 0
      forall(j in i+1..n) (x[j] = 0)
      /\ % all elements in x before y are > 0
      forall(j in 1..i) (x[j] > 0)
   )
;


predicate all_paths(array[int] of var int: x, 
                    array[int, 1..2] of var int: graph) =
   forall(i in 2..length(x)) (
     x[i] = 0
     \/
     (
       x[i] > 0 
       /\
       x[i-1] > 0
       /\
       exists(j in index_set_1of2(graph)) (
         ( graph[j,1] = x[i-1] /\ graph[j,2] = x[i]   )
         \/
         ( graph[j,1] = x[i]   /\ graph[j,2] = x[i-1] )
       )
     )
   )
;

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


constraint
   all_different_except_0(x) 
   /\
   x[1] = Craig
   /\
   last_not_0(x, Robert)
   /\
   all_paths(x, graph)
;

graph = array2d(1..num_edges, 1..2, 
  [
   Craig, John,
   Craig, Jason,
   Jason, Kiki,
   Jason, Adam, 
   Jason, David,
   Adam, Scott, 
   Adam, Jeremy,
   Jeremy, John,
   Jeremy, Scott,
   Kiki, Chris,
   Chris, David,
   Chris, Adam,
   David, Robert
  ]);