Set-Logic в Z3 .NET API

Question

Как использовать set-logic при использовании функции .NET API .parseSmtlib2String (String) при использовании Z3 версии 3.1?

Я всегда получаю исключение Z3Error-Exception.

Разве это не нужно в этом случае?

Answer 1

К сожалению, команда (set-logic <symbol>) не поддерживается при использовании API parseSmtlib2String.

У нас есть это ограничение по техническим причинам.В текстовом интерфейсе команду set-logic можно использовать только до инициализации контекста.Контекст инициализируется на основе выбранной логики.Когда используется API parseSmtlib2String, контекст уже инициализирован пользователем.Таким образом, команда set-logic не выполняется и выдает ошибку синтаксического анализа.

Я признаю, что это не идеальное поведениеЯ буду исследовать альтернативы.