Спасибо за предложение. Я рассмотрю возможность для будущих версий Z3. Однако пользователь не будет иметь контроля над сигнатурой символа функции сколем, генерируемой Z3. Z3 выполняет много упрощений до сколемизации, и шаг сколемизации пытается минимизировать число зависимостей от универсальных переменных. Я обновил свой ответ примером того, как извлечь экзистенциальную переменную, вложенную в универсальный квантификатор.
аю с решателем 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или какой-то другой механизм?
Спасибо..