セットを含む制約のモデルを見つけることができるように、Z3 でセットをモデル化しようとしています。
現在、配列を使用してセットを表しています。配列内の対応するエントリが true の場合、要素はセットに属します。次に、制約で使用するいくつかの公理があります。
SMT 2.0 の例を次に示します。
(define-sort Set (T) (Array T Bool))
(declare-fun |Set#Card| ((Set Int)) Int)
(assert (forall ((s (Set Int)))
(!
(<= 0 (|Set#Card| s))
:pattern ((|Set#Card| s)))))
(declare-fun |Set#Singleton| (Int) (Set Int))
(assert (forall ((r Int))
(!
(select (|Set#Singleton| r) r)
:pattern ((|Set#Singleton| r)))))
(assert (forall ((r Int) (o Int))
(iff (select (|Set#Singleton| r) o) (= r o))))
(assert (forall ((r Int)) (= (|Set#Card| (|Set#Singleton| r)) 1)))
(declare-fun s () (Set Int))
(assert (= 1 (|Set#Card| s)))
;(assert (= 1 (|Set#Card| (|Set#Singleton| 1))))
;(assert (not (= 1 (|Set#Card| (|Set#Singleton| 1)))))
(check-sat)
(get-info :reason-unknown)
(get-model)
私の問題は、unknown
ほとんどの場合、モデルが得られないことです。私の公理化は弱すぎると思います。s
上記の例では、 1 つの要素を含むセットのモデルを取得したいと考えています。
セットを含む制約のモデルを取得するために Z3 を使用する方法を知っている人はいますか?
どの回答も参考になります。つまり、Z3 でできることとできないことを誤解しているのかもしれません。この問題に対処する方法についてのアイデアも大歓迎です (他のツールの提案など)。