feat: Support for arbitrary versions of z3

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 for the language server. Dafny is still distributed with z3 4.8.5 and uses that version by default. (https://github.com/dafny-lang/dafny/pull/2820)
 - fix: Missing related position in failing precondition (https://github.com/dafny-lang/dafny/pull/2658)
 - fix: No more IDE crashing on the elephant operator (https://github.com/dafny-lang/dafny/pull/2668)
 - fix: Use the right comparison operators for bitvectors in Javascript (https://github.com/dafny-lang/dafny/pull/2716)

Source/DafnyCore/DafnyOptions.cs

@@ -1332,9 +1332,8 @@ focal predicate P to P#[_k-1].
 
 /extractCounterexample
     If verification fails, report a detailed counterexample for the
-    first failing assertion. Requires specifying the /mv option as well
-    as /proverOpt:O:model_compress=false and
-    /proverOpt:O:model.completion=true.
+    first failing assertion. Requires specifying the /mv:<file> option as well
+    as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and /proverOpt:O:model.completion=true.
 
 /countVerificationErrors:<n>
     (deprecated)

Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs

@@ -873,7 +873,10 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
       return result;
     }
 
-    private const string PleaseEnableModelCompressFalse = "Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values.";
+    private const string PleaseEnableModelCompressFalse =
+      "Please enable /proverOpt:O:model_compress=false (for z3 version < 4.8.7)" +
+      " or /proverOpt:O:model.compact=false (for z3 version >= 4.8.7)," +
+      " otherwise you'll get unexpected values.";
 
     /// <summary>
     /// Return the name of the field represented by the given element.

Source/DafnyLanguageServer/DafnyLanguageServer.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics;
+using System.Text.RegularExpressions;
 using Microsoft.Dafny.LanguageServer.Handlers;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Workspace;
@@ -14,7 +15,7 @@
 using System.Threading.Tasks;
 using Microsoft.Boogie.SMTLib;
 using Microsoft.Extensions.Options;
-using OmniSharp.Extensions.LanguageServer.Protocol.Window;
+using Action = System.Action;
 
 namespace Microsoft.Dafny.LanguageServer {
   public static class DafnyLanguageServer {
@@ -55,20 +56,61 @@ private static Task InitializeAsync(ILanguageServer server, InitializeParams req
       return Task.CompletedTask;
     }
 
+    private static readonly Regex Z3VersionRegex = new Regex(@"Z3 version (?<major>\d+)\.(?<minor>\d+)\.(?<patch>\d+)");
+
     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);
       } catch (Exception e) {
         solverPath = $"Error while determining solver path: {e}";
       }
 
       telemetryPublisher.PublishSolverPath(solverPath);
     }
 
+    private static void HandleZ3Version(ITelemetryPublisher telemetryPublisher, SMTLibSolverOptions proverOptions) {
+      var z3Process = new ProcessStartInfo(proverOptions.ProverPath, "-version") {
+        CreateNoWindow = true,
+        RedirectStandardError = true,
+        RedirectStandardOutput = true,
+        RedirectStandardInput = true
+      };
+      var run = Process.Start(z3Process);
+      if (run == null) {
+        return;
+      }
+
+      var actualOutput = run.StandardOutput.ReadToEnd();
+      run.WaitForExit();
+      var versionMatch = Z3VersionRegex.Match(actualOutput);
+      if (!versionMatch.Success) {
+        // Might be another solver.
+        return;
+      }
+
+      telemetryPublisher.PublishZ3Version(versionMatch.Value);
+      var major = int.Parse(versionMatch.Groups["major"].Value);
+      var minor = int.Parse(versionMatch.Groups["minor"].Value);
+      var patch = int.Parse(versionMatch.Groups["patch"].Value);
+      if (major <= 4 && (major < 4 || minor <= 8) && (minor < 8 || patch <= 6)) {
+        return;
+      }
+
+      var toReplace = "O:model_compress=false";
+      var i = DafnyOptions.O.ProverOptions.IndexOf(toReplace);
+      if (i == -1) {
+        telemetryPublisher.PublishUnhandledException(new Exception($"Z3 version is > 4.8.6 but I did not find {toReplace} in the prover options:" + string.Join(" ", DafnyOptions.O.ProverOptions)));
+        return;
+      }
+
+      DafnyOptions.O.ProverOptions[i] = "O:model.compact=false";
+    }
+
     /// <summary>
     /// Load the plugins for the Dafny pipeline
     /// </summary>

Source/DafnyLanguageServer/Workspace/DocumentOptions.cs

@@ -28,7 +28,7 @@ static DocumentOptions() {
 
     public List<string> AugmentedProverOptions =>
       DafnyOptions.O.ProverOptions.Concat(new List<string>() {
-        "O:model_compress=false",
+        "O:model_compress=false", // Replaced by "O:model.compact=false" if z3's version is > 4.8.6
         "O:model.completion=true",
         "O:model_evaluator.completion=true"
       }).ToList();

Source/DafnyLanguageServer/Workspace/ITelemetryPublisher.cs

@@ -11,7 +11,8 @@ public interface ITelemetryPublisher {
     protected enum TelemetryEventKind {
       UpdateComplete,
       UnhandledException,
-      SolverPath
+      SolverPath,
+      Z3Version
     }
 
     /// <summary>
@@ -38,5 +39,9 @@ public void PublishUnhandledException(Exception e) {
     public void PublishSolverPath(string solverPath) {
       PublishTelemetry(TelemetryEventKind.SolverPath, solverPath);
     }
+
+    public void PublishZ3Version(string z3Version) {
+      PublishTelemetry(TelemetryEventKind.Z3Version, z3Version);
+    }
   }
 }

docs/DafnyRef/Options.txt

@@ -343,9 +343,8 @@ Usage: Dafny [ option ... ] [ filename ... ]
 
   /extractCounterexample
       If verification fails, report a detailed counterexample for the
-      first failing assertion. Requires specifying the /mv option as well
-      as /proverOpt:O:model_compress=false and
-      /proverOpt:O:model.completion=true.
+      first failing assertion. Requires specifying the /mv:<file> option as well
+      as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and /proverOpt:O:model.completion=true.
 
   /countVerificationErrors:<n>
       (deprecated)

docs/DafnyRef/README.md

@@ -24,11 +24,11 @@ other aspects that are dissimilar between the pdf and online versions.
 
 GitHub pages are rendered (converted from markdown to html) using Jekyll.
 The result is a single, long html page.
-There are a number of configuration files for Jekyll in the docs folder and
+There are a number of configuration files for Jekyll in the `docs` folder and
 subfolders. In order to render files locally you must
-* have ruby, bundler and jekyll installed on your machine
-* set the working directly (cd) to the docs folder (Windows or Ruby 3.0 users, see below for some tweaks)
-* run the jekyll server: bundle exec jekyll server
+* have `ruby`, `bundler` and `jekyll` installed on your machine
+* set the working directly (`cd`) to the `docs` folder (Windows or Ruby 3.0 users, see below for some tweaks)
+* run the jekyll server: `bundle exec jekyll server`
 * open a browser on the page http://localhost:4000 or directly to http://localhost:4000/DafnyRef/DafnyRef
 * the server rerenders when files are changed -- but not always quite completely. Sometimes one must kill the server process, delete all the files in the _saite folder, and restart the server.
 
@@ -38,6 +38,8 @@ The Makefile does some preprocessing of the markdown files: it removes some
 markdown lines that are not interpreted by pandoc and adds some additional
 directives, such as page breaks.
 
+To re-generate `Options.txt`, run `make options` in the `DafnyRef` folder.
+
 ## Windows users or Ruby 3.0 users
 
 You might want to apply this diff to the file `../GemFile`
@@ -111,4 +113,4 @@ file as well.
 ## LSP
 
 Many IDEs interact with Language Servers (via LSP). Possibly an LSP protocol
-will be generated in the future.
+will be generated in the future.