Позвоните в 'eval' Тайм-аут

Question

Леонардо: Спасибо за быстрые ответы!Очень ценится.

Если я передаю следующий скрипт в Z3:

(set-option :MBQI true)
(set-option :produce-models true)
(declare-fun s1 ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((s0 (_ BitVec 16))) (bvuge s0 (s1 s0))))
(check-sat)
(get-model)
(eval (s1 #x0000))

Z3 успешно создает модель, где s1 задается функция идентификации.Однако вызов eval приводит к таймауту Z3.Есть ли конкретный параметр, который мне нужно установить?

Кроме того, я заметил, что если я удалю строку:

(set-option :MBQI true)

, то Z3 отвечает unknown.Поскольку QBVF разрешима, было немного удивительно, что мне нужно было установить опцию.Это тот случай, когда мы должны установить MBQI на true во всех проблемах QBVF, или есть что-то особенное в этом экземпляре?

Спасибо ..

Answer 1

Z3 имеет несколько механизмов для обработки квантификаторов: E-match, MBQI, суперпозиция и т. Д. Хотя QBVF является разрешимым фрагментом, только механизм MBQI может решить это. Модуль электронного соответствия эффективен только для того, чтобы показать, что формулы являются неудовлетворительными. Он всегда будет неудачным (вернет неизвестное) для удовлетворительных случаев. Модуль суперпозиции эффективен в чистых (без теорий) логических формулах первого порядка.

В некоторых версиях Z3 модуль MBQI не включен по умолчанию, поскольку он очень дорогой. Некоторые приложения, такие как VCC и Spec #, используют очень сложные количественные формулы, которых нет ни в одном разрешаемом фрагменте, который может поддерживаться MBQI. Таким образом, модуль MBQI просто накладные расходы для этих приложений. В Z3 3.1 (доступно для загрузки на веб-сайте Z3) MBQI включен по умолчанию.

В грядущем Z3 3.2 будет официально поддерживаться логика UFBV. UFBV - это имя SMT-LIB для QBVF. Таким образом, вы сможете использовать (set-logic UFBV), и Z3 автоматически настроится для этой логики.

Что касается команды eval, это ошибка, я ее исправлю. Исправление будет доступно в Z3 3.2.