在Z3中优化带符号的位向量

问题描述

我正在尝试优化由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。除了在CVC4 minimize/maximize model optimization中具有不同约束条件（即b＆b）对Z3进行多次调用之外，在Z3中还有什么方法可以做到这一点吗？有人知道其他任何求解器（最好使用smtlibv2输入）来做到这一点吗？

解决方法

SMT中的所有位向量都是无符号的，但是有bvslt之类的特殊比较运算符具有符号语义。您可以添加另一个约束以强制x为正值：

(assert (bvslt #x00000000 x))

然后产生预期结果（7）。

另一种方法是将数字上移2 ^ n-1（或翻转其第一位），然后将其输入目标函数：

(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))

根据我的经验，最简单的方法是适当地增加数字。也就是说，最大化（或最小化）n位有符号位向量x等效于对n位无符号位向量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

optimization optimization smt z3