3 ms·

You can propagate bitwise bounds (whether each bit may be 0 or 1) over arithmetic operations efficiently as well. I worked this out a decade ago too, I forget t

You can propagate bitwise bounds (whether each bit may be 0 or 1) over arithmetic operations efficiently as well. I worked this out a decade ago too, I forget the specifics but I remember for addition/subtraction I think it had something to do with interleaving upper/lower bounds bitmasks. If I can dig up my code I'll post it here.

someguydave 3y ago
Yes please!
- colanderman 3y ago
  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.

someguydave 3y ago

Yes please!

colanderman 3y ago
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.