Converting bit-operations to arithmetic

[ThomasHaas]

Context: Some benchmarks involve a few bit-operations, potentially introduced through the compiler or by manual optimization. This can include xors to negate booleans (i1 Variables in LLVM) or shifts to perform multiplication.

Problem: Mixing the theories of bit-vectors and integers may slow down the solver.

Solution: If possible, bit-operations should be converted to integer or boolean operations if possible.

• xor on i1 variables -> boolean negation (already implemented)
• left-shifts -> multiplication
• bitwise or/and on i1 variables -> boolean or/and

Example: bresenham's algorithm uses multiplication by 2. The compiler tends to replace this by bit-shifts, causing mixing of theories.

[hernanponcedeleon]

Does this one make sense still?

[ThomasHaas]

Yes, if we want to keep supporting integer encoding.

[hernanponcedeleon]

Isn't this the same as #538?

[ThomasHaas]

It's not the same, but heavily outdated