使用 z3.prove 时生成更多反例

Question

是否有可能让 Z3Py 在合理的时间内生成更多的反例？

我可以使用z3.prove 生成一个反例，如下所示：

import z3

x = z3.Real("x")

rule = x > 0
goal = x < 0
z3.prove(z3.Implies(rule, goal))

给出以下输出，

counterexample
[x = 1]

但是如果我想产生更多的反例呢？

是不是唯一的方法是根据反例逐步添加规则？

对于上述情况，我可以通过这样做得到一个不同的反例，

z3.prove(z3.Implies(z3.And(rule, x!=1), goal))

但我认为当涉及到许多规则时这会很慢，所以我希望有一个更快的方法。

Answer 1

您的建议是获取多个反例的“通常”建议。 Z3 没有产生多个反例的方法，因为从外部很容易做到这一点。但是，它确实支持优化，因此如果您的目标是找到一个“最佳”或“至少一样好”的解决方案，那么这可能是一个解决方案。

对微不足道的反例添加的一个简单优化是检查反例中的所有分配是否确实需要。例如，反例可能是 (x = 5, y = 0)，但没有什么依赖于 y = 0，所以我们可以删除它，这使得反例更小（因此会有少一些）。