c# - Z3.NETAPIのSet-Logic

Question

Z3バージョン3.1を使用しているときに.NETAPI関数.parseSmtlib2String（String）を使用しているときにset-logicを使用するにはどうすればよいですか？

私はいつもZ3Error-Exceptionで終わります。

その場合は必要ありませんか？

Answer 1

残念ながら、APIを使用する場合、このコマンド(set-logic <symbol>)はサポートされていませんparseSmtlib2String。

技術的な理由により、この制限があります。テキストインターフェイスでは、コマンドset-logicはコンテキストが初期化される前にのみ使用できます。コンテキストは、選択したロジックに基づいて初期化されます。APIparseSmtlib2Stringを使用する場合、コンテキストはユーザーによってすでに初期化されています。そのため、コマンドset-logicは失敗し、解析エラーが発生します。

これは理想的な動作ではないことを認めます。代替案を調査します。