Мне нужно назвать некоторые утверждения в моей модели z3, чтобы она могла генерировать ненасыщенные ядра.
Я могу сделать это вручную следующим образом:
(assert (! (assertion) :named x))
Мне просто нужно сделать это напрямую с помощью .NET API.
любая помощь?
Z3 не поддерживает это напрямую через .NET API. Вместо этого следует создать логическую константу (имя, например, x), которую затем можно использовать для утверждения условных ограничений, например,
solver.AssertAndTrack(constraint, x);
Затем ограничение получает имя x, и эта константа используется для ссылки на него в ненасыщенных ядрах. Пример на Python см. также в этом другом вопросе; стратегия та же самая в .NET API, только имена функций немного отличаются.
