Add --solver-option flag and move others around #3943

atomb · 2023-05-02T23:12:06Z

Adds a --solver-option flag to correspond to the old (Boogie) /proverOpt flag. In the process, this also refactors a few things:

Rearranges some of the option code to move some Boogie-related options from CommonOptionBag to BoogieOptionBag.
Makes --solver-option, --solver-path, --solver-plugin, --solver-log, and --resource-limit available to the generate-tests and find-dead-code commands.

Includes some refactoring to DafnyTestGenerator, thanks to @Dargones, to make it easier to support arbitrary options there.

Addresses #3468 but doesn't entirely resolve it.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Dargones · 2023-05-04T20:24:50Z

Thank you, @atomb! I have made a PR to this PR's branch that should make --solver-option, --solver-path, --solver-log, and --resource-limit work with test generation (I also did some refactoring that should hopefully make addition of new options easier in the future).

Re: --boogie and --solver-plugin options - would you have any pointer on how to copy these from one DafnyOptions instance to another?

atomb · 2023-05-04T21:25:17Z

Thank you, @atomb! I have made a PR to this PR's branch that should make --solver-option, --solver-path, --solver-log, and --resource-limit work with test generation (I also did some refactoring that should hopefully make addition of new options easier in the future).

Thanks!

Re: --boogie and --solver-plugin options - would you have any pointer on how to copy these from one DafnyOptions instance to another?

I think, for --solver-plugin, it should be sufficient to copy the ProverDllName and TheProverFactory fields. I think it should be safe for multiple threads to share a reference to the same factory, since we're already doing that when solving multiple goals in parallel during normal Dafny verification.

As for --boogie, it may be more trouble than it's worth. I considered adding that as a catch-all for any Boogie option that I didn't think to add, but I don't specifically know that it's needed.

Make Test Generation work with a custom Z3 version

keyboardDrummer · 2023-05-05T08:16:35Z

Source/DafnyTestGeneration/GenerateTestsCommand.cs

@@ -10,9 +10,16 @@ namespace Microsoft.Dafny;
 public class GenerateTestsCommand : ICommandSpec {
  public IEnumerable<Option> Options =>
    new Option[] {
+      // IMPORTANT: Before adding new options, make sure they are


This seems frail. Why not make the code more robust instead of adding this comment? Why doesn't CopyForProcedure use the DafnyOptions clone constructor?

Merging this one line PR to Boogie would allow using the DafnyOption's clone constructor and indeed make the code more robust.

The problem is that the ProcsToCheck field of DafnyOptions (inherited from Boogie's CommadLineOptions) does not have a setter. The clone constructor copies the field anyway using reflection but ProcsToCheck is a list, so the constructor copies the reference and one cannot modify the 'copied' list without modifying the original. The best solution would be to add a setter, like I do in the PR to Boogie above.

keyboardDrummer · 2023-05-05T08:18:47Z

Source/DafnyTestGeneration/DeadCodeCommand.cs

@@ -8,9 +8,15 @@ namespace Microsoft.Dafny;
 public class DeadCodeCommand : ICommandSpec {
  public IEnumerable<Option> Options =>
    new Option[] {
+      // IMPORTANT: Before adding new options, make sure they are


This seems frail. Why not make the code more robust instead of adding this comment? Why doesn't CopyForProcedure use the DafnyOptions clone constructor?

keyboardDrummer · 2023-05-05T08:18:56Z

Source/DafnyTestGeneration/DeadCodeCommand.cs

@@ -21,6 +27,8 @@ public class DeadCodeCommand : ICommandSpec {
  }

  public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
+    // IMPORTANT: Before adding new default options, make sure they are


This seems frail. Why not make the code more robust instead of adding this comment? Why doesn't CopyForProcedure use the DafnyOptions clone constructor?

keyboardDrummer · 2023-05-05T08:22:04Z

Source/DafnyCore/Options/BoogieOptionBag.cs

+    "Can be used to specify a custom SMT solver to use for verifying Dafny proofs.") {
+  };
+  public static readonly Option<IList<string>> SolverOption = new("--solver-option",
+    "Specify an option to control how the solver works.") {


This line doesn't tell me how to use this. Could you mention that these arguments are passed directly to the solver CLI; that the default solver is Z3 with a link to its CLI documentation; and that Dafny is already configuring some options, so not all of options might be usable.

I added a --solver-option-help flag that describes what all the options are, and expanded the help text for --solver-option.

keyboardDrummer · 2023-05-05T08:41:40Z

Source/DafnyCore/Options/BoogieOptionBag.cs

+
+  public static readonly Option<bool> IsolateAssertions = new("--isolate-assertions", @"Verify each assertion in isolation.");
+
+  public static readonly Option<FileInfo> SolverPath = new("--solver-path",


I would set SolverPath, SolverOption and SolverPlugin (which I still think should be named BoogiePlugin) to hidden, since using them requires looking up additional documentation outside of Dafny. If there are particular Z3 options that we think users are likely to get a benefit front, I suggest we expose them as first class Dafny options.

Yeah, my goal with #3938 is to expose more control over the verification process in a friendly way. But this allows expert users to get that control immediately, if they know they could benefit from it. And it allows us to conveniently experiment with various options to help decide which might be worth exposing in a nicer way.

I agree that SolverOption should be hidden, and I've made it that way. I'm less convinced about the two Path options, which I think will be used more frequently.

As far as the name of SolverPlugin, Boogie plugins can only control how it interfaces with the solver. It doesn't provide any mechanism for them to do anything else. So I still prefer --solver-plugin.

The line breaks in the previous version were preserved in the output, leading to awkwardly-displayed text.

This explains the valid arguments to `--solver-option`.

Add --solver-option flag and move others around

10d9aee

atomb mentioned this pull request May 2, 2023

Add --verbosity and --solver-opt flags #3625

Closed

Allow --boogie with generate-tests and find-dead-code

1da3ebb

atomb marked this pull request as ready for review May 2, 2023 23:33

atomb requested review from davidcok, keyboardDrummer and alex-chew May 2, 2023 23:33

Make sure options are copied in ProgramModification

0db7ca2

atomb marked this pull request as draft May 3, 2023 17:46

Dargones added 7 commits May 4, 2023 14:44

Fix prover lookup

c78a52f

remove redundant import

06ee8e4

Move copy method to GenerateTestsCommand to make future changes easier

70a4790

Remove unused imports

4f2c5cc

add clarification nnote

da78f30

Remove an unused option

d423d1c

Fix typos

43a40e5

atomb added 4 commits May 4, 2023 14:29

Merge pull request #3 from Dargones/merge-to-fork

309d694

Make Test Generation work with a custom Z3 version

Fix test

daf39f9

Merge remote-tracking branch 'upstream/master' into more-solver-options

bfdbca2

Add --solver-plugin back in

e79acb4

atomb marked this pull request as ready for review May 4, 2023 23:08

keyboardDrummer reviewed May 5, 2023

View reviewed changes

atomb added 2 commits May 5, 2023 08:49

Reformat help for --solver-resource-limit

5d4cde6

The line breaks in the previous version were preserved in the output, leading to awkwardly-displayed text.

Add a --solver-option-help option

c7128a9

This explains the valid arguments to `--solver-option`.

keyboardDrummer approved these changes May 8, 2023

View reviewed changes

Merge branch 'master' into more-solver-options

588db98

keyboardDrummer enabled auto-merge (squash) May 8, 2023 08:55

atomb added 3 commits May 8, 2023 12:35

Merge branch 'master' into more-solver-options

def37e6

Merge branch 'master' into more-solver-options

259a21b

Merge branch 'master' into more-solver-options

6369c89

keyboardDrummer merged commit e48820a into dafny-lang:master May 8, 2023

atomb self-assigned this Aug 28, 2023

atomb deleted the more-solver-options branch January 4, 2024 17:07

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add --solver-option flag and move others around #3943

Add --solver-option flag and move others around #3943

atomb commented May 2, 2023 •

edited

Loading

Dargones commented May 4, 2023 •

edited

Loading

atomb commented May 4, 2023

keyboardDrummer May 5, 2023 •

edited

Loading

Dargones May 5, 2023 •

edited

Loading

keyboardDrummer May 5, 2023

keyboardDrummer May 5, 2023

keyboardDrummer May 5, 2023

atomb May 5, 2023

keyboardDrummer May 8, 2023

keyboardDrummer May 5, 2023

atomb May 5, 2023

keyboardDrummer May 8, 2023


		public static readonly Option<bool> IsolateAssertions = new("--isolate-assertions", @"Verify each assertion in isolation.");

		public static readonly Option<FileInfo> SolverPath = new("--solver-path",

Add --solver-option flag and move others around #3943

Add --solver-option flag and move others around #3943

Conversation

atomb commented May 2, 2023 • edited Loading

Dargones commented May 4, 2023 • edited Loading

atomb commented May 4, 2023

keyboardDrummer May 5, 2023 • edited Loading

Choose a reason for hiding this comment

Dargones May 5, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb commented May 2, 2023 •

edited

Loading

Dargones commented May 4, 2023 •

edited

Loading

keyboardDrummer May 5, 2023 •

edited

Loading

Dargones May 5, 2023 •

edited

Loading