Adds support for e1 & e2, e1 | e2 and e1 ^ e2, where both expressions can be either bools or integers.
We use the SMT bitvector theory for the encoding. That theory unfortunately only supports fixed-size bitvectors, which cannot represent Python's arbitrarily large integers. Additionally, for large bitvectors, things get really really slow.
So, as a compromise, we require that all integers on which bitwise operations are performed are inside some fixed range.
To set this range, there is a new command line parameter --int-bitops-size, whose default value is 8 (so 8-bit signed integers). That's obviously a very small default value, but things are realllly slow with something like 32 bits, and in the interest of having terminating tests, we use this small default, and clients can choose something larger if needed.
Adds support for
e1 & e2,e1 | e2ande1 ^ e2, where both expressions can be either bools or integers.We use the SMT bitvector theory for the encoding. That theory unfortunately only supports fixed-size bitvectors, which cannot represent Python's arbitrarily large integers. Additionally, for large bitvectors, things get really really slow. So, as a compromise, we require that all integers on which bitwise operations are performed are inside some fixed range.
To set this range, there is a new command line parameter
--int-bitops-size, whose default value is 8 (so 8-bit signed integers). That's obviously a very small default value, but things are realllly slow with something like 32 bits, and in the interest of having terminating tests, we use this small default, and clients can choose something larger if needed.This change is