Next: , Previous: Comparison functions for <code>poly_int</code>, Up: Comparisons involving <code>poly_int</code>


10.3.2 Properties of the poly_int comparisons

All “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:

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.