Next: Comparing potentially-unordered poly_ints, Previous: Comparison functions for poly_int, Up: Comparisons involving poly_int [Contents][Index]
poly_int comparisonsAll “maybe” relations except maybe_ne are transitive, so for example:
maybe_lt (a, b) && maybe_lt (b, c) implies maybe_lt (a, c)
for all a, b and c. maybe_lt, maybe_gt
and maybe_ne are irreflexive, so for example:
!maybe_lt (a, a)
is true for all a. maybe_le, maybe_eq and maybe_ge
are reflexive, so for example:
maybe_le (a, a)
is true for all a. maybe_eq and maybe_ne are symmetric, so:
maybe_eq (a, b) == maybe_eq (b, a) maybe_ne (a, b) == maybe_ne (b, a)
for all a and b. In addition:
maybe_le (a, b) == maybe_lt (a, b) || maybe_eq (a, b) maybe_ge (a, b) == maybe_gt (a, b) || maybe_eq (a, b) maybe_lt (a, b) == maybe_gt (b, a) maybe_le (a, b) == maybe_ge (b, a)
However:
maybe_le (a, b) && maybe_le (b, a) does not imply !maybe_ne (a, b) [== known_eq (a, b)] maybe_ge (a, b) && maybe_ge (b, a) does not imply !maybe_ne (a, b) [== known_eq (a, b)]
One example is again ‘a == 3 + 4x’
and ‘b == 1 + 5x’, where ‘maybe_le (a, b)’,
‘maybe_ge (a, b)’ and ‘maybe_ne (a, b)’
all hold. maybe_le and maybe_ge are therefore not antisymetric
and do not form a partial order.
From the above, it follows that:
known_ne are transitive.
known_lt, known_ne and known_gt are irreflexive.
known_le, known_eq and known_ge are reflexive.
Also:
known_lt (a, b) == known_gt (b, a) known_le (a, b) == known_ge (b, a) known_lt (a, b) implies !known_lt (b, a) [asymmetry] known_gt (a, b) implies !known_gt (b, a) known_le (a, b) && known_le (b, a) == known_eq (a, b) [== !maybe_ne (a, b)] known_ge (a, b) && known_ge (b, a) == known_eq (a, b) [== !maybe_ne (a, b)]
known_le and known_ge are therefore antisymmetric and are
partial orders. However:
known_le (a, b) does not imply known_lt (a, b) || known_eq (a, b) known_ge (a, b) does not imply known_gt (a, b) || known_eq (a, b)
For example, ‘known_le (4, 4 + 4x)’ holds because the runtime
indeterminate x is a nonnegative integer, but neither
known_lt (4, 4 + 4x) nor known_eq (4, 4 + 4x) hold.