max value in set z3

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

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)