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

:- op(700, xfx, ≡). /* Unicode 0x2261 */
:- op(700, xfx, ∈). /* Unicode 0x2208 */

/********************************************************/
/* Post Extensions                                      */
/********************************************************/

% post(+Event)
:- multifile post/1.
^ post(attr_bound(R, T)) :- !,
sys_melt_var(R, T).
^ post(attr_refer(R, S)) :- !,
sys_melt_var(R, T),
sys_melt_var(S, T).

% hook(+Var, +Term)
hook(V, W) :- var(W), !,
sys_freeze_var(V, R),
sys_freeze_var(W, S),
post(refer(R, S)).
hook(V, T) :- integer(T), !,
sys_freeze_var(V, R),
post(bound(R, T)).
hook(_, T) :-
sys_throw_error(type_error(integer, T)).

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

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

unit &:-
&- refer(_, _).

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

unit &:-
&- bound(_, _).

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

zero &:-
domain(_, []), !.
attr_bound(X, Y) &:-
&- domain(X, [Y]), !.
domain(Y, A) &:-
&- domain(X, A) && sys_bound_var(X), sys_melt_var(X, H), var(H), !, sys_freeze_var(H, Y).
zero &:-
&- domain(X, A) && sys_bound_var(X), sys_melt_var(X, C), integer(C), \+ member(C, A), !.
unit &:-
&- domain(X, _) && sys_bound_var(X), sys_melt_var(X, C), integer(C), !.
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
attr_bound(X, 0) &:-
attr_bound(Y, 0) &:-
&- addvv(X, Y, Z) && sys_bound_var(X), sys_melt_var(X, H), var(H), !, sys_freeze_var(H, T).
&- addvv(X, Y, Z) && sys_bound_var(Y), sys_melt_var(Y, H), var(H), !, sys_freeze_var(H, T).
&- addvv(X, Y, Z) && sys_bound_var(Z), sys_melt_var(Z, H), var(H), !, sys_freeze_var(H, T).
&- addvv(X, Y, Z) && sys_bound_var(X), sys_melt_var(X, C), integer(C), !.
&- addvv(X, Y, Z) && sys_bound_var(Y), sys_melt_var(Y, C), integer(C), !.
&- addvv(X, Y, Z) && sys_bound_var(Z), sys_melt_var(Z, C), integer(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
attr_refer(X, Y) &:-
zero &:-
&- addcv(X, C, Y) && sys_bound_var(X), sys_melt_var(X, H), var(H), !, sys_freeze_var(H, Z).
&- addcv(X, C, Y) && sys_bound_var(Y), sys_melt_var(Y, H), var(H), !, sys_freeze_var(H, Z).
attr_bound(Y, E) &:-
&- addcv(X, C, Y) && sys_bound_var(X), sys_melt_var(X, D), integer(D), !, E is D+C.
attr_bound(X, E) &:-
&- addcv(X, C, Y) && sys_bound_var(Y), sys_melt_var(Y, D), integer(D), !, E is D-C.
refer(X, Z) && &- addcv(X, C, Y).
refer(Y, Z) && &- addcv(X, C, Y), X \== Y.
attr_bound(Y, E) &:-
bound(X, D) && &- addcv(X, C, Y), E is D+C.
attr_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) && sys_bound_var(X), sys_melt_var(X, H), var(H), !, sys_freeze_var(H, Z).
&- addvc(X, Y, C) && sys_bound_var(Y), sys_melt_var(Y, H), var(H), !, sys_freeze_var(H, Z).
attr_bound(Y, E) &:-
&- addvc(X, Y, C) && sys_bound_var(X), sys_melt_var(X, D), integer(D), !, E is C-D.
attr_bound(X, E) &:-
&- addvc(X, Y, C) && sys_bound_var(Y), sys_melt_var(Y, D), integer(D), !, E is C-D.
refer(X, Z) && &- addvc(X, Y, C).
refer(Y, Z) && &- addvc(X, Y, C), X \== Y.
attr_bound(Y, E) &:-
bound(X, D) && &- addvc(X, Y, C), E is C-D.
attr_bound(X, E) &:-
bound(Y, D) && &- addvc(X, Y, C), X \== Y, E is C-D.

/********************************************************/
/* External Representation                              */
/********************************************************/

% ensure_attr(+Var)
ensure_attr(X) :- sys_attr(X), !.
ensure_attr(X) :- sys_new_attr(X).

% ensure_hook(+Freezer)
ensure_hook(R) :- sys_clause_hook(R, hook, _), !.
ensure_hook(R) :- sys_compile_hook(hook, C), assume_hook(R, C).

% +Expr ∈ +Set
X ∈ {Y} :-  var(X), !,
set_to_list(Y, A),
ensure_attr(X),
ensure_hook(X),
sys_bind_serno(X),
sys_freeze_var(X, B),
post(domain(B, A)).
X ∈ {Y} :- integer(X), !,
set_to_list(Y, A),
member(X, A), !.
X ∈ {_} :-
sys_throw_error(type_error(integer, X)).

% set_to_list(+Set, -List)
set_to_list(X, _) :- var(X),
sys_throw_error(instantiation_error).
set_to_list((X,Y), C) :- !,
set_to_list(X, A),
set_to_list(Y, B),
union(A, B, C).
set_to_list(X, [X]) :- integer(X), !.
set_to_list(X, _) :- var(X),
sys_throw_error(type_error(integer, X)).

% +Expr + +Expr ≡ +Expr
X ≡ _ :- var(X),
sys_throw_error(instantiation_error).
X + Y ≡ Z :- var(X), var(Y), var(Z), !,
ensure_attr(X),
ensure_hook(X),
sys_bind_serno(X),
sys_freeze_var(X, A),
ensure_attr(Y),
ensure_hook(Y),
sys_bind_serno(Y),
sys_freeze_var(Y, B),
ensure_attr(Z),
ensure_hook(Z),
sys_bind_serno(Z),
sys_freeze_var(Z, C),
X + Y ≡ Z :- var(X), var(Y), integer(Z), !,
ensure_attr(X),
ensure_hook(X),
sys_bind_serno(X),
sys_freeze_var(X, A),
ensure_attr(Y),
ensure_hook(Y),
sys_bind_serno(Y),
sys_freeze_var(Y, B),
X + Y ≡ Z :- var(X), integer(Y), var(Z), !,
ensure_attr(X),
ensure_hook(X),
sys_bind_serno(X),
sys_freeze_var(X, A),
ensure_attr(Z),
ensure_hook(Z),
sys_bind_serno(Z),
sys_freeze_var(Z, B),
Y + X ≡ Z :- var(X), integer(Y), var(Z), !,
ensure_attr(X),
ensure_hook(X),
sys_bind_serno(X),
sys_freeze_var(X, A),
ensure_attr(Z),
ensure_hook(Z),
sys_bind_serno(Z),
sys_freeze_var(Z, B),
X + Y ≡ Z :- var(X), integer(Y), integer(Z), !,
T is Z-Y,
X = T.
Y + X ≡ Z :- var(X), integer(Y), integer(Z), !,
T is Z-Y,
X = T.
X + Y ≡ Z :- integer(X), integer(Y), var(Z), !,
T is X+Y,
Z = T.
X + Y ≡ Z :- integer(X), integer(Y), integer(Z), !,
T is X+Y,
Z == T.
X + _ ≡ _ :- \+ integer(X), \+ var(X),
sys_throw_error(type_error(integer, X)).
_ + Y ≡ _ :- \+ integer(Y), \+ var(Y),
sys_throw_error(type_error(integer, Y)).
_ + _ ≡ Z :-
sys_throw_error(type_error(integer, Z)).

:- multifile sys_pretty_event/1.

% sys_pretty_event(-Goal)
sys_pretty_event(X ∈ {Y}) :-
domain(B, A),
list_to_set(A, Y),
sys_melt_var(B, X).
sys_pretty_event(X+Y ≡ Z) :-
sys_melt_var(A, X),
sys_melt_var(B, Y),
sys_melt_var(C, Z).
sys_pretty_event(X+Y ≡ Z) :-
sys_melt_var(A, X),
sys_melt_var(C, Z).
sys_pretty_event(X+Y ≡ Z) :-
sys_melt_var(A, X),
sys_melt_var(B, Y).

% list_to_set(+List, -Set)
list_to_set([X,Y|T], (X,C)) :- !,
list_to_set([Y|T], C).
list_to_set([X], X).

/********************************************************/
/* 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).

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

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

% ?- X ∈ {1}, stored.
% X = 1

% ?- X ∈ {1,2,3}, Y ∈ {2,3,4}, stored.
% X ∈ {1,2,3}.
% Y ∈ {2,3,4}.
% Yes

% ?- X ∈ {1,2,3}, X ∈ {2,3,4}, stored.
% X ∈ {2,3}.
% Yes

% ?- X ∈ {2,3}, X ∈ {2,3,4}, stored.
% X ∈ {2,3}.
% Yes

% ?- X ∈ {1,2,3}, X ∈ {2,3}, stored.
% X ∈ {2,3}.
% Yes

% ?- X ∈ {1,2,3}, X = 4, stored.
% No

% ?- X ∈ {1,2,3}, X = 2, stored.
% X = 2

% ?- X = 4, X ∈ {1,2,3}, stored.
% No

% ?- X = 2, X ∈ {1,2,3}, stored.
% X = 2

% ?- X ∈ {1,2,3}, X = Y, Y ∈ {2,3,4}, stored.
% Y ∈ {2,3}.
% Y = X

% ?- X ∈ {1,2,3}, Y ∈ {2,3,4}, X = Y, stored.
% Y ∈ {2,3}.
% Y = X

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

% ?- X + Y ≡ Z, X = 1, Y = 2, stored.
% X = 1,
% Y = 2,
% Z = 3.

% ?- X = 1, X + Y ≡ Z, Y = 2, stored.
% X = 1,
% Y = 2,
% Z = 3.

% ?- X = 1, Y = 2, X + Y ≡ Z, stored.
% X = 1,
% Y = 2,
% Z = 3.

% ?- X + Y ≡ Z, Z = X, stored.
% Y = 0,
% Z = X

% ?- Z = X, X + Y ≡ Z, stored.
% Z = X,
% Y = 0

% ?- X + Y ≡ 3, Y + Z ≡ 5, X + Z ≡ 6, Y = 1, stored.
% X = 2,
% Y = 1,
% Z = 4

% ?- X + Y ≡ 3, Y + Z ≡ 5, X + Z ≡ 6, Y = 2, stored.
% No```