Use exact comparision for doubles

Thorsten Wißmann requested to merge double-round into master

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.

Merge request reports