/* 

  Lady and tiger: Eighth day in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 44. Eighth day

  Each of the two rooms contains either a lady or a tiger. There could be tigers in both
  rooms or ladies in both rooms. There is a sign on each room. If a lady is in room 1,
  then the sign on the door is true. If a tiger is in room 1, then the sign on the door is
  false. For room 2, the situation is opposite. If a lady is in room 2, then the sign on the
  door is false. If a tiger is in room 2, then the sign on the door is true. Now, the prob-
  lem is that signs are not already put on the doors. That is, the two messages can appear
  either on the first door or on the second one. The signs are either both true of both
  false. Which door to open in order to find the lady, marry her, and get half of the king-
  dom as compensation? (Smullyan 2009)

  Sign 1 (Room 1 or Room 2): This room contains a tiger
  Sign 2 (Room 1 or Room 2): Both rooms contain tigers
  """

  [sign1 = 2,sign2 = 1,room1 = 0,room2 = 0,who1 = 2,who2 = 1]
  Sign 1 is for room 2
  Sign 2 is for room 1
  Room 1 sign is false
  Room 2 sign is false
  Room 1: Tiger Room 2: Lady

  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,

  [Room1,Room2] :: 0..1,
  [Sign1,Sign2] :: 1..2, % To what room does the two signs belong
  [Who1,Who2] :: Lady..Tiger,

  % One sign for each door
  Sign1 #!= Sign2,

  % First sign: This room contains a tiger:
  Sign1 #= 1 #=> (Room1 #<=> Who1 #= Tiger), % Sign 1 at room 1
  Sign1 #= 2 #=> (Room2 #<=> Who2 #= Tiger), % Sign 2 at room 2

  % Second sign: Booth rooms contains tigers
  Sign2 #= 1 #=> (Room1 #<=> (Who1 #= Tiger #/\ Who2 #= Tiger)), % Sign 2 at room 1
  Sign2 #= 2 #=> (Room2 #<=> (Who1 #= Tiger #/\ Who2 #= Tiger)), % Sign 2 at room 2

  
  % If a lady is in room 1, then the sign on the door is true.
  Who1 #= Lady #<=> Room1 #= 1,
  % If a tiger is in room 1, then the sign on the door is false.
  Who1 #= Tiger #<=> Room1 #= 0,  

  % For room 2, the situation is opposite.
  % If a lady is in room 2, then the sign on the door is false.
  Who2 #= Lady #<=> Room2 #= 0,  
  % If a tiger is in room 2, then the sign on the door is true.
  Who2 #= Tiger #<=> Room2 #= 1,    

  % The signs are either both true or both false.
  Room1 #= Room2,

  Vars = [sign1=Sign1,sign2=Sign2,room1=Room1,room2=Room2,who1=Who1,who2=Who2],
  solve(Vars),

  println(Vars),
  printf("Sign 1 is for room %w\n",Sign1),
  printf("Sign 2 is for room %w\n",Sign2),    
  printf("Room 1 sign is %w\n",cond(Room1 == 1,true,false)),
  printf("Room 2 sign is %w\n",cond(Room2 == 1,true,false)),
  Map = new_map([1="Lady",2="Tiger"]),  
  printf("Room 1: %w Room 2: %w\n",Map.get(Who1),Map.get(Who2)),
  nl,  
  fail,
  
  nl.
go => true.