如何使用z3获得变量的有效范围

问题描述

在某些约束条件下，我想查找变量可以具有的有效值范围。例如，

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：我不是在寻找所有答案，我只是想将多个约束简化为有效范围。如果变量两侧的约束不能合并，则至少在上述问题中提到的一侧。

解决方法

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

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

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）
对于值不影响可满足性的变量，必须完成模型；因为任何值都可以，所以它们在模型中不会明确显示

相关问题，其答案提供了更多详细信息：

这个问题偶尔会出现，不幸的是答案不是很简单。这实际上取决于您的约束条件以及您要尝试执行的操作。参见：

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

从本质上讲，如果您有多个变量，则问题将非常棘手（我想说的甚至定义不明确）。如果您只有一个变量，则可以在一定程度上使用优化器，前提是该变量确实是有界的。如果您有多个变量，则一个想法可能是将除一个之外的所有变量都固定为满足常数，然后根据对其他变量的常数分配来计算最后一个变量的范围。但同样，这取决于您真正想要实现的目标。

请查看以上两个答案，看看是否有帮助。如果没有，请向我们展示您的尝试：在您发布一些代码并查看如何对其进行改进/修复时，堆栈溢出的效果最佳。

z3 z3py