Choose from set, or multi set

Mar 23, 2013 at 8:41 AM
Hi --- Is there a bug in the compiling of choose? The code

method ChooseSeq() {
var x:| x in [1]; // This accepted.

method ChooseSet() {
var x:| x in {1}; // This rejected.

method ChooseSetVar() {
var s:= {1};
var x:| x in s; // This accepted.
assert x==1; // And this too.


input(6,8): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
Dafny program verifier finished with 5 verified, 1 error.

It seems you can choose from a constant sequence, but not a constant set. Is that a bug?
Mar 26, 2013 at 2:39 AM
Thanks. I checked in a fix.

(In these cases, there is a proof obligation to show the existence of some value for the LHS of the assignment. This boils down to finding a witness, which SMT solvers are not very good at. Therefore, Dafny (as Spec# had done) tries to come up with some potential witnesses, which it gives to the SMT solver to try. Previously, that logic in Dafny did not look inside set/seq displays like these. Things still often worked, but Dafny optimizes "x in {1}" to "x == 1", and for it, the SMT solver definitely needs help finding the witness. It now gets that help.)
Mar 26, 2013 at 8:30 AM
Great! Thank you.

How do fixes work their way through --- do they turn up in Rise4Fun first? Or in a download?
Mar 26, 2013 at 8:39 AM
In the following order:
(0) source code
(1) binary download
(2) rise4fun
I usually proceed from (0) to (1) when something more user visible takes place. We used to have an automatic nightly build, but have not (yet) put that back into place since the split.
Step (2) requires involving a few more people here, because I don't have direct access to the rise4fun server. Therefore, I tend to do it less often.

Mar 27, 2013 at 9:58 PM
Some additional information: As of today, the Dafny compiler can compile the assign-such-that statements above into executable code.