Prolog Text add

/**
 * Prolog code for the little solver.
 * With a union find element.
 * With add constraints.
 *
 * 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, _).

/********************************************************/
/* Add Constraints                                      */
/********************************************************/

% addvv(+Atom, +Atom, +Atom)
% addvv(X, Y, Z) == X+Y = Z
:- forward addvv/3.
bound(X, 0) &:-
   &- addvv(X, Y, Y), !.
bound(Y, 0) &:-
   &- addvv(X, Y, X), !.
addvv(T, Y, Z) &:-
   &- addvv(X, Y, Z) && refer(X, T), !.
addvv(X, T, Z) &:-
   &- addvv(X, Y, Z) && refer(Y, T), !.
addvv(X, Y, T) &:-
   &- addvv(X, Y, Z) && refer(Z, T), !.
addcv(Y, C, Z) &:-
   &- addvv(X, Y, Z) && bound(X, C), !.
addcv(X, C, Z) &:-
   &- addvv(X, Y, Z) && bound(Y, C), !.
addvc(X, Y, C) &:-
   &- addvv(X, Y, Z) && bound(Z, C), !.
addvv(T, Y, Z) &:-
   refer(X, T) && &- addvv(X, Y, Z).
addvv(X, T, Z) &:-
   refer(Y, T) && &- addvv(X, Y, Z), X \== Y.
addvv(X, Y, T) &:-
   refer(Z, T) && &- addvv(X, Y, Z), X \== Z, Y \== Z.
addcv(Y, C, Z) &:-
   bound(X, C) && &- addvv(X, Y, Z).
addcv(X, C, Z) &:-
   bound(Y, C) && &- addvv(X, Y, Z), X \== Y.
addvc(X, Y, C) &:-
   bound(Z, C) && &- addvv(X, Y, Z), X \== Z, Y \== Z.

% addcv(+Atom, +Elem, +Atom)
% addcv(X, C, Y) == X+C = Y
:- forward addcv/3.
refer(X, Y) &:-
   &- addcv(X, 0, Y), !.
zero &:-
   &- addcv(X, _, X), !.
addcv(Z, C, Y) &:-
   &- addcv(X, C, Y) && refer(X, Z), !.
addcv(X, C, 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.
addcv(Z, C, Y) &:-
   refer(X, Z) && &- addcv(X, C, Y).
addcv(X, C, Z) &:-
   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(+Atom, +Atom, +Elem)
% addvc(X, Y, C) == X+Y = C
:- forward addvc/3.
addvc(Z, Y, C) &:-
   &- addvc(X, Y, C) && refer(X, Z), !.
addvc(X, Z, C) &:-
   &- 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.
addvc(Z, Y, C) &:-
   refer(X, Z) && &- addvc(X, Y, C).
addvc(X, Z, 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

% ?- post(addvv(x,y,z)), post(refer(z,x)), posted.
% refer(z, x).
% bound(y, 0).
% Yes

% ?- post(refer(z,x)), post(addvv(x,y,z)), posted.
% refer(z, x).
% bound(y, 0).
% Yes

% ?- post(addvc(x,y,3)), post(addvc(y,z,5)), post(addvc(x,z,6)), post(bound(y,1)), posted.
% bound(y, 1).
% bound(z, 4).
% bound(x, 2).
% Yes

% ?- post(addvc(x,y,3)), post(addvc(y,z,5)), post(addvc(x,z,6)), post(bound(y,2)), posted.
% No

Comments