% 
% Smullyan Knight, Knave, and Normal problems in MiniZinc.
%
% This are the problem 39 to 43 from Raymond Smulluan's 
% book "What is the name of this book?".
% 
% Model created by Hakan Kjellerstrand, hakank@bonetmail.com
% See also my MiniZinc page: http://www.hakank.org/minizinc


include "globals.mzn"; 

int: knight = 1; % always tells the truth
int: normal = 2; % sometimes tells the truth, sometimes lies
int: knave  = 3; % always lies

array[1..3] of var {knight, knave, normal}: p;

% uncomment for problem 43
% var bool: p43_C_says_B_higher_rank_than_A;


%
% a knight always speaks the truth
% a knave always lies
% a normal sometimes lies
%
% says(kind of person, what the person say)
%
predicate says(var int: kind, var bool: says) =
   (kind = knight /\ says = true )
   \/
   (kind = knave  /\ says = false )
   \/ % if not a knight or a knave
   (kind = normal)
;

solve satisfy;

constraint
    %%  Problem 39
    %% A: A is normal   
    %% B: A is normal
    %% C: C is not normal
    %% Solution: A: knave, B, normal, C, knight
    says(p[1], p[1] = normal)
    /\
    says(p[2], p[1] = normal)
    /\
    says(p[3], not(p[3] = normal))
    /\  
    all_different(p)

    %% 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
    % p[3] = 1 /\ % ignore C
    % says(p[1], p[2] = knight)
    % /\
    % says(p[2], not(p[1] = knight))


    %% 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.
    %% Three solutions:
    %%   A is knave, B is normal
    %%   B is normal, B is knave
    %%   A is normal, B is normal
    % p[3] = 1 /\ % ignore C
    % says(p[1], p[2] = knight)
    % /\
    % says(p[2], p[1] = knave)


    %% 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
    % p[3] = 1 /\ % ignore C
    % says(p[1], -p[1] < -p[2])
    % /\
    % says(p[2], not(-p[1] < -p[2]))


    %% Problem 43
    %% A: B is of higher rank than C
    %% B: C is of higher rank than A
    %% C is asked "Who has higher rank, A or B?"
    %% The book's solution: 
    %% Whether C is a knight or knave he says that B i of higher rank than A
    %% NOTE: 
    %% This model don't give the same answer as the book, 
    %% (which means that the model is wrong or not).
    %% 
    % all_different(p)
    % /\
    % says(p[1], -p[2] > -p[3])
    % /\
    % says(p[2], -p[3] > -p[1])
    % /\
    % says(p[3], p43_C_says_B_higher_rank_than_A)
    % /\
    % p43_C_says_B_higher_rank_than_A = (-p[2] > -p[1])


;

output [
  "1:knight (alway true), 2=normal (sometimes lie), 3=knave (always false), \n",
  "p: ", show(p),"\n",
  % "p43_C_says_B_higher_rank_than_A: ", show(p43_C_says_B_higher_rank_than_A), "\n", % uncomment for problem 43
]
;