/**
 * Warranty & Liability
 * To the extent permitted by applicable law and unless explicitly
 * otherwise agreed upon, XLOG Technologies AG makes no warranties
 * regarding the provided information. XLOG Technologies AG assumes
 * no liability that any problems might be solved with the information
 * provided by XLOG Technologies AG.
 *
 * Rights & License
 * All industrial property rights regarding the information - copyright
 * and patent rights in particular - are the sole property of XLOG
 * Technologies AG. If the company was not the originator of some
 * excerpts, XLOG Technologies AG has at least obtained the right to
 * reproduce, change and translate the information.
 *
 * Reproduction is restricted to the whole unaltered document. Reproduction
 * of the information is only allowed for non-commercial uses. Selling,
 * giving away or letting of the execution of the library is prohibited.
 * The library can be distributed as part of your applications and libraries
 * for execution provided this comment remains unchanged.
 *
 * Restrictions
 * Only to be distributed with programs that add significant and primary
 * functionality to the library. Not to be distributed with additional
 * software intended to replace any components of the library.
 *
 * Trademarks
 * Jekejeke is a registered trademark of XLOG Technologies AG.
 */

:- ensure_loaded(library(sequence)).
:- use_module(library(clpb)).
:- use_module(library(boole/clpb)).

sat_show(H, W) :-
   model(H, W, M), term_variables(M, L),
   call_nth(labeling(L),N), write('Solution '), write(N), nl,
   show(H, W, M), fail; true.

count(H, W, C) :-
   model(H, W, M), term_variables(M, L),
   sat_count(+([1|L]), C).

show(H, W, M) :-
   between(1, H, Y),
   (between(1, W, X), X2 is X+1, write('+'),
      (member(((Y,X)-(Y,X2))-1, M) -> write('-'); write(' ')),
      fail; nl, true),
   (between(1, W, X), Y2 is Y+1,
      (member(((Y,X)-(Y2,X))-1, M) -> write('|'); write(' ')),
      write(' '), fail; nl, true),
    fail; true.

/*******************************************************************/
/* Construct Model                                                 */
/*******************************************************************/

model(H, W, M) :-
   rect(H, W, V, E),
   hamilton(V, E, [], M, C, []),
   diffuse(V, E, M, N, D, []),
   witness(V, N, K, [P|Q]),
   counter(V, *(D) * (~P) * +(Q), K, _, F),
   sat(*(C) * ~F).

rect(H, W, V, E) :-
   findall((Y,X), (between(1,H,Y),between(1,W,X)), V),
   findall((Y,X)-(Y2,X2), (between(1,H,Y),between(1,W,X),
        (X<W, X2 is X+1,Y2=Y;
         Y<H, Y2 is Y+1,X2=X)), E).

hamilton([], _, M, M) --> [].
hamilton([X|V], E, M, N) -->
   {connects(E, X, M, H, R)},
   [card([2],R)],
   hamilton(V, E, H, N).

diffuse([], _, M, M) --> [].
diffuse([X|V], E, M, N) -->
   {connects(E, X, M, H, R),
    neighbours(E, X, H, J, S),
    sumprod(R, S, T),
    lookup(J, X, U, K)},
   [T=<U],
   diffuse(V, E, K, N).

counter([], E, M, M, E).
counter([X|V], E, M, N, U^F) :-
   lookup(M, X, U, H),
   counter(V, E, H, N, F).

witness([], M, M, []).
witness([X|V], M, N, [U|W]) :-
   lookup(M, X, U, H),
   witness(V, H, N, W).

/*******************************************************************/
/* Construct Helper                                                */
/*******************************************************************/

neighbours([], _, M, M, []).
neighbours([X-Y|E], X, M, N, [Z|R]) :- !,
   lookup(M, Y, Z, H),
   neighbours(E, X, H, N, R).
neighbours([Y-X|E], X, M, N, [Z|R]) :- !,
   lookup(M, Y, Z, H),
   neighbours(E, X, H, N, R).
neighbours([_|E], X, M, N, R) :-
   neighbours(E, X, M, N, R).

connects([], _, M, M, []).
connects([X-Y|E], X, M, N, [Z|R]) :- !,
   lookup(M, X-Y, Z, H),
   connects(E, X, H, N, R).
connects([Y-X|E], X, M, N, [Z|R]) :- !,
   lookup(M, Y-X, Z, H),
   connects(E, X, H, N, R).
connects([_|E], X, M, N, R) :-
   connects(E, X, M, N, R).

lookup(M, X, V, M) :- member(X-V, M), !.
lookup(M, X, V, [X-V|M]).

sumprod([], [], 0).
sumprod([X|L], [Y|R], X*Y+Z) :- sumprod(L, R, Z).

% ?- sat_show(4,4).
% Solution 1
% +-+ +-+
% | | | |
% + + + +
% | | | |
% + +-+ +
% |     |
% +-+-+-+
%
% Solution 2
% +-+ +-+
% | | | |
% + +-+ +
% |     |
% + +-+ +
% | | | |
% +-+ +-+
%
% Solution 3
% +-+-+-+
% |     |
% + +-+ +
% | | | |
% + + + +
% | | | |
% +-+ +-+
%
% Solution 4
% +-+-+-+
% |     |
% + +-+-+
% | |
% + +-+-+
% |     |
% +-+-+-+
%
% Solution 5
% +-+-+-+
% |     |
% +-+ +-+
%   | |
% +-+ +-+
% |     |
% +-+-+-+
%
% Solution 6
% +-+-+-+
% |     |
% +-+-+ +
%     | |
% +-+-+ +
% |     |
% +-+-+-+

% ?- count(4,4,C).
% C = 6.