Я хочу знать, может ли Z3 сейчас дать минимальное неудовлетворительное ядро. Или есть кто разработал хорошую поддержку для этого? Кто-нибудь знает это?
Спасибо большое.
Дает ли Z3 минимальное невыполнимое ядро до сих пор?
Ответы (1)
Z3 производит неудовлетворительные ядра, но они не обязательно минимальны.
Вот пример того, как извлечь ненасыщенные ядра: http://rise4fun.com/Z3/smtc_core
Вы также можете проверить следующие вопросы:
Мягкие/жесткие ограничения в Z3
Ярлык утверждений SMT-LIB 2.0 в z3
person
Leonardo de Moura
schedule
11.05.2012
