z3py: использование экзистенциального квантификатора

Этот сценарий

from z3 import *
solver = z3.Solver()
x = Int('x')
def f(y):
    return y+y
solver.add(x >= 0, x < 10, Exists(x, f(x) == 4) )
print solver.check()
print solver.model()

дает мне

sat
[x = 0]

как ответ. Это не то, чего я хочу или ожидаю. В ответ хотелось бы увидеть

sat
[x = 2]

Я нашел два других сообщения, идущих в том же направлении ((Z3Py), объявляющая функцию и Quantifier в Z3), но что-то не получается.

Как в этом случае использовать квантор существования, чтобы получить адекватный ответ?


z3 z3py quantifiers
person John Smith    schedule 24.08.2017    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Экзистенциальное связывает другой x, область действия которого ограничена телом формулы. Следовательно, ваши ограничения фактически равны (0 ≤ x ‹10) ∧ (∃ x '. F (x') == 4). Оба конъюнкта удовлетворяются моделью, в которой x = 0; в частности, второй конъюнкт удовлетворяется в этой модели, потому что x ' может быть 2.

Похоже, вы хотите еще больше ограничить x, а не только неравенством. Попробуйте следующее (не проверено)

solver.add(x >= 0, x < 10, f(x) == 4)

а затем распечатайте модель.

person Malte Schwerhoff    schedule 24.08.2017
comment
Большой. Тогда моей первой проблемой была сфера действия exists. Я изменил утверждение на solver.add(Exists(x, And(f(x) == 4, x >= 0, x < 10))), и теперь решатель SMT возвращает sat или unsat в зависимости от моего ввода правильно. Тем не менее, я не могу заставить решатель дать мне подсказку о x, удовлетворяющем утверждению. Как ты можешь это сделать? Решение, о котором вы упомянули выше, является правильным, поскольку оно делает то, что вы говорите, но я хочу использовать квантификаторы в другом контексте (проверка модели) и мне нужен результат. - person John Smith; 24.08.2017
comment
Лучший способ добиться этого - сколемизировать формулу самостоятельно, то есть вставить новые функциональные символы, которые заменяют экзистенциальные элементы и которые зависят от универсальности в области видимости. Таким образом, вы контролируете имена этих функций, и они будут иметь интерпретацию функций в модели. - person Christoph Wintersteiger; 24.08.2017