1

Int、Bool、S1、S2 など、いくつかの組み込みおよびユーザー定義の Z3 ソートの使用を想定すると、ソート A からBを並べ替えて戻る？例えば

(declare-const a S1)
(declare-const b S2)
(declare-const c Int)

(WRAP[S1] b) ; Expression is of sort S1
(WRAP[S1] c) ; Expression is of sort S1
(WRAP[Int] (WRAP[S1] c)) ; Expression is of sort Int

私は現在、各ケースを手動でカバーしています。

(declare-fun $boolToInt (Bool) Int)
(declare-fun $intToBool (Int) Bool)

(assert (forall ((x Int))
  (= x ($boolToInt($intToBool x)))))

(assert (forall ((x Bool))
  (= x ($intToBool($boolToInt x)))))

このようなラッパーは、特定の種類のセットから自動的に作成できますが、可能性のある一般的なソリューションをお勧めします。

4

1 に答える 1

3

データ型を使用して「共用体型」をエンコードできます。次に例を示します。

(declare-sort S1)
(declare-sort S2)

(declare-datatypes () ((S1-S2-Int (WRAP-S1 (S1-Value S1))
                                  (WRAP-S2 (S2-Value S2))
                                  (WRAP-Int (Int-Value Int)))))

(declare-const a S1)
(declare-const b S2)
(declare-const c Int)

(simplify (WRAP-S1 a))
(simplify (= (WRAP-S1 a) (WRAP-Int 10)))
(simplify (S1-Value (WRAP-S1 a)))
(simplify (is-WRAP-S2 (WRAP-S1 a)))
(simplify (is-WRAP-S1 (WRAP-S1 a)))
(simplify (is-WRAP-Int (WRAP-Int c)))
(simplify (S1-Value (WRAP-S2 b)))

データ型の詳細については、Z3 ガイドを参照してください。データ型には、 、およびのS1-S2-Int3 つのコンストラクタがあります。Z3 は、認識述語、および を自動的に生成します。アクセサー、およびは、値を「分解」するために使用されます。たとえば、すべての. の値が指定されていません。この場合、Z3 は未解釈の関数として扱われます。WRAP-S1WRAP-S2WRAP-Intis-WRAP-S1is-WRAP-S2is-WRAP-IntS1-ValueS2-ValueInt-ValueS1-S2-Inta(S1-Value (WRAP-S1 a)) = a(S1-Value (WRAP-S2 b))S1-Value

ところで、公理

(assert (forall ((x Int))
  (= x ($boolToInt($intToBool x)))))

false と同等です。基本的に、整数をブール値に挿入しようとしています。

于 2012-03-12T14:55:03.760 に答える