On: Propagating bounds through bitwise operations

[colanderman]

Took me a while but I found it!! The algorithm is surprisingly simple.

I represented the combined artihmetic and bitwise bounds for each variable as a triple, (arithLow, arithHigh, bitMask). bitMask specified which bits of the variable were fixed/known; these known bits were reflected in the arithmetic bounds. This way, `arithLow | ~bitMask` gives a bitwise lower bound, and `arithLow & bitMask` gives a bitwise upper bound. (Using arithLow or arithHigh doesn't matter here as they are identical in the known bits.)

Summing the arithmetic bounds is as you'd expect (add the lower bounds together, add the upper bounds together, deal with overflow appropriately); I won't detail that here.

The bitmasks can then be summed, for an expression `x+y`, as:

    x.bitMask & y.bitMask &
      ~(((x.arithLow | ~x.bitMask) + (y.arithLow | ~y.bitMask)) ^
        ((x.arithLow & x.bitMask) + (y.arithLow & y.bitMask)))

Essentially, this is using addition of the bitwise bounds to propagate "unknown" bits for both the lower and upper bitwise bounds, and updating the "known bits" mask from that.

I just discovered, this expression looks elegant rewritten in terms of the bitwise bounds:

    ~(x.bitwiseLower ^ x.bitwiseUpper) &
      ~(y.bitwiseLower ^ y.bitwiseUpper) &
      ~((x.bitwiseLower + y.bitwiseLower) ^ (x.bitwiseUpper + y.bitwiseUpper))

Of course these days you'd use BDDs or throw the whole problem at Z3. But this is very efficient and captures most common cases.