Z3 4.0: получить полную модель

Question

мне нужна полная модель формулу SMTLIB2:

http://pastebin.com/KiwFJTrK

Z3 (версия 3,2 и 4,0) возвращает значения для всех переменных, но не для var4. Я попробовал некоторые настройки конфигурации, такие как

MODEL_COMPLETION = true 

но, похоже, это не сработало. Есть ли у кого-нибудь предложение? CVC3 по сравнению возвращает модель (включая var4), поэтому это не проблема SMTLIB или моего примера.

Причина, по которой мне нужно это объяснение here in detail. Короче говоря, я хочу использовать C API для инкрементного решения. По этой причине я должен использовать функцию Z3_parse_smtlib2_string несколько раз. Эта функция нуждается в ранее объявленных функциях и константах в качестве параметров. Я не могу получить эту информацию через Z3_get_smtlib_decl, потому что такого рода функции работают только тогда, когда z3_parse_smtlib_string называется, не Z3_parse_smtlib2_string.

Answer 1

Вы можете избежать этой проблемы, добавив следующий параметр в начале вашего скрипта.

(set-option :auto-config false) 

Я исправлю его для следующего выпуска. Вот краткое объяснение того, что происходит. Z3 имеет решателя для 0-1 целых задач. После предварительной обработки ваш скрипт помечен как целое число 0-1 на Z3. Значение var4 «не заботится», когда проблема рассматривается как проблема 0-1, но это не «не заботит», когда проблема рассматривается как целочисленная проблема (var4 должно быть 0 или 1). По умолчанию Z3 не отображает значения переменных «не заботятся».

MODEL_COMPLETION=true заполнит модель при запросе значений для констант, которые не входят в модель. Например, если мы выполним (eval var4), Z3 произведет инцефляцию для var4.