0

ときどき (または多くの場合)、問題が大きすぎて Z3 ソルバーで多くのタイムアウトが発生することがあります。そのような場合、問題をより小さなサブ問題に分割すると有益であると思います。

Theory PluginsZ3の について具体的にお聞きしたいです。

3 つの変数があるとしますA,B and C。そして、それぞれに値を割り当てています。私が指定したいくつかの制約により、割り当てられる値がA=0と であるとしB=1ます。現在、 のこれらの値に応じてA and B、Cはおそらく制約としてエンコードされていない別の一連の方程式で計算されます。その場合、A and B特定の値が割り当てられたときに、いくつかの関数にコールバックして の値を返すという理論プラグインを作成することは可能ですかC?

examples ディレクトリで理論的な例を見ましたが、あまり明確ではありません。また、ドキュメントを読んでみました。

4

1 に答える 1

1

理論プラグインは、問題をサブ問題に分割するための理想的なテクノロジーではありません。理論プラグインは通常、Z3でサポートされている理論のセットを拡張する場合に定義されます。たとえば、文字列について推論できるモジュールを含めたいとします。substringこのモジュールは、： 、などの新しい解釈されたシンボルを提供しますcontains。 この記事では、セット+カーディナリティ制約の決定手順について説明します。この手順は、Z3の理論プラグインとして実装されました。

そうは言っても、理論プラグインは現在非推奨です。これらは引き続きZ3でサポートされていますが、新しいSolverAPIとは互換性がありません。プラグインを使用するには、古い（非推奨の）APIを使用する必要があります。

Z3の理論プラグインAPIの現在の状態を説明するいくつかの関連する投稿は次のとおりです。

于 2013-02-21T00:20:41.410 に答える