3

Z3 は、解析するプログラムのセマンティクスがホーン節として与えられている場合、帰納的不変条件 (目的のプロパティを意味する) の解決をサポートするようになりました。

ただし、 z3.codeplex.commasterの Z3 ソース コードのブランチにあるバージョンは、この機能をサポートしていません。Z3 はこれらのホーン節の問題を、補間を使用する PDR アルゴリズムによって解決するため、代わりに、 をサポートするブランチ ( ) をコンパイルしました。interpd8b31773b809(set-logic HORN)

私の知る限り、ホーン節問題は不変量を表す未知の述語で指定され、X×Y の述語は X×Y から Bool への単なる関数です。ここまでは順調ですね。

for(int i=0; i<=10; i++)最初に試した例は、ループの帰納的不変条件を推論する問題です。

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((I Int)) (or (> I 10) (not (inv I)) (inv (+ I 1)))))
(check-sat)

これまでのところとても良いsatです。追加(assert (not (inv 15))したばかりで、 unsat. 私はそれから試しました

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (not (inv 15)))
(check-sat)

そして得unsatた。

私は何を間違っていますか？

4

1 に答える 1

2

「不安定」ブランチを使用します。「interp」ブランチは内部開発用であり、このブランチの状態は変動する可能性があります。あなたの2番目の問題について「座った」という答えが得られました。

最初の問題のもう少し興味深いバージョンは次のとおりです。

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((I Int)) (or (> I 10) (not (inv I)) (inv (+ I 1))))) 
(assert (forall ((I Int)) (=> (inv I) (<= I 11))))
(check-sat)
(get-model)

それは明らかな誘導不変量を生成します。最後のアサーションを

(assert (forall ((I Int)) (=> (inv I) (<= I 10))))

代わりに、(読みにくい) 証明が得られます。

于 2013-07-05T17:00:28.467 に答える