```/**
* Prolog code for the little solver.
* With a union find element.
*
* Copyright 2012-2013, XLOG Technologies GmbH, Switzerland
* Jekejeke Minlog 0.6 (minimal logic extension module)
*/

/********************************************************/
/* Little Solver with Union Find                        */
/********************************************************/

% refer(+Atom, +Atom)
% refer(X, Y) == X = Y
:- forward refer/2.

unit &:-
&- refer(X, X), !.
refer(Z, Y) &:-
&- refer(X, Y) && refer(X, Z), !.
refer(X, Z) &:-
&- refer(X, Y) && refer(Y, Z), !.

% bound(+Atom, +Elem)
% bound(X, C) == X = C
:- forward bound/2.

bound(Y, C) &:-
&- bound(X, C) && refer(X, Y), !.
zero &:-
&- bound(X, C) && bound(X, D), C =\= D, !.
unit &:-
&- bound(X, _) && bound(X, _), !.
bound(Y, C) &:-
refer(X, Y) && &- bound(X, C).

% domain(+Atom, +List)
% domain(X, A) == X in A
:- forward domain/2.

zero &:-
domain(_, []), !.
bound(X, Y) &:-
&- domain(X, [Y]), !.
domain(Y, A) &:-
&- domain(X, A) && refer(X, Y), !.
zero &:-
&- domain(X, A) && bound(X, C), \+ member(C, A), !.
unit &:-
&- domain(X, _) && bound(X, _), !.
domain(X, C) &:-
&- domain(X, B) && &- domain(X, A), intersect(A, B, C), C \== A, !.
unit &:-
&- domain(X, _) && domain(X, _), !.
domain(Y, A) &:-
refer(X, Y) && &- domain(X, A).
zero &:-
bound(X, Y) && &- domain(X, A), \+ member(Y, A), !.
unit &:-
bound(X, _) && &- domain(X, _).

/********************************************************/
/********************************************************/

% addvv(X, Y, Z) == X+Y = Z
bound(X, 0) &:-
bound(Y, 0) &:-
&- addvv(X, Y, Z) && refer(X, T), !.
&- addvv(X, Y, Z) && refer(Y, T), !.
&- addvv(X, Y, Z) && refer(Z, T), !.
&- addvv(X, Y, Z) && bound(X, C), !.
&- addvv(X, Y, Z) && bound(Y, C), !.
&- addvv(X, Y, Z) && bound(Z, C), !.
refer(X, T) && &- addvv(X, Y, Z).
refer(Y, T) && &- addvv(X, Y, Z), X \== Y.
refer(Z, T) && &- addvv(X, Y, Z), X \== Z, Y \== Z.
bound(X, C) && &- addvv(X, Y, Z).
bound(Y, C) && &- addvv(X, Y, Z), X \== Y.
bound(Z, C) && &- addvv(X, Y, Z), X \== Z, Y \== Z.

% addcv(X, C, Y) == X+C = Y
refer(X, Y) &:-
zero &:-
&- addcv(X, C, Y) && refer(X, Z), !.
&- addcv(X, C, Y) && refer(Y, Z), !.
bound(Y, E) &:-
&- addcv(X, C, Y) && bound(X, D), !, E is D+C.
bound(X, E) &:-
&- addcv(X, C, Y) && bound(Y, D), !, E is D-C.
refer(X, Z) && &- addcv(X, C, Y).
refer(Y, Z) && &- addcv(X, C, Y), X \== Y.
bound(Y, E) &:-
bound(X, D) && &- addcv(X, C, Y), E is D+C.
bound(X, E) &:-
bound(Y, D) && &- addcv(X, C, Y), X \== Y, E is D-C.

% addvc(X, Y, C) == X+Y = C
&- addvc(X, Y, C) && refer(X, Z), !.
&- addvc(X, Y, C) && refer(Y, Z), !.
bound(Y, E) &:-
&- addvc(X, Y, C) && bound(X, D), !, E is C-D.
bound(X, E) &:-
&- addvc(X, Y, C) && bound(Y, D), !, E is C-D.
refer(X, Z) && &- addvc(X, Y, C).
refer(Y, Z) && &- addvc(X, Y, C), X \== Y.
bound(Y, E) &:-
bound(X, D) && &- addvc(X, Y, C), E is C-D.
bound(X, E) &:-
bound(Y, D) && &- addvc(X, Y, C), X \== Y, E is C-D.

/********************************************************/
/* List Processing                                      */
/********************************************************/

% member(+Elem, +List)
member(X, [X|_]).
member(X, [_|Y]) :-
member(X, Y).

% intersect(+List, +List, -List)
intersect([], _, []).
intersect([X|Y], Z, [X|T]) :-
member(X, Z), !, intersect(Y, Z, T).
intersect([_|Y], Z, T) :-
intersect(Y, Z, T).

/********************************************************/
/* Test Cases I                                         */
/********************************************************/

% ?- post(domain(x,[1])), posted.
% bound(x, 1).
% Yes

% ?- post(domain(x,[1,2,3])), post(domain(y,[2,3,4])), posted.
% domain(x, [1,2,3]).
% domain(y, [2,3,4]).
% Yes

% ?- post(domain(x,[1,2,3])), post(domain(x,[2,3,4])), posted.
% domain(x, [2,3]).
% Yes

% ?- post(domain(x,[2,3])), post(domain(x,[2,3,4])), posted.
% domain(x, [2,3]).
% Yes

% ?- post(domain(x,[1,2,3])), post(domain(x,[2,3])), posted.
% domain(x, [2,3]).
% Yes

% ?- post(domain(x,[1,2,3])), post(bound(x,4)), posted.
% No

% ?- post(domain(x,[1,2,3])), post(bound(x,2)), posted.
% bound(x, 2).
% Yes

% ?- post(bound(x,4)), post(domain(x,[1,2,3])), posted.
% No

% ?- post(bound(x,2)), post(domain(x,[1,2,3])), posted.
% bound(x, 2).
% Yes

% ?- post(domain(x,[1,2,3])), post(refer(x,y)), post(domain(y,[2,3,4])), posted.
% refer(x, y).
% domain(y, [2,3]).
% Yes

% ?- post(domain(x,[1,2,3])), post(domain(y,[2,3,4])), post(refer(x,y)), posted.
% refer(x, y).
% domain(y, [2,3]).
% Yes

/********************************************************/
/* Test Cases II                                        */
/********************************************************/

% ?- post(addvv(x,y,z)), post(bound(x,1)), post(bound(y,2)), posted.
% bound(x, 1).
% bound(y, 2).
% bound(z, 3).
% Yes

% ?- post(bound(x,1)), post(addvv(x,y,z)), post(bound(y,2)), posted.
% bound(x, 1).
% bound(y, 2).
% bound(z, 3).
% Yes

% ?- post(bound(x,1)), post(bound(y,2)), post(addvv(x,y,z)), posted.
% bound(x, 1).
% bound(y, 2).
% bound(z, 3).
% Yes

% refer(z, x).
% bound(y, 0).
% Yes

% refer(z, x).
% bound(y, 0).
% Yes