如何使用 z3 获取变量的有效范围答案

【问题标题】：how to use z3 to get valid range of a variable如何使用 z3 获取变量的有效范围
【发布时间】：2020-08-12 07:40:17
【问题描述】：

在给定一些约束的情况下，我想找到变量可以具有的有效值范围。例如，

x = Int('x')
s = Solver()
s.add(x >= 1)
s.add(x < 5+2)

有什么方法可以让 z3 为这个变量打印 1..6 吗？

我尝试使用以下方法，但 range() 仅适用于声明。

print("x.range():", x.range()) # this does not work

注意： 1.这个question好像问的一样，但是我没看懂它的答案，正在找python的答案。

回复@Malte：我不是在寻找所有答案，我只是想将多个约束简化到一个有效范围内。如果变量两侧的约束不能合并，那么至少只有一侧的约束，如上述问题中所述。

【问题讨论】：

我不明白让 Z3 打印 [1,6] 的潜在值范围 x 与让 Z3 打印所有有效模型有何不同。请说清楚。请注意，您链接到的问题似乎与您的不同，因为您希望找到所有模型的简单表示，而在链接的问题中，需要初始约束集的简化表示。
范围是否很大很重要。例如，如果范围恰好是 [1,10000]，我不想枚举所有 10k 答案来确定其范围。
在链接的答案中，它简化了一侧的所有约束，即 >= 一侧。但是我要求的是范围，这相当于简化了双方的约束。
正如我的回答中提到的，Z3 不直接支持您的要求。列举所有可能的答案是您唯一的选择。连同提交功能请求 (github.com/Z3Prover/z3/issues)，当然 :-)
感谢您的确认。顺便说一句，提到的问题有一个非 python 的答案，是否有对应的 python 等效项？

标签： z3 z3py

【解决方案1】：

作为 SAT/SMT 求解器，Z3“只”需要找到一个模型（满足分配）来表明一个公式是可满足的。因此不直接支持查找所有模型。

不过，问题经常出现，解决方案是反复查找然后阻止（假设为否定形式）模型，直到找不到更多模型为止。例如，对于您的 sn-p 代码：

x = Int('x')
s = Solver()
s.add(x >= 1)
s.add(x < 5+2)

result = s.check()

while result == sat:
  m = s.model()
  print("Model: ", m)
  
  v_x = m.eval(x, model_completion=True)

  s.add(x != v_x)
  result = s.check()

print(result, "--> no further models")

执行脚本会产生您要求的解决方案，尽管形式不太简洁：

Model:  [x = 1]
Model:  [x = 2]
Model:  [x = 3]
Model:  [x = 4]
Model:  [x = 5]
Model:  [x = 6]
unsat --> no further models

一般来说，

您将遍历所有变量（此处：仅x）
模型完成对于其值不影响可满足性的变量是必要的；由于任何值都可以，因此它们不会在模型中明确显示

回答提供更多详细信息的相关问题：

【讨论】：

感谢您的回答。我在问题中添加了更多细节。

【解决方案2】：

这个问题偶尔会出现，不幸的是，答案不是很简单。这实际上取决于您的约束是什么以及您正在尝试做什么。见：

Is it possible to get a legit range info when using a SMT constraint with Z3

和

(Sub)optimal way to get a legit range info when using a SMT constraint with Z3

本质上，如果您有多个变量，问题就太难了（我想说甚至没有很好的定义）。如果你只有一个变量，你可以在某种程度上使用优化器，假设变量确实是有界的。如果您有多个变量，一个想法可能是将除一个之外的所有变量都固定为满足常量，并根据对其他变量的常量分配计算最后一个变量的范围。但同样，这取决于您真正想要实现的目标。

请看看上面的两个答案，看看它是否对你有帮助。如果没有，请向我们展示您的尝试：当您发布一些代码并查看如何改进/修复它时，Stack-overflow 效果最佳。

【讨论】：