feat: Support for arbitrary versions of z3 #2820

MikaelMayer · 2022-09-30T14:56:36Z

Added documentation on how to make Dafny work for other versions of Z3 Added automatic overriding of prover options if Z3 version 4.8.7 or newer is detected in the language server

I tested it manually with Z3 version 4.8.7. I verified the version of Z3 was correctly sent to VSCode using the telemetry handler, and that counter-examples were working as usual (which they weren't before if the option wasn't changed)

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Added documentation on how to make Dafny work for other versions of Z3 Added automatic overriding of prover options if Z3 version 4.8.7 or newer is detected in the language server

atomb

Thanks for doing this! I have a few very small changes to request, but it overall looks great.

It'd be hard to test this without installing multiple versions of Z3 in CI, which is probably a bigger step than we want to take quite yet. We probably will do that sometime before long, though, and when we do it might be worth coming back and adding a test for this feature.

atomb · 2022-09-30T15:29:41Z

Source/DafnyCore/DafnyOptions.cs

-    /proverOpt:O:model.completion=true.
+    first failing assertion. Requires specifying the /mv:<file> option as well
+    as /proverOpt:O:model_compress=false (or /proverOpt:O:model.compact=false if
+    your version of z3 is >= 4.8.7) and /proverOpt:O:model.completion=true.


We'll probably want to swap what's in parentheses once we adopt a newer version by default.

Or maybe update this text to match what's in the message in DafnyModel.cs, which is more symmetric?

Source/DafnyLanguageServer/DafnyLanguageServer.cs

atomb · 2022-09-30T15:38:00Z

Source/DafnyLanguageServer/DafnyLanguageServer.cs

    private static void PublishSolverPath(ILanguageServer server) {
      var telemetryPublisher = server.GetRequiredService<ITelemetryPublisher>();
      string solverPath;
      try {
        var proverOptions = new SMTLibSolverOptions(DafnyOptions.O);
        proverOptions.Parse(DafnyOptions.O.ProverOptions);
        solverPath = proverOptions.ExecutablePath();
+        HandleZ3Version(telemetryPublisher, proverOptions);


In the very long run, I think we may want to handle solvers other than Z3, and perhaps condition on their versions, too. But that's probably somewhat far in the future. :)

Agreed, and then we can rename this method. For now, it specifically do nothing if there is no "z3 version" in the output of the process.

atomb · 2022-09-30T15:39:02Z

docs/DafnyRef/README.md

@@ -24,11 +24,11 @@ other aspects that are dissimilar between the pdf and online versions.



Did you mean to include changes to this file as part of this PR?

Oh yes, that seems unrelated, but I needed this information to update this PR, so I put it in the PR itself.

atomb · 2022-09-30T16:36:03Z

RELEASE_NOTES.md

@@ -4,6 +4,7 @@
 - feat: Support for parsing Basic Multilingual Plane characters from UTF-8 in code and comments (https://github.com/dafny-lang/dafny/pull/2717)
 - feat: Command-line arguments are now available from `Main` in Dafny programs, using `Main(args: seq<string>)` (https://github.com/dafny-lang/dafny/pull/2594)
 - feat: Generate warning when 'old' has no effect (https://github.com/dafny-lang/dafny/pull/2610)
+- feat: Support arbitrary version of z3 (https://github.com/dafny-lang/dafny/pull/2820)


I wonder whether this would be better as "Support arbitrary versions of z3 when using the /proverOpt:PROVER_PATH=/path/to/local/z3 option. Dafny is still distributed with z3 4.8.5 and uses that version by default."

I think Dafny already supports arbitrary version of z3 with this parameter. I was surprised but there was nothing to do there. It's just that model_compress cannot be passed for versions of z3 greater than 4.8.6
What about "Support arbitrary versions of z3 for the language server" ?

Yeah, I like "Support arbitrary versions of z3 for the language server", but perhaps also with the second sentence included? We could even say something about how we plan to make a newer version the default before too long.

Co-authored-by: Aaron Tomb <[email protected]>

RELEASE_NOTES.md

docs/DafnyRef/Options.txt

Source/DafnyCore/DafnyOptions.cs

docs/DafnyRef/Options.txt

atomb

One tiny additional change and then I think it's good to go!

Source/DafnyCore/DafnyOptions.cs

Co-authored-by: Aaron Tomb <[email protected]>

atomb

Looks great!

keyboardDrummer · 2022-10-04T08:57:55Z

@atomb Are we planning to figure out how to configure the latest Z3 version so that it performs as well for Dafny as 4.8.5, or do we think there's no such configuration?

atomb · 2022-10-04T14:55:18Z

@atomb Are we planning to figure out how to configure the latest Z3 version so that it performs as well for Dafny as 4.8.5, or do we think there's no such configuration?

We don't yet know of a configuration that performs as well (and we have tried several possibilities), but this would give us a way to enable a better configuration if we discover one.

cpitclaudel · 2022-10-07T16:06:31Z

Looks like the RELEASE_NOTES entry ended up in the wrong place. I will fix that in #2848

hmijail · 2022-11-23T07:16:49Z

Regarding performance of Z3, just a comment to ensure this is in the radar: version 4.8.16 was the first one available natively to MacOS on ARM, before that it's only available for Intel so it runs emulated in those computers. I'd imagine this worsens performance but haven't compared.

feat: Support for arbitrary versions of z3

dff0620

Added documentation on how to make Dafny work for other versions of Z3 Added automatic overriding of prover options if Z3 version 4.8.7 or newer is detected in the language server

MikaelMayer requested a review from atomb September 30, 2022 14:56

Update RELEASE_NOTES.md

ea909bb

atomb requested changes Sep 30, 2022

View reviewed changes

atomb reviewed Sep 30, 2022

View reviewed changes

Update Source/DafnyLanguageServer/DafnyLanguageServer.cs

d1ca994

Co-authored-by: Aaron Tomb <[email protected]>

MikaelMayer commented Sep 30, 2022

View reviewed changes

RELEASE_NOTES.md Outdated Show resolved Hide resolved

Update RELEASE_NOTES.md

4db01bd

MikaelMayer commented Sep 30, 2022

View reviewed changes

docs/DafnyRef/Options.txt Outdated Show resolved Hide resolved

Update docs/DafnyRef/Options.txt

15bb18a

MikaelMayer commented Sep 30, 2022

View reviewed changes

Source/DafnyCore/DafnyOptions.cs Outdated Show resolved Hide resolved

Update Source/DafnyCore/DafnyOptions.cs

b219ce2

MikaelMayer commented Sep 30, 2022

View reviewed changes

docs/DafnyRef/Options.txt Outdated Show resolved Hide resolved

Update docs/DafnyRef/Options.txt

93d4224

MikaelMayer requested a review from atomb September 30, 2022 20:15

atomb requested changes Sep 30, 2022

View reviewed changes

Source/DafnyCore/DafnyOptions.cs Outdated Show resolved Hide resolved

Update Source/DafnyCore/DafnyOptions.cs

0f8dcc3

Co-authored-by: Aaron Tomb <[email protected]>

MikaelMayer requested a review from atomb September 30, 2022 20:24

Merge branch 'master' into feat-support-all-z3-versions

8b8e47f

atomb previously approved these changes Sep 30, 2022

View reviewed changes

MikaelMayer enabled auto-merge (squash) October 4, 2022 19:21

Fixed the failing integration test

d7d1f21

MikaelMayer dismissed atomb’s stale review via d7d1f21 October 4, 2022 19:23

MikaelMayer added 3 commits October 4, 2022 14:27

Update Options.txt

682bbaa

Merge branch 'master' into feat-support-all-z3-versions

dfb4316

Merge branch 'master' into feat-support-all-z3-versions

4c5b350

MikaelMayer requested a review from atomb October 5, 2022 19:35

atomb approved these changes Oct 5, 2022

View reviewed changes

MikaelMayer added 2 commits October 6, 2022 09:52

Merge branch 'master' into feat-support-all-z3-versions

2905fa7

Merge branch 'master' into feat-support-all-z3-versions

eef7602

MikaelMayer merged commit 5e00d8e into master Oct 6, 2022

MikaelMayer deleted the feat-support-all-z3-versions branch October 6, 2022 15:43

MikaelMayer self-assigned this Oct 6, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Support for arbitrary versions of z3 #2820

feat: Support for arbitrary versions of z3 #2820

MikaelMayer commented Sep 30, 2022

atomb left a comment

atomb Sep 30, 2022

atomb Sep 30, 2022

atomb Sep 30, 2022

MikaelMayer Sep 30, 2022

atomb Sep 30, 2022

MikaelMayer Sep 30, 2022

atomb Sep 30, 2022

MikaelMayer Sep 30, 2022

atomb Sep 30, 2022

atomb left a comment

atomb left a comment

keyboardDrummer commented Oct 4, 2022

atomb commented Oct 4, 2022

cpitclaudel commented Oct 7, 2022

hmijail commented Nov 23, 2022

		@@ -24,11 +24,11 @@ other aspects that are dissimilar between the pdf and online versions.

feat: Support for arbitrary versions of z3 #2820

feat: Support for arbitrary versions of z3 #2820

Conversation

MikaelMayer commented Sep 30, 2022

atomb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb left a comment

Choose a reason for hiding this comment

atomb left a comment

Choose a reason for hiding this comment

keyboardDrummer commented Oct 4, 2022

atomb commented Oct 4, 2022

cpitclaudel commented Oct 7, 2022

hmijail commented Nov 23, 2022