将 SMT 约束与 Z3 一起使用时获取合法范围信息的(次)最佳方法 [英] (Sub)optimal way to get a legit range info when using a SMT constraint with Z3
问题描述
这个问题与我之前的问题有关
This question is related to my previous question
因此，考虑到典型的 32 位向量等，有效地"找到最大范围信息似乎是不合适的.但另一方面，我在考虑找到某些次最大"范围信息是否可行，这有望变得更有效率.另一件事是我们可能希望有一定的安全"保证，比如对于次最大范围内的所有元素，它们必须满足约束，但可能存在一些其他解决方案满足也有约束.
So it seems that "efficiently" finding the maximum range info is not proper, given typical 32-bit vectors and so on. But on the other hand, I am thinking whether it is feasible to find certain "sub-maximum" range info, which hopefully becomes more efficient. Another thing is that we may want to have certain "safe" guarantee, say for all elements in the sub-maximum range, they must satisfy the constraint, but there could exist some other solutions that would satisfy the constraint as well.
我目前正在探索 模型计数 技术在此设置中是否有意义.任何想法将不胜感激.谢谢.
I am currently exploring whether model counting technique could make sense in this setting. Any thoughts would be appreciated very much. Thanks.
推荐答案
一般情况
这不仅仅是效率问题.考虑一个问题，您有两个变量 a 和 b，以及一个约束:
General case
This is not just a question of efficiency. Consider a problem where you have two variables a and b, and a single constraint:
a != b
b 的范围是多少?(最大还是其他?)
What's the range of b? (maximum or otherwise?)
您可以说所有值都是合法的.但那是错误的，因为a 的选择显然会影响b 的选择.你周围的变量越多，问题就会变得越复杂.我认为在这种情况下问题甚至没有得到很好的定义，因此寻找解决方案(有效或其他方式)没有多大意义.
You can say all values are legitimate. But that would be wrong, as obviously the choice of a impacts the choice of b. The more variables you have around, the more complicated the problem will become. I don't think the problem is even well defined in this case, so searching for a solution (efficient or otherwise) doesn't make much sense.
话虽如此，如果您假设系统中只有一个变量，我认为您可以想出一个解决方案.(或者，如果您将所有其他变量固定为一些预定义的常量.)如果您愿意沿着这条路走下去，那么您可以通过简单地证明量化公式来实现二分搜索算法来找到合理大小的范围
Having said that, I think you can come up with a solution if you assume there's precisely one variable in the system. (Or, alternatively, if you fix all the other variables to some predefined constants.) If you're willing to go down this path, then you can implement a binary search algorithm to find a reasonably sized range by simply proving the quantified formula
Exists([b], And(b >= minBound, b <= maxBound, Not(constraints)))
一旦你获得了unsat，你就有了你的范围.只要你得到 sat，你就可以调整你的 minBound/maxBound 以在更小的范围内搜索.在最坏的情况下，这可能会变成线性游走，但是您可以通过确保在每一步中都减小一个显着的大小来减少"这个搜索.这可能是整个搜索的参数，具体取决于您希望间隔有多大.必须在尝试找到最大范围和您想在此搜索中花费多长时间之间做出选择.当然，如果你削减太多，你可能会错过一个很大的间隔，但这是效率的代价.
Once you get unsat for this, you have your range. So long as you get sat, you can adjust your minBound/maxBound to search within smaller ranges. In the worst case, this can turn into a linear walk, but you can "cut-down" this search by making sure you go down a significant size in each step. That could be a parameter to the whole search, depending on how large you want your intervals to be. It'll have to be a choice between trying to find a maximal range, and how long you want to spend in this search. Of course, if you cut-down too much, you can miss a big interval, but that's the cost of efficiency.
Example1(很好的例子)有一个约束条件是 b != 5.然后你的搜索会很快，根据你要去的分支，你会找到 [0, 4] 或 [6, 255] 假设 8 位话.
Example1 (Good case) There's a single constraint that says b != 5. Then your search will be quick and depending on which branch you'll go, you'll either find [0, 4] or [6, 255] assuming 8-bit words.
Example2(坏情况)有一个约束条件是b is even.那么您的搜索将表现出最坏情况的行为，如果您的缩减"大小为 1，您可能会在确定 [0, 0] 之前迭代 255 次；假设 z3 为您提供每次调用中的最大奇数.
Example2 (Bad case) There's a single constraint that says b is even. Then your search will exhibit worst-case behavior, and if your "cut-down" size is 1, you'll possibly iterate 255 times before you settle down on [0, 0]; assuming z3 gives you the maximum odd number in each call.
我希望这说明了这一点.不过，总的来说，我认为您会更接近实际应用程序的好案例"，即使您的缩减尺寸很小，您也很可能会在几次迭代中收敛.当然，这完全取决于您的问题域，但我希望它适用于一般的软件分析.
I hope that illustrates the point. In general, though, I'd assume you'd be closer to the "good case" for practical applications and even if your cut-down size is minimal you can most likely converge in a few iterations. Of course, this entirely depends on your problem domain, but I'd expect it to hold for software analysis in general.
这篇关于将 SMT 约束与 Z3 一起使用时获取合法范围信息的(次)最佳方法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
