В 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]