Efficient modular arithmetic in Z3

Question

I want to work with integer modulo 3 under addition in BitVec, so basically (a+b)%3. Note BitVec is much faster than integer so I want to make sure all operations are inside BitVec.

I would need to create bit vectors of size 3. This is because compute a+b would need 3 bits, although taking the modulus, the result is 2 bits.

For example, I would need to do the following.

a = BitVecVal(3, 3)
b = BitVecVal(3, 3)

simplify(URem(a+b,3))

However, it would be nice if I only have to use BitVec(2) through out.

Is there a way to do this?

Answer 1

Short answer is, no you can't, at least not easily. A bit-vector of size N encodes exactly 2^N elements. Hence, whichever bit-vector size you choose, you can't represent exactly 3 elements. You'll have some "junk" left over even with 2-bits. This means that you have to "modify" each operation (by essentially applying remainder operation) to adjust the results properly. And none of that is going to be pretty, and if done haphazardly can cause efficiency issues.

Since you didn't really tell us what your original problem is, it's hard to opine any further. If your "universe" is 3 elements wide, then a better alternative would be to just use an enumeration of those 3 elements. Then you can encode addition by applying the distributive law: (a + b) mod 3 = ((a mod 3) + (b mod 3)) mod 3), and a similar law for multiplication. Perhaps that's sufficient to transform all your constraints? It all depends on what problem you're trying to solve. If you tell us more about your original problem, perhaps we can provide a more relevant answer.