Z3 は、再帰関数を含む式の充足可能性をチェックできないことを知っています。しかし、 Z3は境界のあるデータ構造を超えてそのような数式を処理できるのだろうか。たとえば、私はZ3 プログラムlastで最大 2 つの長さのリストと、リストの最後の要素を返すという関数を定義しました。ただし、Z3 は、 を含む数式の充足可能性を確認するように求められたときに終了しませんlast。
Z3 で制限付きリストに対して再帰関数を使用する方法はありますか?
1351 次
2 に答える
3
（これはあなたの他の質問にも関連していることに注意してください。）私たちはLeon ベリファイアプロジェクトの一部としてそのようなケースを調べました。ここで行っているのは、量指定子の使用を避け、代わりに再帰関数の定義を「展開」することです。式に length(lst) という用語がある場合は、新しい等式を導入して長さの定義を使用して拡張します: length( lst) = if(isNil(lst)) 0 else 1 + length(tail(lst))。これは、量指定子の手動インスタンス化手順と見なすことができます。
最大 2 つの長さのリストに興味がある場合は、すべての用語を手動でインスタンス化してから、用語を追加する限り、新しいリストの用語に対してもう一度それを行うだけで十分です。
isCons(lst) => ((isCons(tail(lst)) => isNil(tail(tail(lst))))
リストごとに。実際には、もちろん、これらの等式と含意を手動で生成したくはありません。私たちの場合、必要に応じてそのような公理を追加する、本質的に Z3 の周りのループであるプログラムを作成しました。
非常に興味深い特性（あなたの質問に非常に関連しています）は、一部の関数（長さなど）では、連続した展開を使用すると完全な決定手順が得られることがわかります。すなわち。データ構造のサイズを制限しなくても、最終的には SAT または UNSAT を結論付けることができます (量指定子のない場合)。
詳細については、私たちの論文Satisfiability Modulo Recursive Programsを参照してください。または、喜んでここで詳しく説明します。
于 2011-08-16T11:27:42.060 に答える
2
SULFAに関するErikReeberの研究、「ACL2の展開可能なリスト式のサブクラス」に興味があるかもしれません。彼は博士論文で、関数定義を展開して適用することにより、リスト指向の式の大規模なクラスを証明する方法を示しました。 SATベースの方法。彼は、これらのメソッドを使用して、SULFAクラスの決定可能性を証明しました。
たとえば、http：//www.cs.utexas.edu/~reeber/IJCAR-2006.pdfを参照してください。
于 2011-08-20T01:17:24.563 に答える