ある状況で論理公理が適用される可能性があることを 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 は、私が言及した公理をインスタンス化する場合、式が不飽和であることを証明することに成功する可能性があります。