z3变量类型切换

在玩Z3时，我发现变量在变化类型时会出现问题。我已经能够得到Int与Real发挥很好。我也得到Int转换为BitVec，然后回来。但是，似乎一旦我达到了在Int和BitVec之间转换的阈值，z3解算器就会退出轨道并且不会返回。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来解决这类问题？

来源

2016-03-15 Owl Owl

对于int2bv和bv2int转换没有特别的调整，所以你经常留下的回退机制会发生位冲突，然后进行位向量和算术推理的精细组合。我建议您尝试延迟从位向量到整数的转换，直到您在前端的最后一招。在这个例子中，没有特别的理由继续将中间位向量转换为整数。 Z3不检测这种冗余。它还必须考虑到整数到位矢量转换可能是有损的，因为它是以位宽为模的。

来源

2016-03-15 13:09:27

感谢您的反馈意见。如你所述，我肯定会延迟转换。不过，我也希望在某些时候能够更多地投入到这些转换中，因为我认为将来可能需要更有效的转换方法（或者甚至是两者之间的隐式转换）。 –

出于兴趣，您是否有一个实际需要两种理论之间转换的应用程序，或者您是否为了方便而在它们之间进行转换，并且所有这些都可以完全在其中一种理论中完成？ –

z3变量类型切换

回答

相关问题