how can I make a datatype that contains a set of another objects. Basically, I am doing the following code:
(define-sort Set(T) (Array Int T))
(declare-datatypes () ((A f1 (cons (value Int) (b (Set B))))
(B f2 (cons (id Int) (a (Set A))))
))
But Z3 tells me unknown sort for A and B. If I remove "Set" it works just as the guide states. I was trying to use List instead but it does not work. Anyone knows how to make it work?
定期的に出てくる質問に取り組んでいます:データ型と配列を (セット、マルチセット、または範囲内のデータ型として) 混合するにはどうすればよいですか?
前述のように、Z3 は単一の宣言でのデータ型と配列の混在をサポートしていません。解決策は、混合データ型 + 配列理論用のカスタム ソルバーを開発することです。Z3 には、カスタム ソルバーを開発するためのプログラム API が含まれています。
量指定子とトリガーを使用したエンコード理論の機能と制限を説明するために、この例を作成することは依然として有用です。A を使用して例を単純化しましょう。回避策として、補助ソートを定義できます。ただし、回避策は理想的ではありません。これは、いくつかの公理「ハッキング」を示しています。これは、検索中に量指定子がどのようにインスタンス化されるかという操作上のセマンティクスに依存しています。
(set-option :model true) ; We are going to display models.
(set-option :auto-config false)
(set-option :mbqi false) ; Model-based quantifier instantiation is too powerful here
(declare-sort SetA) ; Declare a custom fresh sort SetA
(declare-datatypes () ((A f1 (cons (value Int) (a SetA)))))
(define-sort Set (T) (Array T Bool))
次に、(Set A)、SetA の間の全単射を定義します。
(declare-fun injSA ((Set A)) SetA)
(declare-fun projSA (SetA) (Set A))
(assert (forall ((x SetA)) (= (injSA (projSA x)) x)))
(assert (forall ((x (Set A))) (= (projSA (injSA x)) x)))
これは、ほとんどのデータ型宣言の状態です。正当性を強制するために、序数を A のメンバーに関連付けて、正当な順序で SetA のメンバーを小さくすることができます。
(declare-const v Int)
(declare-const s1 SetA)
(declare-const a1 A)
(declare-const sa1 (Set A))
(declare-const s2 SetA)
(declare-const a2 A)
(declare-const sa2 (Set A))
これまでの公理では、a1 はそれ自体のメンバーになることができます。
(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(get-model)
(pop)
ここで、序数を A のメンバーに関連付けます。
(declare-fun ord (A) Int)
(assert (forall ((x SetA) (v Int) (a A))
(=> (select (projSA x) a)
(> (ord (cons v x)) (ord a)))))
(assert (forall ((x A)) (> (ord x) 0)))
デフォルトでは、Z3 の量指定子のインスタンス化はパターンベースです。上記の最初の定量化されたアサートは、関連するすべてのインスタンスでインスタンス化されるわけではありません。代わりに次のように断言できます。
(assert (forall ((x1 SetA) (x2 (Set A)) (v Int) (a A))
(! (=> (and (= (projSA x1) x2) (select x2 a))
(> (ord (cons v x1)) (ord a)))
:pattern ((select x2 a) (cons v x1)))))
このような 2 つのパターン (マルチパターンと呼ばれる) を使用する公理は、非常にコストがかかります。(select x2 a) と (cons v x1) のすべてのペアのインスタンス化を生成します。
以前からのメンバーシップの制約は、満足できなくなりました。
(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(pop)
しかし、モデルはまだ十分に形成されているとは限りません。セットのデフォルト値は「true」です。これは、モデルが、メンバーシップ サイクルがない場合にメンバーシップ サイクルがあることを意味することを意味します。
(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)
次のアプローチを使用して、データ型で使用されるセットが有限であることを強制することにより、より忠実なモデルを近似できます。たとえば、セット x2 のメンバーシップ チェックがある場合は常に、セットの「デフォルト」値が「false」であることを強制します。
(assert (forall ((x2 (Set A)) (a A))
(! (not (default x2))
:pattern ((select x2 a)))))
あるいは、セットがデータ型コンストラクターで発生するときはいつでも、それは有限です
(assert (forall ((v Int) (x1 SetA))
(! (not (default (projSA x1)))
:pattern ((cons v x1)))))
(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)
追加の公理を含めると、Z3 は「不明」という答えを生成し、さらに生成されたモデルはドメイン SetA が有限であることを示します (シングルトン)。したがって、デフォルトにパッチを当てることはできますが、このモデルはまだ公理を満たしていません。これは、インスタンス化を法とする公理のみを満たします。
これは Z3 ではサポートされていません。データ型宣言で配列を使用できますが、宣言するデータ型への「参照」を含めることはできません。たとえば、 を使用しても問題ありません(Set Int)。