在Z3上使用SMT约束时是否可以获得合法范围信息 [英] Is it possible to get a legit range info when using a SMT constraint with Z3

问题描述

因此，基本上，我正在尝试使用通用约束求解器（如Z3）解决以下SMT约束：

So basically I am trying to solve the following SMT constraint with a generic constraint solver like Z3:

>>> 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 。

Note that obviously, the constraint should be sat whenever b falls within the range of [0x00000000, 0xffffff00].

这是我的问题，像 Z3 这样的SMT求解器提供范围信息，约束是否可以满足？谢谢。

So here is my question, is it in general feasible for a SMT solver like Z3 to provide the "range" information, of a satisfiable constraint? Thanks.

推荐答案

如果您要求有效的最大值范围，以使您的财产满足该范围内的所有数字，这将是一个量化的优化问题。 （此外，在这种情况下最广泛的含义可能很难表达。）不幸的是，目前，z3或我所知的任何其他SMT求解器都无法处理此类问题。

If you are asking for a valid "widest" range of values such that your property will be satisfied for all numbers in that range, that would be a quantified optimization problem. (Also, what "widest" means in this context can be hard to express.) Currently, neither z3 nor any other SMT solver I'm aware of can handle such problems, unfortunately.

但是，如果要查找 b 的最小值和最大值以使您的财产得以保留，则可以使用 Optimize 类：

However, if you are looking for the minimum and maximum values of b such that your property will hold, then you can use the Optimize class for that:

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 s；因此 c1 和 c2 将等于 b 。因此，这里没有任何内容真正以任何方式约束 b 。

[Aside: The max value of b differs from what you predicted it would be. But what z3 is saying looks good to me: If you pick a to be 0x7fffffdf, then a+32 will be 0x7fffffff, which is all 1s; and thus c1 and c2 will be equivalent for any value of b. So nothing here really constrains b in any way. Perhaps you had a different constraint in mind?]

但更重要的是，请注意这不是 表示您的财产对所有值都是正确的在此范围内的 b ：就是说，满足您的财产的所有 b 值是 b 可以假定的最小值和最大值。 （在这种情况下，事实证明该范围内的所有值都满足该条件，但这是我们自己推论的。）例如，如果添加一个约束，则 b 为不是 5 ，您仍然会获得这些界限。我希望这很清楚！

But more importantly, note that this does not mean your property will be true for all values of b in this range: All it's saying is that of all the values of b that satisfy your property, these are the minimum and maximum values b can assume. (In this particular case, it turns out that all values within that range satisfy it, but that's something we deduced ourselves.) For instance, if you add a constraint that b is not 5, you will still get these bounds. I hope that's clear!

这篇关于在Z3上使用SMT约束时是否可以获得合法范围信息的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！