:- use_module(library(clpz)).
:- use_module(library(lists)).
:- use_module(library(dcgs)).
:- use_module(library(format)).
:- use_module(library(lambda)).
:- use_module(library(pio)).

% ~byakuren
%    ^ ^
%  =(o.o)=
%    m m

% Representation:
% - A clock time is a 3-digit integer HMM with H in 1..9 and MM in 00..59.
% - Clock positions are 1..8, left to right, and each has a digit triple [Hour, MinTens, MinOnes].

% Representation helpers

clock_time_digits(Time, [Hour, MinTens, MinOnes]) :-
    Hour in 1..9,
    MinTens in 0..5,
    MinOnes in 0..9,
    Time #= Hour * 100 + MinTens * 10 + MinOnes.

clock_layout(ClockTimes, ClockDigits) :-
    length(ClockTimes, 8),
    length(ClockDigits, 8),
    maplist(clock_time_digits, ClockTimes, ClockDigits).

% Memo helpers

is_on_the_hour([_, MinTens, MinOnes], B) :-
    B #<==> (MinTens #= 0 #/\ MinOnes #= 0).

has_repeat_digit([Hour, MinTens, MinOnes]) :-
    Hour #= MinTens #\/ Hour #= MinOnes #\/ MinTens #= MinOnes.

has_digit(D, [Hour, MinTens, MinOnes]) :-
    Hour #= D #\/ MinTens #= D #\/ MinOnes #= D.

digits_exclude_1_4([Hour, MinTens, MinOnes]) :-
    Hour in 5..9,
    MinTens in 0 \/ 5,
    MinOnes in 0 \/ 5..9.

is_reverse_digits_of([Hour1, MinTens1, MinOnes1], [Hour2, MinTens2, MinOnes2], B) :-
    B #<==> (Hour1 #= MinOnes2 #/\ MinTens1 #= MinTens2 #/\ MinOnes1 #= Hour2).

% Memo 1: each of these clocks should be set to a different time.

memo(1, ClockTimes, _ClockDigits) :-
    all_distinct(ClockTimes).

% Memo 2: five of these clocks should be set to a time ending on the hour.

memo(2, _ClockTimes, ClockDigits) :-
    maplist(is_on_the_hour, ClockDigits, Flags),
    sum(Flags, #=, 5).

% Memo 3: this clock should not have all different digits.

memo(3, _ClockTimes, ClockDigits) :-
    nth1(3, ClockDigits, Third),
    has_repeat_digit(Third).

% Memo 4: this clock's neighbours should both be set to a time containing a 7.

memo(4, _ClockTimes, ClockDigits) :-
    nth1(3, ClockDigits, Third),
    nth1(5, ClockDigits, Fifth),
    has_digit(7, Third),
    has_digit(7, Fifth).

% Memo 5: this clock should be set on the hour (ending in :00).

memo(5, _ClockTimes, ClockDigits) :-
    nth1(5, ClockDigits, Fifth),
    is_on_the_hour(Fifth, 1).

% Memo 6: none of these clocks should be set to times that contain 1, 2, 3, or 4.

memo(6, _ClockTimes, ClockDigits) :-
    maplist(digits_exclude_1_4, ClockDigits).

% Memo 7: this clock should be set to a time that contains the same three numbers as another clock but in reverse order.

memo(7, _ClockTimes, ClockDigits) :-
    nth1(7, ClockDigits, Seventh),
    maplist(is_reverse_digits_of(Seventh), ClockDigits, Flags),
    nth1(7, Flags, 0),
    sum(Flags, #>=, 1).

% Memo 8: the clocks are positioned so that their times go up in ascending order.

memo(8, ClockTimes, _ClockDigits) :-
    chain(#<, ClockTimes).

% Output

print_solution(ClockDigits) :-
    phrase_to_stream(solution_output(ClockDigits), user_output).

solution_output(ClockDigits) -->
    "[",
    time_strings(ClockDigits),
    format_("].~n", []).

time_strings([]) --> [].
time_strings([Digits|Rest]) -->
    time_string(Digits),
    time_strings_tail(Rest).

time_strings_tail([]) --> [].
time_strings_tail([Digits|Rest]) -->
    ",",
    time_string(Digits),
    time_strings_tail(Rest).

time_string([Hour, MinTens, MinOnes]) -->
    format_("\"~d:~d~d\"", [Hour, MinTens, MinOnes]).

% Solver and entrypoint

memos(ClockTimes, ClockDigits, Ns) :-
    findall(N, memo(N, ClockTimes, ClockDigits), Ns).

clockdigits_(ClockDigits, ClockTimes) :-
    clock_layout(ClockTimes, ClockDigits),
    memos(ClockTimes, ClockDigits, Ns),
    maplist([ClockTimes, ClockDigits]+\N^memo(N, ClockTimes, ClockDigits), Ns).

clockdigits(ClockDigits) :-
    clockdigits_(ClockDigits, ClockTimes),
    labeling([ffc], ClockTimes).

run :-
    clockdigits(ClockDigits),
    print_solution(ClockDigits),
    false.