Может ли выход промежуточных моделей быть отключен?

Question

Формула с квантификаторами содержит объявление функции trans. Z3 успешно находит модель и печатает ее. Но он также печатает модели для таких функций, как trans!1!4464, trans!7!4463 .. которые не используются нигде в модели. Что это? Как я могу отключить этот вывод?

Вот запрос: http://dl.dropbox.com/u/444947/asyn_arbiter_bound_16.smt2 и здесь выход Z3 в - http://dl.dropbox.com/u/444947/asyn_arbiter_bound_16_result.txt

Answer 1

Напомним, что модели, возвращаемые Z3 можно рассматривать как простые функциональные программы. Ваша формула находится в фрагменте UFBV. Z3 использует несколько модулей для определения этого фрагмента. Каждый модуль преобразует формулу F в «более простую» формулу F' и производит процедуру, которая преобразует модель для F' в модель для F. Мы называем эти процедуры: «преобразователи моделей». Модельные преобразователи, например, исключит интерпретации для вспомогательных функций и констант, введенных в преобразование F в F'. Некоторые вспомогательные определения не могут быть удалены, поскольку они используются для интерпретации других определений. Мы должны рассматривать их как «вспомогательные функции». Они также создают интерпретацию для символов, которые были устранены.

В вашем примере происходит следующее: последний модуль создает модель, содержащую символы и k!.... Эта модель предназначена для формулы, которая даже не содержит trans. Функция trans устранена. При применении модельных преобразователей интерпретация для trans строится на основе интерпретации всех trans!.... В этот момент все еще используются символы trans!... и k!..., поскольку интерпретация trans имеет ссылку на все символы trans!..., а интерпретация функций trans!... имеет ссылки на функциональные символы k!.... На этом этапе в модели нет ненужных символов. Однако на более позднем этапе интерпретация trans упрощается путем раскрытия определений trans!... и k!.... Таким образом, после этого этапа упрощения trans!... и k!... по существу являются «мертвым кодом».

Это, как говорится, модель, возвращаемая Z3, правильная, то есть модель для вашей формулы. Я признаю, что эти дополнительные символы раздражают и не нужны. Чтобы устранить их, мы применяем эквивалент шага устранения «мертвого кода». Мы действительно близки к следующему выпуску. Таким образом, эта функция не будет доступна в следующей версии, но я добавлю ее для выпуска следующего за ней.