所以基本上我正在尝试使用像 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 求解器提供可满足约束的"范围"信息通常是否可行？谢谢。
如果您要求一个有效的"最宽"值范围，以便您的属性将满足该范围内的所有数字，那将是一个量化优化问题。(此外，在这种情况下，"最广泛"的含义可能很难表达。不幸的是，目前，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的，这就是1;因此，对于任何b值，c1和c2将等效。所以这里没有什么能真正以任何方式限制b。也许你心里有不同的约束？
但更重要的是，请注意，这并不意味着您的属性对于此范围内的所有b值都是正确的：它所说的只是在满足您的属性的所有b值中，这些是b可以假设的最小值和最大值。(在这种特殊情况下，事实证明该范围内的所有值都满足它，但这是我们自己推断出来的。例如，如果添加b不5的约束，您仍将获得这些边界。我希望这是清楚的！
Levent Erkok提供的答案在一般情况下是有效的，并且在大多数实际情况下，它是唯一值得考虑的答案。
然而，从技术上讲，这不是一个完全超出OMT求解器范围的问题，至少当所考虑的值域是有限的并且可能很小时。在这种情况下，可以简单地枚举问题公式中的所有可能值。当然，不应期望这种方法能够很好地扩展。
例。
这个模型的目标是找到包含在[low, upp]中的最大区间delta，使得对于区间内的所有值，某个布尔属性Prop成立。
文件：测试.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相同.这些约束只是为了使解决方案变得有趣。您的问题应该已经包含一些属性Prop不能为truebvX值。
最佳解决方案与所需值匹配：
~$ 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来解决。