0

ある状況で論理公理が適用される可能性があることを Z3 に伝える方法はありますか? たとえば、 P(x) ==> \exists x P(x) は常に有効です。しかし、P が十分に複雑な場合、Z3 は混乱して不明と言うことができます。

(declare-const size Int)
(declare-const h (Array Int Int))
(assert  (forall ((j Int) (k Int)) (=> (and (<= 0 k) (< k size) (<= 0 j) (< j size) (not (= k j))) (not (= (select h j) (select h k))))))
(assert (not (exists ((g (Array Int Int))) (forall ((j Int) (k Int)) (=> (and (<= 0 k) (< k size) (<= 0 j) (< j size) (not (= k j))) (not (= (select g j) (select g k))))))))
(check-sat)

最初のアサーションは、h が 0..size-1 からの個別の整数を個別の整数にマップする配列であることを示しています。そして 2 番目の主張は、そのような配列は存在できないと述べています。P(x) ==> \exists x P(x) などの単純で有効な公理を SMT ファイルで提供して、Z3 を支援することはできますか? この例で何が起こっているのかを誤解している可能性があります。しかし、私の限られた理解によると、Z3 は、私が言及した公理をインスタンス化する場合、式が不飽和であることを証明することに成功する可能性があります。

4

1 に答える 1

1

これは、引き金となる問題のようです。つまり、Z3 は、存在量化された公理を具体化していません (おそらく、普遍的に量化された公理もそうではありません)。次の簡単な例を見てください。

(set-option :AUTO_CONFIG false)
(set-option :SMT.MBQI false)

(declare-fun f (Int) Bool)

(assert (forall ((x Int))
  (=> (<= 0 x) (f x))
))

(assert (not (exists ((x Int))
  (=> (<= 0 x) (f x))
)))

; (assert (f -10))

(check-sat)

Z3 (バージョン 4.3.2、64 ビット、ビルド ハッシュコード 96f4606a7f2d) は を報告しunknownますが、最後のアサーションのコメントを外すと、それは を報告しますunsat。したがって、Z3 が両方の公理について推論するパターンは であると仮定します。:pattern ((f x))つまりf x、公理がインスタンス化される前に構文的に発生する必要があります。

数量詞パターンの詳細については、z3 ガイドを参照してください。

于 2013-04-18T11:27:04.403 に答える