在Z3Py中，证明returns无反例
In Z3Py, prove returns no counterexample
Z3return怎么可能是一个有效的反例呢？
以下代码
from z3 import *
set_param(proof=True)
x = Real('x')
f = ForAll(x, x * x > 0)
prove(f)
输出counterexample [].
我不必使用 prove，但我想为示例中的 f 等公式找到一个有效的反例。我该怎么做？
要获得模型，您应该真正使用 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]
Z3return怎么可能是一个有效的反例呢？ 以下代码
from z3 import *
set_param(proof=True)
x = Real('x')
f = ForAll(x, x * x > 0)
prove(f)
输出counterexample [].
我不必使用 prove，但我想为示例中的 f 等公式找到一个有效的反例。我该怎么做？
要获得模型，您应该真正使用 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]