Inlining a clause changes the result

[rhendrix42]

Hi guys,
Consider the following program.

.decl A(x:float)
.decl CnAF(A:float, B:float)
.decl EluV(A:float)
.decl iNJe(A:float)
.decl out(A:float)
A(0.0).


A(x+1)  :- A(x), x=0.0.
CnAF(u,max(-e,u)) :- A(e), A(u).
EluV(min(q,gKa)) :- A(Fli), A(gKa), A(q).
iNJe(G) :- CnAF(G,G), EluV(tgY).
out(b) :- iNJe(b), iNJe(a), A(a).

.output out

$ /soffle -w rules.dl
$ cat out.csv
0
1

If I now inline CnAF, -0 is added in the result.

.decl A(x:float)
.decl CnAF(A:float, B:float) inline
.decl EluV(A:float)
.decl iNJe(A:float)
.decl out(A:float)
A(0.0).


A(x+1)  :- A(x), x=0.0.
CnAF(u,max(-e,u)) :- A(e), A(u).
EluV(min(q,gKa)) :- A(Fli), A(gKa), A(q).
iNJe(G) :- CnAF(G,G), EluV(tgY).
out(b) :- iNJe(b), iNJe(a), A(a).

.output out

$ /soffle -w rules.dl
$ cat out.csv
-0
0
1

Souffle revision I am using: fbb4c4b

[rhendrix42]

I have another simpler example:

.decl A(x:float)
.decl B(A:float, B:float, C:float) inline
.decl out(A:float)


A(x+1)  :- A(x), x=-0.0.
B(e,e,max(-D,e)) :- A(D), A(e).
out(R) :- A(R), B(a,b,a).

.output out

A(0.0).

If I run the above program, I get:

0
1

If I now modify the out clause a little, without changing anything else in the program:

.decl A(x:float)
.decl B(A:float, B:float, C:float) inline
.decl out(A:float)


A(x+1)  :- A(x), x=-0.0.
B(e,e,max(-D,e)) :- A(D), A(e).
out(R) :- A(R), B(a,R,a), B(a,R,R), B(R,R,R).

.output out

A(0.0).

I get:

-0
0
1

[b-scholz]

This is a consequence of working with floating numbers and transforming floating-point numbers algebraically using inline.

The problem is that we don't have an epsilon check for set membership, e.g.,
https://stackoverflow.com/questions/19837576/comparing-floating-point-number-to-zero

[TomasPuverle]

I think the problem is slightly different, and inline is coincidental in this case. The issue I see is that while the floating point unit and C++ code have to treat -0 and 0 as identical, they have a different bit pattern. Looking at the code, since everything is getting cast-ed to RamDomain (int32/64_t), these do, in fact, appear as two different elements inside the btree's.

I would propose a simple fix (but before implementing, want to check you're ok with this): At the point of the insert (when generating the insertion tuple), if we are dealing with a float, effectively do the following:

if (ramBitCast<RamFloat>(val) == 0) {
  val = 0;  //always set to positive zero before insertion
}

By the way, here's a much shorter version which illustrates the problem without using inline:

.decl A(x:float)

A(0.0).
A(-0.0).

.decl out(x: float)
.decl out2(x: float)

out(x) :- A(x).
out2(x+1) :- A(x).

.output out, out2
.output out

➜  bug git:(master) ✗ ../src/souffle bug.dl -D-
---------------
out
x
===============
-0
0
===============
---------------
out2
x
===============
1
===============

The first relation just memoizes the results, so you get both positive and negative zeros. The second uses arithmetic and since IEEE requires +-0 to be treated equally, you get just one.

Hope that makes sense.

PS: An alternative solution would be to port all of the floating point code to unum's. (j/k)

[TomasPuverle]

I should also point out that NaN's has multiple representations in IEEE, too.
(But, as per @b-scholz's comment in #1513, I'm happy to defer the discussion/handling of NaN's till later)