z3 变量类型切换

Question

在玩 Z3 时，我发现了变量改变类型时的问题。我已经能够让 Int 与 Real 一起玩得很好。我还得到了 Int 转换为 BitVec 并返回。然而，一旦我达到 Int 和 BitVec 之间的转换阈值，z3 求解器就会偏离轨道并且不会 return.

我的求解器状态示例如下所示：

[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 将永远不会 return 而我必须杀死 python。同样，问题是这些变量实际上在它们可能采用的类型方面非常不稳定。我曾考虑过只使用 BitVec，但如果我想将 BitVec 和 Real 一起添加，那会导致问题。

我是不是想用 Z3 来做它不适合做的事情？有什么方法可以使用 Z3 解决此类问题吗？

Answer 1

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

z3 变量类型切换

z3 variable types switching

python

python-3.x

z3

z3py