I have a number of constraints asserting for bits in BitVec and I wonder what is the most efficient way of asserting constraints for a specific bit in a BitVec?
Assume I want to assert that the 5th bit in a BitVec is 1, is there any way that is more efficient (lower check time) than this?
bitvec = BitVec('bitvec',10)
s.add(Extract(5,5,bitvec)==1)
From what I understand about the internals of Z3 (from experimenting and looking at the source) this is the most efficient way possible.
As I understand it extracts and concats have no solver runtime cost. They just split the bits into parts.
The only alternative would be to apply an and operation to extract the bit. But that should turn into an extract after simplification (which indeed you can test by running the simplify tactic. It's a fun rewrite to observe).
