/* 

  Knight and knaves: Three inhabitants and not enough information in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 66. Three inhabitants and not enough information

  Suppose instead, A and B say the following: A: "All of us are knaves". B: "Exactly
  one of us is a knave". Can it be determined what B is? Can it be determined what C
  is? (puzzle 32 from Smullyan (2011))
  """  


  [0,0,1]
  A: Knave  B: Knave  C: Knight
  [0,1,1]
  A: Knave  B: Knight  C: Knight

  I.e. we can infer that 
  - A is a Knave
  - C is a Knight
  - But we don't know what type B is

  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 #= Knave) + (B #= Knave) + (C #= Knave) #= 2),
  B #<=> sum(Ps) #= 2,

  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.