1

z3 の map 演算子の制限について知りたいです。z3 のチュートリアル ( http://rise4fun.com/z3/tutorial ) によると、「Z3 は、配列に対してパラメーター化されたマップ関数を提供します。配列の範囲に任意の関数を適用できます。」

組み込み関数または(declare-fun ...)構文で宣言された関数をマップしているときに、マップが機能しているように見えます。(define-fun ...)構文で定義された関数 (実際にはマクロ) でマップを使用しようとすると、「無効な関数宣言参照、名前付き式 (別名マクロ) を参照できません」というエラーが表示されます。

ユーザー定義関数を配列にマップする標準的な方法はありますか?

これが私の混乱を示すコードです。

;simple function, equivalent to or
(define-fun my-or ((x Bool) (y Bool)) Bool (or x y))
(assert (forall ((x Bool) (y Bool)) (= (my-or x y) (or x y))))
(check-sat)

;mapping or with map works just fine
(define-sort Set () (Array Int Bool))
(declare-const a Set)
(assert ( = a ((_ map or) a a) ))
(check-sat)

;but this fails with error
(assert ( = a ((_ map my-or) a a) ))

私は現在、この問題を次のようにハッキングしています。

(define-fun my-or-impl ((x Bool) (y Bool)) Bool (or x y))
(declare-fun my-or (Bool Bool) Bool)
(assert (forall ((x Bool) (y Bool)) (= (my-or x y) (my-or-impl x y))))
(check-sat)

しかし、普遍量指定子を使用しない方法でこれを解決できることを願っています。

4

2 に答える 2

1

残念ながら、define-funZ3 では単なるマクロ定義です。それらは Z3 SMT 2.0 パーサーに実装されています。それらは Z3 カーネルの一部ではありません。つまり、Z3 ソルバーはこれらの定義を「見る」ことさえできません。量指定子を使用するアプローチはdeclare-fun機能しますが、あなたが言ったように、量指定子はパフォーマンスの問題を引き起こすため避けるべきであり、Z3 が解決できない量指定子を使用すると問題が発生しやすくなります。最良のオプションは、 を使用すること(_ map or)です。

于 2013-10-12T19:18:11.410 に答える