Set Comprehensions / Set Builder Notation

[pieter-bos]

The old encoding for set comprehensions was not sound:

set<int> xs = {x+y | int x, int y; x == 0 && y == 1}

//~~>

ensures (\forall int x, int y; (x+y) \in \result == (x == 0 && y == 1));
pure set<int> xs();

//~~>

assert (0 + 1) \in xs;
assert !((1 + 0) \in xs); // ↯

I'm currently only aware of an existential encoding being sound, but surely this is generally not tractable to use directly in proofs:

ensures (\forall int e; e \in xs == (\exists int x, int y; e == x + y && x == 0 && y == 1));
pure set<int> xs();

Pending a better encoding there currently is no implementation for set comprehensions.