:- op(760, yfx, #<==>).
:- op(740, yfx, #\/).
:- op(720, yfx, #/\).
:- op(700, xfx, #>).
:- op(700, xfx, #<).
:- op(700, xfx, #>=).
:- op(700, xfx, #=<).
:- op(700, xfx, #=).
:- op(700, xfx, #\=).
:- op(700, xfx, in).
:- op(700, xfx, ins).
:- op(450, xfx, ..).
:- op(150, fx, #).

:- use_module(library(clpz)).
:- use_module(library(lists), [member/2, reverse/2]).

% Load knights_tour_monotonic.pl before running run_tests/0.

run_tests :-
        assertz(clpz:monotonic),
        test_basic_successors,
        test_reified_equivalence,
        test_next_candidates_equivalence,
        test_no_labeling,
        test_order_independence,
        test_monotonic_subset,
        test_boolean_total,
        test_conjunction_order,
        halt.

must(Goal) :-
        (   call(Goal) -> true
        ;   throw(error(test_failed, Goal))
        ).

must_fail(Goal) :-
        (   call(Goal) -> throw(error(test_expected_failure, Goal))
        ;   true
        ).

test_basic_successors :-
        square_domain(6, Squares),
        list_comp(Squares, n_k_next_t(6, 1), Nexts),
        must(Nexts == [9,14]).

test_reified_equivalence :-
        square_domain(6, Squares),
        list_comp(Squares, n_k_next_t(6, 1), Nexts),
        check_equiv(1, Squares, Nexts).

check_equiv(_, [], _).
check_equiv(K, [E|Es], Nexts) :-
        (   n_k_next_t(6, K, E, true) -> must(member(E, Nexts))
        ;   must_fail(member(E, Nexts))
        ),
        check_equiv(K, Es, Nexts).

test_next_candidates_equivalence :-
        square_domain(6, Squares),
        next_candidates(6, 1, Nexts),
        check_equiv(1, Squares, Nexts).

test_no_labeling :-
        n_k_next_t(6, 1, Next, true),
        must(var(Next)).

test_order_independence :-
        must((#Next #= 9, n_k_next_t(6, 1, Next, true))),
        must((n_k_next_t(6, 1, Next, true), #Next #= 9)),
        must_fail((#Next #= 10, n_k_next_t(6, 1, Next, true))),
        must_fail((n_k_next_t(6, 1, Next, true), #Next #= 10)).

gt10_t(E, T) :-
        #B #<==> (#E #> 10),
        zo_t(B, T).

test_monotonic_subset :-
        square_domain(6, Squares),
        list_comp(Squares, n_k_next_t(6, 1), Nexts),
        list_comp(Nexts, gt10_t, Nexts2),
        must(Nexts2 == [14]),
        reverse(Nexts, Rev),
        list_comp(Rev, n_k_next_t(6, 1), RevNexts),
        reverse(RevNexts, Nexts).

test_boolean_total :-
        square_domain(6, Squares),
        check_boolean_total(Squares).

check_boolean_total([]).
check_boolean_total([E|Es]) :-
        must(n_k_next_t(6, 1, E, T)),
        must((T == true ; T == false)),
        must_fail((n_k_next_t(6, 1, E, true), n_k_next_t(6, 1, E, false))),
        check_boolean_total(Es).

test_conjunction_order :-
        square_domain(6, Squares),
        list_comp(Squares, both_t_order1, L1),
        list_comp(Squares, both_t_order2, L2),
        must(L1 == L2).

both_t_order1(E, T) :-
        n_k_next_t(6, 1, E, T1),
        gt10_t(E, T2),
        and_t(T1, T2, T).

both_t_order2(E, T) :-
        gt10_t(E, T2),
        n_k_next_t(6, 1, E, T1),
        and_t(T1, T2, T).

and_t(T1, T2, T) :-
        zo_t(B1, T1),
        zo_t(B2, T2),
        #B #<==> (#B1 #/\ #B2),
        zo_t(B, T).