2

Microsoft の Z3 SMT ソルバーを使用しており、カスタム ソートの定数を定義しようとしています。そのような定数はデフォルトでは等しくないようです。次のプログラムがあるとします。

(declare-sort S 0)

(declare-const x S)
(declare-const y S)

(assert (= x y))
(check-sat)

もちろん、同じ種類の 2 つの定数が等しいことは完全に可能であるため、これは "sat" を返します。定数が互いに異なる必要があるモデルを作成しているので、これは、フォームの公理を追加する必要があることを意味します

(assert (not (= x y)))

同じ種類の定数のすべてのペアに対して。ソートの各定数がデフォルトで一意になるように、このジェネリックを行う方法があるかどうか疑問に思っていました。

4

1 に答える 1

3

データ型を使用して、多くのプログラミング言語で見られる列挙型をエンコードできます。次の例では、並べ替えSに 3 つの要素があり、それらは互いに異なります。

(declare-datatypes () ((S a b c)))

完全な例を次に示します: http://rise4fun.com/Z3/ncPc

(declare-datatypes () ((S a b c)))

(echo "a and b are different")
(simplify (= a b))

; x must be equal to a, b or c
(declare-const x S)

; since x != a, then it must be b or c
(assert (not (= x a)))
(check-sat)
(get-model)
; in the next check-sat x must be c
(assert (not (= x b)))
(check-sat)
(get-model)

別の可能性は、 を使用することdistinctです。

(assert (distinct a b c d e))
于 2012-10-14T17:01:02.840 に答える