1

Z3 を使用して、セット内の要素の包含と除外をモデル化しようとしています。具体的には、個別の値を持つ要素を含め、ターゲット セットにまだ含まれていない要素を除外します。したがって、基本的には、セット U が必要であり、Z3 に、U の異なる値を持つ要素のみを含むセット U_d を見つけてもらいたいと考えています。

私の現在のアプローチでは量指定子を使用していますが、U に表示される場合は常に U_d に要素を含めたいと述べる方法を理解するのに苦労しています.

( set-option :produce-models true)

;;; Two simple sorts.
;;; Sets and Zs.

( declare-sort Z   0 )
( declare-sort Set 0 )

;;; A set can contain a Z or not.
;;; Zs can have a value.

( declare-fun contains (Set Z) bool )
( declare-fun value (Z) Int )

;;; Two sets and two Z instances for use in the example.

( declare-const set Set )
( declare-const distinct_set Set )

( declare-const A Z )
( declare-const B Z )

;;; The elements and sets are distinct.     

( assert ( distinct A B ) )
( assert ( distinct set distinct_set ) )

;;; Set 'set' contains A but not B

( assert ( = ( contains set A ) true ) )
( assert ( = ( contains set B ) false ) )

;;; Assert that all elements contained by distinct_set have different values unless they're the same variable.
( assert
  ( forall ( (x Z) (y Z) )
    ( =>
        ( and 
            ( contains distinct_set x )
            ( contains distinct_set y )
            ( = ( value x ) ( value y ) ) )
        ( = x y ) )))

;;; distinct_set can contain only elements that appear in set.
;;; In other words, distinct_set is a proper set.
( assert
( forall ( ( x Z ) )
    ( =>
        ( contains distinct_set x )
        ( contains set x ))))

;;; Give elements some values.
( assert ( = (value A) 0 ) )
( assert ( = (value B) 1 ) )

( push )
( check-sat )
( get-value (( contains distinct_set A )))
( get-value (( contains distinct_set B )))
( pop )

それが生成する割り当ては次のとおりです。

sat
((( contains distinct_set A ) false))
((( contains distinct_set B ) false))

希望する課題は次のとおりです。

sat
((( contains distinct_set A ) true))
((( contains distinct_set B ) false))

A と B の両方に false を割り当てることが論理的に正しいことは理解していますが、そのような場合を除外するような方法で物事を述べる方法がわかりません。

おそらく私は問題について正しく考えていません。

アドバイスをいただければ幸いです。:)

4

1 に答える 1

1

次の主張についてどう思いますか。

(assert
(forall ((x Z))
        (=> (contains set x)
            (exists ((y Z))
                    (and (= (value x) (value y))
                         (contains set y)
                         (contains distinct_set y))))))

（つまり、U）xのすべての要素に対して、 stがあると言いますsety

  • の値は の値yと等しいx
  • yの要素でもありますset
  • ydistinct_set(つまり、U_d)の要素です。

このアサーションはset、 に同じ値を持つ 2 つの要素がある場合、そのうちの 1 つだけが の要素であることを確認しdistinct_setます。それはあなたが望むものですか？

このアサーションを追加するだけでも、Z3 はモデルを生成することに注意してください。

((( contains distinct_set A ) false))
((( contains distinct_set B ) false))

を使用して Z3 によって作成されたモデルを検査すると、 とは異なる別の要素(get-model)が含まれていることがわかります。したがって、要素のみを強制的に含めるには、アサートする必要がありますsetAsetA

(assert
 (forall ((x Z))
         (= (contains set x) (= x A))))

このアサーションを追加すると、次の 2 つのアサーションが冗長になります。

( assert ( = ( contains set A ) true ) )
( assert ( = ( contains set B ) false ) )

ここで、とのset2 つの値が含まれ、両方とも同じ値を持つ場合を考えてみましょう。次のスクリプトは、次のような質問もします。AC

  • distinct_set含まないA

  • distinct_setも含まAないC

  • distinct_setを含みA、C

脚本：

( set-option :produce-models true)

;;; Two simple sorts.
;;; Sets and Zs.

( declare-sort Z   0 )
( declare-sort Set 0 )

;;; A set can contain a Z or not.
;;; Zs can have a value.

( declare-fun contains (Set Z) bool )
( declare-fun value (Z) Int )

;;; Two sets and two Z instances for use in the example.

( declare-const set Set )
( declare-const distinct_set Set )

( declare-const A Z )
( declare-const B Z )
( declare-const C Z )

;;; The elements and sets are distinct.     

( assert ( distinct A B C) )
( assert ( distinct set distinct_set ) )

;;; set contains only A and C
 (assert
 (forall ((x Z))
         (= (contains set x) (or (= x A) (= x C)))))

;;; Assert that all elements contained by distinct_set have different values unless they're the same variable.
( assert
  ( forall ( (x Z) (y Z) )
    ( =>
        ( and 
            ( contains distinct_set x )
            ( contains distinct_set y )
            ( = ( value x ) ( value y ) ) )
        ( = x y ) )))

;;; distinct_set can contain only elements that appear in set.
;;; In other words, distinct_set is a proper set.
( assert
( forall ( ( x Z ) )
   ( =>
       ( contains distinct_set x )
       ( contains set x ))))

;;; Give elements some values.
( assert ( = (value A) 0 ) )
( assert ( = (value B) 1 ) )
( assert ( = (value C) 0 ) )

(assert
(forall ((x Z))
        (=> (contains set x)
            (exists ((y Z))
                    (and (= (value x) (value y))
                         (contains set y)
                         (contains distinct_set y))))))

( push )
( check-sat )
( get-model )
( get-value (( contains distinct_set A )))
( get-value (( contains distinct_set B )))
( get-value (( contains distinct_set C )))
( echo "Is there another model where A is not in distinct_set")
( assert (not ( contains distinct_set A )))
(check-sat)
( get-value (( contains distinct_set A )))
( get-value (( contains distinct_set B )))
( get-value (( contains distinct_set C )))
( echo "Is there another model where A and C are not in distinct_set")
( assert (not ( contains distinct_set C )))
(check-sat)
( pop ) ;; retracting the last two assertions
( push )
( echo "Is there a model where A and C are in distinct_set")
( assert ( contains distinct_set A ))
( assert ( contains distinct_set C ))
( check-sat )
于 2012-03-15T05:48:39.100 に答える