Attributed variables: Interface convergence

[triska]

There are two major deficits of the current attributed variable interface predicate attr_unify_hook/2:

1. It is called only after the unification has already taken place.
2. In the case of simultaneous unifications like [X,Y] = [a,b], it is called with all bindings already in place.

However, there are cases where we need to reason about variables before the unification takes place or, equivalently, any pre-existing triggering unifications are undone before the hook is called. See below for the justification.

I recommend convergence with the interface used by SICStus Prolog, also to increase portability across different Prolog systems, or the design of an interface that is at least as general.

Specifically, it would help tremendously if verify_attributes/3 were called upon unifications with the same semantics as in SICStus Prolog:

1. first, the unifications are undone
2. verify_attributes(+Variable, +Value, -Goals) is called
3. the unifications are redone
4. Goals are executed

---

Real-world examples

I give two examples to explain why attr_unify_hook/2 is insufficient. The first example is shown in git commit 988ea20b7. It shows that the current interface is extremely error prone to use, because it can unexpectedly bind several variables at once and then trigger the hook with an arbitrary number of bindings suddenly in place. Realistically, nobody can exhaustively think of all cases that can simultaneously happen and cover them. The author of dif/2 also ran into this exact problem, as evidenced by a filed issue about dif/2.

The second example arises in a CLP(B) implementation that uses Zero-suppressed Binary Decision Diagrams (ZDDs). A ZDD is interpreted like any decision diagram, but with the following twist: Variables that do not occur in a branch must be 0. Here is an example showing the ZDD for X=\=Y, with the dotted lines indicating 0:

When working with ZDDs, we must keep track of all CLP(B) variables that appear in constraints, because we need to figure out "all variables that do not occur in the ZDD".

If unifications are performed step by step, i.e., just as with individual unifications, no problems arise, even with attr_unify_hook/2. For example, suppose we have X = 1, Y = 1. The first unification leads us into the right branch of the ZDD. We arrive at true, which means that this is true if all variables that do not occur in the ZDD (i.e., Y), are 0. Therefore, we post Y=0 from within attr_unify_hook/2. The second unification will therefore automatically fail.

But suppose the unifications are performed simultaneously, as in [X,Y] = [1,1]. The first unification again leads us into the right branch of the ZDD, but now we cannot find out which variables do not occur in the ZDD, because Y is no longer a variable at the time the hook is called!

More information about this issue: Minato task.

There may be ways to work around this, but they involve essentially duplicating the Prolog view of variables within the program, using IDs of variables to distinguish them. Also, this is not at all how we expect to reason about our datastructures.

For these reasons, it is very desirable that the unification hooks are called before the bindings are in place, and for each binding individually.

[TeamSPoon]

Secretly my mental picture of attribute variables had always been that they are not bound before calls to hooks. When I saw that so many people (yourself @triska included) seeming to be fine with them being bound at the time of the hooks I was really really impressed how you could still do CLP(??) . But, when I started ported to port a version of Description Logic, which amounts to porting CHR, (another todo list convergence LOL). I was stuck doing a mind numbing workaround of linearizing args: That means I was cloning attributed variables just to send them off to their impending "death by unification" in which attrib_unify_hook would send the original copy a gold star (a practice perhaps started in the Great War) .. But i needed to know where to send it and that meant every original variable needed to gensym a module for attrib_unify_hook) .

So let's discuss this issue, I have been working on a branch of SWI-Prolog capable of your needs this but will need help to make it lean towards convergence as well.

moved unrelated content/comments to https://github.com/logicmoo/swipl-devel/issues/1

[JanWielemaker]

FYI, I don't have a strong opinion on the attvar interface. I'm happy with everything as long as the old interface remains supported or can be supported using an emulation layer that doesn't make it much slower. Please do look at existing interfaces, probably notably SICStus and ECLiPSe and design things to be as compatible as possible.

If you delay binding, be careful about cyclic terms and the occur check. See e.g., unifiable/3 in pl-prims.c, which performs the normal unification and then unbinds by examining the trail.

[triska]

Douglas, it is awesome that you are looking into this! Using the current interface (for clarity, please note the exact spelling: attr_unify_hook/2) to implement actual constraint solvers is an uphill battle: I managed to do it for CLP(FD), but for CLP(B) it is definitely not general enough. In addition, it is extremely error prone to use, because all variables may already be aliased when the hook is called. So, it is not at all like I'm happily using the interface and everything is fine; in fact, it's more of the opposite: When implementing constraint solvers, I'm continuously struggling with the current SWI interface and always wish for a cleaner one. Thank you for helping to finally solve this issue, I am looking forward to working with you on this and will help in every way I can to port all constraint libraries to the new interface once it becomes available!

To (massively!) improve the situation, having verify_attributes/3 exactly as in SICStus Prolog would be my personal preference: It is very declarative, and most importantly is called with the bindings undone. Please check out the SICStus documentation. Note that the other predicates are all either already available in SWI, or can be easily mapped for compatibility, but verify_attributes/3 can not, because in SWI, the hook (attr_unify_hook/2) is called with the binding already in place.

I therefore suggest you do the following: In your branch, provide verify_attributes/3 with the same semantics as in SICStus Prolog. In that branch, I will rewrite CLP(FD) and CLP(B) to use this new interface. (This will bring both of these systems closer to running in SICStus Prolog too, as a nice side-effect.) I will have some suggestions on how to support libraries that still use the attr_unify_hook/2 interface for the time being.

Most importantly, please first focus on getting the semantics right. This will allow us to run test cases and port actual solvers to the interface. Please let us postpone the discussion about performance: It is also important, but let us discuss it after having the SICStus-compatible semantics in place. If it is any reassurance, recall that SICStus is much faster than SWI-Prolog in many constraint benchmarks even though its interface for attributed variables is much more general than that of SWI, so this is a good indication that the SICStus interface can also be implemented efficiently.

[TeamSPoon]

Markus,

Nice, that get_attr/2 put_attr/2 are named differently than get_attrs/2 or put_attrs/2. Yes, we can for now (or later) map them.

Looks like I can very easily make verify_attributes/3 work as documented though it will be called only on Module:verify_attributes/3 that has either put_attr/3 or put_attrs/2 in the identical manner and call order that we do with attr_unify_hook/2 Like Sicstus says: "Var might have no attributes present in Module; the unification extension mechanism is not sophisticated enough to filter out exactly the variables that are relevant for Module."

Interesting.. So for our mainstream inclusion into SWI we could leave attr_unify_hook/2 as-is and only called if verify_attributes/3 did not veto the unification?

I see that verify_attributes/3is documented with the ability to create new choice points.. that won't be a problem (we will see if @JanWielemaker will need to answer a few questions.. But at least on one branch of this, I extended the pl-vmi.c )

I'll get a little bit ahead of myself: In fact, I am glad to create new choice points, this will make labeling/2 magically easier in the future.

[triska]

Yes, for backward compatibility, we could simply either just call attr_unify_hook/2 after the unification (as is currently the case), or, more elegantly, simply remove special provisions for attr_unify_hook/2 entirely from the core, and automatically add a definition of verify_attributes/3 that yields [attr_unify_hook(Attr,Value)] to modules that define attr_unify_hook/2. This expresses attr_unify_hook/2 in terms of verify_attributes/3, and requires only support for this predicate in the core.

Please expand on where verify_attributes/3 will be called: Note that the SICStus documentation says that verify_attributes/3 may even be called in modules where there are no attributes defined for that variable. It would be OK if that goes down to what you are saying, i.e., only where attributes are actually put on the variable, but it would still be interesting why the unification mechanism of SICStus does not do it as precisely. It may help you to improve the mechanism's performance in some cases if you know that it is OK to call verify_attributes/3 even in modules where the variable has no attribute attached.

[TeamSPoon]

Yes that can be a good with with core..

foo:attr_unify_hook(Attrib,Value):- ...CODE...

can be be replaced by

foo:verify_attributes(Var,Value,[]):-get_attr(Var,foo,Attrib), ...CODE...

Expanding on where verify_attributes/3 can be called is very easy to do in fact. But first off our present situation:

At present in core as you know attr_unify_hook/2 must be present for all modules that wish to add attributes. Why? Optimization, because it is cheaper to assume a predicate exists and call it rather than doing something slow like current_predicate/N. (I was thinking about this before I read your comments) Wondering if this should also be a requirement of verify_attributes/3 to be defined as well. Personally I don't like either being a requirement.. (so I made it iterated thru the Modules to call verify_attributes/3 I first have it check current_predicate/1) And it did slow things down a little. Then I argued to myself, "Any module willing to put_attr/3 should be willing to step up and define hooks."

So right now this is how I have verify_attributes/3 implemented

%%  '$wakeup'(+List)
%
%   Called from the kernel *before* assignments have been made to
%   attributed variables.

'$wakeup'(L):- 
  wno_hooks('$wakeup_attrs'(L)).

% 4096 disables the unification hooks presently running
% don't worry, hook code still be able to use wakeups on other variables.
% This wrapper is only for safe debugging 
wno_hooks(G):-  '$sinkmode'(W,W),T is W  \/ 4096, '$sinkmode'(_,T),                 call_cleanup(G,'$sinkmode'(_,W)).

% version only calling it where modules have defined an attribute
'$wakeup_attrs'([]).
'$wakeup_attrs'(wakeup(Var, Attrs3, Value, Rest)) :-           
        call_all_attr_verify_hooks(Var, Attrs3, Value),
        (nonvar(Var)->true;Var=Value),
        call_all_attr_uhooks(Var, Attrs3, Value),
    '$wakeup'(Rest).

% Allow someone who binds this Var to move us onto the next stage 
% In fact, they do not even need to use the original value .. for example ...
% ==
%   verify_attributes(Var, "between one and three", _Goals) :- member(Var,[1,2,3]).
% ==
% (this is for later labeling ..  this does not conflict with Sicstus)
call_all_attr_verify_hooks(Var, _, _) :- nonvar(Var),!.  
call_all_attr_verify_hooks(Var, [], Value).
call_all_attr_verify_hooks(Var, att(Module, AttVal, Rest), Value) :-        
   (current_predicate(Module:verify_attributes/3)->
     (attvar_residuals(att(Module,AttVal,[]), Var, Goals, [])-> Module:verify_attributes(Var, Value, Goals)) ;true),
    call_all_attr_verify_hooks(Var,  Rest, Value).

call_all_attr_uhooks([], _).
call_all_attr_uhooks(att(Module, AttVal, Rest), Value) :-
    uhook(Module, AttVal, Value),
    call_all_attr_uhooks(Rest, Value).

The alternative that gives that flexibility

% Searches for modules defining verify_attributes/3.
% unused pseudocode :)
call_all_attr_verify_hooks(Var, Attr3, Value) :-  
  Template= Module:verify_attributes(Var,Value,Goals),
 ((  current_predicate(_,Template) ,
   \+ predicate_property(Template,imported_from(_)),
    attrs_to_residual_goals(Attr3,Goals),
   (Template -> true ; (!,fail)) )
          *-> true ; fail)). 

Which I would be happy with if we didn't have to use current_predicate/2

[JanWielemaker]

current_predicate/2 and predicate_property/2 are out of the question. For one thing, ISO current_predicate/2 is not supposed to work for static code (works in SWI). Second, these are just too slow operations. A simple option is to define

system:verify_attributes(_Var, _Attr3, _Value) :- fail.

I think I'm more in favour of having an undefined predicate trap, as that is far easier to debug instead of a failing unification because somebody adds an attribute without defining a hook.

Can you help clarifying what will happen if we do put_attr(V, test, a) and call V = v. This is my picture with holes:

• Unify V=v, this pushes the wakeup goals.
  • Does the actual binding happen?
  • if yes, when and how is it undone? Immediately after unification? Just before wakeup?
  • if no, how to we protect against the occur check? This would be problematic if the answer above is Immediately after unification because there may be multiple unifications before wakeup is called.
• If wakeup is called
  • We call verify_attributes(Var, AttrList, Value) in every module where we now call attr_unify_hook/2. The difference is that the binding is not yet made and you have access to all other attributes on this variable.
  • We can easily provide all attributes to all hooks without changing anything to the C code. Why do we need access to the variable bound (also next question)?
• When is the binding actually done? Do the hooks to that? That would mean X = Y, X == Y is no longer necessarily true. That would worry me.

[TeamSPoon]

Agreed about current_predicate/2 and predicate_property/2.

I am sure you thought of (and maybe this is what you meant) as well

:- multifile(prolog:verify_attributes/3).
:- dynamic(prolog:verify_attributes/3).

And modules could do.

:- multifile(prolog:verify_attributes/3).
:- dynamic(prolog:verify_attributes/3).
prolog:verify_attributes(Var,Value,Goals):-  \+ mymodule:verify_attributes(Var,Value,Goals) ->  (!,fail);true.

mymodule:verify_attributes(Var,Value,Goals):- ...MODULE_CODE...

Answers to the next questions (filling in outline).

But in preview I did test this...

 ?- leash(-all),trace,notrace(new_mvar(+skipAssign,X)),X=Y,Y==X.
   Call: (8) [$syspreds] leash(-all)
   Unify: (8) [$syspreds] leash(-all)
   Exit: (8) [$syspreds] leash(-all)
   Call: (8) [system] _G307319{}=_G306598
   Exit: (8) [system] _G307319{}=_G307319{}
   Call: (8) [system] _G307319{}==_G307319{}
   Exit: (8) [system] _G307319{}==_G307319{}
X = Y.

[trace]  ?- leash(-all),trace,notrace(new_mvar(+skipAssign,X)),X=Y,Y==X,X==Z.
   Call: (8) [$syspreds] leash(-all)
   Unify: (8) [$syspreds] leash(-all)
   Exit: (8) [$syspreds] leash(-all)
   Call: (8) [system] _G307384{}=_G306598
   Exit: (8) [system] _G307384{}=_G307384{}
   Call: (8) [system] _G307384{}==_G307384{}
   Exit: (8) [system] _G307384{}==_G307384{}
   Call: (8) [system] _G307384{}==_G306604
   Fail: (8) [system] _G307384{}==_G306604
false.

[JanWielemaker]

Not sure what to think about the trace. In a hurry ...

For the modules, I meant system. The trick is that whenever you have a module that has no verify_attributes/3 definition, it will default (first to user) to the system module definition. I definitely do not want to use the prolog module.

[TeamSPoon]

Ahah, i get it.. great idea!

the small change of ...

system:verify_attributes(_Var, _Attr3, _Value). 

(At least i think)

[triska]

There are several misconceptions here, so I would like to first clear up a few important high-level aspects by using the SICStus documentation to walk through the example that Jan posted: Suppose we have put_attr(V, test, a), and then post V = v.

1. Engine: First, the binding is undone. The precise timing when this happens is still to be defined, let us discuss it separately. I think we can undo it any time we like, as long as it is before verify_attributes/3 is called. In fact, if you can implement that, I think the binding need not even take place at all before (5), see below.
2. Engine: test:verify_attributes(V, v, Gs) is called. Note that the second argument is the value that the variable is about to be bound to, not a list of all attributes.
3. User: test:verify_attributes/3 is the user-defined predicate. If it is not defined, failure is definitely not an option because that would silently break existing user code. It is also a misconception that the current "attr_unify_hook/2 must be present for all modules that wish to add attributes": This is not the case, as you can easily test, and the current state is desirable for the important reason that we often attach attributes to variables just for efficient lookup in certain datastructures, and these variables are never even unified with anything, so users should not have to define attr_unify_hook/2 for them. In my view, if test:verify_attributes/3 is undefined, it should be equivalent to test:verify_attributes(_, _, []).
4. User: test:verify_attributes/3 must not bind the variable itself. Instead, it communicates via the third argument all goals that are to be invoked after the unification. For instance, the obvious emulation of the current test:attr_unify_hook/2 would be:

   test:verify_attributes(Var, Value, [test:attr_unify_hook(Attr,Value)]) :-
      get_attr(Var, test, Attr).

5. Engine: The original variable binding is redone. V = v.
6. Engine: The goals computed by the third argument of test:verify_attributes/3 are called.

Note specifically that, due to (5), if X = Y succeeds, then X == Y will also succeed.

I would also like to state the most important high-level goal: The current interface falls extremely short in the case of simultaneous unifications like [X,Y] = [a,b]. This is because at the time attr_unify_hook/2 is called for X, Y is no longer a variable and its attributes cannot be directly accessed. Therefore, both unifications must be undone in such cases to truly benefit from verify_attributes/3. As I understand it, the occurs check may as well take place after (5): Semantically, a unification that is STO is false, so the only downside I see is that an STO unification may fail instead of yielding an error when occurs_check is set to error.

[TeamSPoon]

if we do put_attr(V, test, a) and call V = v.

• Unify V=v, this pushes the wakeup goals.
  • No actual binding happens. Instead, binding is scheduled to happen outside of C via $wakeup/1
  • With the occurs_check code there might be some difficulties yet.
  • Since there may be multiple unifications before wakeup is called. Each successive unification schedules more wakeup. The attributed variable continues to delay. And remains a variable so it can continue to claim it is free.
• If wakeup is called
  • We disable the delay system temporarily for the V so unification treats it like a common variable.
  • We call verify_attributes(Var, AttrList, Value) in every module where we now call attr_unify_hook/2. The difference is that the binding is not yet made and we have access to all other attributes on this variable.
  • We can easily provide all attributes to all hooks without changing anything to the C code.
  • Why do we need access to the variable bound? We really do not need to access it bound since most hooks can see the Value.
  • Though I did design a usecase where it is partially bound and the hooks further bind it (like as a workspace) .. (Though a sane person would do that in attributes)
  • attr_unify_hook/2 is agnostic to whether it was bound or not.
  • Once I had left it unbound, and was able to implement a common prolog variable!

plvar(X):- mvar_set(X,+remainVar),put_attr(X,plvar,binding(X,_)).
plvar:attr_unify_hook(binding(Var,Prev),Value):-  Value=Prev,put_attr(Var,plvar,binding(Var,Value)).

• When is the binding actually done it is by the hooks.
  • The hooks if poorly written (or brilliantly written) could even make X = Y, X == Y fail. For example they could decide whenever X is bound to a variable to make X = 1 instead. (thus 1==Y fails) ..
  • Some case that could be worrisome but other cases useful.
  • I did leave in one barrier to hooks when unifying with a plain old prolog variable. Most likely the X=Y will have put X into Y (instead of the other way around) thus never calling wakeups on X. so X==Y.. will effectively be seen as X==X
  • I gave us the ability to remove that barrier, that is the more experimental part
    Marked with "eager" is where most C code that would call Trail(Y,makeRef(X)). will instead call unifyAttVar(X,Y) which will add a $wakeup/1

test:attr_unify_hook(nonvar,Value):-nonvar(Value).
test:attr_unify_hook(var,Value):- var(Value).

?- put_attr(X, test, nonvar), mvar_set(X,+skipAssign+eager(assignment)),X=Y,X==Y. 
false.

?- put_attr(X, test, nonvar), mvar_set(X,+skipAssign),X=Y,X==Y. 
X=Y.  /*this is why *I* like eager  it prevents ignoring the hooks  */

?- put_attr(X, test, var), mvar_set(X,+skipAssign+eager(assignment)),X=Y,X==Y. 
X=Y.

(BTW: I typed this before reading @triska's post above this one)

[TeamSPoon]

@triska Point 4, Perhaps I'll should throw an exception when I get the Var back and it's been bound?

[TeamSPoon]

• Engine: First, the binding is undone. The precise timing when this happens is still to be defined, let us discuss it separately. I think we can undo it any time we like, as long as it is before verify_attributes/3 is called. In fact, if you can implement that, I think the binding need not even take place at all before (5), see below.

:heavy_check_mark: completed

Engine: test:verify_attributes(V, v, Gs) is called. Note that the second argument is the value that the variable is about to be bound to, not a list of all attributes.

:heavy_check_mark: completed

User: test:verify_attributes/3 is the user-defined predicate. If it is not defined, failure is definitely not an option because that would silently break existing user code. It is also a misconception that the current "attr_unify_hook/2 must be present for all modules that wish to add attributes":

This is not the case, as you can easily test, and the current state is desirable for the important reason that we often attach attributes to variables just for efficient lookup in certain datastructures, and these variables are never even unified with anything, so users should not have to define attr_unify_hook/2 for them.

system:attr_unify_hook(_,_).

:heavy_check_mark: completed

In my view, if test:verify_attributes/3 is undefined, it should be equivalent to test:verifyattributes(, _, []).

system:test:verify_attributes(_,_,[]).

:heavy_check_mark: completed

User: test:verify_attributes/3 must not bind the variable itself. Instead, it communicates via the third argument all goals that are to be invoked after the unification. For instance, the obvious emulation of the current test:attr_unify_hook/2 would be:

test:verify_attributes(Var, Value, [test:attr_unify_hook(Attr,Value)]) :-
    get_attr(Var, test, Attr).

I think we are almost there .. Perhaps that can happen last and over the course of days and testing (I seem to picture swathes of legacy code).. Not that the above definition would break anything it just seems like we'll need to add it to every module at once .. Since we wont be calling attr_unify_hook/2. on it own

[5] Engine: The original variable binding is redone. V = v.

:heavy_check_mark: completed

Engine: The goals computed by the third argument of test:verify_attributes/3 are called.

:heavy_check_mark: completed

I would also like to state the most important high-level goal: The current interface falls extremely short in the case of simultaneous unifications like [X,Y] = [a,b]. This is because at the time attr_unify_hook/2 is called for X, Y, is no longer a variable and its attributes cannot be directly accessed. Therefore, both unifications must be undone in such cases to truly benefit from verify_attributes/3.

In the case of [X,Y] = [a,b].

Right now X isn't bound yet at the time that verify_attributes(Y,b,Out) will be called .. I like that .. but to make it useful I need to add that burden on the user to tell me when X needs bound ..

Here is an example case

[X,Y] = [a,b(X)]. 

verify_attributes(Y,b(X),Out) vs verify_attributes(Y,b(a),Out) .

Currently I implemented the C to allow both.

So perhaps test:verify_attributes(Var, Value, [=(Var,Value)]) If they want verify_attributes(Y,b(a),Out) . to show up?

I need guidence here

As I understand it, the occurs check may as well take place after (5): Semantically, a unification that is STO is false, so the only downside I see is that an STO unification may fail instead of yielding an error when occurs_check is set to error.

unify_with_occurs_check as I understanding it usually takes place before .. it "sanity checks" for potential cyclic results and eventually deems that do_unify() will be mostly unharmed (It cant really protect the system from unifying "child term" which it deemed safe.. ( it wasn't crafty enough to search outside of the unify for a the parent compound structure that our "child term" just changed into a Cyclic term .. I like unify_with_occurs_check and believe its extremely important to have but I need help picturing an example scenario that isn't the fault of the hooks doing something by mistake

[TeamSPoon]

https://github.com/logicmoo/swipl-devel/issues/1

[JanWielemaker]

Hmmm. I'm a bit lost :( Time to look at the source and the docs. Where do I start?

[TeamSPoon]

I am getting ahead of myself :) and needing to set up some cases to confirm things are working as expected .. And when i Clicked on the link below I saw a I saw a couple silly things I meant to fix in attvar.pl and pl-attvars.c anyhow .. https://github.com/SWI-Prolog/swipl-devel/compare/master...logicmoo:treading-lightly

Also I need to find a saner place to store the int value I am keeping around for getSinkMode/setSinkMode .. You (Jan) have probably thought of 100 ways to store extra data for transient variables. Since my system must be error prone (since maybe the global stack moves) and I was surprised it even worked ( it was just to get myself started ) https://github.com/SWI-Prolog/swipl-devel/compare/master...logicmoo:treading-lightly#diff-71d04f2fb2968a749c485db7ea5627caR307

A thought, I realized we an keep the calls to attr_unify_hook/2 as-is since it is defined having a fallback in system

[triska]

Please let us keep the discussion focused on ensuring compatibility with SICStus Prolog first, and by this I mean for now only the correct implementation of verify_attributes/3. First, please all read the actual documentation of verify_attributes/3, and then check out the following sample code that runs with SICStus Prolog (4.3.2):

:- module(test,
          []).

:- use_module(library(atts)).
:- attribute a/0.

verify_attributes(X, Value, []) :-
        format("verifying: ~w = ~w\n", [X,Value]).

Please consider the example:

| ?- test:put_atts(X, +a), X = 3.
verifying: _6279 = 3
X = 3 ? ;
no

In SWI-Prolog, the code will look like this:

:- module(test,
          []).

verify_attributes(X, Value, []) :-
        format("verifying: ~w = ~w\n", [X,Value]).

Douglas, when I try it with your branch, I get:

?- put_attr(X, test, a), X = a.
X = a ;
false.

Thus, it seems that verify_attributes/3 is not even called in this case.

verify_attributes/3 is really all that is needed to unlock the increased generality of the SICStus interface, everything else can be rather trivially worked around.

[triska]

For reference, here is the example posted earlier, to test simultaneous unifications with SICStus Prolog:

:- module(test,
          []).

:- use_module(library(atts)).
:- attribute a/1.

verify_attributes(X, Value, []) :-
        get_atts(X, a(Other)),
        format("verifying: ~w(~w) = ~w\n", [X,Other,Value]).

Please study carefully the following query and result:

| ?- test:put_atts(X, +a(Y)), test:put_atts(Y, +a(X)), [X,Y] = [x,y(X)].
verifying: _3101(_3121) = x
verifying: _3121(x) = y(x)
X = x,
Y = y(x) ? ;
no

Note especially that Y is not instantiated in the first invocation, but X [sic!] is already instantiated in the second invocation of verify_attributes/3. This is exactly as documented, and is also what we intuitively expect. In the SWI port, please also implement this semantics.

Generalizing, to see the behaviour for 3 variables in simultaneous unifications:

:- module(test,
          []).

:- use_module(library(atts)).
:- attribute a/1.

verify_attributes(X, Value, []) :-
        get_atts(X, a(Vs)),
        format("verifying: ~w = ~w; vars: ~w\n", [X,Value,Vs]).

Example query with SICStus:

?- A = a([X,Y,Z]), test:put_atts(X, +A), test:put_atts(Y, +A), test:put_atts(Z, +A), [X,Y,Z]=[0,1,2].
verifying: _359 = 0; vars: [_359,_371,_383]
verifying: _371 = 1; vars: [0,_371,_383]
verifying: _383 = 2; vars: [0,1,_383]
A = a([0,1,2]),
X = 0,
Y = 1,
Z = 2 ? ;
no

[TeamSPoon]

@triska Thank you for those examples.. yep my branched regressed .. and looks like I didn't commit it in the last working state (so even if my earlier commits called verify_attributes/3, there were other things that I needed to change).. so now hopefully w/in 12 hours of me posting this message I'll have an unregressed + have a the above multiple unification patterns.

[JanWielemaker]

In that case, I'll wait a little ... Should be able to find some time before X-mas for this.

[TeamSPoon]

test:verify_attributes(X, Value, []) :-
    get_attr(X, test, Attr),
    format("~Nverifying: ~w = ~w;  (attr: ~w)\n", [X,Value,Attr]).

/*

?- put_attr(X, test, a), X = a.
verifying: _G389386 = a;  (attr: a)
X = a.

?-  put_attr(X,test, vars(Y)), put_attr(Y,test, vars(X)), [X,Y] = [x,y(X)].
verifying: _G389483 = x;  (attr: vars(_G389490))
verifying: _G389490 = y(x);  (attr: vars(x))

?- VARS = vars([X,Y,Z]), put_attr(X,test, VARS), put_attr(Y,test,VARS), put_attr(Z,test, VARS), [X,Y,Z]=[0,1,2].
verifying: _G389631 = 0;  (attr: vars([_G389631,_G389638,_G389645]))
verifying: _G389638 = 1;  (attr: vars([0,_G389638,_G389645]))
verifying: _G389645 = 2;  (attr: vars([0,1,_G389645]))
VARS = vars([0, 1, 2]),
X = 0,
Y = 1,
Z = 2.

*/

[TeamSPoon]

Note that the SICStus documentation says that verify_attributes/3 may even be called in modules where there are no attributes defined for that variable. It would be OK if that goes down to what you are saying, i.e., only where attributes are actually put on the variable, but it would still be interesting why the unification mechanism of SICStus does not do it as precisely. It may help you to improve the mechanism's performance in some cases if you know that it is OK to call verify_attributes/3 even in modules where the variable has no attribute attached.

Looks like Yap (and Sicstus keep track of these "potentially interested" modules that do not place attributes onto variables (modules who have placed attributes at least on one variable once)

I would like do it in this order:

1) Modules with attributes on the variable first 2) Next the source module of the code that is using the attributes. (if not already tried) 3) The current module at the top level (if not already tried) 4) Modules in which YAP stored in :- dynamic attributes:modules_with_attributes/1. (not already tried)

[TeamSPoon]

moved unrelated content/comments to https://github.com/logicmoo/swipl-devel/issues/1

[TeamSPoon]

moved unrelated content/comments to https://github.com/logicmoo/swipl-devel/issues/1

[TeamSPoon]

put_atts/2 get_atts/2

I wonder if it would be best to store..

?- test:put_atts(X,+a(Y)),test:put_atts(X,+b(Y)),test:put_atts(X,+c(Y)),test:put_atts(X,-b(Y)),get_attrs(X,Attrs).

Attrs = att(test,[a(Y),c(Y)],[]).

[triska]

Very nice job Douglas! I have pushed versions of CLP(FD) and CLP(B) that use the new verify_attributes/3 to your branch, so that you can try them.

The new interface has allowed me to simplify the code in CLP(B), and will enable several performance improvements in CLP(FD), because the continuation goals now can be stated explicitly instead of via the detour involving the global queue. I will now work more on this, and also run more tests with the new interface, because there are still some errors I found (probably both in the branch and also in my changes).

The new interface will turn problems like this one into distant memories, and for this I am extremely grateful. Thank you for working on this, and I hope a cleaned up version of your changes will soon make it into the SWI core.

This is a great example how a concrete contribution will make SWI easier to use and more robust for everybody who is working with constraints, paving the way for more interesting and reliable applications!

[TeamSPoon]

@triska Thank you!

If it seems slower on orders of magnitudes.. don't despair, I can speed it up to what it was before pretty easily. (Just at the moment doing stuff that makes the code a little deeper in prolog frames than I need to in the long run.. (Finding the balance between minimalism in the Prolog<->C))

[triska]

One thing I noticed is that if verify_attributes/3 itself vetoes the binding then the unification unexpectedly still succeeds. For example:

?- [library(clpfd)].
true.
?- X #\= 3, X = 3.
X in inf..2\/4..sup.

It works as expected with the continuation goals: If they fail, then the unification also fails, which is exactly as one would expect.

[TeamSPoon]

Now if verify_attributes/3 itself vetoes the binding then the unification expectedly fails.

[JanWielemaker]

Hi Douglas,

I had a look using git diff HEAD..logicmoo/treading-lightly. Seems some great work is done in that branch. Getting more powerful attributed variables is certainly something to strive for, in particular for exploring the sweet spot between classical Prolog and ASP that CLP provides us in my opinion.

I'm also worried about this patch. It is huge, it includes sources from various other projects with unclear license conditions, it includes a lot of stuff that does not follow the SWI-Prolog coding conventions including PlDoc documentation, it surely has some mistakes/misconceptions (see below) and (possibly incorrectly), some performance alarm-bells are ringing. Considering the level at which this integrates with the system, that must all be resolved.

Most of this is just work, which should be fine if you or someone else is willing to invest the time. I'm afraid I won't spend much time on this considering the pile of work I promised long time ago but still has not materialized. Roughly, this is what needs to be done:

• Get agreement to distribute this under the simplified BSD license (which will become the SWI-Prolog license somewhere in 2016).
• Get all code conforming to the SWI-Prolog coding conventions, including PlDoc usage.
• Make sure all existing code runs (e.g., coroutining, clp(qr), CHR) and worst case performance degradation is not much more than (say) 20%
• Integrate both conceptual and reference documentation in the manual.

I'm pretty worried looking at '$wakeup'/1. It seems to be doing a lot of expensive stuff now. Some is debugging that I assume will disappear. $module'/2 and '$set_source_module'/2 are out of the question. We don't want code to behave differently depending on the default module of the toplevel or the current compilation context. Dealing with modes using

    set_something,
    call_cleanup(G, reset_something)

is highly dubious. If G is nondet, the reset will not happen after G succeeds but much later if G is exhausted or its choice point is committed. Passing some global context to a goal that is nondet is hard and expensive. Can this be avoided using an additional parameter? If actual access to the context is rare another option is to store it in an argument and walk the local stack to find it if you need it.

Hope this helps and we will see a nice, lean and fast new attvar API

Cheers --- Jan

[triska]

So far, I have seen a few strange things in the branch, which may be due to the issues that Jan mentioned. For example, the current HEAD behaves differently after throwing an exception:

$ swipl -g "use_module(library(clpb))"
?- sat(A+B*C), B=C, B=A.
A = B, B = C, C = 1 ;
false.
?- throw(e) ; throw(e).
ERROR: Unhandled exception: e
?- sat(A+B*C), B=C, B=A.
A = B, B = 1,
sat(C=:=C) ;
false.

It also differs from upstream SWI in that an unexpected choice point is left in both cases.

At this point, issue #30 also comes into play: Users who would like to help with SWI development are encouraged to write good test cases for the constraint libraries, and share them in this tracker. This way, we have a chance to implement the interface more reliably.

[TeamSPoon]

Yeah $wakeup/1 I still has unneeded clutter (even though it looks like i scaled back since you've posted) and debugging.. it will thin out considerably.

Even the '$module'/2 and '$set_source_module'/2 was for debugging. trying to find a sweet spot as far as "to the caller of the unification " that will be wakeup/N param.

[TeamSPoon]

Whew, @triska

Looks like the extra choice point problem is now cleared up, can you confirm that is for you?

#swipl -g "use_module(library(clpb))"
?- sat(A+B*C), B=C, B=A.
A = B, B = C, C = 1.

?-  sat(A+B*C), B=C, B=A.
A = B, B = C, C = 1.

May have been some of the extraneous debugging code I removed.

[triska]

Sample query that unexpectedly fails with the current HEAD, but worked as expected previously:

?- sat(A+B), A = B.
false.

At this stage, it is always hard to tell whether the mistake is in the branch or the library. I have created a small test program for CLP(B) that never stops if the library is working correctly:

:- use_module(library(clpb)).
sat(_)  --> [].
sat(X*Y) --> [_], sat(X), sat(Y).
sat(X+Y) --> [_], sat(X), sat(Y).
sat(X#Y) --> [_], sat(X), sat(Y).
vs_eqs(Vs, Eqs) :- phrase(vs_eqs(Vs), Eqs).
vs_eqs([]) --> [].
vs_eqs([V|Vs]) --> vs_eqs_(Vs, V), vs_eqs(Vs).
vs_eqs_([], _) --> [].
vs_eqs_([V|Vs], X) --> vs_eqs_(Vs, X), ( [X=V] ; [] ).
run :-
        length(Ls, N),
        portray_clause(N),
        phrase(sat(Sat), Ls),
        term_variables(Sat, Vs0),
        permutation(Vs0, Vs),
        vs_eqs(Vs, Eqs),
        findall(Vs, (sat(Sat),maplist(call, Eqs),labeling(Vs)), Sols1),
        findall(Vs, (labeling(Vs),maplist(call,Eqs),sat(Sat)), Sols2),
        (   sort(Sols1, Sols), sort(Sols2, Sols) -> true
        ;   throw(neq-Sat-Eqs-Vs0-Vs-Sols1-Sols2)
        ),
        false.

You start it by invoking run/0. I hope this helps you to test your changes.

The test is based on the important declarative property that labeling/1 and posting constraints are commutative, that is: If the Prolog goal G posts any constraints among the variables Vs (including sat/1 constraints and unifications), then labeling(Vs),G and G,labeling(Vs) must yield the exact same set of solutions. The critical part here are the mixed in unifications: Most errors in constraint systems are due to unexpected aliasing between logical variables, and this is unfortunately also the area in which the current SWI interface falls short.

The witness above was found by this program, since the commutativity of conjunction is violated by the current HEAD:

?- sat(A+B), A = B, labeling([A,B]).
false.
?- labeling([A,B]), sat(A+B), A = B.
A = B, B = 1.

[TeamSPoon]

Next HEAD ....

root@gitlab:/devel/LogicmooDeveloperFramework/swipl-devel# swipl -g "use_module(library(clpb))"
?-  labeling([A,B]), sat(A+B), A = B.
A = B, B = 1.

?- sat(A+B), A = B, labeling([A,B]).
A = B, B = 1.

We did just bump from swipl-7.3.13 to swipl-7.3.14 (The banner though will still show the version listed below)

% Version: ............. 7.3.13-121-gb96f7f7-DIRTY
% Address bits: ........ 64
% Architecture: ........ x86_64-linux
% Installed at: ........ /usr/local/lib/swipl-7.3.14

[TeamSPoon]

root@gitlab:/devel/LogicmooDeveloperFramework/swipl-devel# swipl -f clpb_santytest.pl
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.13-121-gb96f7f7-DIRTY)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.

For help, use ?- help(Topic). or ?- apropos(Word).

?- run.
0.
1.
2.
3.
4.

It's working hard. Failures in a abnormal code would happen on 2 or 3 ?

[triska]

This looks very nice! Failures can happen at any term depth, but if it passes 3 and 4 that's definitely already a good sign. I also have many other test cases which I am currently also using to test the solvers. So far, it looks very nice! Awesome work, thank you!

I will now work on enhancements that will use the new interface more thoroughly. Notably CLP(FD) should benefit from the continuation goals.

[TeamSPoon]

The extra choice point problem is gone, correct?

?- G1 = sat(A#(B#C+(D#E))), G2 = labeling([A,B,C,D,E]), findall(t, (G1,G2), Ls), length(Ls, L).
G1 = sat(A# (B#C+ (D#E))),
G2 = labeling([A, B, C, D, E]),
Ls = [t, t, t, t, t, t, t, t, t|...],
L = 16.

?- G1 = sat(A#(B#C+(D#E))), G2 = labeling([A,B,C,D,E]), findall(t, (G2,G1), Ls), length(Ls, L).
G1 = sat(A# (B#C+ (D#E))),
G2 = labeling([A, B, C, D, E]),
Ls = [t, t, t, t, t, t, t, t, t|...],
L = 16.

What is the best way for me to reproduce the state? Also are you on 32 bits or 64 bits?

[triska]

I am testing this on a 64-bit system. The 12/16 discrepancy was with an older version, I cannot reproduce it with the current HEAD, so please consider it fixed. The choice-point problem is gone. Thank you!

[triska]

As the next example, please consider the program shower.pl:

:- use_module(library(clpfd)).
shower(S, Done) :-
        D = [5, 3, 8, 2, 7, 3, 9, 3],
        R = [1, 1, 1, 1, 1, 1, 1, 1],
        length(D, N),
        length(S, N),
        S ins 0..100,
        Done in 0..100,
        maplist(ready(Done), S, D),
        tasks(S, D, R, 1, Tasks),
        cumulative(Tasks, [limit(3)]),
        labeling([], [Done|S]).
tasks([], _, _, _, []).
tasks([S|Ss], [D|Ds], [R|Rs], ID0, [task(S,D,_,R,ID0)|Ts]) :-
        ID1 #= ID0 + 1,
        tasks(Ss, Ds, Rs, ID1, Ts).
ready(Done, Start, Duration) :- Done #>= Start+Duration.

With upstream SWI:

?- time(shower(S, Done)).
% 2,099,829 inferences, 0.275 CPU in 0.275 seconds (100% CPU, 7632861 Lips)
S = [0, 0, 0, 3, 5, 8, 5, 11],
Done = 14 .

In contrast, with the branch HEAD:

$ swipl -f shower.pl -O
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.13-122-g86b039c-DIRTY)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.
For help, use ?- help(Topic). or ?- apropos(Word).
?- time(shower(S, Done)).
[Thread 1 (main) at Tue Dec 22 22:59:28 2015] pl-wam.c:1201: TrailAssignment__LD: Assertion failed: (__PL_ld->stacks.global.top)+1 <= (__PL_ld->stacks.global.max) && (__PL_ld->stacks.trail.top)+2 <= (__PL_ld->stacks.trail.max)
C-stack trace labeled "assert_fail":
  [0] save_backtrace() at :? [0x7f51abca3c6a]
  [1] __assert_fail() at ??:? [0x7f51abc6544a]
  [2] TrailAssignment__LD() at :? [0x7f51abbf079a]
  [3] appendToWakeup() at pl-attvar.c:? [0x7f51abc6e840]
  [4] unifyAttVar() at :? [0x7f51abc71ce6]
  [5] do_unify() at pl-prims.c:? [0x7f51abc3529a]
  [6] unify_ptrs() at :? [0x7f51abc3687b]
  [7] PL_next_solution() at ??:? [0x7f51abc0533f]
  [8] query_loop() at :? [0x7f51abc3ac0e]
  [9] prologToplevel() at :? [0x7f51abc3b40b]
  [10] PL_toplevel() at ??:? [0x7f51abbf879d]
  [11] swipl(main+0x2d) [0x40083d]
  [12] __libc_start_main() at ??:? [0x7f51ab624b45]
  [13] swipl(+0x881) [0x400881]

The crash depends on both the "-O" switch and using time/1.

When I omit the time/1 call around the query, then I get (with and without "-O"):

?- shower(S, Done).
(long wait without result)

[TeamSPoon]

Hopefully will get this fixed over the next 48 hours .. I had been doing xmas travels.. If you note any other interesting failures don't hesitate to mention

[TeamSPoon]

@triska OK, it should be working..

@JanWielemaker Made this patch nice and light see https://github.com/SWI-Prolog/swipl-devel/compare/master...logicmoo:treading-lightly

[triska]

The CLP(B) test case above is broken with the latest changes:

?- run.
0.
ERROR: Unhandled exception: neq-_G143-[]-[_G143]-[_G143]-[]-[[1]]

I recommend you always run the tests when making changes in this branch to be more certain about its correctness.

[TeamSPoon]

Odd even shower/2 is failing Oops I may have been testing upstream

[TeamSPoon]

OK, it is back to the running state again. Luckily, I wasn't testing the upstream. The initial version was working, but I had broken it since announcement since I hadn't tested the next few commits.

?- time(shower(S, Done)).
% 5,388,802 inferences, 0.818 CPU in 0.820 seconds (100% CPU, 6587099 Lips)
S = [0, 0, 0, 3, 5, 8, 5, 11],
Done = 14 .

?- run.
0.
1.
2.
3.
4.

[triska]

Awesome job Douglas, thank you a lot! I have pushed changes to your branch that document the new interface also in the user documentation.

As to performance, the following shows the performance degradation (normalized for original performance = 1, no performance = 0) of inferences and CPU time for some benchmarks:

?- comparison.
sudoku1             0.860     0.857
sudoku7             0.697     0.795
queens80            0.946     0.998
alpha_ff            0.639     0.660
knight              0.909     0.959
shower1             0.383     0.509
alpha               0.814     0.826
queens25            0.901     0.994
starpic             0.437     0.454
golf9               0.990     0.979
mhex                0.908     0.938
shower2             0.406     0.465
false.

I find this completely acceptable, taking into account the increased generality and ease of use of the new verify_attributes/3 implementation. I may also be able to improve the remaining cases by more intelligent use of the new interface.

[TeamSPoon]

I am probably paraphrasing what you just said: When converting code that has had development time centered around exclusively using attr_unify_hook/2 and where attr_unify_hook/2 was adequate, it will be very likely that verify_attributes/3 will add the extra time since one might end up calling get_attrs/3. However there are many more cases that attr_unify_hook/2 would have been inadequate. So there might e a delicate balance in which hook to use in which code.

[triska]

For inclusion in SWI-Prolog, I recommend you clean up the code. For example, use a DCG to collect all continuation goals, like this:

do_verify_attributes(_, Var, _ , _) --> {\+ attvar(Var), ! }.
do_verify_attributes(AttsModules, Var, att(Module, _AttVal, Rest), Value) -->
        { Module:verify_attributes(Var, Value, Goals),
          '$delete'(AttsModules,Module,RemainingMods) },
        list(Goals),
        do_verify_attributes(RemainingMods, Var,  Rest, Value).

% Call verify_attributes/3 in rest of modules
call_verify_attributes([],_Var, _Att3s, _Value) --> [].
call_verify_attributes([Module|AttsModules], Var, [], Value):-
        { Module:verify_attributes(Var, Value, Goals) },
        list(Goals),
        call_verify_attributes(AttsModules, Var, [], Value).

list([]) --> [].
list([L|Ls]) --> [L], list(Ls).

This way, you avoid the mess of having to deal with defaulty data structures like (Goal1,Goal2). Instead, it will be a clean list like [Goal1,Goal2,...], and you can simply use maplist(call, Goals) to call such a list of collected goals.

Also, please do not change the continuation goals that the individual verify_attributes/3 goals produce! I.e., do not prepend different modules etc.

[triska]

Any code that has had significant development time dedicated to making attr_unify_hook/2 somehow work is very likely to contain mistakes, and should also be converted to use verify_attributes/3 instead. You cannot exhaustively think about or test all cases where simultaneous unifications may be in place, so I highly recommend verify_attributes/3 in all situations. I can understand that users prefer to get wrong results over correct ones when they see a performance improvement of an order or two of magnitude (as tragic as that may be in itself). But a factor ~2 performance impact is definitely not worth yielding wrong results, even for users who care least about correctness and more about performance (as is typically the case).