使用带有 Z3 的 SMT 约束时是否可以获得合法的范围信息

Question

所以基本上我正在尝试使用像 Z3 这样的通用约束求解器来解决以下 SMT 约束：

>>> from z3 import *
>>> a = BitVec("a", 32)
>>> b = BitVec("b", 32)
>>> c1 = (a + 32) & (b & 0xff)
>>> c2 = (b & 0xff)
>>> s = Solver()
>>> s.add(c1 == c2)
>>> s.check()
sat
>>> s.model()
[b = 0, a = 4294967199]

注意，很明显，只要b 落在[0x00000000, 0xffffff00] 的范围内，约束就应该是sat。

所以这是我的问题，对于像Z3 这样的 SMT 求解器来说，提供可满足约束的“范围”信息通常是否可行？谢谢。

Answer 1

如果您要求一个有效的“最宽”值范围，以便您的属性满足该范围内的所有数字，那将是一个量化的优化问题。 （此外，在这种情况下，“最宽”的含义很难表达。）不幸的是，目前，z3 和我所知道的任何其他 SMT 求解器都无法处理此类问题。

但是，如果您正在寻找 b 的最小值和最大值以使您的属性保持不变，那么您可以为此使用 Optimize 类：

from z3 import *

a = BitVec("a", 32)
b = BitVec("b", 32)
c1 = (a + 32) & (b & 0xff)
c2 = (b & 0xff)

s = Optimize()
s.add(c1 == c2)

min_b = s.minimize(b)
max_b = s.maximize(b)
s.set('priority', 'box')
s.check()

print "min b = %s" % format(min_b.value().as_long(), '#x')
print "max b = %s" % format(max_b.value().as_long(), '#x')

打印出来：

min b = 0x0
max b = 0xffffffff

[旁白：b 的最大值与您预测的不同。但是 z3 所说的对我来说看起来不错：如果您选择 a 为 0x7fffffdf，那么 a+32 将是 0x7fffffff，这都是 1s；因此c1 和c2 将等效于b 的任何值。所以这里没有什么能以任何方式真正限制b。也许你有不同的约束？]

但更重要的是，请注意，这不意味着您的属性对于b 在此范围内的所有值都是正确的：它所说的只是b 的所有值满足您的属性，这些是b 可以假设的最小值和最大值。 （在这种特殊情况下，结果表明该范围内的所有值都满足它，但这是我们自己推断出来的。）例如，如果您添加一个约束 b 是 not 5 ，你仍然会得到这些界限。我希望这很清楚！

Answer 2

Levent Erkok 提供的答案总体上是有效的，并且在大多数实际情况下，它是唯一值得考虑的答案。

但是，从技术上讲，这并不是一个完全超出 OMT 求解器范围的问题，至少在考虑的值域是有限时，并且，可能，小。在这种情况下，可以简单地枚举问题表述中的所有可能值。自然，不应期望这种方法能够很好地扩展。

---

示例。

此模型的目标是找到包含在[low, upp] 中的最大区间delta，这样对于区间内的所有值，某个布尔属性Prop 都成立。

文件： test.smt2

(set-option :produce-models true)

(declare-fun low () (_ BitVec 4))
(declare-fun upp () (_ BitVec 4))
(declare-fun delta () (_ BitVec 4))

(declare-fun Prop () Bool)

(assert (bvule low upp))
(assert (= delta (bvadd upp (bvneg low) (_ bv1 4))))

; Put in relation a domain value with the desired Property
(assert (=> (and (bvule low (_ bv0 4)) (bvule (_ bv0 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv1 4)) (bvule (_ bv1 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv2 4)) (bvule (_ bv2 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv3 4)) (bvule (_ bv3 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv4 4)) (bvule (_ bv4 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv5 4)) (bvule (_ bv5 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv6 4)) (bvule (_ bv6 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv7 4)) (bvule (_ bv7 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv8 4)) (bvule (_ bv8 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv9 4)) (bvule (_ bv9 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv10 4)) (bvule (_ bv10 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv11 4)) (bvule (_ bv11 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv12 4)) (bvule (_ bv12 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv13 4)) (bvule (_ bv13 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv14 4)) (bvule (_ bv14 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv15 4)) (bvule (_ bv15 4) upp)) Prop))

; These are just to make the solution "interesting"
; Your problem should already entail some values bvX for
; which Prop is false
(assert (=> (and (bvule low (_ bv5 4)) (bvule (_ bv5 4) upp)) (not Prop)))
(assert (=> (and (bvule low (_ bv6 4)) (bvule (_ bv6 4) upp)) (not Prop)))
(assert (=> (and (bvule low (_ bv13 4)) (bvule (_ bv13 4) upp)) (not Prop)))

(maximize delta)

(check-sat)
(get-objectives)
(get-model)

简短的解释。目标函数的目标是最大化区间[low, upp] 的大小，该区间由delta 衡量。 delta的最大值为2^N，对应区间[0, 2^N - 1]。

约束：

(assert (=> (and (bvule low (_ bv0 4)) (bvule (_ bv0 4) upp)) Prop))

表示，如果值bv0 包含在当前区间[low, upp] 中，那么属性Prop 必须成立。

约束：

(assert (=> (and (bvule low (_ bv5 4)) (bvule (_ bv5 4) upp)) (not Prop)))

表示，对于值bv5，属性Prop 不成立。 bv6 和 bv13 相同。这些约束只是为了使解决方案变得有趣。您的问题应该已经包含一些值bvX，而属性Prop 不能为true。

最优解匹配期望值：

~$ time ./optimathsat test.smt2 
sat

(objectives
 (delta (_ bv6 4))
)
( (low (_ bv7 4))
  (upp (_ bv12 4))
  (delta (_ bv6 4))
  (Prop true) )

real    0m0,042s
user    0m0,029s
sys     0m0,013s

当然，同样的公式也可以用z3解。