Z3: извлечение значений экзистенциальной модели - PullRequest
Новая
       34

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

2 голосов
/ 24 августа 2011

Я играю с решателем QBVF Z3 и задаюсь вопросом, возможно ли извлечь значения из экзистенциального утверждения.Допустим, скажем, у меня есть следующее: 

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

Это в основном говорит о том, что существует «наименьшее» 16-битное значение без знака.Тогда я могу сказать: 

(check-sat)
(get-model)

И Z3-3.0 радостно отвечает: 

sat
(model  (define-fun x!0 () (_ BitVec 16)
#x0000)
)

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

(get-value (x))
(get-value (x!0))

В каждом случае Z3 справедливо жалуется, что такой константы нет.Очевидно, что Z3 имеет эту информацию, о чем свидетельствует ответ на вызов (check-sat).Есть ли способ автоматически получить доступ к экзистенциальному значению через get-value или каким-либо другим механизмом?

Спасибо ..

1 Ответ

3 голосов
/ 25 августа 2011

В 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. В Википедии есть запись на сколем нормальной формы

При этом я так и не нашел удовлетворительного решения описанной вами проблемы. Например, формула может иметь много разных экзистенциальных переменных с одинаковым именем. Таким образом, не ясно, как ссылаться на каждый экземпляр в команде 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. Пример выше становится: 

(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.

...