0

セットを含む制約のモデルを見つけることができるように、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 でできることとできないことを誤解しているのかもしれません。この問題に対処する方法についてのアイデアも大歓迎です (他のツールの提案など)。

4

1 に答える 1