/* 

  Smullyan Knight, Knave, and Normal problems in Picat.

  These are the problem 39 to 42 from Raymond Smullyan's 
  book "What is the name of this book?".

  Solutions:

  problem_39
  [3,2,1] = [Knave,Normal,Knight]

  problem_40
  [2,1] = [Normal,Knight]
  [2,2] = [Normal,Normal]
  [3,2] = [Knave,Normal]

  problem_41
  [2,2] = [Normal,Normal]
  [2,3] = [Normal,Knave]
  [3,2] = [Knave,Normal]

  problem_42
  [2,2] = [Normal,Normal]


  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 =>
  _ = findall(_,problem_39),
  nl,
  _ = findall(_,problem_40),  
  nl,
  _ = findall(_,problem_41),  
  nl,
  _ = findall(_,problem_42),  
  nl.

%
% Problem 39
% A: A is normal   
% B: A is normal
% C: C is not normal
% A, B, C are of different kind.
%
% Solution: A: knave, B, normal, C, knight
%
problem_39 => 
  Problem = problem_39,
  types(Knight,Normal,Knave),
  P = new_list(3),
  P :: Knight..Knave,
  all_different(P),
  
  Cs = $[says(P[1], P[1] #= Normal),      % A: A is normal
         says(P[2], P[1] #= Normal),      % B: B is normal
         says(P[3], #~(P[3] #= Normal))], % C: C is not normal
         
  knights_knaves_normals(Problem,P,Cs),
  fail,
  nl.

%
% Problem 40
%
% A: B is a knight
% B: A is not a knight
% Prove that at least one of them is telling the truth but is not a knight
% (Ignore C)
% 
% Three solutions:
%  A knave, B normal
%  A normal, B knight
%  A normal, B normal
%
problem_40 =>
  Problem = problem_40,
  types(Knight,Normal,Knave),
  P = new_list(2),
  P :: Knight..Knave,
  
  Cs = $[says(P[1], P[2] #= Knight),
         says(P[2], #~(P[1] #= Knight))],
         
  knights_knaves_normals(Problem,P,Cs),
  fail,
  nl.


%
% Problem 41
%
% A: B is a knight
% B: A is a knave
% Prove that either one of them is telling the truth but is not a knight
% or one is lying but is not a knave.
% x
% Three solutions:
%   A is knave, B is normal
%   B is normal, B is knave
%   A is normal, B is normal
%
problem_41 =>
  Problem = problem_41,
  types(Knight,Normal,Knave),
  P = new_list(2),
  P :: 1..3,
  Cs = $[says(P[1], P[2] #= Knight),
         says(P[2], P[1] #= Knave)],
  knights_knaves_normals(Problem,P,Cs),
  fail,
  nl.

%
% Problem 42
% Rank: knight >  normal > knaves
% Note: The coding of the types in this model is the opposite of the ranks.
% A: A < B
% B: That is not true
% 
% Solution: A: normal, B: normal
%
problem_42 =>
  Problem = problem_42,
  types(Knight,Normal,Knave),
  P = new_list(2),
  P :: 1..3,
  Cs = $[
         says(P[1], -P[1] #< -P[2]),
         says(P[2], #~(-P[1] #< -P[2]))
        ],
  knights_knaves_normals(Problem,P,Cs),
  fail,
  nl.



% General solver
knights_knaves_normals(Problem,P,Cs) =>

  println(Problem),
  Types = ["Knight","Normal","Knave"],  
  foreach(C in Cs)
    C
  end,

  solve(P),
  println(P=[Types[P[I]] : I in 1..P.len]).


% Numeric values for the types
types(Knight,Normal,Knave) =>
  Knight = 1,
  Normal = 2,
  Knave  = 3.

%
% a knight always speaks the truth
% a knave always lies
% a normal sometimes lies
%
% says(kind of person, what the person say)
%
says(Kind, Says) =>
  types(Knight,Normal,Knave),
  (Kind #= Knight #/\ Says #= 1 )
  #\/
  (Kind #= Knave  #/\ Says #= 0 )
  #\/ % if not a knight or a knave
  (Kind #= Normal).