Я хочу перевести boolExpression в Z3 в представление infix. Например, существует выражение z3 (> = t 3), я хочу получить строку infix «t> = 3», является ли любой существующий Z3 api для реализации в C#?Как преобразовать выражение z3 в выражение infix?
Нет, официальный API не поддерживает отображение выражений в нотации infix. Эта функциональность может быть реализована поверх API для прохождения выражений. API Z3 Python реализует инфиксный принтер. На самом деле, он реализует два: один для синтаксиса типа Python и один для синтаксиса по математике HTML. Исходный код этих принтеров включен в дистрибутив Z3. Код написан на python, но может быть легко преобразован в любой язык программирования. Код находится по адресу python\z3printer.py.