任何人都知道如何在 Z3 中将有符号位向量转换为有符号整数？

Question

(>  (bv2int (bvxor ((_ int2bv 32) x1) ((_ int2bv 32) y1))) 0)

x1 和y1 是两个有符号的int，并且在xor 之后。如何将它们转换回带符号的 int？

Answer 1

您可以使用int2bv 和bv2int，但在大多数情况下，这些函数将被视为未解释（参见例如API doc）。如果您需要实际的语义，则必须自己实现它们。这一点都不难（只是2^i*x1[i] 术语的 if-then-elses 的一个很大的总和），但是您以这种方式获得的约束是高度非线性的，因此整数理论很可能会放弃并返回未知数。例如，请参阅 Z3 Performance with Non-Linear Arithmetic、How does Z3 handle non-linear integer arithmetic? 和 Z3 : Questions About Z3 int2bv?。