包含Z3中的兩組

Question

如果我想檢查一組中是否有另一組元素也是可能的？

例如（包含SET1 SET2）：

contains [1,2] [3,5] -> is false 
contains [1] [2,3, 1] -> is true 

的集合是有限的。和集合的最大值是5，最小值爲0，則組可以不具有值大於5既不小於0

例如：

[1,5,3] -> valid set 
[1,8,2] -> invalid set 

假如它是用於一組並檢查該集合中是否存在值很容易。它是以下列方式：

(declare-sort Set 0) 

(declare-fun contains (Set Int) bool) 

(declare-const set Set) 

(declare-const A Int) 

(assert (contains set A)) 
(assert (not (contains set 0))) 
(check-sat) 

但是對於兩組我看不到它是如何完成的。

感謝您的關注。

Answer 1

您在消息中描述的操作(contains S1 S2)是子集關係。如果我們編碼整數集從詮釋功能布爾（如在：max value in set z3），然後S1和S2被聲明爲：

(declare-fun S1 (Int) Bool) 
(declare-fun S2 (Int) Bool) 

然後，我們可以說，S1是S2一個子組斷言

(assert (forall ((x Int)) (=> (S1 x) (S2 x)))) 

我們只是說S1中的任何元素也是S2的元素。

EDIT

我們可以使用表達(exists ((x Int)) (and (S1 x) (S2 x)))檢查套S1和S2是否具有共同或元素不

END EDIT

一組的最小元件可以像我們在max value in set z3中那樣進行編碼。例如，假設最小元素S1是min_S1。

; Now, let min_S1 be the min value in S1 
(declare-const min_S1 Int) 
; Then, we now that min_S1 is an element of S1, that is 
(assert (S1 min_S1)) 
; All elements in S1 are bigger than or equal to min_S1 
(assert (forall ((x Int)) (=> (S1 x) (not (<= x (- min_S1 1)))))) 

如果您正在編碼的集合的最小值在「編碼時間」（並且很小）時是已知的。我們可以使用另一種基於比特向量的編碼。 在這種編碼中，一個集合是一個位向量。如果這些集合只包含0到5之間的值，那麼我們可以使用大小爲6的位向量。這個想法是：如果i位爲真，如果i是該集合的元素。

這裏是與主操作的示例：

(declare-const S1 (_ BitVec 6)) 
(declare-const S2 (_ BitVec 6)) 
(declare-const S3 (_ BitVec 6)) 

; set equality is just bit-vector equality 
(assert (= S1 S2)) 

; set intersection, union, and complement are encoded using bit-wise operations 

; S3 is S1 union S2 
(assert (= S3 (bvor S1 S2))) 

; S3 is S1 intersection of S2 
(assert (= S3 (bvand S1 S2))) 

; S3 is the complement of S1 
(assert (= S3 (bvnot S1))) 

; S1 is a subset of S2 if S1 = (S1 intersection S2), that is 
(assert (= S1 (bvand S1 S2))) 

; S1 is the empty set if it is the 0 bit-vector 
(assert (= S1 #b000000)) 

; To build a set that contains only i we can use the left shift 
; Here, we assume that i is also a bit-vector 
(declare-const i (_ BitVec 6)) 
; S1 is the set that contains only i 
; We are also assuming that i is a value in [0, 5] 
(assert (= S1 (bvshl #b000001 i)))