diff options
Diffstat (limited to 'Source/Dafny/DafnyOptions.cs')
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 27 |
1 files changed, 20 insertions, 7 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 59d0eb2c..2d8756d2 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -65,11 +65,12 @@ namespace Microsoft.Dafny public bool AllowGlobals = false; public bool CountVerificationErrors = true; public bool Optimize = false; - public bool AutoTriggers = false; + public bool AutoTriggers = false;
+ public bool RewriteFocalPredicates = false;
public bool PrintTooltips = false; public bool PrintStats = false; public bool PrintFunctionCallGraph = false; - public bool WarnShadowing = false; + public bool WarnShadowing = false;
public bool IronDafny = #if ENABLE_IRONDAFNY true @@ -216,12 +217,20 @@ namespace Microsoft.Dafny case "printTooltips": PrintTooltips = true; - return true; + return true;
+
+ case "autoTriggers": {
+ int autoTriggers = 0;
+ if (ps.GetNumericArgument(ref autoTriggers, 2)) {
+ AutoTriggers = autoTriggers == 1;
+ }
+ return true;
+ } - case "autoTriggers": { - int autoTriggers = 0; - if (ps.GetNumericArgument(ref autoTriggers, 2)) { - AutoTriggers = autoTriggers == 1; + case "rewriteFocalPredicates": {
+ int rewriteFocalPredicates = 0;
+ if (ps.GetNumericArgument(ref rewriteFocalPredicates, 2)) {
+ RewriteFocalPredicates = rewriteFocalPredicates == 1; } return true; } @@ -369,6 +378,10 @@ namespace Microsoft.Dafny 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. 1 - Add a {:trigger} to each user-level quantifier. Existing annotations are preserved. + /rewriteFocalPredicates:<n> + 0 (default) - Don't rewrite predicates in the body of prefix lemmas. + 1 - In the body of prefix lemmas, rewrite any use of a focal predicate + P to P#[_k-1]. /optimize Produce optimized C# code, meaning: - selects optimized C# prelude by passing /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires |