missing simplification

[redianthus]

Hi,

I noticed a missed simplification, which is stuff looking like:

(shr_u (shr_u symbol_0 1) 1)

That could be simplified into:

(shr_u symbol_0 2)

(actually, I have a much longer chain in practice and it can be other constants, not only 1)

I don't have the time to implement it myself right now so I'm opening the issue not to forget about it.

[filipeom]

I think this might be a good case to try and use our simplification DSL! @joaomhmpereira told me it should be straightforward. It would be something like:

ShrU(ShrU(s, Int(i1)), Int(i2)) ==> ShrU(s, Int(i1+i2))

Although, it's probably not ints that the unsigned shift right operator receives. I think it's actually bitvectors. I don't know if we can already specify things like Bitv 1 and Bitv (i1 + i2). So maybe we can't use it this way just yet.

[hra687261]

Is there support for dependent types? So that the simplifications can be defined for any bit-vector of size n.

There are also simplifications in #348 that it might be worth rewriting using the DSL.

[filipeom]

Is there support for dependent types? So that the simplifications can be defined for any bit-vector of size `n`.

Not yet, might be a good addition to have them! Currently the DSL is only expressive enough to allow us to write the current simplifications we have on it

[hra687261]

I think only bv32 and bv64 (maybe bv8 as well?) are used in owi so it should be sufficient for now to simply write them for these types.