0

Z3 如何返回一个有效的反例?以下代码

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

输出counterexample []

我不必使用prove,但我想为f示例中的公式找到一个有效的反例。我该怎么做?

4

1 回答 1

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]
于 2018-06-11T15:22:41.190 回答