[Test Generation] Deprecate support for old command line interface

Source/DafnyCore/DafnyOptions.cs

@@ -792,8 +792,8 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
           return true;
       }
 
-      // Unless this is an option for test generation, defer to superclass
-      return TestGenOptions.ParseOption(name, ps) || base.ParseOption(name, ps);
+      // Defer to superclass
+      return base.ParseOption(name, ps);
     }
 
     private static string[] ParseInnerArguments(string argumentsString) {
@@ -1462,8 +1462,6 @@ focal predicate P to P#[_k-1].
     /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and
     /proverOpt:O:model.completion=true.
 
----- Test generation options -----------------------------------------------
-{TestGenOptions.Help}
 ---- Compilation options ---------------------------------------------------
 
 /compile:<n>

Source/DafnyCore/TestGenerationOptions.cs

@@ -5,76 +5,14 @@
 namespace Microsoft.Dafny {
 
   public class TestGenerationOptions {
-
-    public static readonly string TestInlineAttribute = "testInline";
-    public static readonly string TestEntryAttribute = "testEntry";
+    public const string TestInlineAttribute = "testInline";
+    public const string TestEntryAttribute = "testEntry";
     public bool WarnDeadCode = false;
     public enum Modes { None, Block, Path };
     public Modes Mode = Modes.None;
     public uint SeqLengthLimit = 0;
     [CanBeNull] public string PrintBpl = null;
-    public bool DisablePrune = false;
+    public bool ForcePrune = false;
     public const uint DefaultTimeLimit = 10;
-
-    public bool ParseOption(string name, Bpl.CommandLineParseState ps) {
-      var args = ps.args;
-
-      switch (name) {
-
-        case "warnDeadCode":
-          WarnDeadCode = true;
-          Mode = Modes.Block;
-          return true;
-
-        case "generateTestMode":
-          if (ps.ConfirmArgumentCount(1)) {
-            Mode = args[ps.i] switch {
-              "None" => Modes.None,
-              "Block" => Modes.Block,
-              "Path" => Modes.Path,
-              _ => throw new Exception("Invalid value for generateTestMode")
-            };
-          }
-          return true;
-
-        case "generateTestSeqLengthLimit":
-          var limit = 0;
-          if (ps.GetIntArgument(ref limit)) {
-            SeqLengthLimit = (uint)limit;
-          }
-          return true;
-
-        case "generateTestPrintBpl":
-          if (ps.ConfirmArgumentCount(1)) {
-            PrintBpl = args[ps.i];
-          }
-          return true;
-
-        case "generateTestNoPrune":
-          DisablePrune = true;
-          return true;
-      }
-
-      return false;
-    }
-
-    public string Help => @"
-/warnDeadCode
-    Use counterexample generation to warn about potential dead code.
-/generateTestMode:<None|Block|Path>
-    None (default) - Has no effect.
-    Block - Prints block-coverage tests for the given program.
-    Path - Prints path-coverage tests for the given program.
-    Using /definiteAssignment:3, /generateTestNoPrune, 
-    /generateTestSeqLengthLimit, and /loopUnroll is highly recommended
-    when generating tests.
-/generateTestSeqLengthLimit:<n>
-    Add an axiom that sets the length of all sequences to be no greater 
-    than <n>. 0 (default) indicates no limit.
-/generateTestPrintBpl:<fileName>
-    Print the Boogie code used during test generation.
-/generateTestNoPrune
-    Disable axiom pruning that Dafny uses to speed up verification.";
-
   }
 }

Source/DafnyTestGeneration/DeadCodeCommand.cs

@@ -6,16 +6,17 @@
 using System.CommandLine;
 using System.CommandLine.Invocation;
 using System.Linq;
+using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 
 public class DeadCodeCommand : ICommandSpec {
   public IEnumerable<Option> Options =>
     new Option[] {
-      // IMPORTANT: Before adding new options, make sure they are
-      // appropriately copied over in the GenerateTestCommand.CopyForProcedure method 
       GenerateTestsCommand.LoopUnroll,
       GenerateTestsCommand.SequenceLengthLimit,
+      GenerateTestsCommand.ForcePrune,
+      GenerateTestsCommand.PrintBpl,
       BoogieOptionBag.SolverLog,
       BoogieOptionBag.SolverOption,
       BoogieOptionBag.SolverOptionHelp,
@@ -32,16 +33,7 @@ public Command Create() {
   }
 
   public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
-    // IMPORTANT: Before adding new default options, make sure they are
-    // appropriately copied over in the GenerateTestCommand.CopyForProcedure method 
-    dafnyOptions.Compile = true;
-    dafnyOptions.RunAfterCompile = false;
-    dafnyOptions.ForceCompile = false;
-    dafnyOptions.ForbidNondeterminism = true;
-    dafnyOptions.DefiniteAssignmentLevel = 2;
-
-    dafnyOptions.TestGenOptions.Mode = TestGenerationOptions.Modes.Block;
+    GenerateTestsCommand.PostProcess(dafnyOptions, options, context, TestGenerationOptions.Modes.Block);
     dafnyOptions.TestGenOptions.WarnDeadCode = true;
-    dafnyOptions.Set(DafnyConsolePrinter.ShowSnippets, false);
   }
 }

Source/DafnyTestGeneration/GenerateTestsCommand.cs

@@ -4,6 +4,8 @@
 using System.CommandLine.Invocation;
 using System.Linq;
 using DafnyCore;
+using Microsoft.Boogie;
+
 // Copyright by the contributors to the Dafny Project
 // SPDX-License-Identifier: MIT
 
@@ -23,7 +25,7 @@ public class GenerateTestsCommand : ICommandSpec {
       BoogieOptionBag.SolverResourceLimit,
       BoogieOptionBag.VerificationTimeLimit,
       PrintBpl,
-      DisablePrune
+      ForcePrune
     }.Concat(ICommandSpec.ConsoleOutputOptions).
       Concat(ICommandSpec.ResolverOptions);
 
@@ -57,23 +59,25 @@ public Command Create() {
   }
 
   public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
-    // IMPORTANT: Before adding new default options, make sure they are
-    // appropriately copied over in the CopyForProcedure method above
+    var mode = context.ParseResult.GetValueForArgument(modeArgument) switch {
+      Mode.Path => TestGenerationOptions.Modes.Path,
+      Mode.Block => TestGenerationOptions.Modes.Block,
+      _ => throw new ArgumentOutOfRangeException()
+    };
+    PostProcess(dafnyOptions, options, context, mode);
+  }
+
+  internal static void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context, TestGenerationOptions.Modes mode) {
     dafnyOptions.CompilerName = "cs";
     dafnyOptions.Compile = true;
     dafnyOptions.RunAfterCompile = false;
     dafnyOptions.ForceCompile = false;
     dafnyOptions.DeprecationNoise = 0;
     dafnyOptions.ForbidNondeterminism = true;
     dafnyOptions.DefiniteAssignmentLevel = 2;
+    dafnyOptions.TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates;
     dafnyOptions.Set(DafnyConsolePrinter.ShowSnippets, false);
-
-    var mode = context.ParseResult.GetValueForArgument(modeArgument);
-    dafnyOptions.TestGenOptions.Mode = mode switch {
-      Mode.Path => TestGenerationOptions.Modes.Path,
-      Mode.Block => TestGenerationOptions.Modes.Block,
-      _ => throw new ArgumentOutOfRangeException()
-    };
+    dafnyOptions.TestGenOptions.Mode = mode;
   }
 
   public static readonly Option<uint> SequenceLengthLimit = new("--length-limit",
@@ -86,8 +90,8 @@ public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationCo
     "Print the Boogie code used during test generation.") {
     ArgumentHelpName = "filename"
   };
-  public static readonly Option<bool> DisablePrune = new("--no-prune",
-    "Disable axiom pruning that Dafny uses to speed up verification.") {
+  public static readonly Option<bool> ForcePrune = new("--force-prune",
+    "Enable axiom pruning that Dafny uses to speed up verification. This may negatively affect the quality of tests.") {
   };
   static GenerateTestsCommand() {
     DafnyOptions.RegisterLegacyBinding(LoopUnroll, (options, value) => {
@@ -99,15 +103,15 @@ static GenerateTestsCommand() {
     DafnyOptions.RegisterLegacyBinding(PrintBpl, (options, value) => {
       options.TestGenOptions.PrintBpl = value;
     });
-    DafnyOptions.RegisterLegacyBinding(DisablePrune, (options, value) => {
-      options.TestGenOptions.DisablePrune = value;
+    DafnyOptions.RegisterLegacyBinding(ForcePrune, (options, value) => {
+      options.TestGenOptions.ForcePrune = value;
     });
 
     DooFile.RegisterNoChecksNeeded(
       LoopUnroll,
       SequenceLengthLimit,
       PrintBpl,
-      DisablePrune
+      ForcePrune
     );
   }
 }

Source/DafnyTestGeneration/ProgramModification.cs

@@ -115,7 +115,7 @@ private static void SetupForCounterexamples(DafnyOptions options) {
       options.ErrorTrace = 1;
       options.EnhancedErrorMessages = 1;
       options.ModelViewFile = "-";
-      options.Prune = !options.TestGenOptions.DisablePrune;
+      options.Prune = options.TestGenOptions.ForcePrune;
     }
 
     /// <summary>

docs/DafnyRef/Options.txt

@@ -326,24 +326,6 @@ Usage: dafny [ option ... ] [ filename ... ]
       /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and
       /proverOpt:O:model.completion=true.
 
-  ---- Test generation options -----------------------------------------------
-
-  /warnDeadCode
-      Use counterexample generation to warn about potential dead code.
-  /generateTestMode:<None|Block|Path>
-      None (default) - Has no effect.
-      Block - Prints block-coverage tests for the given program.
-      Path - Prints path-coverage tests for the given program.
-      Using /definiteAssignment:3, /generateTestNoPrune, 
-      /generateTestSeqLengthLimit, and /loopUnroll is highly recommended
-      when generating tests.
-  /generateTestSeqLengthLimit:<n>
-      Add an axiom that sets the length of all sequences to be no greater 
-      than <n>. 0 (default) indicates no limit.
-  /generateTestPrintBpl:<fileName>
-      Print the Boogie code used during test generation.
-  /generateTestNoPrune
-      Disable axiom pruning that Dafny uses to speed up verification.
   ---- Compilation options ---------------------------------------------------
 
   /compileSuffix:<value>

docs/dev/news/4385.fix

@@ -0,0 +1 @@
+Old command line interface for test generation is no longer supported, all calls should use dafny generate-tests