Z3中的高效模运算

Question

我想在 BitVec 中进行整数模 3 的加法运算，也就是 (a+b)%3。因为 BitVec 的速度比整数快很多，所以我想确保所有的操作都在 BitVec 内部进行。

我需要创建大小为 3 的位向量。这是因为计算 a+b 需要 3 位，虽然最后取模后结果只需要 2 位。

比如，我需要做以下操作。

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

simplify(URem(a+b,3))

不过，如果我能一直使用 BitVec(2) 就好了。

有没有办法做到这一点呢？

Answer 1

简单来说，不可以，至少不容易。一个大小为 N 的位向量可以精确表示 2^N 个元素。因此，无论你选择多大的位向量，都无法准确表示 3 个元素。即使用 2 位，也会有一些“多余”的部分。这意味着你需要“修改”每个操作（基本上就是用取余操作）来正确调整结果。而且这样做并不好看，如果处理得不当，可能会导致效率问题。

因为你没有告诉我们你最初的问题是什么，所以很难进一步发表意见。如果你的“范围”是 3 个元素，那么一个更好的选择就是直接列出这 3 个元素。这样你可以通过使用分配律来编码加法：(a + b) mod 3 = ((a mod 3) + (b mod 3)) mod 3)，乘法也有类似的规律。也许这就足够解决你所有的约束了？这完全取决于你想解决什么问题。如果你能多告诉我们一些关于你原始问题的情况，也许我们能提供更相关的答案。