Attributed Variables

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 [6] and ECL$^i$PS$^e$ [3].

Attributes of variables are compound terms whose arguments are the actual attribute values. They are defined with a declaration

:- attribute $AttributeSpec, \ldots, 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).

get_atts(-Var, ?AccessSpec)

atts
Gets the attributes of Var according to AccessSpec. If AccessSpec is unbound, it will be bound to a list of all set attributes of Var. Non-variable terms in Var cause a type error. AccessSpec is either +(Attribute), -(Attribute), or a list of such (prefix + may be dropped for convenience). The prefixes in the AccessSpec have the following meaning:

+(Attribute):

The corresponding actual attribute must be present and is unified with Attribute.

-(Attribute):

The corresponding actual attribute must be absent. The arguments of Attribute are ignored, only the name and arity are relevant.

put_atts(-Var, +AccessSpec)

atts
Sets the attributes of Var according to AccessSpec. Non-variable terms in Var cause a type error. The effect of put_atts/2 are undone on backtracking. The prefixes of AccessSpec have the following meaning:

+(Attribute):

The corresponding actual attribute is set to Attribute. If the actual attribute was already present, it is simply replaced.

-(Attribute):

The corresponding actual attribute is removed. If the actual attribute is already absent, nothing happens.

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:

attv_unify(-Var, +Value)

machine
This is an internal built-in predicate which is supposed to be used only in the definition of verify_attributes/2. It binds the attributed variable Var to Value without triggering attributed variable interrupt. Value is a non-variable term or another attributed variable.

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
    | ?-