Find centralized, trusted content and collaborate around the technologies you use most.
Teams
Q&A for work
Connect and share knowledge within a single location that is structured and easy to search.
Z3 如何返回一个有效的反例?以下代码
from z3 import * set_param(proof=True) x = Real('x') f = ForAll(x, x * x > 0) prove(f)
输出counterexample []。
counterexample []
我不必使用prove,但我想为f示例中的公式找到一个有效的反例。我该怎么做?
prove
f
要获得模型,您应该真正使用check,并在求解器上下文中断言您的公式的否定:
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]