使用 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

你提出的是"usual"建议多取一个反例。 Z3 没有产生多个反例的方法，因为从外部很容易做到这一点。但是，它确实支持优化，因此如果您的目标是准确找到一个 "best" 或 "at least as good" 解决方案，那么这可能是一个解决方案。

对简单的反例添加的一个简单优化是检查反例中的所有赋值是否实际上是必需的。例如，反例可能是 (x = 5, y = 0)，但不依赖于 y = 0，因此我们可以删除它，这会使反例变小（因此会有少一些）。

Generate more counterexamples when using z3.prove