Z3Py：在使用z3.p时生成更多的反例

Question

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

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

import z3

x = z3.Real("x")

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

产生以下输出

^{pr2}$

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

唯一的方法是根据反例递增地添加规则吗？在

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

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

但我相信这是缓慢的，当涉及到许多规则，所以我希望有一个更快的方法。在

谢谢！在

Answer 1

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

对简单的计数器示例加法的一个简单优化是检查是否实际需要计数器示例中的所有赋值。例如，反例可能是（x=5，y=0），但是没有任何东西依赖于y=0，所以我们可以去掉它，这使得反例更小（这样反例就会更少）。在