/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  Written by Markus Triska, triska@gmx.at, Aug. 12th 2005
  Public domain code.

  A king, wishing to determine which of his three wise men is the
  wisest, puts a white spot on each of their foreheads, and tells them
  that at least one of the spots is white. The king arranges the wise
  men in a circle so that they can see and hear each other (but cannot
  see their own spot) and asks each man in turn what is the colour of
  his spot. The first two say they don't know, and the third says that
  his spot is white.


  Usage (tested with SWI-Prolog 5.5.25):

  ?- setup([white,white,white]), ask(1), ask(2), ask(3), clean.
  say(3, white)
  say(2, dontknow)
  say(1, dontknow)

  Another example:

  ?- setup([white,notwhite,notwhite]), ask(1), clean.
  say(1, white)

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */


:- use_module(library(chr)).

:- chr_constraint know/2, know/3, ask/1, say/2, sees/2, wrong_assumption/2, either/2, clean/0.

know(Player,Fact) \ know(Player,Fact) <=> true.
know(Player,AID,F) \ know(Player,AID,F) <=> true.
know(Player,col(Other1,notwhite)), know(Player,col(Other2,notwhite))
	<=> all_dif([Other1,Other2,Player])
	| know(Player, col(Player,white)).
know(P,AID,col(P2,notwhite)), know(P,col(P3,notwhite))
	==> dif(P2,P3), player_others(WP, [P2,P3])
	| know(P, AID, know(WP,col(WP,white))).

either(F1,col(Player,Col)), know(P,AID,know(Player,col(P,C)))
	==> contradict(F1,col(P,C))
	| know(P, AID, know(Player,col(Player,Col))).
either(col(Player,Col),F2), know(P,AID,know(Player,col(P,C)))
	==> contradict(F2,col(P,C))
	| know(P, AID, know(Player,col(Player,Col))).

know(Player,AID,col(Player,Col)), sees(Other,Player)
	==> know(Player, AID, know(Other,col(Player,Col))).
know(P,AID,know(Player,col(Player,_))), say(Player,dontknow)
	==> wrong_assumption(AID, P).
know(Player,col(Player,Col)) \ ask(Player) <=> say(Player,Col).

% make two assumptions: w(_), assuming I am white, and n(_), assuming I am not
% white - in the hope that one can be proved incorrect later
know(Player,col(Other,white))
	==> dif(Other,Player)
	| know(Player, w(Player), col(Player,white)),
	  know(Player, n(Player), col(Player,notwhite)).
know(Player,AID,col(Player,Col)), wrong_assumption(AID, Player)
	<=> complement(Col,CC)
	| know(Player, col(Player,CC)).
know(Player,col(Other,white)) \ ask(Player)
	<=> dif(Other,Player) | say(Player,dontknow).
know(Player,AID,col(Player,white)), sees(P,Player)
	==> know(Player, AID, dontknow(P)).

say(Player,dontknow)
	==> player_others(Player, [O1,O2])
	| either(col(O1,white), col(O2,white)).
say(Player,Col), know(P,AID,dontknow(Player))
	==> dif(Col,dontknow) | wrong_assumption(AID,P).

% if requested, remove everything but "say"-terms from the constraint store:
clean \ know(_,_,_) <=> true.
clean \ know(_,_) <=> true.
clean \ either(_,_) <=> true.
clean \ sees(_,_) <=> true.
clean \ wrong_assumption(_,_) <=> true.
clean <=> true.


all_dif([P1,P2,P3]) :-
	dif(P1, P2),
	dif(P2, P3),
	dif(P1, P3).

flip_know(Fact, Player) :- know(Player, Fact).

player_others(P, Os) :- select(P, [1,2,3], Os).

complement(white, notwhite).
complement(notwhite, white).

contradict(col(Player,Col1), col(Player,Col2)) :-
	complement(Col1, Col2).

setup([C1,C2,C3]) :-
	maplist(sees(1), [2,3]),
	maplist(sees(2), [1,3]),
	maplist(sees(3), [1,2]),
	maplist(flip_know(col(1,C1)), [2,3]),
	maplist(flip_know(col(2,C2)), [1,3]),
	maplist(flip_know(col(3,C3)), [1,2]).