Attributed Variables in Prolog

The most important thing you need to know about attributed variables is that Prolog application programmers normally need not use them. This chapter is intended mainly for Prolog library authors who want to improve or implement more declarative language constructs.

Attributed variables are a low-level mechanism for implementing declarative constructs. However, when considered in isolation, they have the potential to prevent and run counter to the declarative reading we want to apply to pure Prolog programs.

For this reason, attributed variables should only be used as a building block for higher-level mechanisms.

If you are a Prolog library author, your interest in this topic may be warranted. To application programmers, my recommendation is to use existing libraries that provide equivalent functionality under more declarative wrappers.

Prolog implementors may be interested in the Minato task and in the Equivalence task to assess the generality of their interface predicates.

How it started

Already the first Prolog system, sometimes called Prolog 0, supported the constraint dif/2.

To Prolog implementors and practitioners, the question soon became: By which general mechanism can we we implement further constraints conveniently, correctly and efficiently?

The first mechanism to solve this was proposed by Ulrich Neumerkel in his 1990 paper Extensible Unification by Metastructures.

Here is a salient quote from the paper:

When considering existing approaches of extensions to syntactic unification, we observe: highly specialized implementations, where the unification algorithm cannot be manipulated by the user (e.g. [Col87,JaLa87,vH89]), approaches too general to be implemented efficiently and too general to allow the reuse of existing Prolog programs [Ko84], or extensions allowing definitions in a procedural language [CLiST89] only.

Our approach focuses on a sufficient abstract yet efficient interface, which permits to write implementations of constraints in Prolog, neglecting the actual representation of the constrained variables. Metastructures are applicable, but not restricted to the following areas:

...

Among the projected use cases, stream-based side effect free I/O is already mentioned in the paper. This is now available in library(pio).

How it continued

Christian Holzbaur, who back then was a very close colleague of Ulrich Neumerkel, used metastructures in his 1990 dissertation, Specification of Constraint Based Inference Mechanism through Extended Unification, in which he implemented CLP(Q).

After this experience, and having observed some shortcomings of metastructures, Holzbaur proposed an alternative yet very strongly related mechanism called attributed variables.

Holzbaur later published a comparison paper, Metastructures vs. Attributed Variables in the Context of Extensible Unification.

The proposal by Christian Holzbaur was adopted in SICStus Prolog, one of the leading systems in the area of constraint programming.

To quote from the Attributed Variables section in the SICStus documentation:

This package implements attributed variables. It provides a means of associating with variables arbitrary attributes, i.e. named properties that can be used as storage locations as well as to extend the default unification algorithm when such variables are unified with other terms or with each other.

This facility was primarily designed as a clean interface between Prolog and constraint solvers, but has a number of other uses as well. The basic idea is due to Christian Holzbaur and he was actively involved in the final design. For background material, see the dissertation [Holzbaur 90].

If you are interested in more information about the origin of these developments, I recommend you ask the involved people in person.

The same interface is also implemented in other Prolog systems, such as in Scryer Prolog and Ciao.

What we have now

The concrete features of attributed variables vary between Prolog systems. However, in all systems that provide attributed variables, we have essentially the following features at our disposal:

We can attach information to variables.
This information can be taken into account when a variable is being unified.
This information can be displayed in answers on the Prolog toplevel.

In the following, we consider one specific implementation of these features in more detail.

Attributed variables in Scryer Prolog

Preliminaries

To illustrate the key concepts of attributed variables, we consider Scryer Prolog because it is freely available, and it implements the same interface for attributed variables as SICStus Prolog.

I would like to stress again that attributed variables normally need not and also should not be used in typical Prolog applications. Instead, and also in Scryer Prolog, attributed variables are available to implement features from Constraint Logic Programming such as dif/2 and CLP(ℤ), and you should use these higher-level predicates instead in typical use cases.

When working with attributed variables, you need to know 3 kinds of interface predicates, in accordance with the features outlined above:

Predicates for adding, changing and removing attributes.
Predicates to reason about the unification of variables that have attributes attached.
Predicates that let you display attributes on the toplevel in some form.

We now consider these kinds of predicates in turn. For more information, see especially Attributed Variables in the SICStus Prolog manual. Even though the details differ in other Prolog systems, the kinds of predicates are the same also in other systems.

Adding and changing attributes

An attributed variable is a relation between a variable, a module and a value.

With the interface of SICStus and Scryer Prolog, we declare attributes in a module with the attribute/1 directive, using Name/Arity pairs:

:- attribute Name₁/Arity₁, Name₂/Arity₂, ..., Name_n/Arity_n.

This directive is made available via library(atts).

An attribute can be added and changed via:

Module:put_atts(Var, AccessSpec):
If AccessSpec is of the form +(Attribute), then the corresponding attribute is set to the specified value. If AccessSpec is of the form -(Attribute), then the attribute is removed. For convenience, the wrapper + can be omitted.

To try this, let us define a sample module, say attrmod.pl, where we declare the attribute a/1:

:- module(attrmod, []).

:- use_module(library(atts)).

:- attribute a/1.

After consulting the file, we can use the toplevel to attach attributes to variables. For example:

?- attrmod:put_atts(X, a(test)).
   attrmod:put_atts(X,a(test)).

We see that in response, the Prolog toplevel simply repeats what we said. Thus, the toplevel retains the important invariant that the answer is declaratively equivalent to the original query. In this concrete case, all there is to say is: The attribute a(test) is associated with the variable X in module attrmod, and that's exactly what this answer states. We call a variable that has an attribute attached an attributed variable.

Importantly, when you use put_attr/3 repeatedly with the same variable and module, then any previously attached value is simply overwritten. For example:

?- attrmod:put_atts(X, a(hi)),
   attrmod:put_atts(X, a(ho)).
   attrmod:put_atts(X,a(ho)).

Thus, after these two calls, a(ho) is the single remaining attributed that is attached to X in module attrmod.

We say that put_atts/2 destructively modifies an attribute. For this reason, you can use put_atts/2 also as a somewhat more declarative and less error-prone alternative to setarg/3.

Note also that the effect of put_atts/2 is undone on backtracking. For example:

?- ( attrmod:put_atts(X, a(hello))
   ; true
   ).
   attrmod:put_atts(X,a(hello))
;  true.

When the alternative is reported, we see from the absence of any goals besides true that no more attribute is attached to X. For this reason, assigning attributes to variables blends well with Prolog's built-in search strategy, and is similar to unification in that respect. We say that the modification is backtrackable.

Unification of attributed variables

The key distinction between variables and attributed variables is what happens at the time of unification.

Attributed variables are special in that an extensible predicate is automatically invoked when they are unified. In SICStus and Scryer, the particular predicate that is invoked is verify_attributes/3 residing in the module where the attribute is attached. You, the Prolog programmer, can provide a custom definition of this predicate, and it will be automatically invoked by the Prolog engine when a variable that has attributes attached is being unified.

For example, let us define a very rudimentary version of verify_attributes/3 in our module attrmod:

verify_attributes(X, Y, _) :- throw(cannot_unify(X,Y)).

With this definition, which simply throws an exception when it is invoked, we get for example:

?- attrmod:put_atts(X, a(1)),
   attrmod:put_atts(Y, a(2)),
   X = Y.
   throw(cannot_unify(_397,_399)).

M:verify_attributes(-Var, +Value, -Goals):

This predicate is called whenever a variable Var that might have attributes in Module is about to be bound to Value (it might have none). The unification resumes after the call to verify_attributes/3. Value is a nonvariable, or another attributed variable. Var might have no attributes present in Module.

verify_attributes/3 is called before Var has actually been bound to Value. If it fails, the unification is deemed to have failed. It may succeed nondeterminately, in which case the unification might backtrack to give another answer. It is expected to return, in Goals, a list of goals to be called after Var has been bound to Value. Finally, after calling Goals, any goals blocked on Var are called.

verify_attributes/3 may invoke arbitrary Prolog goals, but Var should not be bound by it. Binding Var will result in undefined behavior. If Value is a nonvariable, verify_attributes/3 will typically inspect the attributes of Var and check that they are compatible with Value and fail otherwise. If Value is another attributed variable, verify_attributes/3 will typically copy the attributes of Var over to Value, or merge them with Value’s, in preparation for Var to be bound to Value. In either case, verify_attributes/3 may determine Var’s current attributes by calling get_atts(Var, List) with an unbound List.

In the case when a single unification binds multiple attributed variables, first all such bindings are undone, then the following actions are carried out for each relevant variable:

For each relevant module M, M:verify_attributes/3 is called, collecting a list of returned Goals.
The variable binding is redone.
Any Goals are called.
Any blocked goals are called.

First, let us try out what the documentation states: For example, let us make the unification fail.

verify_attributes(_, _, _) :- false.

Example query and answer:

?- attrmod:put_atts(X, a(n(1))),
   attrmod:put_atts(Y, a(n(2))),
   X = Y.
   false.

OK, this works as advertised. In this example and the following, we use compound terms of the form n(N) to represent the integer N. We could also use the integers directly instead. However, this would risk ending up with a defaulty representation, and also prevent us from symbolically distinguishing attributes from variables in the code below.

Second, let us modify the involved attributes upon unification. If a unification involves two (or more) variables, we must state how such a unification affects the involved variables.

Let us extend the example from above: In the above case, we have associated the Prolog terms n(1) and n(2) with the variables X and Y, using the attribute a/1. To gather experience with the interface, let us say that upon unification of two variables with respective attributes a(n(A)) and a(n(B)), where A and B are integers, we want to attach the new attribute a(n(C)) to the resulting (single) variable, where C is the sum of A and B.

To accomplish this, we need a way to reason about existing attributes of variable. The predicate get_atts/2 is available for this purpose:

get_atts(Var, AccessSpec):
If AccessSpec is of the form +(Attribute), then the corresponding attribute must be present and is unified with Attribute. For convenience, the wrapper + can be omitted.

Thus, we shall now implement the following steps:

Upon unification of two variables with attributes from module attrmod, fetch their a/1 attributes.
Compute the sum of the integers in the attributes, using integer arithmetic.
Attach the sum as the new attribute.

In Prolog, this becomes:

verify_attributes(Var, Value, []) :-
        get_atts(Var, a(n(A))),
        get_atts(Value, a(n(B))),    % step (1)
        C #= A + B,                  % step (2)
        put_atts(Value, a(n(C))).    % step (3)

Now, let us try it out:

?- attrmod:put_atts(X, a(n(1))),
   attrmod:put_atts(Y, a(n(2))),
   X = Y.
   X = Y, attrmod:put_atts(Y,a(n(3))).

And indeed this works: After the unification, a(n(3)) is associated with the resulting single variable, which is X or, equivalently, Y, and 3 is the result of 1+2.

The following yields an uninstantiation error, because because get_atts/2—which is used in our definition of verify_attributes/3)—requires its first argument to be a variable, whereas we use the atom b:

?- attrmod:put_atts(X, a(n(1))),
   X = b.
   error(uninstantiation_error(b),get_atts/2).

In fact, with the above definition of verify_attributes/3, only very specific kinds of unifications will succeed. In particular, every unification with a ground value will yield an uninstantiation error. However, in actual constraint systems, we are very interested in ground terms, because they typically represent concrete solutions.

Let us therefore generalize the above definition of verify_attributes/3 (in module attrmod) in such a way that it still illustrates a key feature of the whole interface, namely the ability to selectively veto unifications. For example, in our concrete case, let us allow unifications with a concrete integer iff that integer matches the associated integer value that is stored in the involved variable's attribute.

We hence must distinguish two different cases when two terms X and Y are unified. Let us consider it from the perspective of X, i.e., let us suppose that verify_attributes/3 is invoked with X as the first argument. (Of course, the other case is completely symmetric, but we need to draw this distinction to discuss the cases.) Then, either Y is an integer k. In that case, we must veto the unification (i.e., fail) if k does not match the integer that is stored in the attribute of X. Or Y is an attributed variable. In that case, we proceed exactly as previously: We compute the sum of the two integers that are stored in the attributes of the involved variables, and associate that sum with the unified variable.

In Prolog, we can express this distinction with the built-in predicate integer/1:

verify_attributes(Var, Value, []) :-
        get_atts(Var, a(n(A))),
        (   integer(Value) ->
            Value =:= A
        ;   get_atts(Value, a(n(B)))
            C #= A + B,
            put_atts(Var, -a(n(_))),
            put_atts(Value, a(n(C)))
        ).

Here are a few sample queries and their results:

?- attrmod:put_atts(X, a(n(1))), X = 1.
   X = 1.

?- attrmod:put_atts(X, a(n(1))), X = 3.
   false.

?- attrmod:put_atts(X, a(n(1))),
   attrmod:put_atts(Y, a(n(2))),
   X = Y,
   X = 3.
   X = Y, Y = 3.

Thus, everything seems to work as intended. We have successfully created a simplistic constraint solver, which admittedly has quite peculiar semantics but implements what we have outlined. However, this concrete solver has a very severe declarative flaw, which becomes apparent if you eliminate the goal X = Y in the above conjunction:

?- attrmod:put_atts(X, a(n(1))),
   attrmod:put_atts(Y, a(n(2))),
   X = 3.
   false.

In this case, generalizing a query (by removing a constraint) has created a more specific program (which is now equivalent to false). This violates elementary properties we expect from logic programs and prevents for example declarative debugging.

The key takeaway from this is that the interface for attributed variables does not by itself provide any guarantees of the resulting constraint solver. You, the programmer, must implement your system in such a way that desirable properties are preserved in resulting programs. We return to this point below.

For now, let us conclude this section with a more interesting and also more realistic example: We now implement a simplistic constraint solver over finite domains, where the attribute of each involved variable is an ordered list of elements, representing the admissible domain of the variable.

A suitable unification hook for such a constraint solver could look like this:

verify_attributes(Var, Other, []) :-
        (   get_atts(Var, domain(Dom1)) ->
            (   var(Other),
                get_atts(Other, domain(Dom2)) ->
                ord_intersection(Dom1, Dom2, Dom),
                dif(Dom, []),
                (   Dom = [Value] ->
                    Other = Value
                ;   put_atts(Other, domain(Dom))
                )
            ;   ord_memberchk(Other, Dom1)
            )
        ;   true
        ).

Informally, we can read this as:

If Var has an associated domain Dom1, and Other is a variable that has an associated domain Dom2, then we build the intersection Dom = Dom1 ∩ Dom2. This ordered list contains all elements that are admissible for both variables that have been unified.
We only proceed if Dom is different (dif/2) from the empty list [], and hence there is at least one remaining domain element that is admissible for the resulting unified variable.
If Dom has only a single remaining element, then that element must be equal to the unified variable (because there is no other choice).
Otherwise, assign the intersection Dom as an attribute to the unified variable.
If Other has no associated domain, then the unification is only admissible if Other is a member of the domain Dom1.

In addition, let us use the following definition to associate a variable with its domain:

domain(X, List) :-
        list_to_ord_set(List, Dom),
        put_atts(X, domain(Dom)).

With these definitions in place, we can query:

?- domain(X, "abc"),
   domain(Y, "cde"),
   X = Y.

In response, we get the concrete solution:

   X = Y, Y = c.

This works because upon unification, the hook is invoked, builds the intersection of the two domains, determines that they have only a single element in common, and hence unifies the resulting variable with that element. Note that X and Y have become completely indistinguishable. Unification has truly unified them.

Exercise (hard): The following property is highly desirable for a constraint solver. Prove that it holds in this case, or provide a counterexample:
For every Prolog query Q that consists only of domain/2 and (=)/2 goals, removing one of the goals makes the resulting query Q' at least as general as Q, in the sense that the set of solutions of Q is a subset of those of Q'.

Displaying attributes

In an actual constraint solver, we are not content with answers that look like attrmod:put_atts(X,a(test)). Instead, what we expect from a constraint solver is a representation of remaining attributes that is meaningful to humans. Thus, we expect a constraint solver to emit more high-level Prolog goals as answers, which have a well-defined meaning no matter how they are internally implemented.

For this purpose, there is the DCG nonterminal M:attribute_goals//1. In Scryer Prolog, you can define this nonterminal in a module M, and it is automatically invoked by the Prolog engine for each variable X that has an attribute in M. It is defined as follows:

M:attribute_goals(V):
This is a DCG nonterminal describing a list of Prolog goals which caused the presence of V's attributes in module M. This means that executing these goals should lead to equivalent attributes on X in module M.

For example, let us apply this feature to our simple finite domain constraint solver that we considered above. It only has a single interface predicate, called domain/2. Ideally, answers that are reported on the toplevel should only use public interface predicates, since their meaning is known to users.

Thus, it remains for us to translate attributes to so-called residual goals, using the above nonterminal. In the concrete case above, we can do it like this:

attribute_goals(Var) -->
        (   { get_atts(Var, domain(Dom)) } ->
            [domain(Var, Dom)]
        ;   []
        ).

This simply fetches the attribute, and describes a list with a single goal. Here is an example that illustrates that this predicate is automatically invoked by the toplevel when reporting answers:

?- domain(X, "abc").
   domain(X, "abc").

It also works for more complex queries:

?- domain(X, "abc"),
   domain(Y, "bcd"),
   X = Y.
   X = Y,
   domain(Y, "bc").

Using this mechanism, you can always translate internal attributes to Prolog goals that are more meaningful to users.

The toplevel provides this functionality by internally invoking the predicate copy_term/3. This predicate creates a copy of variables that may be involved in constraints, and uses attribute_goals//1 to create a list of goals that, when called, create equivalent attributes on the copy. You can use copy_term(X, X, Gs) to reason about the constraints Gs that X is involved in. Note that a list of goals is used, since this is a clean representation of goals that allows convenient further analysis.

Pitfalls and Errands

Working with attributed variables is very error-prone. In my experience, no amount of education, research and practice saves one from making quite elementary mistakes when working with them.

It is all the more important that system implementors make the lives of Prolog programmers as easy as possible by providing interfaces that make certain classes of errors impossible. Implementors are sometimes tempted to provide low-level interfaces to gain performance at the cost of convenience and correctness.

For example, in 2002, Bart Demoen published a highly influential paper called Dynamic attributes, their hProlog implementation, and a first evaluation.

Bart Demoen is an extremely prolific and highly regarded member of the Prolog community, and several systems therefore adopted the approach he proposed.

The interface he proposed and implemented deliberately falls short in a critical respect. I quote from the paper and highlight the key passages:

4 Basic choice III: no pre_unify

The most profound difference between attributed variables in SICStus Prolog and ECLiPSe is the state of the variable at the moment the unifcation handler is called.

As an example: assume the attributed variable X has one attribute A (with module user) and X is unifed with the integer 666. In SICStus Prolog, verify_attributes is called with X still being unbound. In ECLiPSe, the unify handler is called with A as an argument - X has been bound to 666 already.

The SICStus Prolog behavior follows [6] which claims that it is important to have the variables as if not yet bound.

ECLiPSe people on the other hand (Joachim Schimpf) claim that this is not needed.

We do not want to take a stand in this issue: we had implemented at some point the full SICStus Prolog behavior (but on dynamic attributes of course) and were not convinced that the extra implementation complexity was worth the gain. However, we were not impressed by the manuals of SICStus Prolog and ECLiPSe, which claim that binding the X during a pre_unify yields unexpected results: in our opinion (and experience), it just shows that full support for pre_unify is too cumbersome to implement and maintain in a full system like SICStus Prolog or ECLiPSe. So we switched to the ECLiPSe model, but without the compromise to support pre_unify for compatibility reasons: Occam's razor is a blessing :-)

Unfortunately, despite the smiley, the above passage was taken seriously by Prolog implementors, and this limited interface is what for example SWI-Prolog now provides.

Occam's razor

Occam's razor, in its most popular version, states that "Entities are not to be multiplied without necessity".

I ask you, then, why do we have 3 different interfaces for attributed variables, two of which are clearly less general than the other?

A conservative approach, more than 20 years after the work of Neumerkel and Holzbaur, could look as follows:

Let us consider 4 widely used Prolog systems, such as SICStus, GNU-Prolog, ECLiPSe and SWI, and 4 widely used types of constraints: CLP(H), CLP(FD), CLP(B) and CLP(Q).

SICStus supports 4 of them. SWI supports 3 of them. ECLiPSe and GNU-Prolog support 2 of them. Of these systems, which has the most general interface for attributed variables? Take this system as the one we want to strive towards. By Occam's razor, chances are that they have only done what is needed to support the constraint solvers they provide.

The core shortcoming of the SWI-Prolog interface for attributed variables is that verify_attributes/3 is not supported, and only a much less general predicate called attr_unify_hook/2 is provided instead. Critically, attr_unify_hook/2 is only invoked after a variable has already been unified.

This may seem quite innocent at first: After all, the (previous) attribute of that variable is an argument of attr_unify_hook/2, so everything we need to know is available, right? Let us suppose that this is the case (although it isn't, as we discuss below). Even then, several variables may at once become instantiated, for example via a goal like [X,Y] = [0,1]. It is easy to see that if such a unification involves n variables, then there are at least 2ⁿ different kinds of possible instantiation patterns that may arise in a single unification. Nobody is able to think all cases through completely. An example of a situation that can arise due to simultaneous unifications is explained in commit 9c8ea20b7. A highly experienced expert in constraint programming ran into the same issue in his own implementation of the dif/2 constraint, even though it is one of the simplest and most elementary constraints Prolog systems provide. A few years later, another mistake was found and corrected in the implementation of SWI-Prolog's dif/2 constraint, then another mistake was found and corrected, then another mistake was found and corrected, and to this day, dif/2 remains incorrectly implemented in SWI-Prolog, even for acyclic terms.

But still, maybe the interface is not to blame, right? Maybe we have only not tried hard enough to work with the interface. After all, only poor craftspeople blame their tools, right?

Wrong! If an interface not only makes possible but downright enforces such mistakes, then it is time to reconsider the interface. Normally, such issues should be reason enough to seriously rethink the interface. However, in the Prolog community, the error-prone nature of this interface is not by itself enough reason for change. Traditionally, it is performance that matters most, and who cares about correctness as long as your system is fast, right? Therefore, I give you a second argument:

The SWI-Prolog interface is not sufficient to express important classes of constraint solvers. Consider again the unification [X,Y] = [0,1]. This means that the attributes of both variables become unavailable at the same time. It is true: When attr_unify_hook/2 is run for X, you have access to its former attribute. But at that time, you can no longer access the former attribute of Y via get_attr/3, and in fact you can no longer even tell that Y was a variable. The next section shows an example where this is needed, but not possible.

Minato task

Let us now consider a specific task, which is easily encountered when implementing a CLP(B) system based on Zero-suppressed decision diagrams (ZDDs). ZDDs are a very important data structure, and Donald Knuth has called them "the most beautiful construct in computer science" in a talk.

I call this task Minato task, in honor of 湊　真一(みなと　しんいち), MINATO Shin-ichi, the inventor of ZDDs (see Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems). We shall use this task to determine whether a Prolog system's interface predicates for attributed variables are general enough to naturally express a certain class of constraints that are of great practical importance.

A ZDD is a decision diagram. This means that we can simply follow the lines of the diagram to arrive at a truth value. The nodes of a ZDD are branching variables: If a variable is 1, then we take the plain line, and if a variable is 0, then we take the dotted line. In that respect, a ZDD is like a Binary Decision Diagram (BDD). However, a ZDD is interpreted with the following distinguishing twist: If a variable does not appear on a path that leads to true, then that variable must be equal to 0.

For example, here is a ZDD that represents the truth value of the Boolean function X xor Y:

We can represent a ZDD as a Prolog term. The truth values true and false can be represented as atoms, and an inner node can be represented as ( X → Then ; Else ), where:

X is a branching variable
Then and Else are nodes.

In analogy to Prolog syntax, Then is taken to mean that X is 1 (true), and Else means that X is 0 (false).

For example, the ZDD above can be represented as:

( X -> true ; ( Y -> true ; false ) )

Both variables, X and Y, participate in this decision diagram. Therefore, to reason about such constraints in Prolog, it is natural to attach this diagram as an attribute to both variables. Here is how we can do this with put_attr/3:

?- ZDD = ( X -> true ; ( Y -> true ; false ) ),
   put_attr(X, zdd, ZDD),
   put_attr(Y, zdd, ZDD).

We now consider a series of unifications, and you tell us how you use your system's interface predicates to arrive at the correct truth values for X and Y.

As a start, consider the following unification: X = 0.

You reply for example with: That's easy, I simply take a look at the decision diagram, which now is:
```
( 0 -> true ; ( Y -> true ; false ) )
    
```
Since the first branching variable is now instantiated, it is clear which branch we must take, so we can replace the whole diagram with:
```
( Y -> true ; false )
    
```
From there, further unifications are easy.
Here is a slightly harder case: X = 1.

This means that the ZDD could be reduced to:
```
true
    
```
But wait, that's not all! As we explained, a variable that does not appear in a path to true must be equal to 0. In this case, Y is such a variable, so we must set it to 0. But how? Well, one way to do this is to keep track of all variables that have so far appeared in constraints, and to represent the ZDD for example as a pair of terms, such as:
```
( X -> true ; ( Y -> true ; false ) )-[X,Y]
    
```
This means that in the above case, we would end up with:
```
true-[1,Y]
    
```
and from there it is easy to state that Y = 0.
Here is a third case: [X,Y] = [1,1].

And you solve the Minato task by telling us how your interface predicates can be used to determine that this unification is not admissible due to the constraints the variables are involved in.

For comparison, the unification must succeed if the ZDD is for example:
```
ZDD = ( X -> Inner ; Inner ), Inner = ( Y -> true ; false )
        
```
This illustrates that you cannot look into other branches of the ZDD to recover any information about Y.

Note especially the following: There is no doubt that this issue can be solved somehow, even with a very primitive interface for attributed variables. One example would be to duplicate all kinds of attributes so that they are available redundantly in all data structures that occur anywhere. However, an interface that demands such contortions cannot be taken seriously. In addition, and especially when reasoning with decision diagrams, memory is often the primary bottleneck, and we therefore want to avoid copying data also for this reason.

In my view, the key questions are:

How naturally can an interface be used to solve such tasks?
How likely are mistakes by application programmers who use it?
How hard do we want to make our lives for the sake of negligible additional performance?

In my opinion, we should strive for convenient and general interface predicates that make mistakes as unlikely as possible. People have suggested that I "want the SICStus interface". I would in fact prefer an interface that provides even stronger guarantees. However, from those interfaces that are currently available, I consider the SICStus interface the most desirable, and therefore recommend its emulation.

Solution with SICStus Prolog

For completeness, here is a possible solution of the Minato task, using SICStus Prolog and its very general interface for attributed variables.

First, of course, let us use a clean representation of nodes, such as:

a leaf is represented as b(true) or b(false)
an inner node is represented as ( Var -> Then ; Else ), where Then and Else are nodes.

Note in particular that we can now symbolically distinguish leaves from inner nodes, thanks to the b/1 wrapper we use for concrete Boolean values.

As a warm-up, let us express the so-called restriction of a ZDD. This means the relation between one ZDD, and a new ZDD that arises when the variable Var is unified with the concrete Boolean truth value Value, which is either 0 or 1:

zdd_restriction(b(T), _, _, b(T)).
zdd_restriction(( Var0 -> Then0 ; Else0), Var, Value, ZDD) :-
        (   Var0 == Var ->
            (   Value =:= 0 -> ZDD = Else0
            ;   Value =:= 1 -> ZDD = Then0
            ;   throw(no_boolean)
            )
        ;   zdd_restriction(Then0, Var, Value, Then),
            zdd_restriction(Else0, Var, Value, Else),
            ZDD = ( Var0 -> Then ; Else )
        ).

Example query:

?- zdd_restriction((X -> b(true) ; b(false)), X, 1, ZDD).
ZDD = b(true).

Note that the above method is an extremely inefficient way to compute the restriction of a ZDD. Making it faster by using memoization is left as an exercise.

We need a single public predicate to demonstrate how our solution works: variables_set_zdd(Vs, ZDD) shall attach the given ZDD as an attribute to all variables in Vs. The attribute shall be of the form zdd_vs(ZDD, Vs) and store the ZDD as well as all variables we want to reason about.

In SICStus Prolog, we use library(atts) to declare and reason about attributes. For example:

:- use_module(library(atts)).

:- attribute zdd_vs/2.

variables_set_zdd(Vs, ZDD) :-
        maplist(set_zdd(ZDD, Vs), Vs).

set_zdd(ZDD, Vs, V) :-
        put_atts(V, +zdd_vs(ZDD, Vs)).

We are now ready to implement verify_attributes/3. When a ZDD is reduced to the leaf node b(true), then all variables that were not encountered in that branch must be 0. We enforce this with a DCG that describes a list of V=0 goals, one for each remaining variable:

verify_attributes(Var, Value, Goals) :-
        (   get_atts(Var, +zdd_vs(ZDD0,Vs)) ->
            (   integer(Value) ->
                zdd_restriction(ZDD0, Var, Value, ZDD)
            ;   throw(aliasing_not_implemented)
            ),
            phrase(remaining_vars_0(ZDD, Var, Vs), Goals)
        ;   Goals = []
        ).

remaining_vars_0(b(true), Var, Vs) --> all_others_0(Vs, Var).
remaining_vars_0((_;_), _, _) --> [].

all_others_0([], _) --> [].
all_others_0([V|Vs], Var) -->
        (   { var(V), V \== Var } -> [V=0]
        ;   []
        ),
        all_others_0(Vs, Var).

The full code is available from: minatotask.pl

A few sample queries are included. In particular, the Minato task works as desired:

?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ),
   Vs = [X,Y],
   variables_set_zdd(Vs, ZDD),
   Vs = [1,1].
no

It is clear that the general and declarative SICStus interface has some performance impact in comparison with more limited hooks. However, in addition to its generality, SICStus Prolog is also widely known as one of the most efficient Prolog systems. The argument that we should sacrifice correctness for efficiency, even if it were a sensible one, can therefore not be applied in this case.

Equivalence task

We now consider a second task, which I call Equivalence task, and which also arises in connection with CLP(B). I hope this task is useful for you to assess the generality and expressiveness of your system's interface predicates.

The SICStus documentation states for sat(Expression), which is true iff Expression is satisfiable:

If a variable X, occurring in the expression, is subsequently unified with some term T, this is treated as a shorthand for the constraint
| ?- sat(X=:=T).

To implement this in Prolog, an interface for attributed variables must have the ability to reason about a unification before it takes place. Again, a different implementation strategy necessitates highly unnatural and error-prone encodings.

Consider for example the query:

?- sat(X=:=Z), X = X+1.

and ask yourself how this could be handled in your system. According to the SICStus documentation, it should be equivalent to:

?- sat(X=:=Z), sat(X=:=X+1).

This is satisfiable and should therefore yield for example:

X = Z, Z = 1.

If your system cannot yield such an answer, think about what a suitable approximation may look like, and how it can be computed.

For example, with your interface predicates for attributed variables, can you at least somehow distinguish the above case from:

?- sat(X=:=Z), X = ~X.

which ought to be equivalent to:

?- sat(X=:=Z), sat(X =:= ~X).

and hence fail.