/* 

  Ladies and Tigers in jail in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 37. Ladies and tigers in jail

  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. One of the signs is true
  and the other is false. Which door to open in order to find the lady, marry her, and get
  half of the kingdom as compensation? (adapted from Smullyan 2009)

  Room 1: In this room there is a lady and in the other room there is a tiger.
  Room 2: In one of these rooms there is a lady and in one of these rooms there is
          a tiger.
  """

  Solution:
  [room1 = 0,room2 = 1,lady = 2,tiger = 1]
  Room 1 sign is false
  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, % Truthfulness of the room's sign
  [Lady,Tiger] :: 1..2, % in what room is the lady and tiger

  Room1 #<=> (Lady #= 1 #/\ Tiger #= 2),
  Room2 #<=> ((Lady #= 1 #/\ Tiger #= 2) #\/ (Lady #= 2 #/\ Tiger #= 1)),

  Room1 + Room2 #= 1,

  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.


/*
  Alternative encoding:

  [0,1,2,1]
  Room 1 sign:false
  Room 2 sign:true
  Who1:Lady Who2:Tiger

*/
go2 ?=>
  Lady = 1, Tiger = 2,
  [Room1,Room2] :: 0..1, % Truthfulness of the room's sign
  [Who1,Who2] :: [Lady,Tiger], % Who is in the room, a lady or a tiger

  Room1 #<=> (Who1 #= Lady #/\ Who2 #= Tiger),
  
  % Room2 #<=> ((Who1 #= Lady #/\ Who2 #= Tiger)
  %              #\/
  %             (Who1 #= Tiger #/\ Who2 #= Lady)),
  Room2 #<=> (Who1 #!= Who2),
  
  % Room1 + Room2 #= 1,
  Room1 #!= Room2,

  Vars = [Room1,Room2,Who1,Who2],
  solve(Vars),

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