Finite sets

[shazqadeer]

Is there any plan to support finite sets with cardinality reasoning in Z3? This feature would be very useful for verifying concurrent and distributed systems.

[LeventErkok]

z3 used to support sets via arrays mapping elements to booleans. Of course, you can still do the same, but in the past it also allowed for cardinality checking. At some point they dropped support, unfortunately. Related tickets:

• https://github.com/Z3Prover/z3/issues/2287
• https://github.com/Z3Prover/z3/issues/4700

It'd indeed be nice to have better support for this theory indeed, though I can also see that it's a non-trivial amount of work.

As an alternative, CVC5 has an implementation:https://cvc5.github.io/docs/cvc5-1.0.0/theories/sets-and-relations.html#finite-sets

[shazqadeer]

I am aware that Set T can be modeled as an Array T bool. In fact, I use this modeling style all the time. However, applying the cardinality operator on values of sort Array T bool is problematic for the usual reasons. Hence, I was surprised to learn that Z3 had made attempts in the past to provide such a feature. Dropping support for cardinality over boolean arrays seems like a totally reasonable decision to me.

I was actually asking about a slightly different feature which seems much more reasonable to me. I want a sort of finite sets with constructors such as empty-set, add-element, remove-element, union, intersection, difference, etc. And I want the cardinality operator over the sort of finite sets.

It is good to know that CVC5 already supports finite sets. All the more reason to have them in Z3 also :-). My happiness would be complete if I also got finite multisets with cardinality operator at the same time.