/* 

  Arranged royal marriage puzzle in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 80. Arranged royal marriage

  You are a young prince in situation to choose marrying one of the three princesses:
  one from the north neigbouring country, one from the south, or one from the east.
  Each princess secretly sent you some messages. The first one says: "If you marry the
  princess from the south, there will be war". The second one says: "Marrying any of us
  will not bring peace". You learn from the third princess that: "Marry me and it will be
  peace, marry the south princess and there will be war". Given that you know that all
  the princesses are liars, can you choose a princess that brings peace for sure?
  """

  peace = 1
  ps = [0,0,0]
  marry = [0,1,0]
  princess_to_marry = South

  The princess to marry is the South princess.

  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 ?=>
  Peace :: [0,1],

  % Which princess to marry?
  Marry = [_North,South,East],
  Marry :: 0..1,
  MarryS = ["North","South","East"],
  
  % The princess' statements
  Ps = [NorthT,SouthT,EastT],
  Ps :: 0..1,

  % The first one says: "If you marry the princess from the south, there will be war".
  NorthT #<=> (South #=> Peace #= 0),

  % The second one says: "Marrying any of us  will not bring peace".
  % SouthT #<=> ((North #=> Peace #= 0) #/\ (South #=> Peace #= 0) #/\ (East #=> Peace #= 0)),
  SouthT #<=> Peace #= 0, % simpler

  % You learn from the third princess that:
  % "Marry me and it will be peace, marry the south princess and there will be war".
  EastT #<=> ((East #=> Peace #= 1) #/\ (South #=> Peace #= 0)),

  % Given that you know that all the princesses are liars, can you choose a princess
  % that brings peace for sure?
  
  % All princesses are lying
  sum(Ps) #= 0,

  % We marry exactly one princess
  sum(Marry) #= 1,

  % There will be peace  
  Peace #= 1,

  solve(Ps ++ Marry ++ [Peace]),
  
  println(peace=Peace),  
  println(ps=Ps),
  println(marry=Marry),
  println(princess_to_marry=[MarryS[I] : I in 1..3, Marry[I] == 1].first),
  nl,
  fail,
  
  nl.
go => true.