/* 

  Lady and Tiger: A lady, a tiger, and an empty room in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 47. A lady, a tiger, and an empty room

  One room contains a lady, another a tiger, and the third room is empty. The sign of the
  door containing a lady is true. The sign of the door containing a tiger is false. The sign
  of the empty room can be either true or false. Which door to open in order to find the
  lady, marry her, and get half of the kingdom as compensation? (Smullyan 2009)

  Room 1: Room 3 is empty
  Room 2: The tiger is in room 1
  Room 3: This room is empty
  """  

  [room1 = 1,room2 = 0,room3 = 1,who1 = 1,who2 = 2,who3 = 0]
  Room 1 sign is true
  Room 2 sign is false
  Room 3 sign is true
  Room 1:Lady  Room 2:Tiger Room 3:Empty

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

*/

import cp.

main => go.

go ?=>
  Rooms = [Room1, Room2, Room3], % Is Room<I> true or false
  Rooms :: 0..1,
  
  Empty = 0, Lady = 1, Tiger = 2,   
  Whos = [Who1,Who2,Who3], % Who is in which room
  Whos :: [Empty,Lady,Tiger],

  % One room contains a lady, another a tiger, and the third room is empty. 
  all_different(Whos),

  % sum(Rooms) #>= 1,

  Room1 #<=> Who3 #= Empty,  
  Room2 #<=> Who1 #= Tiger,
  Room3 #<=> Who3 #= Empty,

  % The sign of the door containing a lady is true. 
  (Who1 #= Lady) #=> Room1 #= 1,
  (Who2 #= Lady) #=> Room2 #= 1,
  (Who3 #= Lady) #=> Room3 #= 1,  

  % The sign of the door containing a tiger is false. 
  (Who1 #= Tiger) #=> Room1 #= 0,
  (Who2 #= Tiger) #=> Room2 #= 0,
  (Who3 #= Tiger) #=> Room3 #= 0,  

  % The sign of the empty room can be either true or false. 
  % Who1 #= Empty #=> (Room1 #= 0 #\/ Room1 #= 1),
  % Who2 #= Empty #=> (Room2 #= 0 #\/ Room2 #= 1),
  % Who3 #= Empty #=> (Room3 #= 0 #\/ Room3 #= 1),  

  Vars = [room1=Room1,room2=Room2,room3=Room3,who1=Who1,who2=Who2,who3=Who3],
  solve(Vars),

  println(Vars),
  printf("Room 1 sign is %w\n",cond(Room1 == 1,true,false)),
  printf("Room 2 sign is %w\n",cond(Room2 == 1,true,false)),
  printf("Room 3 sign is %w\n",cond(Room3 == 1,true,false)),  
  Map = new_map([0="Empty",1="Lady",2="Tiger"]),  
  printf("Room 1:%w  Room 2:%w Room 3:%w\n",Map.get(Who1),Map.get(Who2),Map.get(Who3)),
  fail,

  nl.
go => true.