simplifying redundant ULE signext

[Notselwyn]

Hello everybody, given the following z3 expression, is it possible to simplify it to ULE(63, x)? If so, which tactic should be used?

from z3 import *

x = BitVec("x", 8)

expr = ULE(63, 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))

[Notselwyn]

By the way, it seems this is the result of ULE(63, SignExt(24, BitVec('x', 8))). In order to simplify this, I think it would be necessary to recognize the unsigned comparison and if the original sign-extended value (8 bits) has more bits than the compared value 63 (6 bits), which would mean the sign-extension is unnecessary if I'm not mistaken

Given the fact that the z3 simplifier probably has this sign ext info before simplifying, I guess it would mean checking if a sign-extended value gets used as unsigned?

[Notselwyn]

Would be great if this simplification could be looked into, since this is slowing my high-performance application down drastically (it will not solve larger equations containing these within at least 60 seconds, whilst everything else is solved within 500ms).

Considering ULT(43, SignExt(32, BitVec('x', 8))) is properly simplified to Not(And(Extract(7, 6, x) == 0, Extract(7, 7, x) == 0, ULE(Extract(5, 0, x), 43))), I wrote a special rule in my program that rewrites ULE(x, y) to Or(ULT(x, y), x == y, but it seems this slows the application down a bit. Hence, I think extended this tactic from ULT to ULE would be great.

[wintersteiger]

is it possible to simplify it to ULE(63, x)?

No, because 63 is apparently of size 32 in your context, so x has to be be extended to the same size before the comparison can be made. This looks like Python, which may automatically convert machine integers. Try replacing 63 with BitVecVal(63, 8) to make it clear that you want 8 bits here.

[Notselwyn]

Thanks for reaching out. I think I may have worded my question in a misleading way, because this SignExt is generated by my own program in a correct way, but I want z3 to simplify it away. The bitsize of 63 is supposed to be 32 in that example.

I find it odd that ULT(x, y) is properly simplified but ULE(x, y) is not, whilst logically the only difference is adding an Or(..., x == y). You could try simplify(ULT(BitVecVal(53, 32), SignExt(24, BitVec('x', 8)))) versus simplify(ULE(BitVecVal(53, 32), SignExt(24, BitVec('x', 8)))) for example. Hence, I suspect this may be a bug.

>>> 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))

[Notselwyn]

This discussion has been linked in #7389.