Improve Z3 detection #3233

atomb · 2022-12-20T22:16:20Z

Be more explicit about the path of the executable to invoke.
Identify the version and set different Z3 options accordingly.

Fixes #2370
Enables a fix for #1477
Interacts with #1914 (which may already be fixed)

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

* Be more explicit about the path of the executable to invoke. * Identify the version and set different Z3 options accordingly. Fixes dafny-lang#2370 Enables a fix for dafny-lang#1477 Interacts with dafny-lang#1914 (which may already be fixed)

This avoids errors when not doing verification.

MikaelMayer

Some slight changes, but otherwise, thanks for migrating z3 detection from DafnyLanguageServer to Dafny and making it even more robust!

MikaelMayer · 2023-01-09T19:35:18Z

Source/DafnyCore/DafnyOptions.cs


- var z3binName = isUnix ? "z3" : "z3.exe";
+ var platform = System.Environment.OSVersion.Platform;
+ var isUnix = platform == PlatformID.Unix || platform == PlatformID.MacOSX || (int)platform == 128;


Can you please add a comment about this 128?

I honestly don't know what it is. The code previously compared with three constant integers that weren't explained. I saw that two of them were equal to named constants in the PlatformID class, so I changed the code to refer to those, but the third one didn't correspond to any documented value. I suspect it actually shows up in practice, but I don't know when. This version seems better than the old code, even if not perfect.

I would feel comfortable removing it as, according to the documentation, 128 is not a valid value:
https://learn.microsoft.com/en-us/dotnet/api/system.platformid?view=net-7.0

Sounds good to me.

MikaelMayer · 2023-01-09T19:38:18Z

Source/DafnyCore/DafnyOptions.cs

+ if (z3Version is not null && z3Version.Major == 4 && z3Version.Minor == 8 && z3Version.Build == 5) {
+ // These options tend to help with Z3 4.8.5 but hurt with newer versions of Z3.
+ SetZ3Option("smt.case_split", "3");
+ SetZ3Option("smt.arith.solver", "2");


How much are they hurting? Can you please describe the problem in a separate issue?

Also consider describing a range of versions in the conditional, rather than an exact version. Perhaps refactor this:
https://github.com/dafny-lang/dafny/pull/3233/files#diff-b3d55f76ae78d57880964c42ed16a37e9e6a8a3a7ca4022cb96367bccda8d667R80

My experience is that any version newer than 4.8.5 works better with those options removed. I considered adding code to produce an error if it detects a version older than 4.8.5. If I do that, then the conditional above really should just be for a single version. What do you think?

If you add this error if we detect a version older than 4.8.5, then yes that's fine. Where would you add this error?
If you do not add it in this PR, then I would prefer to see a version "<=" instead of just "=".

I went for changing it to <= for now, since it's a little awkward to a signal an error from that location and I haven't actually seen evidence that versions < 4.8.5 don't work. Before we release 4.0 we may want to test those early versions and have a more complete strategy for how to handle the entire range of available versions.

MikaelMayer · 2023-01-09T19:46:28Z

Source/DafnyCore/DafnyMain.cs

@@ -319,6 +319,12 @@ private class IncludeComparer : IComparer<Include> {
 Microsoft.Boogie.Program boogieProgram, string programId) {
 var moduleId = (programId ?? "main_program_id") + "_" + moduleName;

+ var proverPath = DafnyOptions.O.ProverOptions.Find(o => o.StartsWith("PROVER_PATH="));
+ if (proverPath is null && DafnyOptions.O.Verify) {
+ Console.WriteLine("Z3 not found in explicit --solver-path option, Dafny distribution, or PATH environment variable.");


Suggested change

Console.WriteLine("Z3 not found in explicit --solver-path option, Dafny distribution, or PATH environment variable.");

Console.WriteLine("Z3 not found. Please either provide a path to the z3 executable using the `--solver-path <path>` option, or manually place the `z3` folder next to the Dafny executable you are using (this folder should contain `bin/z3` or `bin/z3.exe`), or set the PATH environment variable to also target the folder containing the z3 executable.");

Errors with explicit action items are always appreciated.

I updated the text to a slightly reworded version of your suggestion.

And check for versions <= 4.8.5, rather than just ==.

* Be more explicit about the path of the executable to invoke. * Identify the version and set different Z3 options accordingly. Fixes dafny-lang#2370 Enables a fix for dafny-lang#1477 Interacts with dafny-lang#1914 (which may already be fixed) By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

This returns to the behavior prior to PR dafny-lang#3233. It seems that the case_split change makes "time travelling triggers" more likely: dafny-lang#3362 And, although the arith_solver change sped up verification of some programs, it seems that it slowed down more programs. I'd still like to leave the version detection logic in, though, since the language server uses it, and since I think other parts of the CLI will likely use it soon.

This returns to the behavior prior to PR #3233. It seems that the case_split change makes "time travelling triggers" more likely: #3362 And, although the arith_solver change sped up verification of some programs, it seems that it slowed down more programs. I'd still like to leave the version detection logic in, though, since the language server uses it, and since I think other parts of the CLI will likely use it soon. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Improve Z3 detection

e8a4d17

* Be more explicit about the path of the executable to invoke. * Identify the version and set different Z3 options accordingly. Fixes dafny-lang#2370 Enables a fix for dafny-lang#1477 Interacts with dafny-lang#1914 (which may already be fixed)

atomb mentioned this pull request Dec 20, 2022

Dafny does not check whether it's compatible with the version of Z3 it's using #1477

Open

atomb added 6 commits December 21, 2022 16:21

Merge remote-tracking branch 'upstream/master' into z3-path-version

47c1878

Merge remote-tracking branch 'upstream/master' into z3-path-version

94de5e6

Small cleanups

b58c19d

Include z3 in more test packages

56e2038

Error later when failing to find Z3

4f47175

This avoids errors when not doing verification.

Really only try to detect Z3 when it's being used

aff298e

atomb marked this pull request as ready for review January 6, 2023 21:02

atomb requested review from MikaelMayer, keyboardDrummer and robin-aws January 6, 2023 21:02

atomb added 3 commits January 6, 2023 13:34

Improve behavior with bad prover path

886c414

Fix expected test output

ba21bc8

Merge remote-tracking branch 'upstream/master' into z3-path-version

a9b8343

atomb enabled auto-merge (squash) January 6, 2023 22:22

MikaelMayer requested changes Jan 9, 2023

View reviewed changes

atomb added 4 commits January 9, 2023 14:42

Improve message when Z3 not found

ce36954

Remove undocumented/invalid Unix platform comparison

dbc9e84

Compare Z3 version more idiomatically

45e6b7b

And check for versions <= 4.8.5, rather than just ==.

Merge remote-tracking branch 'upstream/master' into z3-path-version

ca458ea

atomb requested a review from MikaelMayer January 9, 2023 22:44

MikaelMayer approved these changes Jan 9, 2023

View reviewed changes

atomb merged commit 1ad148e into dafny-lang:master Jan 9, 2023

atomb mentioned this pull request Jan 20, 2023

Set all Z3 options regardless of Z3 version #3385

Merged

keyboardDrummer mentioned this pull request Feb 15, 2023

Stop creating dafny options (expensive) more than once #3543

Merged

atomb deleted the z3-path-version branch January 4, 2024 17:12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improve Z3 detection #3233

Improve Z3 detection #3233

atomb commented Dec 20, 2022 •

edited

Loading

MikaelMayer left a comment

MikaelMayer Jan 9, 2023

atomb Jan 9, 2023

MikaelMayer Jan 9, 2023

atomb Jan 9, 2023

MikaelMayer Jan 9, 2023

atomb Jan 9, 2023

MikaelMayer Jan 9, 2023

atomb Jan 9, 2023

MikaelMayer Jan 9, 2023

atomb Jan 9, 2023

	Console.WriteLine("Z3 not found in explicit --solver-path option, Dafny distribution, or PATH environment variable.");
	Console.WriteLine("Z3 not found. Please either provide a path to the z3 executable using the `--solver-path <path>` option, or manually place the `z3` folder next to the Dafny executable you are using (this folder should contain `bin/z3` or `bin/z3.exe`), or set the PATH environment variable to also target the folder containing the z3 executable.");

Improve Z3 detection #3233

Improve Z3 detection #3233

Conversation

atomb commented Dec 20, 2022 • edited Loading

MikaelMayer 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

Choose a reason for hiding this comment

atomb commented Dec 20, 2022 •

edited

Loading