/* 

  The first trial (Smullyan) puzzle in Picat.

  From Martin Chlond Integer Programming Puzzles:
  http://www.chlond.demon.co.uk/puzzles/puzzles3.html, puzzle nr. 3.
  Description  : The First Trial
  Source       : Smullyan, R., (1991), The Lady or The Tiger, Oxford University Press
  """
  The following [...] puzzles are taken from Raymond Smullyan's "The Lady or the Tiger". 
  In each puzzle a prisoner is faced with a decision where he must open one of two doors. 
  Behind each door is either a lady or a tiger. They may be both tigers, both ladies 
  or one of each. If the prisoner opens a door to find a lady he will marry her and 
  if he opens a door to find a tiger he will be eaten alive. Of course, the prisoner 
  would prefer to be married than eaten alive. Each of the doors has a sign bearing a 
  tatement that may be either true or false.

  3. The First Trial
  The statement on door one says, "In this room there is a lady, and in the other 
                                   room there is a tiger."
  The statement on door two says, "In one of these rooms there is a lady, and in 
                                   one of these rooms there is a tiger."
  The prisoner is informed that one of the statements is true and one is false.


  Door 1 - tiger
  Door 2 - lady
  """

  This model was inspired by the XPress Mosel model created by Martin Chlond.
  http://www.chlond.demon.co.uk/puzzles/sol3s3.html


  This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/


import cp.
import util.


main => go.


go =>
  
  Door = 2,
  Prize = 2, % 1 = Lady, 2 = Tiger

  % x(i,j) = 1 if door i hides prize j, else 0
  X = new_array(Door,Prize),
  X :: 0..1, 

  % t(i) = 1 if statement on door i is true, else 0
  T = new_list(Door),
  T :: 0..1, 

  % dummy variables
  D = new_list(2),
  D :: 0..1,

  % each door hides 1 prize
  foreach(I in 1..Door) 
    sum([X[I,J] : J in 1..Prize]) #= 1
  end,

  % if statement on door 1 is true then set t[1] = 1, else t[1] = 0
  X[1,1]+X[2,2]-T[1] #<= 1,
  X[1,1]+X[2,2]-2*T[1] #>= 0,

  % if statement on Door 2 is true then set t[2] = 1, else t[2] = 0
  X[1,1]-X[2,2]-2*D[1] #<= -1,
  X[1,1]-X[2,2]-D[1] #>= -1,

  X[1,1]-X[2,2]+2*D[2] #>= 1,
  X[1,1]-X[2,2]+2*D[2] #<= 2,

  D[1]+D[2]-T[2] #<= 1,
  D[1]+D[2]-2*T[2] #>= 0,

  % only one statement is true
  T[1]+T[2] #= 1,


  Vars = X.vars() ++ T ++ D,

  solve(Vars),

  println(t=T),
  printf("Statement on door %d is true.\n", find_first_of(T,1)),
  println(x=X),
  printf("The Lady is behind door %d\n", find_first_of(X[1],1)),
  printf("The Tiger is behind door %d\n", find_first_of(X[2],1)),

  nl.