CODEWITHSUNDEEP
z3
Robert
Robert

Reputation: 211

contains for two sets in Z3

If I want to check if a set has elements of another set is also possible?

For example (contains Set1 Set2):

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

The sets are finite. And the maximum value of the sets is five and the minimum is 0, the sets may not have values greater than 5 neither smaller than 0.

For example:

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

If it were only for a set and check whether a value exist in the set was easy. It was in the following way:

( 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 )

But for two sets I do not see how it's done.

Thank you for your attention.

Upvotes: 0

Views: 718

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

The operation (contains S1 S2) that you describe in your message is the subset relation. If we encode sets of integers as functions from Int to Boolean (like in: max value in set z3), then S1 and S2 are declared as:

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

Then, we can say that S1 is a subset of S2 by asserting

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

We just saying that any element in S1 is also an element of S2.

EDIT

We can use the expression (exists ((x Int)) (and (S1 x) (S2 x))) to check whether the sets S1 and S2 have an element in common or not

END EDIT

The minimal element of a set can be encoded as we did in max value in set z3. For example, suppose the minimal element of S1 is 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))))))

If the minimal values of the sets you are encoding are known at "encoding time" (and are small). We can use yet another encoding based on Bit-vectors. In this encoding, a set is a Bit-vector. If the sets only contain values between 0 and 5, then we can use a Bit-vector of size 6. The idea is: if bit i is true iff i is an element of the set.

Here is an example with the main operation:

(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)))

Upvotes: 3

Related Questions