/* 

  Smullyan Knight, Knave, and Normal, Island of Bahava problems in Picat.

  This are the problem 44, 45, 46 from Raymond Smullyan's 
  book "What is the name of this book?".

  The rules for The Island of Bahava:
  A knight must marry a knave
  A knave must marry a knight
  A normal must marry a normal

  Solutions:

   Problem 44
   mr_p = [Normal]
   mrs_p = [Normal]

   Problem 45
   mr_p = [Normal]
   mrs_p = [Normal]

   Problem 45
   mr_p = [Normal,Normal]
   mrs_p = [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_44),
  nl,
  _ = findall(_,problem_45),
  nl,
  _ = findall(_,problem_46),
  nl,
  
  nl.

%
% Problem 44
% Mr A: My wife is not normal
% Mrs A: My husband is not normal
% 
% Solution: Both are normal
% ignore mr and mrs B
%
problem_44 =>
  println("Problem 44"),
  types(Knight,Normal,Knave),
  N = 1,
  MrP = new_list(N),
  MrP :: [Knight,Normal,Knave],
  MrsP = new_list(N),
  MrsP :: [Knight,Normal,Knave],  
  Says = $[
          says(MrP[1], #~(MrsP[1] #= Normal)),
          says(MrsP[1], #~(MrP[1] #= Normal))
          ],
  smullyan(MrP,MrsP,Says),
  fail,
  nl.

%
% Problem 45
% Mr A: My wife is normal
% Mrs A: My husband is normal
% 
% Solution: Both are normal
%
problem_45 =>
  println("Problem 45"),

  types(Knight,Normal,Knave),
  N = 1,
  MrP = new_list(N),
  MrP :: [Knight,Normal,Knave],
  MrsP = new_list(N),
  MrsP :: [Knight,Normal,Knave],  

  Says = $[ 
           says(MrP[1], MrsP[1] #= Normal),
           says(MrsP[1], MrP[1] #= Normal)
          ],
  smullyan(MrP,MrsP,Says),
  fail,
  nl.

%
% Problem 46
%
% Mr A: Mr B is a knight
% Mrs A: My husband is right. Mr B is a knight
% Mrs B: That's right. My husband is indeed a knight.
% 
% Solution: All are normal
%
problem_46 =>
  println("Problem 45"),

  types(Knight,Normal,Knave),
  N = 2,
  MrP = new_list(N),
  MrP :: [Knight,Normal,Knave],
  MrsP = new_list(N),
  MrsP :: [Knight,Normal,Knave],  

  Says = $[
            says(MrP[1], MrP[2] #= Knight),
            says(MrsP[1], MrP[2] #= Knight),
            says(MrsP[2], MrP[2] #= Knight)
          ],

  smullyan(MrP,MrsP,Says),
  fail,
  nl.


smullyan(MrP,MrsP,Says) =>
  N = MrP.len,
  types(_Knight,_Normal,_Knave,TypesS),
  marriage_rules(MrP, MrsP),

  foreach(S in Says)
    S
  end,

  Vars = MrP ++ MrsP,
  solve(Vars),
  
  println(mr_p=[TypesS[MrP[I]] : I in 1..N]),
  println(mrs_p=[TypesS[MrsP[I]] : I in 1..N]).




%
% 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).

% 
% The marriage rules for The Island of Bahava:
% A knight must marry a knave
% A knave must marry a knight
% A normal must marry a normal
%
marriage_rules(MrP, MrsP) =>
  types(Knight,Normal,Knave,_),
  foreach(I in 1..MrP.len) 
     (MrP[I] #= Normal #/\ MrsP[I] #= Normal) 
     #\/
     (MrP[I] #= Knight #/\ MrsP[I] #= Knave)
     #\/
     (MrP[I] #= Knave #/\ MrsP[I] #= Knight)
  end.


types(Knight,Normal,Knave) =>
  types(Knight,Normal,Knave,_Types).
types(Knight,Normal,Knave,Types) =>
  Knight = 1, Normal = 2,Knave  = 3,
  Types = ["Knight","Normal","Knave"].