Z3: Извлечение значений экзистенциальной модели

В Z3 get-value позволяет пользователю ссылаться только на «глобальные» объявления. Экзистенциальная переменная x является локальным объявлением. Таким образом, к нему нельзя получить доступ с помощью get-value. По умолчанию Z3 устраняет экзистенциальные переменные, используя процесс, называемый «сколемизацией». Идея состоит в том, чтобы заменить экзистенциальные переменные новыми константами и функциональными символами. Например, формула

exists x. forall y. exists z. P(x, y, z)

превращается в

forall y. P(x!1, y, z!1(y))

Обратите внимание, что z становится функцией, потому что выбор z может зависеть от y. В Википедии есть статья о нормальной форме skolem.

При этом я так и не нашел удовлетворительного решения проблемы, которую вы описали. Например, в формуле может быть много разных экзистенциальных переменных с одинаковыми именами. Таким образом, неясно, как однозначно ссылаться на каждый экземпляр в команде get-value.

Возможный обходной путь для этого ограничения — применить шаг сколемизации «вручную» или, по крайней мере, для тех переменных, значение которых вы хотите узнать. Например,

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))

записывается как:

(declare-const x (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y x)))
(check-sat)
(get-value x)

Если экзистенциальная переменная вложена в универсальный квантификатор, такой как:

(assert (forall ((y (_ BitVec 16))) (exists ((x (_ BitVec 16))) (bvuge y x))))
(check-sat)
(get-model)

Для получения значения x для каждого y можно использовать новую функцию skolem. Приведенный выше пример становится:

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))
(check-sat)
(get-model)

В этом примере sx — это свежая функция. Модель, созданная Z3, назначит интерпретацию для sx. В версии 3.0 интерпретация является функцией идентификации. Эту функцию можно использовать для получения значения x для каждого y.