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

Question

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

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.这个问题好像问的一样，但是我没看懂它的答案，我在找python的答案。

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

标签： z3z3py

Answer 1