/* 

  Knight and knaves: Three inhabitants and two messages in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 65. Three inhabitants and two messages

  Again we have three people, A, B, C, each of them is either a knight or a knave. A and
  B make the following statements: A: "All of us are knaves". B: "Exactly one of us is a
  knight". What are A, B, C? (puzzle 31 from Smullyan (2011))
  """  

  [0,1,0]
  A: Knave  B: Knight  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 ?=>
  Knave = 0, Knight = 1,
  Ps = [A,B,C],
  Ps :: [Knave,Knight],

  % A #<=> (A #= Knave #/\ B #= Knave #/\ C #= Knave),
  A #<=> sum(Ps) #= 0,
  
  % B #<=> ((A #= Knight) + (B #= Knight) + (C #= Knight) #= 1),
  B #<=> sum(Ps) #= 1,

  Vars = [A,B,C],
  solve(Vars),

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