Set in z3

set.smt2

; uninterpreted sort
(declare-sort Elt)
(define-sort Set (Elt) (Array Elt Bool))

; bijection Int <=> Elt
(declare-fun mkint (Int) Elt)
(declare-fun unmkint (Elt) Int)
(assert (forall ((x Int)) (= x (unmkint (mkint x)))))
(assert (forall ((e Elt)) (= e (mkint (unmkint e)))))

; bijection Set Elt <=> Elt (for set of sets)
(declare-fun mkset ((Set Elt)) Elt)
(declare-fun unmkset (Elt) (Set Elt))
(assert (forall ((x (Set Elt))) (= x (unmkset (mkset x)))))
(assert (forall ((e Elt)) (= e (mkset (unmkset e)))))

(define-fun smt_set_emp () (Set Elt) ((as const (Set Elt)) false))
(define-fun smt_set_mem ((x Elt) (s (Set Elt))) Bool (select s x))
(define-fun smt_set_add ((s (Set Elt)) (x Elt)) (Set Elt)  (store s x true))
(define-fun smt_set_cap ((s1 (Set Elt)) (s2 (Set Elt))) (Set Elt) ((_ map and) s1 s2))
(define-fun smt_set_cup ((s1 (Set Elt)) (s2 (Set Elt))) (Set Elt) ((_ map or) s1 s2))
(define-fun smt_set_com ((s (Set Elt))) (Set Elt) ((_ map not) s))
(define-fun smt_set_dif ((s1 (Set Elt)) (s2 (Set Elt))) (Set Elt) (smt_set_cap s1 (smt_set_com s2)))
(define-fun smt_set_sub ((s1 (Set Elt)) (s2 (Set Elt))) Bool (= smt_set_emp (smt_set_dif s1 s2)))

; powerset
(declare-fun smt_set_powerset ((Set Elt)) (Set (Set Elt)))
(assert (forall ((s (Set Elt)) (x (Set Elt))) (= (smt_set_sub x s) (smt_set_mem (mkset x) (smt_set_powerset s)))))