0

Z3初心者です。しかし、Z3に入力された次のプログラムでのタイムアウトの理由を理解したい：

(declare-fun ADDR (Int) Int)
(declare-fun STAR (Int Int) Int)
(declare-fun VAR (Int Int) Int)
(declare-const error Int)

(assert (forall ((x Int)) (= x (STAR (ADDR x) 0))) );causes a timeout?
(assert (forall ((x Int)) (>= (ADDR x) 4000)) )
(assert (not (= (VAR  error 0) 1)))
(check-sat)
(get-model)

もう 1 つの質問は、バージョン 3.2 の forall に何か新しいものはありますか? (x Int) の周りに追加の括弧を配置する必要がありました。そうしないと、エラーがスローされました。

ありがとう。

4

1 に答える 1

1

この式は充足可能であり、Z3 はそのモデルを構築できません。数量化された数式のモデル ファインダーを無効にすると、タイムアウトを回避できます。

(set-option :auto-config false)
(set-option :mbqi false)

そうすると、Z3 は不明で「候補モデル」を返します。この問題は、Z3 ガイドで説明されています。

Z3 3.x はSMT 2.0 標準と完全に互換性があるため、余分な括弧が必要です。

于 2012-02-16T06:47:00.267 に答える