任何人都知道如何将签名的位向量转换为Z3中的带符号整数？

Question

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

X1和Y1在两个符号整数，和异或后。我如何将它们转换为带符号的int？

Answer 1

您可以使用int2bv和bv2int，但在大多数情况下，这些功能将被视为未解释（请参阅，例如API doc）。如果你需要实际的语义，你将不得不自己实现它们。这并不困难（只是对2^i*x1[i]条款的后续处理的一大笔钱），但是您以这种方式获得的限制非常非线性，因此整数理论很可能会放弃并返回未知数。参见例如Z3 Performance with Non-Linear Arithmetic，How does Z3 handle non-linear integer arithmetic?和Z3 : Questions About Z3 int2bv?。