私はそれがZ3 cannot check the satisfiability of formulas that contain recursive functionsを知っています。しかし、私はZ3がこのような公式を有界データ構造上で扱うことができるのだろうかと思います。たとえば、長さが最大2つのリストをmy Z3 programに定義し、関数をlastと定義してリストの最後の要素を返しました。ただし、lastが含まれている数式の充足可能性を確認するよう求められた場合、Z3は終了しません。Z3は、有界データ構造に対する再帰関数の充足可能性をチェックできますか？
Z3の有界リストより再帰関数を使用する方法はありますか？
（これはあなたの他の質問にも関連しています）このようなケースをLeon verifierプロジェクトの一部として検討しました。量子の使用を避け、再帰関数の定義を "アンロール"することです：数式中の長さ（lst）という用語を見ると、長さの定義を使用して長さの定義を使用して展開します。長さlst）= if（isNil（lst））0 else 1 + length（tail（lst））。これを手動定量化器インスタンス化プロシージャとして見ることができます。
あなたが最も2の長さのリストに興味があるなら、すべての用語のマニュアルインスタンス化を行って、その後、新しいリストの条件のために、もう一度それをやってする限り、あなたは用語を追加すると、十分なはずです：
isCons（lst）=>（isCons（tail（lst））=> isNil（tail（tail））））
実際には、もちろんこれらの等質を生成したくない私たちの場合は、本質的にZ3の回りのループであるプログラムを書いて、必要に応じてそのような公理を追加しています。
非常に興味深いプロパティあなたの質問）は、いくつかの機能（長さなど）では、連続したアンロールを使用すると、完全な決定手順が得られることが判明しています。つまりあなたがデータ構造のサイズを制限しなくても、最終的にSATかUNSAT（quantifier-freeの場合）を終えることができます。
私たちの論文Satisfiability Modulo Recursive Programsに詳細が記載されています。詳しくはこちらからもらえます。
あなたは、SULFA、ACL2の「Unrollable List Formulasのサブクラス」に関するErik Reeberの研究に興味があるかもしれません。彼は博士論文で、大量のリスト指向の式がアンロールによってどのように証明できるかを示しましたSATベースのメソッドを適用することができます。彼は、これらの方法を用いてSULFAクラスの決定性を証明した。
たとえば、http://www.cs.utexas.edu/~reeber/IJCAR-2006.pdfを参照してください。
（最後の関数も、私たちの技術が完全な決定手続きをもたらす関数のカテゴリに含まれていると付け加えるべきです） – Philippe
私はPhilippeに同意します。ところで、あなたのスクリプトで 'define-fun'マクロを使って' last'を定義することができます。マクロはZ3によって自動的に展開されます。 http://rise4fun.com/Z3/9xVs –
@Philippeは再利用可能な再帰関数定義をアンロールするために書いたプログラムですか？あなたのプログラムはSMT-LIBプログラムを入力として受け取りますか？ – reprogrammer