排除和包含在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)