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