排除和包含在Z3中

Question

我試圖用Z3模擬包含和排除元素的模型。特別包含具有不同值的元素，排除尚不在目標集中的元素。所以基本上我想有一個集合U並讓Z3找到一個只包含具有不同值的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)) 

我unders假設對A和B都賦值爲false是一個邏輯上正確的賦值，但我不知道如何以某種方式陳述事情以便排除這些事例。

也許我沒有正確地考慮這個問題。

任何意見將不勝感激。 :)

Answer 1

您如何看待下面的斷言？

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

它說，對於每一個元素的setx（即，U），有一個y S.T.

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