I want to test whether a real value is a whole number. There doesn't seem to be a floor function or similar, so I'm trying to use the real_of_int function from the tutorial as follows:
function real_of_int(n:int):real = n **. 1
predicate is_int_r(a:real) = exists v:int . a = real_of_int(v)
goal g1: real_of_int(0) = 0.0
goal g2: exists v:int . real_of_int(v) = 0.0
goal g3: is_int_r(0.0)
File "test2.ae", line 4, characters 10-30: Valid (0.0000) (3 steps) (goal g1)
File "test2.ae", line 5, characters 10-45: I don't know (0.0000) (9 steps) (goal g2)
File "test2.ae", line 6, characters 10-23: I don't know (0.0013) (11 steps) (goal g3)
So the real of int 0 is 0.0 (g1 is valid), but the exists in g2 fails to find it and hence g3 fails too (alt-ergo 2.4.3).
Is there a better way to do this?
Since g1 is valid, I was expecting g2 to find v=0. But it doesn't.