Prolog Text addensure

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

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

% addvv(+Atom, +Atom, +Atom)
% addvv(X, Y, Z) == X+Y = Z
:- forward addvv/3.
attr_bound(X, 0) &:-
   &- addvv(X, Y, Y), !.
attr_bound(Y, 0) &:-
   &- addvv(X, Y, X), !.
addvv(T, Y, Z) &:-
   &- addvv(X, Y, Z) && sys_bound_var(X), sys_melt_var(X, H), var(H), !, sys_freeze_var(H, T).
addvv(X, T, Z) &:-
   &- addvv(X, Y, Z) && sys_bound_var(Y), sys_melt_var(Y, H), var(H), !, sys_freeze_var(H, T).
addvv(X, Y, T) &:-
   &- addvv(X, Y, Z) && sys_bound_var(Z), sys_melt_var(Z, H), var(H), !, sys_freeze_var(H, T).
addcv(Y, C, Z) &:-
   &- addvv(X, Y, Z) && sys_bound_var(X), sys_melt_var(X, C), integer(C), !.
addcv(X, C, Z) &:-
   &- addvv(X, Y, Z) && sys_bound_var(Y), sys_melt_var(Y, C), integer(C), !.
addvc(X, Y, C) &:-
   &- addvv(X, Y, Z) && sys_bound_var(Z), sys_melt_var(Z, C), integer(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.
attr_refer(X, Y) &:-
   &- addcv(X, 0, Y), !.
zero &:-
   &- addcv(X, _, X), !.
addcv(Z, C, Y) &:-
   &- addcv(X, C, Y) && sys_bound_var(X), sys_melt_var(X, H), var(H), !, sys_freeze_var(H, Z).
addcv(X, C, 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.
addcv(Z, C, Y) &:-
   refer(X, Z) && &- addcv(X, C, Y).
addcv(X, C, Z) &:-
   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(+Atom, +Atom, +Elem)
% addvc(X, Y, C) == X+Y = C
:- forward addvc/3.
addvc(Z, Y, C) &:-
   &- addvc(X, Y, C) && sys_bound_var(X), sys_melt_var(X, H), var(H), !, sys_freeze_var(H, Z).
addvc(X, Z, C) &:-
   &- 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.
addvc(Z, Y, C) &:-
   refer(X, Z) && &- addvc(X, Y, C).
addvc(X, Z, 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),
   post(addvv(A,B,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),
   post(addvc(A,B,Z)).
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),
   post(addcv(A,Y,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),
   post(addcv(A,Y,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) :-
   addvv(A, B, C),
   sys_melt_var(A, X),
   sys_melt_var(B, Y),
   sys_melt_var(C, Z).
sys_pretty_event(X+Y ≡ Z) :-
   addcv(A, Y, C),
   sys_melt_var(A, X),
   sys_melt_var(C, Z).
sys_pretty_event(X+Y ≡ Z) :-
   addvc(A, B, 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

Kommentare