z3 - 匿名関数

Question

Yicesでの無名関数（ラムダ式）のサポートは非​​常に役立つことがわかりました。現在、Z3を使用してツールを実装しようとしていますが、この機能がサポートされているかどうかを確認できませんでした。-smt2フラグを使用してツールを呼び出しています。ご協力いただきありがとうございます。

Answer 1

私の知る限り、ラムダ式は Z3 ではサポートされておらず (主な Z3 開発者の 1 人である Nikolaj Bjorner によるこの回答を参照)、SMTLib2 標準の一部でもありません。Yices や veriT などのラムダ式をサポートするソルバーは、SMTLib2 標準のカスタム拡張機能としてサポートしています。

必要に応じて (質問に例を追加して説明したい場合があります)、Z3 マクロ ( define-fun)、またはZ3Pyのようなフロントエンドを試すことができます。これにより、SMTLib コードを手動で記述する場合と比較して、Z3 の操作が大幅に簡素化されます。