3

booleanSMT2と呼ばれる独自のブール値と、boolean_andそれらに対するAND関数を定義しました。私の推測では、ANDは可換です。

(declare-sort boolean)
(declare-const sk_x boolean)
(declare-const sk_y boolean)
(declare-const boolean_false boolean)
(declare-const boolean_true boolean)
(declare-fun boolean_and (boolean boolean) boolean)

;; axiomatize booleans: false /= true and every bool is true or false
(assert (forall ((x boolean)) (or (= x boolean_false)
                                  (= x boolean_true))))

(assert (not (= boolean_false boolean_true)))

;; definition of AND
(assert (forall ((a boolean)) (= (boolean_and boolean_false a) boolean_false)))
(assert (forall ((a boolean)) (= (boolean_and boolean_true a) a)))

;; try to prove that AND is commutative
(assert (not (= (boolean_and sk_x sk_y)
                (boolean_and sk_y sk_x))))

(check-sat)

sk_xただし、z3は、スコーレム化された変数とでケース分割アサーションを使用できるはずだと思っていたにもかかわらず、しばらくするとこの問題について不明であると報告しますsk_y。

不思議なことに、ブール値の公理化を削除して、に置き換えると declare-datatypes、z3は次のように報告しunsatます。

(declare-datatypes () ((boolean (boolean_true) (boolean_false))))

(declare-const sk_x boolean)
(declare-const sk_y boolean)
(declare-fun boolean_and (boolean boolean) boolean)

(assert (forall ((a boolean)) (= (boolean_and boolean_false a) boolean_false)))
(assert (forall ((a boolean)) (= (boolean_and boolean_true a) a)))

(assert (not (= (boolean_and sk_x sk_y)
                (boolean_and sk_y sk_x))))

(check-sat)

私は何が間違っているのですか？公理化を使用してz3をケース分割するにはどうすればよいですか？

4

1 に答える 1

3

あなたは何も悪いことをしていません。公式リリース（v4.3.1）は、次のようなカーディナリティ制約を含む問題で失敗する可能性があります。

(assert (forall ((x boolean)) (or (= x boolean_false)
                                  (= x boolean_true))))

この制約は、解釈されないソートbooleanには最大で2つの要素があることを示しています。この問題を修正しました。修正はunstableブランチですでに利用可能です。 ブランチをコンパイルする方法についての説明は次のとおりです。unstable明日、ナイトリービルドにもこの修正が含まれます。

于 2013-03-18T15:32:41.753 に答える