Гарантии о частичной модели, когда check-sat возвращает неизвестное

Question

У меня вопрос по частичным моделям от z3. Я искал в Интернете информацию о них, но, к сожалению, я не нашел ничего, кроме того, что их иногда можно получить, когда проверка не удалась.

В случае, если (check-sat) возвращает unknown, каковы гарантии в отношении частичной модели (если она может быть получена)? Это гарантированно всегда будет здоровым?

Меня особенно интересует неполнота, связанная с квантификатором, хотя я сомневаюсь, что это имеет значение.

Заранее спасибо.

Answer 1

Поскольку, насколько я знаю, официальных гарантий нет, я ожидаю, что (неудовлетворительный) ответ таков: частичная модель сильно зависит от конкретной проблемы и «средств» (шаги препроцессора, эвристика, решатели, тактика). , случайные семена, тайм-ауты, ...) Z3 применяется для решения проблемы.

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