4

これが私がz3で実行したSMT-LIB2.0ベンチマークです：

(set-logic AUFLIA)
(declare-sort PZ 0)
(declare-fun MS (Int PZ) Bool)

(assert (forall ((x Int)) (exists ((X PZ)) 
            (and (MS x X) 
                 (forall ((y Int)) (=> (MS y X) (= y x)))))))
(check-sat)

sat結果は、少なくともZのべき集合（整数）であり、Zのサブセット（一種の要素）への整数のメンバーシップをテストする述語であるモデルでPZあると予想しました。MSPZ

しかし、z3は答えunsatました。

この結果を理解するのを手伝ってもらえますか？具体的には、z3はソートをどのように解釈しますIntか？それは本当に無限と見なされますか？動的に宣言されたソート（ここではソートPZ）はどうですか？

4

1 に答える 1

3

Z3では、Intは無限大です。あなたは正しいです、結果はでなければなりませんsat。unsat結果は、Z3モジュールの1つのバグが原因です。私はすでにバグを修正しました。実装の1つの一時キャッシュがリセットされていませんでした。この修正は、次のリリースで利用できるようになります。それまでの間、スクリプトの先頭で次のコマンドを使用して、バグのあるモジュールを無効にすることができます。

(set-option :mbqi false)

ところで、このバグは、とがユニバーサル変数(= x y)である形式のリテラルを含む例にのみ影響します。xy

ところで、あなたの例は満足のいくものですが、Z3はそのモデルを構築できません（バグ修正後でも）。実際、バグ修正後、Z3は答えを生成しますunknown。モデルファインダー（Z3で使用）は、解釈されていない種類（PZなど）の解釈が有限であるモデルのみを検索できます。この制限は将来変更される可能性があります。

于 2011-11-17T17:21:54.897 に答える