[BUG] Set constraint `setLe` and `setLt` do not behave as expected

[dimitri-justeau]

Describe the bug

The lexicographic ordering is applied to a boolean representation of the set, in the form: [b0, b1, b2, b3], where b0 is the lexicographically smallest possible number in the set (from UB) and b3 is the largest. For example, if we have a set variable s that takes its values in [ {}, {0, 1, 2, 3, 4} ], the value {1, 2} is represented as 01100.

The problem is that the lexical ordering of this representation is not equivalent to the lexicographic ordering of the sorted set elements. For example (with the same domain [ {}, {0, 1, 2, 3, 4} ]), if s1 = {4} and s2 = {3}, s1 > s2 according to the lexicographic ordering of the sorted set elements. But with the boolean representation we have: s1 = 00001 and s2 = 00010, thus s1 < s2.

Possible solution

One possible solution could be to reverse the boolean representation, with the previous example we would have:

s1 = {4} -> 10000 s2 = {3} -> 01000