优化 Z3 中的带符号位向量

Question

我正在尝试优化由 Z3 中的位向量组成的表达式（代码在例如 https://rise4fun.com/Z3/tutorial/optimization 中运行）：

(declare-const x (_ BitVec 32))
(assert (bvslt x #x00000008))
(maximize x)
(check-sat)
(get-objectives)

我得到的结果是：

sat
(objectives
  (x 4294967295)
)

这是 32 位的最大 int 0xffffffff，将被标记为 -1。但是，我想获得带符号的最大值，即 7。在 Z3 中有什么方法可以做到这一点（除了多次调用具有不同约束（即 b&b）的 Z3，如中）？有谁知道任何其他求解器（最好使用 smtlibv2 输入）来做到这一点？

Answer 1

SMT 中的所有 bit-vectors 都是无符号的，但有一些特殊的比较运算符，如 bvslt，具有带符号的语义。您可以添加另一个约束来强制 x 为正数：

(assert (bvslt #x00000000 x))

然后生成预期结果 (7)。

另一种方法是将数字向上移动 2^n-1（或翻转他们的第一位），然后可以进入 objective 函数：

(declare-const x (_ BitVec 32))
(assert (bvslt x #x00000008))
(maximize (bvadd x #x80000000))
(check-sat)
(get-objectives)
(get-value (x))

说

sat
(objectives
 ((bvadd x #x80000000) 2147483655)
)
((x #x00000007))

Answer 2

根据我的经验，最简单的方法就是适当地向上移动数字。也就是说，最大化（或最小化）n-bit signed bit-vector x 等同于对 n-bit unsigned bit-vector x + 2^{n − 1}。也就是说，就在您调用最大化或最小化之前，将 2^n-1 添加到您要优化的数量，从而使原始值范围超过 [−2^{n − 1}, 2^{n − 1}) 而不是优化器将看到的 [0, 2ⁿ).

您可以在 2017 年的 z3 github 跟踪器中看到结论相同的讨论：https://github.com/Z3Prover/z3/issues/1339

优化 Z3 中的带符号位向量

Optimize signed bitvectors in Z3

optimization

smt

z3