1

我正在尝试使用 Z3 对集合中元素的包含和排除进行建模。特别是包含具有不同值的元素，并排除尚未在目标集中的元素。所以基本上我想要一个集合 U 并让 Z3 找到一个集合 U_d ，它只包含具有不同值的 U 元素。

我当前的方法使用量词，但我无法理解如何声明如果元素出现在 U_d 中，我希望始终将它们包含在 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))

我知道将 false 分配给 A 和 B 在逻辑上是正确的分配，但我不知道如何以排除这些情况的方式陈述事情。

也许我没有正确考虑这个问题。

任何建议将不胜感激。:)

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))))))

它说对于 (ie, U) 的每个元素x，set都有一个yst

  • 的值y等于的值x
  • y也是一个元素set
  • y是distinct_set（即，U_d）的一个元素

这个断言确保如果有两个元素set具有相同的值，那么其中一个且只有一个是 的元素distinct_set。那是你要的吗？

请注意，如果我们只是添加这个断言，Z3 仍然会生成一个模型，其中

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

如果我们使用 来检查 Z3 生成的模型(get-model)，我们会注意到它set包含另一个与 不同的元素A。所以，要强制set只包含元素A，我们必须断言

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

添加此断言后，以下两个断言变得多余：

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

现在，让我们考虑set包含两个值的情况：A和C，并且它们都具有相同的值。以下脚本还提出以下问题：是否有一个模型

  • 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 回答