1

Z3 で「for all」を正しく使用する方法を誰かが教えてくれませんか。ドキュメントを調べましたが、情報が見つかりませんでした。私がやろうとしていることは

「foo」内で、Z3で次のことを言う必要があります

"let (u,r) be runnable(t) in { (assert ((u,r) is in users) (assert (r,t) is in roles)) }"

私が知らないのは、ランナブルの最初の要素を取得してユーザーにあることをアサートし、2 番目の要素をロールにあることをアサートする方法です。

(declare-sort Task) (declare-sort Role) (declare-sort User) (declare-fun runnable (Task) (User Role)) (declare-fun perm (Role Task) Bool) (declare-fun users (User Role) ) ブール)

(assert (forall (t タスク)) (foo))

(check-sat) (get-model)

4

1 に答える 1

1

この例は整形式の SMT2 ではありません。関数は複数のオブジェクトを返すことができません。データ型と量指定子の使用例については、Z3 ガイドを参照してください。

于 2014-06-10T12:14:11.187 に答える