リストなどの任意の複雑なオブジェクトの配列をエンコードするためにZ3がサポートされているかどうかを知りたいです。ありがとう。
質問する
126 次
1 に答える
2
Z3 は再帰的なデータ型をサポートしています。それらを使用して、リスト、ツリーなどを定義できます。 Z3 チュートリアルのセクション データ型 を参照してください。任意のインデックスと値の型を使用して配列を定義することもできます。したがって、配列の配列、リストの配列などを使用できます。以下に例を示します。こちらからオンラインでも入手できます。
(declare-const l (List Int))
(declare-const a (Array Int (List Int)))
(assert (= (select a 0) l))
(assert (not (= l nil)))
(check-sat)
于 2012-12-31T05:53:22.853 に答える