/* 

  Lady and Tiger: A lady and two tigers in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 46. A lady and two tigers

  One room contains a lady and the other two contain tigers. The sign on the door con-
  taining the lady is true and at least one of the other two signs is false. Which door to
  open in order to find the lady, marry her, and get half of the kingdom as compensa-
  tion? (Smullyan 2009)

  Room 1: A tiger is in room 2
  Room 2: A tiger is in this room
  Room 3: A tiger is in room 1
  """

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


  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 ?=>
  Lady = 1, Tiger = 2,

  Rooms = [Room1,Room2,Room3],
  Rooms :: 0..1,
  Whos = [Who1,Who2,Who3],
  Whos :: Lady..Tiger,

  % One room contains a lady and the other two contain tigers. 
  count(Lady,Whos,#=,1),
  count(Tiger,Whos,#=,2),  

  % The room signs
  Room1 #<=> Who2 #= Tiger,
  Room2 #<=> Who2 #= Tiger,
  Room3 #<=> Who1 #= Tiger,

  % The sign on the door containing the lady is true
  % and at least one of the other two signs is false.
  (Who1 #= Lady) #=> (Room1 #= 1 #/\ (Room2 #= 0 #\/ Room3 #= 0)),
  (Who2 #= Lady) #=> (Room2 #= 1 #/\ (Room1 #= 0 #\/ Room3 #= 0)),
  (Who3 #= Lady) #=> (Room3 #= 1 #/\ (Room1 #= 0 #\/ Room2 #= 0)), 

  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([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.