[Xsb-development] [ xsb-Bugs-535270 ] "Simple" bug in Attributed Variables (2)

[<no...@so...>]

Bugs item #535270, was opened at 2002-03-26 16:31
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=101176&aid=535270&group_id=1176

Category: Other
Group: wrong answer
Status: Open
Resolution: None
Priority: 5
Submitted By: Nobody/Anonymous (nobody)
>Assigned to: Terrance Swift (tswift)
>Summary: "Simple" bug in Attributed Variables (2)

Initial Comment:

Here is a bug in attributed variables that seems to 
indicate some strange compiler interaction. The 
offending program was distilled from one where I 
initially suspected indexing instructions, so the 
underlying problem may be more general. The results 
also differ whether we have trace on or off. 

I hope finding the problem would be relatively easy. 
Please let me know when you fix this. 

Happy hunting! 
- CR 
 

:- import put_atts/2, get_atts/2 from atts.
:- import attv_unify/2 from machine.

:- attribute skolem/1.

%% Check if Var can be unified to Value, 
%%    where Var is a skolem constant
%%    Value may be another skolem constant or a term
%%    A skolem constant unifies only with another 
identical constant.
verify_attributes(Var, Value) :-
	get_atts(Var, skolem(X)),  % Get the attribute 
of Var
	var(Value), % Value must be another skolem 
constant
        get_atts(Value, skolem(Y)),  % Get the other 
constant
	X == Y. % Var and Value unify only if their
	        % "constant" fields are identical.

%% Generate a new skolem constant
newvar(Var) :-
	(is_attv(Var)   % is Var already known to be a 
skolem constant?
           -> true      % then no need to do anything 
now
           ;  put_atts(Var, skolem(_))  % generate 
a "fresh" variable as the
                                    % attribute of Var
        ).

same(X, Y) :- X=Y, nop.
nop.

/** Example trace illustrating the bug:
% same/2 differs from =/2 due to a trailing (fact) nop.
% So we'd expect not(same(X,Y)) and not(X=Y) to give 
identical results.
| ?- [bug2].
[Compiling ./bug2]
[bug2 compiled, cpu time used: 0.0500 seconds]
[bug2 loaded]
 
yes
| ?- newvar(X), not(same(X, a)).
 
X = _h191;
 
no
| ?- newvar(X), not(X=a).
 
no
| ?-

*/


----------------------------------------------------------------------

Comment By: Bart Maria Demoen (bartkul)
Date: 2002-10-22 15:38

Message:
Logged In: YES 
user_id=11817

The problem is that not/1 is defined as

not(G) :- call(G), !, fail.
not(_).

and that XSB does not wake the unify handler before the cut.

This is not easily fixed in general - but a good ad hoc fix
is to rewrite not/1 as:

not(G) :- call(G), nop, !, fail.
not(_).

and if the compiler expands not/1 goals, do a similar thing


----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=101176&aid=535270&group_id=1176