/* 

  Knight, Knaves and Spies II in Picat.

  From https://en.wikibooks.org/wiki/Puzzles/Logic_puzzles/Knights,_Knaves_%26_Spies_II
  """
  We have three people one of whom is a knight, one a knave, and one a spy. The knight 
  always tells the truth, the knave always lies, and the spy can either lie or tell 
  the truth. The three persons are brought before a judge who wants to identify the spy.

  A says: "I am not a spy."
  B says: "I am a spy."
  Now C is in fact the spy. The judge asks him: "Is B really a spy?"

  Can C give an answer so that he doesn't convict himself as a spy?
  """

  Here are the possible outcomes. The options we have are:
  - we can force the constraint C #!= Spy (Force = true) or not (Force = false)
  - C can state "Yes, B is a spy" (CAnswer=yes) or "B is not a spy" (CAnswer=no).

  Here's the outcome of the different scenarios:

  canswer = yes
  A: Knight  B: Knave  C: Spy

  canswer = no
  A: Spy  B: Knave  C: Knight
  A: Knight  B: Knave  C: Spy
  A: Knight  B: Spy  C: Knave

  C should answer "No, B is not a spy" which would then make the judge unsure about
  the status of C. If C answers "Yes" then it indicates the C is a spy.


  If we add (force) the constraint C #!= Spy (Force = true), then it's perhaps a little clearer:
  
  force = true
  canswer = yes

  canswer = no
  A: Spy  B: Knave  C: Knight
  A: Knight  B: Spy  C: Knave


  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 ?=>
  member(Force,[false,true]),
  nl,
  println(force=Force),
  member(CAnswer, [yes,no]),
  nl,
  Knave = 0, Knight = 1, Spy = 2,
  Type = [A,B,C],
  Type :: [Knave,Knight,Spy],

  % Speak truth
  Ts = [AT,BT,CT], % Truth
  Ts :: 0..1,
  
  % We know that one is a knight, one is a knave, and one is a spy.
  all_different(Type),
  
  % A says, “I am not a spy”. 
  AT #<=> A #!= Spy,

  % B says, “I am a spy”. 
  BT #<=> B #= Spy,
   
  % C says, “Yes, B is a spy" or "No, B is not a spy"
  println(canswer=CAnswer),
  if CAnswer == yes then
    CT #<=> B #= Spy
  else
    CT #<=> B #!= Spy
  end,

  % C is is fact a spy but he wants us to believe he is not.
  % For the modelling part we state this as a constraint.
  if Force then
    C #!= Spy
  end,

  % Who is the knight, who is the knave, and who is the spy?
  foreach(I in 1..3)
    Ts[I] #= 1 #=> Type[I] :: [Knight,Spy],
    Ts[I] #= 0 #=> Type[I] :: [Knave,Spy] 
  end,

  Vars = Ts ++ Type,
  solve(Vars),

  Map = new_map([0="Knave",1="Knight",2="Spy"]),
  printf("A: %w  B: %w  C: %w\n",Map.get(A), Map.get(B),Map.get(C)),
  fail,
    
  nl.
go => true.