Use exact comparision for doubles

Comparision with (a-b < ɛ) is not transitive and thus doesn't induce
an equality relation. Since the whole job of the algorithm is to
partition according to an equality relation, this may be problematic.

Instead, to compare doubles a and b, we now round both values to
floats and compare those exactly. This means that we get a proper
equality relation, even if it fails to distinguish some states and
wrongly distinguishes others when compared to operations on true real
numbers.