0

4 つの並べ替え (タスク、ロール、ユーザー、および実行) を作成しました。最後のものは 2 つのパラメーターを受け取ります。次に、Run の 1 つを含め、それぞれの楽しみを宣言し、2 つのパラメーターを受け取る P を呼び出して、Run の「インスタンス」を作成します。 . 次に、ユーザーと役割の「関係」(Privs) を含む 2 つの配列と、役割とタスクの「関係」(役割) を含むもう 1 つの配列を作成しました。この 2 つの配列を使用して、ユーザー u を検索するときに Privs で役割 r を持っているかどうか、および Roles で役割 r を検索するときにタスク t を持っているかどうかをアサートします。これまでは、次のように別々の行でこれを行うことができました。

(declare-sort Task)
(declare-sort Role)
(declare-sort User)
(declare-sort Run 2)
(define-sort P (User Role) (Run User Role))
(declare-fun t () Task)
(declare-fun r () Role)
(declare-fun u () User)
(declare-const Privs (Array User Role))
(declare-const Roles (Array Role Task))


(assert (= (select Privs u) r))
(assert (= (select Roles r) t))

しかし今、私は Run (ユーザー、ロールのペア) を受け取り、関数内で同じことをアサートする楽しみを作ろうとしていますが、P のすべてのユーザーとそのすべてのロールに対してです。これは、実行ソート変数を関数に渡すことによって実行できますか??..内部の要素(ユーザー、ロール)にアクセスするために??

4

1 に答える 1

0

パラメトリック型の使用はやり過ぎのようです。「ユーザー」と「ロール」にインスタンス化された並べ替えで「実行」のみを使用します。では、なぜ「実行」をパラメトリックにする必要があるのでしょうか。パラメトリックソートとユースケースの定義はhttp://smtlib.orgで詳細に説明されています。Z3 はこの共通フォーマットを実装しているため、質問について Z3 に固有のものはありません。

于 2014-06-12T09:34:43.807 に答える