Как только вы используете квантификаторы, все ставки отключаются, так как логика становится полуразрешимой. Z3 делает хорошую работу здесь и возвращает одно решение, а затем сдается. Я не думаю, что вы можете ожидать чего-то лучшего, если вы не используете некоторые собственные процедуры принятия решений.
у проверить формулу формы:
Exists p . ForAll x != 0 . f(x, p) > 0
Реализация (которая не работает) следующая:
def f0(x0, x1, x, y):
return x1 ** 2 * y + x0 ** 2 * x
s = Solver()
x0, x1 = Reals('x0 x1')
p0, p1 = Reals('p0 p1')
s.add(Exists([p0, p1],
ForAll([x0, x1],
f0(x0, x1, p0, p1) > 0
)
))
#s.add(Or(x0 != 0, x1 != 0))
while s.check() == sat:
m = s.model()
m.evaluate(x0, model_completion=True)
m.evaluate(x1, model_completion=True)
m.evaluate(p0, model_completion=True)
m.evaluate(p1, model_completion=True)
print m
s.add(Or(x0 != m[x0], x1 != m[x1]))
Формула не выполняется.
С участиемf0() >= 0, единственный выход(0, 0).
я хочу иметьf0() > 0 и сдерживать(x0, x1) != (0, 0).
Что-то, что я ожидал бы, является:p0, p1 = 1, 1 или же2, 2 например, но я не знаю, как удалить0, 0 из возможных значений дляx0, x1.