z3 - z3式を中置式に変換するには?

Question

Z3 の boolExpression を中置表現に変換したいと考えています。たとえば、z3 式 (>= t 3) があります。中置文字列 "t>=3" を取得したいのですが、C# でそれを実装する既存の Z3 API はありますか?

Answer 1

いいえ、公式 API は中置表記での式の表示をサポートしていません。この機能は、式をトラバースするために API の上に実装できます。Z3 Python API はインフィックス プリンターを実装します。実際には、Python に似た構文用と HTML 数学に似た構文用の 2 つを実装しています。これらのプリンタのソース コードは、Z3 ディストリビューションに含まれています。コードは Python で書かれていますが、任意のプログラミング言語に簡単に変換できます。コードは にありpython\z3printer.pyます。