diff options
| author |  wuestholz <unknown> | 2015-10-26 17:36:25 -0500 |
|---|---|---|
| committer | wuestholz <unknown> | 2015-10-26 17:36:25 -0500 |
| commit | 5e4bcf8e63a3351dc3f0f9bc6cbff8176adddd8b (patch) | |
| tree | b68f21a15903606993f46a12e83343e9eae9c0e5 /Source/DafnyExtension | |
| parent | b35216f55d22123ae4c35eacf28e99a2b6dbbfaf (diff) | |
DafnyExtension: Add menu item for automatic induction (mainly developed by Rustan).
Diffstat (limited to 'Source/DafnyExtension')
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 7 | ||||
| -rw-r--r-- | Source/DafnyExtension/MenuProxy.cs | 8 |
2 files changed, 15 insertions, 0 deletions
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index 2ad05e85..27471d56 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -251,6 +251,13 @@ namespace DafnyLanguage return Dafny.DafnyOptions.Clo.VerifySnapshots;
}
+ public static bool ChangeAutomaticInduction() {
+ var old = Dafny.DafnyOptions.O.Induction;
+ // toggle between modes 1 and 3
+ Dafny.DafnyOptions.O.Induction = old == 1 ? 3 : 1;
+ return Dafny.DafnyOptions.O.Induction == 3;
+ }
+
public static bool Verify(Dafny.Program dafnyProgram, ResolverTagger resolver, string uniqueIdPrefix, string requestId, ErrorReporterDelegate er) {
Dafny.Translator translator = new Dafny.Translator(dafnyProgram.reporter);
translator.InsertChecksums = true;
diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs index 9ddc8344..0e061cd3 100644 --- a/Source/DafnyExtension/MenuProxy.cs +++ b/Source/DafnyExtension/MenuProxy.cs @@ -33,6 +33,14 @@ namespace DafnyLanguage && 0 < DafnyDriver.IncrementalVerificationMode();
}
+ public bool ToggleAutomaticInduction(IWpfTextView activeTextView) {
+ return DafnyDriver.ChangeAutomaticInduction();
+ }
+
+ public bool AutomaticInductionCommandEnabled(IWpfTextView activeTextView) {
+ return activeTextView != null;
+ }
+
public bool StopVerifierCommandEnabled(IWpfTextView activeTextView)
{
DafnyLanguage.ProgressTagger tagger;
|