Here are some examples of how what I'm describing would work:
(define-set Complex)
(define-set Imaginary)
(define-set Real)
(define-set Integers)
(define-set Positive)
; define properties these sets must follow
(assert (subset Imaginary Complex))
(assert (subset Real Complex))
(assert (subset Integers Real))
(assert (subset Positive Real))
(assert (disjoint Imaginary Real))
Example 1
(define-var x)
(assert (in x Real))
(assert (in x Imaginary))
; unsat because Real and Imaginary are disjoint
Example 2
(define-var x)
(define-var y)
(assert (in x Real))
(assert (in y Imaginary))
(assert (= y x))
; unsat
Example 3
(define-var x)
(assert (in x Positive))
(assert (not (in Real))
; unsat
I found this stackoverflow question where someone asks how to implement this sort of theory within z3. It doesn't seem like z3 is very good at answering this sort of question.
One important detail is that I want to handle infinite sets.
Do any SMT solvers exist for this sort of theory? Are there papers about how to implement this?
Sets are not formalized by SMTLib, at least not officially.
However, CVC5 comes with an implementation that you can use out-of-the box: https://cvc5.github.io/docs/cvc5-1.0.0/theories/sets-and-relations.html#finite-sets
If CVC5 isn't available to you, then you can model sets by arrays from elements to booleans. z3 comes with certain operations that allow you to model sets this way. See https://microsoft.github.io/z3guide/docs/theories/Arrays/, the section titled "Mapping Functions on Arrays".
You can also model sets by functions, see: https://stackoverflow.com/a/70250257/936310
So, you got a bunch of options to choose from. Which works the best in any given situation is a matter of experimentation. My recommendation would be in the order above: Try CVC5 sets, then z3 array operations, then lambdas. As long as you don't do "cardinality" like queries, then the latter two should work relatively OK. If cardinality is a major concern, then CVC5 is pretty much the only choice you have.