diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 10:01:50 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 10:01:50 -0700 |
| commit | e3fff39c37ed68cf718eab84613e3bbb02858653 (patch) | |
| tree | 58c83ba887ea13c7c64336fecd9a6b120650de0b | |
| parent | 6e935875b5cfbdee8a7f6573f9f01c48db746d56 (diff) | |
Allow users to disable quantifier splitting by with a {:split false} attribute
| -rw-r--r-- | Source/Dafny/Triggers/QuantifierSplitter.cs | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index 4b223856..c50bc9c6 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -85,10 +85,12 @@ namespace Microsoft.Dafny.Triggers { protected override void VisitOneExpr(Expression expr) {
var quantifier = expr as QuantifierExpr;
- if (quantifier != null) {
- var split = SplitQuantifier(quantifier).ToList();
- quantifier.SplitQuantifier = split;
- //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| "));
+ if (quantifier != null && quantifier.SplitQuantifier == null) {
+ bool splitAttr = true;
+ if (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) {
+ var split = SplitQuantifier(quantifier).ToList();
+ quantifier.SplitQuantifier = split;
+ }
}
}
}
|