max value in set z3

Question

I'm a new guy to work with the Z3.

Would like to know how I can calculate the maximum value of a set and two different sets.

For example: [1, 6, 5] - The greater is 6 [1, 6, 5] e [10, 7, 2] - The greater is 6

I use the following code to set:

    (declare-sort Set 0)

(declare-fun contains (Set Int) bool)

( declare-const set Set )
( declare-const distinct_set Set )

( declare-const A Int )
( declare-const B Int )
( declare-const C Int )

( assert ( =  A 0 ) )
( assert ( =  B 1 ) )
( assert ( =  C 2 ) )

( assert ( distinct A C) )
( assert ( distinct set distinct_set ) )

(assert
 (forall ((x Int))
         (= (contains set x) (or (= x A) (= x C)))))

And now would like to know how can I calculate the largest value in the set (set) and the largest value in sets (set and distinct_set).

If it was for all integers was only because it was easy to do:

(define-fun max ((x Int) (y Int)) Int
  (ite (< x y) y x))

But I can not leave with sets by their integers, ie, get the values ​​that have set.

Can you help me?

Thanks

Answer 1

Is the following encoding reasonable for your purposes? It is also available online here.

; We Enconde each set S of integers as a function S : Int -> Bool
(declare-fun S1 (Int) Bool)
; To assert that A and C are elements of S1, we just assert (S1 A) and (S1 C) 
(declare-const A Int)
(declare-const C Int)
(assert (S1 A))
(assert (S1 C))
; To say that B is not an element of S1, we just assert (not (S1 B))
(declare-const B Int)
(assert (not (S1 B)))

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

; Now, let us define a set S2 and S3
(declare-fun S2 (Int) Bool)
(declare-fun S3 (Int) Bool)
; To assert that S3 is equal to the union of S1 and S2, we just assert
(assert (forall ((x Int)) (= (S3 x) (or (S1 x) (S2 x)))))

; To assert that S3 is not equal to S1 we assert
(assert (exists ((x Int)) (not (= (S3 x) (S1 x)))))

(check-sat)

; Now let max_S3 be the maximal value of S3
(declare-const max_S3 Int)
(assert (S3 max_S3))
(assert (forall ((x Int)) (=> (S3 x) (not (>= x (+ max_S3 1))))))

; the set of constraints is still satisfiable
(check-sat)

; Now, let us assert that max_S3 < max_S1.
; It should be unsat, since S3 is a super set of S1
(assert (< max_S3 max_S1))
(check-sat)