/* 

  Knight and knaves: We are both knaves in Picat.

  From Adrian Groza "Modelling Puzzles in First Order Logic"
  """
  Puzzle 61. We are both knaves

  On the island of knights and knaves, knights always tell the truth, while knaves always
  lie. You are approached by two people. The first one says: "We are both knaves". What
  are they actually? (Smullyan 2011)
  """  

  [0,1]
  P1: Knave  P2: Knight


  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,
  [P1,P2] :: 0..1,

  P1 #<=> (P1 #= Knave #/\ P2 #= Knave),

  Vars = [P1,P2],
  solve(Vars),
  println(Vars),

  Map = new_map([0="Knave",1="Knight"]),
  printf("P1: %w  P2: %w\n",Map.get(P1), Map.get(P2)),

  fail,
  
  nl.
go => true.