z3 - カスタムシンプリファイア

Question

昔（つまり昨年）、私たちは理論プラグインをハックとして使用してカスタム単純化を実装することができました。Z3ドキュメントには、「手続き型添付ファイル」の例も含まれていました。

私の質問は非常に単純です。Z3 4.xで同じ目標を達成する方法はありますか？

特に、Z3に地上項の外部計算された評価を提供する方法に興味があります。

Answer 1

Theory プラグインは現在、Z3 4.x で非推奨としてマークされています。そのため、カスタム単純化機能を実装するために引き続き使用できますが、ユーザーは非推奨の API を使用せざるを得なくなります。

Z3 4.x では、カスタム単純化は Tactics として実装する必要があります。新しいビルド システムにより、利用可能な戦術のセットをかなり簡単に拡張できます。Z3コードベース内にタクティクスを書く方法についてのチュートリアルを書こうと思います。もちろん、このアプローチでは、C++ コードを作成する必要があります。主な利点は、戦術がすべてのフロントエンド (C、C++、.Net、Java、Python、OCaml、SMT2) で利用できることです。さらに、外部の開発者は自分の戦術を Z3 コードベースに貢献することができ、すべての Z3 ユーザーが利用できるようになります。

また、ユーザーが提供するコールバックに基づいて単純化タクティックを作成するための API をサポートする予定です。この API を使用すると、ユーザーは好みのプログラミング言語で「カスタム単純化」を作成できます。この新しい API は概念的には単純ですが、すべてのフロントエンド (C++、.Net、Java、Python、OCaml) で使用できるようにするには、多くの「ハッキング」が必要です。外部の開発者がこの機能の実装と維持に関心を持ってくれれば幸いです。多くのユーザーの利益になると確信しています。