Z3の最近のバージョンでは、Z3_contextとの概念が切り離されていZ3_solverます。APIは主にこれらの変更を反映しています。たとえばpush、コンテキストでは推奨されておらず、追加の引数としてソルバーを取るように再指定されています。
ただし、理論のインターフェースは更新されていません。理論は今でもコンテキストから作成されており、私が知る限り、ソルバーに明示的に関連付けられることはありません。
コンテキストから作成された理論は、コンテキストから作成されたすべてのソルバーに常に関連付けられると考えることができますが、私たちの経験からすると、そうではないようです。代わりに、ユーザー定義の理論は完全に無視されているようです。
Z3_solvers とs の組み合わせの正確なステータスは何Z3_theoryですか?
Theory プラグインはずっと前 (バージョン 2.8) に導入されました。それ以来、Z3 は大幅に変更されました。Z3 4.x では非推奨と見なされます。これらは引き続き古い API で使用できますが、新機能、特に Z3 ソルバー オブジェクト ( Z3_solver) では使用できません。
現在の Z3 には、さまざまなソルバーがあります。最も古いもの (フォルダに実装されているsrc/smt) は と呼ばれsmt::contextます。Theory プラグインは、実際にはこの古いソルバーの拡張機能です。smt::context多くの理論と量化子をサポートしているため、汎用ソルバーと言えます。実際、Z3 4.3.1 では、利用可能な唯一の汎用ソルバーです。ただし、Z3 で計画している新機能には適していない古いアーキテクチャに基づいていると思います。私の計画は、将来、ここで説明されているアーキテクチャに基づくソルバーに置き換えることです。さらに、私たちはもう実際に取り組んでいsmt::contextません。私たちは本質的にそれを維持し、バグを修正しているだけです。
Z3 ソース コードをリリースした後、ユーザーが Z3 コード ベース内に拡張機能を追加できるようになるため、セオリー プラグインのサポートはもう必要ないと考えました。ただし、このビューは単純すぎるため、ユーザーはさまざまなプログラミング言語で拡張機能を作成できなくなります。そのため、現在の計画では、Z3 で最終的に利用可能になる新しいソルバー用の理論プラグインを最終的に用意することです。目標は、次のような API を持つことです。
Z3_solver Z3_mk_mcsat_solver(Z3_context ctx, Z3_mcsat_ext ext);
この API は、指定された拡張子を使用して新しいソルバー オブジェクトを作成しますext。
それまでの間、次のような関数を使用して API を拡張することもできます。
Z3_solver Z3_mk_smt_solver(Z3_context ctx, Z3_theory t);
smt::contextこれにより、指定された理論プラグインの使用に基づいて新しいソルバー オブジェクトが作成されます。このソリューションは概念的には単純ですが、それを実現するには多くの「配管」が必要です。オブジェクトを調整し、 (例: )Z3_theoryのコピーを作成する機能で理論プラグインを使用できないようにするいくつかの制限を修正する必要があります。誰かがこのインターフェイスに非常に興味を持っている場合、私はそれにサイクルを投資します (注: 私たちは持っていました理論プラグインのユーザーはほんの一握りです）。計画は最終的に交換することなので、私はそれについてあまり興奮していません.smt::contextMBQIsmt::context