Rename command-line options for VC randomization (boogie-org#678)

* renaming command-line options

* test fix

* address feedback

Source/Core/CoreOptions.cs

@@ -60,7 +60,7 @@ public enum Inlining
  TypeEncoding TypeEncodingMethod { get; set; }
  SubsumptionOption UseSubsumption { get; }
  int VcsCores { get; }
- int RandomSeedIterations { get; }
+ int RandomizeVcIterations { get; }
  List<string> ProverOptions { get; }
  bool Prune { get; }
  bool RunDiagnosticsOnTimeout { get; }

Source/ExecutionEngine/CommandLineOptions.cs

@@ -420,7 +420,7 @@ public bool InstrumentWithAsserts
 
  public int? RandomSeed { get; set; }
 
- public int RandomSeedIterations { get; set; } = 1;
+ public int RandomizeVcIterations { get; set; } = 1;
 
  public bool PrintWithUniqueASTIds {
  get => printWithUniqueAstIds;
@@ -1450,9 +1450,10 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
  ps.GetIntArgument(x => VcsCores = x, a => 1 <= a);
  return true;
 
- case "randomSeedIterations":
- ps.GetIntArgument(x => RandomSeedIterations = x, a => 1 <= a);
- RandomSeed ??= 0; // Using /randomSeedIterations without any randomness isn't very useful
+ case "randomSeedIterations": // old name of the option that should be removed soon
+ case "randomizeVcIterations":
+ ps.GetIntArgument(x => RandomizeVcIterations = x, a => 1 <= a);
+ RandomSeed ??= 0; // Set to 0 if not already set
  return true;
 
  case "vcsLoad":
@@ -2208,25 +2209,23 @@ be n (default 500)
  a linear number of splits. The default way (top-down) is more
  aggressive and it may create an exponential number of splits.
 
- /randomSeed:<n>
- Turn on randomization of the input that Boogie passes to the 
+ /randomSeed:<s>
+ Supply the random seed for /randomizeVcIterations option.
+
+ /randomizeVcIterations:<n>
+ Turn on randomization of the input that Boogie passes to the
  SMT solver and turn on randomization in the SMT solver itself.
- 
+ Attempt to randomize and prove each VC n times using the random
+ seed s provided by the option /randomSeed:<s>. If /randomSeed option
+ is not provided, s is chosen to be zero.
+
  Certain Boogie inputs are unstable in the sense that changes to 
  the input that preserve its meaning may cause the output to change.
- The /randomSeed option simulates meaning-preserving changes to 
- the input without requiring the user to actually make those changes.
-
- The /randomSeed option is implemented by renaming variables and 
- reordering declarations in the input, and by setting 
- solver options that have similar effects.
-
- /randomSeedIterations:<n>
- Attempt to prove each VC n times with n random seeds. If
- /randomSeed has been provided, each proof attempt will use
- a new random seed derived from this original seed. If not,
- it will implicitly use /randomSeed:0 to ensure a difference
- between iterations.
+ This option simulates meaning-preserving changes to the input
+ without requiring the user to actually make those changes.
+ This option is implemented by renaming variables and reordering
+ declarations in the input, and by setting solver options that have
+ similar effects.
 
  ---- Verification-condition splitting --------------------------------------
 

Source/VCGeneration/Checker.cs

@@ -158,7 +158,7 @@ private void SetRlimit(uint rlimit)
  /// </summary>
  private void Setup(Program prog, ProverContext ctx, Split split)
  {
- SolverOptions.RandomSeed = 1 < Options.RandomSeedIterations ? split.NextRandom() : split.RandomSeed;
+ SolverOptions.RandomSeed = 1 < Options.RandomizeVcIterations ? split.NextRandom() : split.RandomSeed;
  var random = SolverOptions.RandomSeed == null ? null : new Random(SolverOptions.RandomSeed.Value);
 
  Program = prog;

Source/VCGeneration/SplitAndVerifyWorker.cs

@@ -105,7 +105,7 @@ async Task DoWorkForMultipleIterations(Split split, CancellationToken cancellati
  {
  int currentSplitNumber = DoSplitting ? Interlocked.Increment(ref splitNumber) - 1 : -1;
  split.SplitIndex = currentSplitNumber;
- var tasks = Enumerable.Range(0, options.RandomSeedIterations).Select(iteration =>
+ var tasks = Enumerable.Range(0, options.RandomizeVcIterations).Select(iteration =>
  DoWork(iteration, split, cancellationToken));
  await Task.WhenAll(tasks);
  }
@@ -130,7 +130,7 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance
  {
  if (options.Trace && DoSplitting) {
  var splitNum = split.SplitIndex + 1;
- var splitIdxStr = options.RandomSeedIterations > 1 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}";
+ var splitIdxStr = options.RandomizeVcIterations > 1 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}";
  run.TraceWriter.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
  split.Stats, splitIdxStr, total, 100 * provenCost / (provenCost + remainingCost));
  }

Test/commandline/RandomSeedIterations.bpl

@@ -1,5 +1,5 @@
-// RUN: %parallel-boogie -randomSeedIterations:2 -xml:"%t-1.xml" "%s"
-// RUN: %parallel-boogie -randomSeedIterations:2 -xml:"%t-2.xml" "%s"
+// RUN: %parallel-boogie -randomizeVcIterations:2 -xml:"%t-1.xml" "%s"
+// RUN: %parallel-boogie -randomizeVcIterations:2 -xml:"%t-2.xml" "%s"
 // RUN: grep -Eo "resourceCount=\"[0-9]+\"" "%t-1.xml" | sort -g > "%t-res1"
 // RUN: grep -Eo "resourceCount=\"[0-9]+\"" "%t-2.xml" | sort -g > "%t-res2"
 // RUN: diff "%t-res1" "%t-res2"