:- module(tor_clpfd_labeling,[label/1,labeling/2,indomain/1]).

:- use_module(library(clpfd),except([label/1,labeling/2,indomain/1])).

:- use_module(library(tor)).

indomain(Var) :- label([Var]).

label(Vs) :- labeling([], Vs).

labeling(Options, Vars) :-
        must_be(list, Options),
        must_be(list, Vars),
        maplist(finite_domain, Vars),
        label(Options, Options, default(leftmost), default(up), default(step), [], upto_ground, Vars).

finite_domain(Var) :-
        (   clpfd:fd_get(Var, Dom, _) ->
            (   domain_infimum(Dom, n(_)), domain_supremum(Dom, n(_)) -> true
            ;   instantiation_error(Var)
            )
        ;   integer(Var) -> true
        ;   must_be(integer, Var)
        ).

domain_infimum(from_to(I, _), I).
domain_infimum(split(_, Left, _), I) :- domain_infimum(Left, I).

domain_supremum(from_to(_, S), S).
domain_supremum(split(_, _, Right), S) :- domain_supremum(Right, S).

label([O|Os], Options, Selection, Order, Choice, Optim, Consistency, Vars) :-
        (   var(O)-> instantiation_error(O)
        ;   override(selection, Selection, O, Options, S1) ->
            label(Os, Options, S1, Order, Choice, Optim, Consistency, Vars)
        ;   override(order, Order, O, Options, O1) ->
            label(Os, Options, Selection, O1, Choice, Optim, Consistency, Vars)
        ;   override(choice, Choice, O, Options, C1) ->
            label(Os, Options, Selection, Order, C1, Optim, Consistency, Vars)
        ;   optimisation(O) ->
            label(Os, Options, Selection, Order, Choice, [O|Optim], Consistency, Vars)
        ;   consistency(O, O1) ->
            label(Os, Options, Selection, Order, Choice, Optim, O1, Vars)
        ;   domain_error(labeling_option, O)
        ).
label([], _, Selection, Order, Choice, Optim0, Consistency, Vars) :-
        maplist(arg(1), [Selection,Order,Choice], [S,O,C]),
        (   Optim0 == [] ->
            label(Vars, S, O, C, Consistency)
        ;   reverse(Optim0, Optim),
            exprs_singlevars(Optim, SVs),
            optimise(Vars, [S,O,C], SVs)
        ).

% Introduce new variables for each min/max expression to avoid
% reparsing expressions during optimisation.

exprs_singlevars([], []).
exprs_singlevars([E|Es], [SV|SVs]) :-
        E =.. [F,Expr],
        Single #= Expr,
        SV =.. [F,Single],
        exprs_singlevars(Es, SVs).

all_dead(fd_props(Bs,Gs,Os)) :-
        all_dead_(Bs),
        all_dead_(Gs),
        all_dead_(Os).

all_dead_([]).
all_dead_([propagator(_, S)|Ps]) :- S == dead, all_dead_(Ps).

label([], _, _, _, Consistency) :- !,
        (   Consistency = upto_in(I0,I) -> I0 = I
        ;   true
        ).
label(Vars, Selection, Order, Choice, Consistency) :-
        (   Vars = [V|Vs], nonvar(V) -> label(Vs, Selection, Order, Choice, Consistency)
        ;   select_var(Selection, Vars, Var, RVars),
            (   var(Var) ->
                (   Consistency = upto_in(I0,I), clpfd:fd_get(Var, _, Ps), all_dead(Ps) ->
                    clpfd:fd_size(Var, Size),
                    I1 is I0*Size,
                    label(RVars, Selection, Order, Choice, upto_in(I1,I))
                ;   Consistency = upto_in, clpfd:fd_get(Var, _, Ps), all_dead(Ps) ->
                    label(RVars, Selection, Order, Choice, Consistency)
                ;   choice_order_variable(Choice, Order, Var, RVars, Vars, Selection, Consistency)
                )
            ;   label(RVars, Selection, Order, Choice, Consistency)
            )
        ).

choice_order_variable(step, Order, Var, Vars, Vars0, Selection, Consistency) :-
        clpfd:fd_get(Var, Dom, _),
        clpfd:order_dom_next(Order, Dom, Next),
        (   (   Var = Next,
            label(Vars, Selection, Order, step, Consistency) )
        tor
        (   clpfd:neq_num(Var, Next),
            clpfd:do_queue,
            label(Vars0, Selection, Order, step, Consistency)
        ) ).
choice_order_variable(enum, Order, Var, Vars, _, Selection, Consistency) :-
        clpfd:fd_get(Var, Dom0, _),
        domain_direction_element(Dom0, Order, Var),
        label(Vars, Selection, Order, enum, Consistency).
choice_order_variable(bisect, Order, Var, _, Vars0, Selection, Consistency) :-
        clpfd:fd_get(Var, Dom, _),
        domain_infimum(Dom, n(I)),
        domain_supremum(Dom, n(S)),
        Mid0 is (I + S) // 2,
        (   Mid0 =:= S -> Mid is Mid0 - 1 ; Mid = Mid0 ),
        (   Order == up -> ( Var #=< Mid tor Var #> Mid )
        ;   Order == down -> ( Var #> Mid tor Var #=< Mid )
        ;   domain_error(bisect_up_or_down, Order)
        ),
        label(Vars0, Selection, Order, bisect, Consistency).

override(What, Prev, Value, Options, Result) :-
        call(What, Value),
        override_(Prev, Value, Options, Result).

override_(default(_), Value, _, user(Value)).
override_(user(Prev), Value, Options, _) :-
        (   Value == Prev ->
            domain_error(nonrepeating_labeling_options, Options)
        ;   domain_error(consistent_labeling_options, Options)
        ).

selection(ff).
selection(ffc).
selection(min).
selection(max).
selection(leftmost).
selection(random_variable(Seed)) :-
        must_be(integer, Seed),
        set_random(seed(Seed)).

choice(step).
choice(enum).
choice(bisect).

order(up).
order(down).
% TODO: random_variable and random_value currently both set the seed,
% so exchanging the options can yield different results.
order(random_value(Seed)) :-
        must_be(integer, Seed),
        set_random(seed(Seed)).

consistency(upto_in(I), upto_in(1, I)).
consistency(upto_in, upto_in).
consistency(upto_ground, upto_ground).

optimisation(min(_)).
optimisation(max(_)).

select_var(leftmost, [Var|Vars], Var, Vars).
select_var(min, [V|Vs], Var, RVars) :-
        find_min(Vs, V, Var),
        delete_eq([V|Vs], Var, RVars).
select_var(max, [V|Vs], Var, RVars) :-
        find_max(Vs, V, Var),
        delete_eq([V|Vs], Var, RVars).
select_var(ff, [V|Vs], Var, RVars) :-
        clpfd:fd_size_(V, n(S)),
        find_ff(Vs, V, S, Var),
        delete_eq([V|Vs], Var, RVars).
select_var(ffc, [V|Vs], Var, RVars) :-
        find_ffc(Vs, V, Var),
        delete_eq([V|Vs], Var, RVars).
select_var(random_variable(_), Vars0, Var, Vars) :-
        length(Vars0, L),
        I is random(L),
        nth0(I, Vars0, Var),
        delete_eq(Vars0, Var, Vars).

find_min([], Var, Var).
find_min([V|Vs], CM, Min) :-
        (   min_lt(V, CM) ->
            find_min(Vs, V, Min)
        ;   find_min(Vs, CM, Min)
        ).

find_max([], Var, Var).
find_max([V|Vs], CM, Max) :-
        (   max_gt(V, CM) ->
            find_max(Vs, V, Max)
        ;   find_max(Vs, CM, Max)
        ).

find_ff([], Var, _, Var).
find_ff([V|Vs], CM, S0, FF) :-
        (   nonvar(V) -> find_ff(Vs, CM, S0, FF)
        ;   (   clpfd:fd_size_(V, n(S1)), S1 < S0 ->
                find_ff(Vs, V, S1, FF)
            ;   find_ff(Vs, CM, S0, FF)
            )
        ).

find_ffc([], Var, Var).
find_ffc([V|Vs], Prev, FFC) :-
        (   ffc_lt(V, Prev) ->
            find_ffc(Vs, V, FFC)
        ;   find_ffc(Vs, Prev, FFC)
        ).


ffc_lt(X, Y) :-
        (   clpfd:fd_get(X, XD, XPs) ->
            domain_num_elements(XD, n(NXD))
        ;   NXD = 1, XPs = []
        ),
        (   clpfd:fd_get(Y, YD, YPs) ->
            domain_num_elements(YD, n(NYD))
        ;   NYD = 1, YPs = []
        ),
        (   NXD < NYD -> true
        ;   NXD =:= NYD,
            props_number(XPs, NXPs),
            props_number(YPs, NYPs),
            NXPs > NYPs
        ).

min_lt(X,Y) :- bounds(X,LX,_), bounds(Y,LY,_), LX < LY.

max_gt(X,Y) :- bounds(X,_,UX), bounds(Y,_,UY), UX > UY.

bounds(X, L, U) :-
        (   clpfd:fd_get(X, Dom, _) ->
            domain_infimum(Dom, n(L)),
            domain_supremum(Dom, n(U))
        ;   L = X, U = L
        ).

delete_eq([], _, []).
delete_eq([X|Xs], Y, List) :-
        (   nonvar(X) -> delete_eq(Xs, Y, List)
        ;   X == Y -> List = Xs
        ;   List = [X|Tail],
            delete_eq(Xs, Y, Tail)
        ).

tor_between(From, To, B) :-
        From =< To,
        (   B = From
        tor
        (   From1 is From + 1,
            tor_between(From1, To, B)
        )).

domain_direction_element(from_to(n(From), n(To)), Dir, E) :-
        (   Dir == up ->
            tor_between(From, To, E)
        ;   tor_between(From, To, E0),
            E is To - (E0 - From)
        ).
domain_direction_element(split(_, D1, D2), Dir, E) :-
        (   Dir == up ->
            (   domain_direction_element(D1, Dir, E)
            tor   domain_direction_element(D2, Dir, E)
            )
        ;   (   domain_direction_element(D2, Dir, E)
            tor  domain_direction_element(D1, Dir, E)
            )
        ).