содержит для двух наборов в Z3

Операция (contains S1 S2), которую вы описываете в своем сообщении, является отношением подмножества. Если мы закодируем наборы целых чисел как функции от Int до Boolean (например, в: максимальное значение в наборе 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.

ИЗМЕНИТЬ

Мы можем использовать выражение (exists ((x Int)) (and (S1 x) (S2 x))), чтобы проверить, имеют ли наборы S1 и S2 общий элемент или нет.

ЗАВЕРШИТЬ РЕДАКТИРОВАНИЕ

Минимальный элемент набора может быть закодирован, как мы это сделали в максимальном значении в наборе 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)))