SMT 问题中基于变量部分赋值的推理

Question

我有一个简单的场景，看看 Z3 是否可以帮助我：假设有一组约束，并且可以转换为初始 SMT 问题来检查可满足性。我可以逐步获取此 SMT 问题中显示的变量值，并且我想在每一步之后检查它是否可以得出 sat/unsat 结果。示例：

a = Int('a')
b = Int('b')
c = Int('c')
s = Solver()
s.add(And(a>5, b<7, c>10))

And(a>5, b<7, c>10)

是原来的问题。然后我就得到了

a == 6

。这个问题可以简化为：

And(b<7, c>10)

。 然后我得到

b==7

，现在问题是不饱和的，即使不知道 c 的值。

有没有一种方法可以让求解器在每次对变量进行赋值后显示当前问题是否已饱和/未饱和，甚至更好的是简化并显示当前约束？

Answer 1

是的，Z3可以帮助您实现这一目标。您可以使用 check() 方法来检查可满足性，并使用 simple() 函数来简化每次分配后的约束。