/* 

  Lady and Tiger: The trials of the second day in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 38. The trials of the second 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. The signs are either both
  true or both 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: At least one of these rooms contains a lady.
  Room 2: A tiger is in the other room.
  """  

  [room1 = 1,room2 = 1,lady = 2,tiger = 1]
  Room 1 sign is true
  Room 2 sign is true
  Lady is in room 2, Tiger is in Room 1

  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 ?=>
  [Room1,Room2] :: 0..1,
  [Lady,Tiger] :: 1..2,

  % Each of the two rooms contains either a lady or a tiger.
  Lady #= 1 #=> Tiger #!= 1,
  Lady #= 2 #=> Tiger #!= 2,  

  % There could be tigers in both rooms or ladies in both rooms.

  % Room 1: At least one of these rooms contains a lady.
  Room1 #<=> (Lady #= 1 #\/ Lady #= 2), % (Lady #= 1 #\/ Lady #= 2 #\/ (Lady #= 1 #/\ Lady #= 2)),
  
  % Room 2: A tiger is in the other room.  
  Room2 #<=> Tiger #= 1,

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

  Vars = [room1=Room1,room2=Room2,lady=Lady,tiger=Tiger],
  
  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("Lady is in room %d, Tiger is in Room %d\n",Lady,Tiger),
  nl,
  
  fail,
  
  nl.
go => true.


/*
  Another encoding

  [room1 = 1,room2 = 1,who1 = 2,who2 = 1]
  Room 1 sign is true
  Room 2 sign is true
  Who 1:Tiger Who 2:Lady

*/
go2 ?=>
  Lady = 1, Tiger = 2,
  [Room1,Room2] :: 0..1,
  [Who1,Who2] :: [Lady,Tiger], % Who is in this room?

  % Room 1: At least one of these rooms contains a lady.
  Room1 #<=> (Who1 #= Lady #\/ Who2 #= Lady),
  
  % Room 2: A tiger is in the other room.  
  Room2 #<=> (Who1 #= Tiger),

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

  Vars = [room1=Room1,room2=Room2,who1=Who1,who2=Who2],
  
  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)),
  Map = new_map([1="Lady",2="Tiger"]),
  printf("Who 1:%w Who 2:%w\n",Map.get(Who1),Map.get(Who2)),
  nl,
  fail,
  
  nl.
go2 => true.