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)

以及类似的乘法定律来对加法进行编码。也许这足以改变你所有的限制？这完全取决于您要解决的问题。如果您告诉我们更多有关您原来的问题的信息，也许我们可以提供更相关的答案。