python - z3变量类型切换

Question

在使用 Z3 时，我发现变量更改类型时会出现问题。我已经能够让 Int 与 Real 很好地配合。我还得到了 Int 来转换为 BitVec 并返回。但是，似乎一旦我达到 Int 和 BitVec 之间转换的阈值，z3 解算器就会偏离轨道并且不会返回。

我的解算器状态的示例如下所示:

[271733878 == a,
562383102 == b,
4023233417 == c,
1732584193 == d,
e ==
BV2Int(int2bv(d) ^
    int2bv(BV2Int(int2bv(b) &
                  int2bv(BV2Int(int2bv(c) ^
                                int2bv(a)))))),
f == e,
305419896 == g]

这实际上工作得很好。然而，如果我再进行一次 int2bv 转换，Z3 将永远不会返回，我必须杀死 python。同样，问题是这些变量实际上非常不稳定，就它们可能采用的类型而言。我曾考虑过只使用 BitVec，但如果我想将 BitVec 和 Real 添加在一起，就会出现问题。

我是否试图将 Z3 用于它不适合的用途？有什么方法可以使用 Z3 来解决此类问题吗？

Answer 1

对于 int2bv 和 bv2int 转换没有特殊的调整，因此您通常会留下后备机制，即位爆炸，然后进行位向量和算术推理的精心组合。我建议您尝试延迟从位向量到整数的转换，直到前端使用最后的手段。在该示例中，没有特殊原因需要继续将中间位向量转换为整数。 Z3 不会检测到这种冗余。它还必须考虑到整数到位向量的转换可能是有损的，因为它是以位宽为模的。