ULT has SignExt simplification, ULE(Q) does not

[Notselwyn]

Hello there,

I have noticed that ULE(a_bv32, SignExt(24, b_bv8)) does not get properly simplified, while ULT(a_bv32, SignExt(24, b_bv8)) is: see the code below. This is not specific to the bitsize of the operands in the example (32).

I may be mistaken, but I believe this simplification should be possible considering ULE(x, y) is equivalent to Or(ULT(x, y), x == y).

>>> simplify(ULT(BitVecVal(53, 32), SignExt(24, BitVec('x', 8))))
Not(And(Extract(7, 6, x) == 0,
        Extract(7, 7, x) == 0,
        ULE(Extract(5, 0, x), 53)))
>>> simplify(ULE(BitVecVal(53, 32), SignExt(24, BitVec('x', 8))))
ULE(53,
    Concat(Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           Extract(7, 7, x),
           x))

As for versioning: I'm using the Python package z3-solver with version 4.13.0.0

Additional substantiation can be found in #7380.

This significantly impacts the performance of my application, so it would be great if this could be looked into. :-)

[Notselwyn]

In fact, like ULT, the simplification does work for UGE. However, it seems UGT and ULE do not feature this simplification.

[NikolajBjorner]

Everyrhing simplifies to ule. The argumenta are swapped and negation added.

[NikolajBjorner]

You are basically aakung for a simplificqtion rule used for x <= k, with k a conatant to apply to k <= x by the equivalence: k<= x iff not(x <= k and x != k).

[Notselwyn]

Thank you for picking this up. The way you mentioned it is correct. I have indeed just noticed that ULE(x, k) is properly simplified but ULE(k, x) is not. It would be a huge lifesaver, and if I may give feedback, I would have never figured out that there's a difference between the position of the constant argument and the simplification manner (ULE(k, x) and ULE(x, k)). Hence, I think it would be a great feature to implement this behaviour for both positions.

[NikolajBjorner]

fa7fc8e