1

标题说明了一切。我尝试将 -1 呈现为以下内容：(_ bv-1 32)，并且 z3 抱怨。

如何呈现约束，例如3x - 5y <= 10位向量？出于某种原因，我不想使用线性整数。

4

1 回答 1

2

这通常通过二进制补码编码来完成。简短的版本是，

-x = flip(x) + 1

whereflip(x)简单地翻转x.

于 2016-05-05T11:19:55.333 回答