在 Z3Py 中，证明不返回反例

Question

Z3 如何返回有效的反例？ 以下代码

from z3 import *
set_param(proof=True)
x = Real('x')
f = ForAll(x, x * x > 0)
prove(f)

输出counterexample [].

我不必使用prove，但我想找到一个有效的反例来代替示例中的公式f。我该怎么做？

Answer 1

要获得模型，您应该真正使用check，并在求解器上下文中断言公式的否定：

from z3 import *
s = Solver()
x = Real('x')
f = x * x > 0
# Add negation of our formula
# So, if it's not valid, we'll get a model
s.add(Not(f))
print s.check()
print s.model()

这会产生：

sat
[x = 0]