Я использую решатель Z3 SMT для решения проблемы, которую я выразил в логике QF_BV, используя язык SMTLIB 2.

Модель неудовлетворительная, и я пытаюсь заставить решатель создать ядро ненадежного.

Моя модель состоит из нескольких «обязательных» ограничений, которые я определяю, используяassert заявления.

Утверждения, которые я хочу рассмотреть для генерации ненасыщенных ядер, были определены с использованием(assert (! (EXPR) :named NAME)) построить.

Z3 дает мнеunsat, как и ожидалось. Тем не менее, Z3 всегда, кажется, сбрасывает «тривиальное» ядро ненасыщенного типа, состоящее из ВСЕХ названных утверждений.

Я знаю, что существует подмножество моих именованных утверждений, которое является несоответствующим ядром. Я нашел это ядро с помощью Yices SMT Solver, который часто дает мне относительно меньшие ненасыщенные ядра. Модель Yices такая же, как модель Z3 (в значительной степени построчный перевод с SMT2 на язык ввода Yices).

Является ли создание "хороших" ненасыщенных ядер особой функцией для решения или есть какие-то общие предложения / изменения, которые я мог бы сделать, чтобы помочь Z3 дать мне лучшее ядро?