summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-20 10:01:50 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-20 10:01:50 -0700
commite3fff39c37ed68cf718eab84613e3bbb02858653 (patch)
tree58c83ba887ea13c7c64336fecd9a6b120650de0b
parent6e935875b5cfbdee8a7f6573f9f01c48db746d56 (diff)
Allow users to disable quantifier splitting by with a {:split false} attribute
-rw-r--r--Source/Dafny/Triggers/QuantifierSplitter.cs10
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;
+ }
}
}
}