smt - Z3 は、再帰関数を含む数式の充足可能性をチェックできますか?

Question

再帰関数を含むZ3 チュートリアルの例をいくつか試しています。次の例を試してみました。

1. フィボナッチ(セクション 8.3)
2. IsNat (セクション 8.3)
3. 誘導性(セクション 10.5)

Z3は、上記のすべての例でタイムアウトします。しかし、チュートリアルは、誘導のみが非終了であることを暗示しているようです。

Z3 は、再帰関数を含む式の充足可能性をチェックできますか? または帰納的な事実を処理できませんか?

Answer 1

Z3 チュートリアルのこれらの例は、Z3 の背後にあるテクノロジーの制限を説明するためにあります。

これらの例では、Z3 は次の 2 つの理由で失敗します。

1. Z3 によって作成されたモデルは、解釈されていない機能記号ごとに解釈を割り当てます。モデルは機能的なプログラムとして見ることができます。現在のバージョンでは、再帰的な定義は生成されません。最初の例は満足できるものですが、再帰的な定義をサポートしていないため、Z3 は fib の解釈を生成できません。Z3 をこの方向に拡張する計画があります。

2. Z3 は帰納法による証明をサポートしていません。例 2 と 3 は満足できませんが、Z3 は帰納法による証明をサポートしていないため失敗します。また、そのための基本的なサポートを追加する計画もあります。

これらの項目は私の TODO リストにありますが、今年は取り掛かりません。