souffle icon indicating copy to clipboard operation
souffle copied to clipboard

`inline` cause `Floating-point arithmetic exception` without divide-by-zero

Open DerZc opened this issue 2 years ago • 1 comments

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

DerZc avatar Oct 25 '22 15:10 DerZc

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.

DerZc avatar Oct 31 '22 01:10 DerZc