Make /randomizeVcIterations:1 the same as normalizeNames:1

[atomb]

This change ensures that, when specifying /randomizeVcIterations:n, the first iteration is equivalent to that achieved by /normalizeNames:1. One consequence of this is that normalized names are always chosen pseudo-randomly (though deterministically, since it always starts with a fixed seed, which is 0 if not otherwise specified). It's slightly unfortunate to spend the computational expense of random generation when not strictly needed, but doing otherwise would require more complex logic.

Fixes dafny-lang/dafny#5126

[keyboardDrummer]

Have you considered always using normalized names if the iteration has 0 for a randomSeed? That way we still use normalized names in the default case, but the first iteration always gets the same SMT, whether you're using --iterations or not.

I think that would require changing this line:

SolverOptions.RandomSeed = 1 < Options.RandomizeVcIterations ? split.NextRandom() : split.RandomSeed;

into just

SolverOptions.RandomSeed = split.RandomSeed;

And then you don't need the other changes in the PR.

The reimplementation of measure-complexity already creates a separate Split with a different split.RandomSeed for each iteration.

You can also clean up Boogie by removing RandomizeVcIterations and Split.NextRandom and Split.randomGen, since Dafny no longer uses them.

[atomb]

Have you considered always using normalized names if the iteration has 0 for a randomSeed? That way we still use normalized names in the default case, but the first iteration always gets the same SMT, whether you're using --iterations or not.

Yeah, I considered doing that, and it was my original goal, but I concluded that the extra complexity in the logic was sufficient that I wasn't sure it was worth it. I haven't conclusively decided that, but it's the direction I'm leaning in.

I think that would require changing this line:

SolverOptions.RandomSeed = 1 < Options.RandomizeVcIterations ? split.NextRandom() : split.RandomSeed;

into just

SolverOptions.RandomSeed = split.RandomSeed;

And then you don't need the other changes in the PR.

I think that's just in the context of Dafny, right? That wouldn't work for Boogie running on its own, I don't think.

The reimplementation of measure-complexity already creates a separate Split with a different split.RandomSeed for each iteration.

You can also clean up Boogie by removing RandomizeVcIterations and Split.NextRandom and Split.randomGen, since Dafny no longer uses them.

The /randomizeVcIterations flag is useful for Boogie on its own, as well. I'd rather leave it in, so that other users of Boogie can benefit from it.

[keyboardDrummer]

I think we should remove the line DafnyOptions.RegisterLegacyBinding(Iterations, (o, v) => o.RandomizeVcIterations = (int)v); from Dafny. It's no longer needed because Dafny does not call the code that uses RandomizeVcIterations to start an iteration, and when this option is not set, SolverOptions.RandomSeed = 1 < Options.RandomizeVcIterations ? split.NextRandom() : split.RandomSeed; will behave as split.RandomSeed

The /randomizeVcIterations flag is useful for Boogie on its own, as well. I'd rather leave it in, so that other users of Boogie can benefit from it.

We can leave it in, but I'm not comfortable with the implementation, for one because it reuses Splits for different iterations. With 0 users, how sure are you that this works well? Even Dafny has migrated off of this to get more reliable behavior.

[atomb]

I think we should remove the line DafnyOptions.RegisterLegacyBinding(Iterations, (o, v) => o.RandomizeVcIterations = (int)v); from Dafny. It's no longer needed because Dafny does not call the code that uses RandomizeVcIterations to start an iteration, and when this option is not set, SolverOptions.RandomSeed = 1 < Options.RandomizeVcIterations ? split.NextRandom() : split.RandomSeed; will behave as split.RandomSeed

Sure, that seems reasonable. And the fact that Dafny now controls the process of measure-complexity suggests that maybe it's better to fix dafny-lang/dafny#5126 in Dafny rather than Boogie. I hadn't realized before now that the logic for doing random iterations in measure-complexity had moved into Dafny.

So I'm going to close this PR, and perhaps create a simpler one that focuses on the Dafny issue. I'm not sure whether any Boogie users care about the difference that issue describes.