Поддержка AUFBV?

Будет ли Z3 поддерживать AUFBV?

Для следующего скрипта:

(set-logic AUFBV)
(declare-fun x () (_ BitVec 16))
(declare-const t (Array (_ BitVec 16) (_ BitVec 16)))
(assert (= (select t #x0000) #x0000))

Онлайн-демонстрация Z3, кажется, довольна вызовом set-logic, но потом жалуется на сортировки BitVec и Array. (Между прочим, онлайн-демонстрация, кажется, устраивает вызов set-logic независимо от логического имени, даже с фиктивными именами, такими как (set-logic blarg).)

Веб-сайт SMT-Lib не упоминает ни UFBV, ни AUFBV, но, учитывая их аналоги без квантификаторов (QF_UFBV и QF_AUFBV), я надеялся, что Z3 также будет поддерживать AUFBV.

Излишне говорить, что массивы играют очень важную роль на практике. Я думаю, что логика AUFBV должна оставаться разрешимой, учитывая аргумент конечности. Было бы очень приятно увидеть поддержку Z3.

Спасибо!


z3
person alias    schedule 14.09.2011    source источник

Ответы (1)


arrow_upward
7
arrow_downward

Z3 использует команду set-logic для настройки себя. Если сценарий SMT не содержит set-logic, то включены все теоретические решатели. Если вы удалите команду set-logic из своего скрипта, то Z3 будет работать как положено.

Как вы сказали, логика AUFBV разрешима. Однако сложность действительно высока (NEXPTIME-complete). Теоретически, модуль Model Based Quantifier Instantiation (MBQI) гарантирует, что Z3 является процедурой принятия решения для этой логики, но из-за высокой сложности Z3 будет давать сбой (выполняться без памяти и/или времени) во многих скриптах.

Логика AUFBV не входит в список официально поддерживаемых логик. Z3 не распознал его и не устанавливал никакого теоретического решателя. Таким образом, чтобы использовать эту логику в Z3 3.1, вы не должны использовать команду set-logic.

Кстати, вам действительно не нужны массивы. Их можно закодировать в UFBV с помощью квантификаторов. Во многих случаях, если кто-то использует квантификаторы, лучше избегать теории массивов. Решатель теории массивов в Z3 оптимизирован для бескванторных задач.

Что касается поддельных команд, таких как (set-logic blarg), я добавил код для отображения предупреждающего сообщения о том, что логика не была распознана, и Z3 будет использовать все доступные теории. Модификация будет доступна в Z3 3.2. Я также включил AUFBV в список официально поддерживаемых логик.

person Leonardo de Moura    schedule 14.09.2011
comment
Z3 3.2 был выпущен. Это устраняет эту проблему. - person Leonardo de Moura; 21.09.2011