Add the --solver-path option (#3184)

### Changes

Add the `--solver-path` option to allow customising the SMT solver used
when using the new Dafny CLI.

### Testing

Option is used in a new littish test.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Author: keyboardDrummer

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -110,6 +110,8 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
 false - The char type represents any UTF-16 code unit.
 true - The char type represents any Unicode scalar value.".TrimStart());
 
+  public static readonly Option<string> SolverPath = new("--solver-path",
+    "Can be used to specify a custom SMT solver to use for verifying Dafny proofs.");
   public static readonly Option<bool> VerifyIncludedFiles = new("--verify-included-files",
     "Verify code in included files.");
   public static readonly Option<bool> WarningAsErrors = new("--warn-as-errors",
@@ -123,50 +125,40 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
     "Include the Dafny runtime as source in the target language.");
 
   static CommonOptionBag() {
+    DafnyOptions.RegisterLegacyBinding(SolverPath, (options, value) => {
+      if (!string.IsNullOrEmpty(value)) {
+        options.ProverOptions.Add($"PROVER_PATH={value}");
+      }
+    });
+
     DafnyOptions.RegisterLegacyBinding(ManualLemmaInduction, (options, value) => {
       if (value) {
         options.Induction = 1;
       }
     });
-    DafnyOptions.RegisterLegacyBinding(IncludeRuntime, (options, value) => {
-      options.UseRuntimeLib = !value;
-    });
-    DafnyOptions.RegisterLegacyBinding(WarnShadowing, (options, value) => {
-      options.WarnShadowing = value;
-    });
-    DafnyOptions.RegisterLegacyBinding(WarnMissingConstructorParenthesis, (options, value) => {
-      options.DisallowConstructorCaseWithoutParentheses = value;
-    });
-    DafnyOptions.RegisterLegacyBinding(WarningAsErrors, (options, value) => {
-      options.WarningsAsErrors = value;
-    });
-    DafnyOptions.RegisterLegacyBinding(VerifyIncludedFiles, (options, value) => {
-      options.VerifyAllModules = value;
-    });
+    DafnyOptions.RegisterLegacyBinding(IncludeRuntime, (options, value) => { options.UseRuntimeLib = !value; });
+    DafnyOptions.RegisterLegacyBinding(WarnShadowing, (options, value) => { options.WarnShadowing = value; });
+    DafnyOptions.RegisterLegacyBinding(WarnMissingConstructorParenthesis,
+      (options, value) => { options.DisallowConstructorCaseWithoutParentheses = value; });
+    DafnyOptions.RegisterLegacyBinding(WarningAsErrors, (options, value) => { options.WarningsAsErrors = value; });
+    DafnyOptions.RegisterLegacyBinding(VerifyIncludedFiles,
+      (options, value) => { options.VerifyAllModules = value; });
 
-    DafnyOptions.RegisterLegacyBinding(Target, (options, value) => {
-      options.CompilerName = value;
-    });
+    DafnyOptions.RegisterLegacyBinding(Target, (options, value) => { options.CompilerName = value; });
 
 
-    DafnyOptions.RegisterLegacyBinding(QuantifierSyntax, (options, value) => {
-      options.QuantifierSyntax = value;
-    });
+    DafnyOptions.RegisterLegacyBinding(QuantifierSyntax, (options, value) => { options.QuantifierSyntax = value; });
 
-    DafnyOptions.RegisterLegacyBinding(Plugin, (options, value) => {
-      options.AdditionalPluginArguments = value;
-    });
+    DafnyOptions.RegisterLegacyBinding(Plugin, (options, value) => { options.AdditionalPluginArguments = value; });
 
     DafnyOptions.RegisterLegacyBinding(Prelude, (options, value) => {
       options.DafnyPrelude = value;
-      options.ExpandFilename(options.DafnyPrelude, x => options.DafnyPrelude = x, options.LogPrefix, options.FileTimestamp);
-    });
-    DafnyOptions.RegisterLegacyBinding(Libraries, (options, value) => {
-      options.LibraryFiles = value.ToHashSet();
-    });
-    DafnyOptions.RegisterLegacyBinding(Output, (options, value) => {
-      options.DafnyPrintCompiledFile = value;
+      options.ExpandFilename(options.DafnyPrelude, x => options.DafnyPrelude = x, options.LogPrefix,
+        options.FileTimestamp);
     });
+    DafnyOptions.RegisterLegacyBinding(Libraries,
+      (options, value) => { options.LibraryFiles = value.ToHashSet(); });
+    DafnyOptions.RegisterLegacyBinding(Output, (options, value) => { options.DafnyPrintCompiledFile = value; });
 
     DafnyOptions.RegisterLegacyBinding(CompileVerbose, (o, v) => o.CompileVerbose = v);
     DafnyOptions.RegisterLegacyBinding(DisableNonLinearArithmetic, (o, v) => o.DisableNLarith = v);
@@ -177,12 +169,13 @@ static CommonOptionBag() {
     RelaxDefiniteAssignment.AddValidator(optionResult => {
       var enforceDeterminismResult = optionResult.FindResultFor(EnforceDeterminism);
       if (enforceDeterminismResult is not null && enforceDeterminismResult.GetValueOrDefault<bool>()) {
-        optionResult.ErrorMessage = $"The option {RelaxDefiniteAssignment.Name} can not be used in conjunction with {EnforceDeterminism.Name}.";
+        optionResult.ErrorMessage =
+          $"The option {RelaxDefiniteAssignment.Name} can not be used in conjunction with {EnforceDeterminism.Name}.";
       }
     });
-    DafnyOptions.RegisterLegacyBinding(RelaxDefiniteAssignment, (options, value) => {
-      options.DefiniteAssignmentLevel = value ? 1 : 2;
-    });
+    DafnyOptions.RegisterLegacyBinding(RelaxDefiniteAssignment,
+      (options, value) => { options.DefiniteAssignmentLevel = value ? 1 : 2; });
 
   }
 }
+

Source/DafnyCore/Options/ICommandSpec.cs

@@ -29,7 +29,8 @@ static ICommandSpec() {
   public static IReadOnlyList<Option> VerificationOptions = new Option[] {
     BoogieOptionBag.VerificationTimeLimit,
     CommonOptionBag.VerifyIncludedFiles,
-    CommonOptionBag.ManualLemmaInduction
+    CommonOptionBag.ManualLemmaInduction,
+    CommonOptionBag.SolverPath,
   }.ToList();
 
   public static IReadOnlyList<Option> ExecutionOptions = new Option[] {

Test/cli/proverPath.dfy

@@ -0,0 +1,6 @@
+// RUN: %baredafny verify %args --solver-path="%z3" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// UNSUPPORTED: windows
+method m() {
+  assert 1 + 1 == 2;
+}

Test/cli/proverPath.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors