Является ли Z3 минимальным неудовлетворительным ядром до сих пор?

Question

Я хочу знать, может ли Z3 теперь дать минимальное неосязаемое ядро. Или кто-то разработал хорошую поддержку для этого? Кто-нибудь знает это?

спасибо.

Answer 1

Z3 производит недопустимые сердечники, но они не обязательно минимальный.

Вот пример того, как извлечь unsat ядер: http://rise4fun.com/Z3/smtc_core

Вы также можете проверить следующие вопросы:

Soft/Hard constraints in Z3

Label on SMT-LIB 2.0 assertions in z3