Attributed variables are a special data type that associates variables with arbitrary attributes as well as supports extensible unification. Attributed variables have proven to be a flexible and powerful mechanism to extend a classic logic programming system with the ability of constraint solving. They have been implemented in SICStus 1.1 [13] and ECLiPSe [5].
Attributes of variables are compound terms whose arguments are the actual attribute values. They are defined with a declaration
:- attribute AttributeSpec,..., AttributeSpec.
where each Attributes has the form Functor/Arity. Each file can have at most one such declaration.
Having declared some attribute names, these attributes can be added, updated and deleted from unbound variables using the following two predicates (get_atts/2 and put_atts/2) defined in the module atts. For each declared attribute name, any variable can have at most one such attribute (initially it has none).
In a file that contains an attribute declaration, one has an opportunity to extend the default unification algorithm by defining the following predicate:
verify_attributes(-Var, +Value)
This predicate is called whenever an attributed variable Var (which has at least one attribute) is about to be bound to Value (a non-variable term or another attributed variable). When Var is to be bound to Value, a special interrupt called attributed variable interrupt is triggered, and then XSB's interrupt handler (written in Prolog) calls verify_attributes/2. If it fails, the unification is deemed to have failed. It may succeed non-deterministically, in which case the unification might backtrack to give another answer.
If Value is a non-variable term, verify_attributes/2 usually inspects the attributes of Var and check whether they are compatible with Value and fail otherwise. If Value is another attributed variable, verify_attributes/2 will typically merge the attributes of Var and Value, bind Var to Value, and then update their attributes. In either case, verify_attributes/2 may determine the attributes of Var (or Value) by calling get_atts/2.
The predicate verify_attributes/2 is also called user-defined unification handler. To help users define this handler, the following predicate is provided in module machine, which can be used to bind an attributed variable to an arbitrary term (might be another attributed variable) without triggering attributed variable interrupt and thus another level call of verify_attributes/2:
Here, by giving the implementation of a simple finite domain constraint solver (see the file fd.P below), we show how these predicates for attributed variables can be used. In this example, only one attribute is declared: dom/1, and the value of this attribute is a list of terms.
%% File: fd.P
%%
%% A simple finite domain constrait solver implemented using attributed
%% variables.
:- import put_atts/2, get_atts/2 from atts.
:- import attv_unify/2 from machine.
:- import member/2 from basics.
:- attribute dom/1.
verify_attributes(Var, Value) :-
get_atts(Var, dom(Da)),
(var(Value) % Value is an attributed variable
-> get_atts(Value, dom(Db)), % has a domain
intersection(Da, Db, [E|Es]), % intersection not empty
(Es = [] % exactly one element
-> attv_unify(Var, Value), % bind Var to Value
attv_unify(Var, E) % bind Var (and Value) to E
; attv_unify(Var, Value), % bind Var to Value
put_atts(Value, dom([E|Es])) % update Var's (and Value's)
% attributes
)
; member(Value, Da), % is Value a member of Da?
attv_unify(Var, Value) % bind Var to Value
).
intersection([], _, []).
intersection([H|T], L2, [H|L3]) :-
member(H, L2), !,
intersection(T, L2, L3).
intersection([_|T], L2, L3) :-
intersection(T, L2, L3).
domain(X, Dom) :-
var(Dom), !,
get_atts(X, dom(Dom)).
domain(X, List) :-
List = [El|Els], % at least one element
(Els = [] % exactly one element
-> X = El % implied binding
; put_atts(Fresh, dom(List)), % create a new attributed variable
X = Fresh % may call verify_attributes/2
).
show_domain(X) :- % print out the domain of X
var(X), % X must be a variable
get_atts(X, dom(D)),
write('Domain of '), write(X),
write(' is '), writeln(D).
The output of some example queries are listed below, from which we can see how attributed variables are unified using verify_attributes/2:
| ?- [fd].
[fd loaded]
yes
| ?- domain(X,[5,6,7,1]), domain(Y,[3,4,5,6]), domain(Z,[1,6,7,8]),
show_domain(X), show_domain(Y), show_domain(Z).
Domain of _h474 is [5,6,7,1]
Domain of _h503 is [3,4,5,6]
Domain of _h532 is [1,6,7,8]
X = _h474
Y = _h503
Z = _h532
yes
| ?- domain(X,[5,6,7,1]), domain(Y,[3,4,5,6]), domain(Z,[1,6,7,8]),
X = Y, show_domain(X), show_domain(Y), show_domain(Z).
Domain of _h640 is [5,6]
Domain of _h640 is [5,6]
Domain of _h569 is [1,6,7,8]
X = _h640
Y = _h640
Z = _h569
yes
| ?- domain(X,[5,6,7,1]), domain(Y,[3,4,5,6]), domain(Z,[1,6,7,8]),
X = Y, Y = Z.
X = 6
Y = 6
Z = 6
yes
| ?-