z3 - Z3 のチェーン (データログ) プログラム

Question

特定のプログラム分析は、制限された形式の Datalog プログラムに属するチェーン プログラム (文脈自由言語に対応) としてエンコードできます。チェーン プログラムの各ルールの形式は次のとおりです。

p(X,Y) :- q0(X,Z1), q1(Z1,Z2), q2(Z2,Z3)..., qn(Zn,Y)

私の質問は、Z3 がチェーン プログラムの構造を利用して、任意のデータログ プログラムを評価するよりも効率的にチェーン プログラムを評価できるかどうかです。

Answer 1

Z3の有限状態データログエンジンは、ボトムアップ評価を使用します。有効にできるマジックセット変換を実行するオプションが含まれています。この変換は、チェーンプログラムを含む場合には不思議に思います。「：magic-sets-for-queries」を「true」に設定すると、このオプションを有効にできます。お役に立てれば