souffle
souffle copied to clipboard
`inline` cause `Floating-point arithmetic exception` without divide-by-zero
Hi,
I find a Floating-point arithmetic exception
caused by inline
, consider the following program:
.decl bydd(A:symbol, B:number)
.decl unoa(A:number, B:number, C:number, D:number, E:number, F:number, G:symbol, H:symbol) inline
.decl ycuc(A:number, B:number, C:number, D:symbol, E:number, F:symbol, G:number, H:symbol)
.decl lwug(B:symbol, E:symbol)
bydd("T", -3).
ycuc(0, 0, 0, "m", 0, "m", 0, "m").
unoa(B/B, B, B, -B, B, B, A, cat(A,A)) :- bydd(A, B).
lwug(H, J) :- ycuc(L, K, K, E, L, B, L, I), unoa(K, K, K, L, K, L, J, H).
.output lwug
I execute this program with souffle -w example.dl
and get the output:
Floating-point arithmetic exception signal in rule:
lwug(cat(J,J),J) :-
ycuc(K,K,K,_,K,_,K,_),
bydd(J,K),
K = (K/K),
K = -(K).
in file example.dl [11:1-11:74]
There is only one division in this program as B/B
in the head of rule of unoa
, but B
only equals to -3
. So there can't be divide-by-zero. The program can execute correctly if I remove the inline
.
The version of Souffle is 29c5921
I reduce it to a simpler version:
.decl bydd(A:number)
.decl unoa(A:number, B:number) inline
.decl ycuc(A:number)
.decl lwug(B:number)
bydd(-3).
ycuc(0).
unoa(B/B, B) :- bydd(B).
lwug(K) :- ycuc(K), unoa(K, K).
.output lwug
Output is:
Floating-point arithmetic exception signal in rule:
lwug(K) :-
ycuc(K),
bydd(K),
K = (K/K).
Hope this is useful.