在 Z3 中使用 SMT 约束时是否可以获得合法范围信息
Is it possible to get a legit range info when using a SMT constraint with Z3
所以基本上我正在尝试使用像 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 求解器来说，提供可满足约束的 "range" 信息通常是否可行？谢谢。
如果您要求有效的 "widest" 值范围，以便您的 属性 满足该范围内的 all 个数字，那么是一个量化的优化问题。 （此外，"widest" 在这种情况下的含义很难表达。）不幸的是，目前，z3 和我所知道的任何其他 SMT 求解器都无法处理此类问题。
但是，如果您正在寻找 b 的最小值和最大值以使您的 属性 成立，那么您可以使用 Optimize class那：
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；因此 c1 和 c2 对于 b 的任何值都是等价的。所以这里没有任何东西真正以任何方式限制 b。也许您有不同的限制？]
但更重要的是，请注意，这 而不是 意味着您的 属性 对于此范围内的所有 b 值都是正确的：这就是说是 b 的所有满足您的 属性 的值，这些是 b 可以假设的最小值和最大值。 （在这种特殊情况下，事实证明该范围内的所有值都满足它，但这是我们自己推导出来的。）例如，如果您添加一个约束 b 是 not 5，你仍然会得到这些界限。我希望这很清楚！
Levent Erkok 提供的答案一般有效，在大多数实际情况下，这是唯一值得考虑的答案。
但是，从技术上讲，这并不是 OMT 求解器完全无法解决的问题，至少当所考虑的值域是 时finite 并且可能 small。在这种情况下，可以简单地列举问题公式中的所有可能值。当然，不应期望这种方法能够很好地扩展。
示例。
该模型的目标是找到包含在 [low, upp] 中的最大区间 delta，这样对于区间内的所有值，某个 Boolean 属性 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)
一个简短的解释。 objective 函数的目标是最大化区间 [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来求解。
所以基本上我正在尝试使用像 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 求解器来说，提供可满足约束的 "range" 信息通常是否可行？谢谢。
如果您要求有效的 "widest" 值范围，以便您的 属性 满足该范围内的 all 个数字，那么是一个量化的优化问题。 （此外，"widest" 在这种情况下的含义很难表达。）不幸的是，目前，z3 和我所知道的任何其他 SMT 求解器都无法处理此类问题。
但是，如果您正在寻找 b 的最小值和最大值以使您的 属性 成立，那么您可以使用 Optimize class那：
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；因此 c1 和 c2 对于 b 的任何值都是等价的。所以这里没有任何东西真正以任何方式限制 b。也许您有不同的限制？]
但更重要的是，请注意，这 而不是 意味着您的 属性 对于此范围内的所有 b 值都是正确的：这就是说是 b 的所有满足您的 属性 的值，这些是 b 可以假设的最小值和最大值。 （在这种特殊情况下，事实证明该范围内的所有值都满足它，但这是我们自己推导出来的。）例如，如果您添加一个约束 b 是 not 5，你仍然会得到这些界限。我希望这很清楚！
Levent Erkok 提供的答案一般有效，在大多数实际情况下，这是唯一值得考虑的答案。
但是，从技术上讲，这并不是 OMT 求解器完全无法解决的问题，至少当所考虑的值域是 时finite 并且可能 small。在这种情况下，可以简单地列举问题公式中的所有可能值。当然，不应期望这种方法能够很好地扩展。
示例。
该模型的目标是找到包含在 [low, upp] 中的最大区间 delta，这样对于区间内的所有值，某个 Boolean 属性 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)
一个简短的解释。 objective 函数的目标是最大化区间 [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来求解。