z3 - リスト理論のサポート

Question

Z3に組み込みのリストソートがあるかどうか知りたいですか？C APIからはそう見えるようですが、C APIを使用するのではなく、SMTLIB / SMTLIB-2形式で入力することに興味があるので、Z3がそのようなサポートを提供しているかどうかを知りたいです。ありがとう。

Answer 1

はい、Z3 にはリストの並べ替え機能が組み込まれています。Z3 ガイドからの引用、セクション Recursive datatypes :

List 再帰データ型は Z3 に組み込まれています。空のリストは nil であり、コンストラクター insert を使用して新しいリストを作成します。アクセサーの head と tail は通常どおり定義されます。

そのセクションの例を次に示します: http://rise4fun.com/Z3/qXj9。