1

Z3初心者からの質問です。オプションで Z3 の動作を変更できますか? それらが終了に影響を与えるか、または変化するsatか、変化unsatするunknownが、その逆ではないことを期待するかもしれません。satunsat

この例:

(set-option :smt.macro-finder true)

(declare-datatypes () ((Option (none) (some (Data Int)))))

(define-sort Set () (Array Option Option))
(declare-fun filter1 (Option) Option)
(declare-fun filter2 (Option) Option)

(declare-var s1 Set)
(declare-var s2 Set)
(declare-var x1 Option)
(declare-var x2 Option)
(declare-var x3 Option)
(declare-var x4 Option)

(assert (not (= x1 none)))
(assert (not (= x2 none)))
(assert (not (= x3 none)))
(assert (not (= x4 none)))
(assert (= (select s1 x1) x2))
(assert (= (select s2 x3) x4))

(assert (forall ((x Option)) (= (filter1 x) (ite (or (= none x) (= (Data x) 1)) x none))))
(assert (forall ((x Option)) (= (filter2 x) (ite (or (= none x) (= (Data x) 2)) x none))))

(assert (= ((_ map filter1) s1) s2))
(assert (= ((_ map filter2) s1) s2))
(check-sat)
(get-model)

sat最初の行とunsatそれなしで戻ります。

これはバグですか、それとも根本的な何かが欠けていますか?

ありがとう、N

4

1 に答える 1

0

これはバグです。filter12 つの量指定子は、基本的にとの「定義」を提供してfilter2います。
このオプションsmt.macro-finderは、これらの定義を拡張して関数シンボルを削除するために使用されます。本質的には「マクロ展開」を行っています。ただし、マクロ エキスパンダーにはバグがあります。マップ構造内のfilter1andの出現は展開されません: and .filter2(_ map filter1)(_ map filter2)

このバグは修正される予定です。mapそれまでの間、コンストラクトとsmt.macro-finderオプションを同時に使用しないでください。

于 2013-10-24T15:29:34.560 に答える