Start committing split quantifiers

This requires rewriting the parts of the AST that contain these quantifiers. We
unfortunately don't have facilities to do such rewrites at the moment (and there
are loops in the AST, so it would be hard to write such a facility). As a
workaround, this commit introduces a field in quantifier expressions,
SplitQuantifiers. Code that manipulate triggers is expected to look for this
field, and ignore the other fields if that one is found.

1 files changed, 17 insertions, 9 deletions

diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index 33be0da2..80381f0a 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -21,30 +21,37 @@ namespace Microsoft.Dafny.Triggers {
     // Unfortunately, this would cause ill-behaved quantifiers to produce

     // exponentially many smaller quantifiers.

 

+    private static UnaryOpExpr Not(Expression expr) {

+      var not = new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type };

+      return not;

+    }

+

     internal static IEnumerable<Expression> SplitExpr(Expression expr, BinaryExpr.Opcode separator) {

       expr = expr.Resolved;

       var unary = expr as UnaryOpExpr;

       var binary = expr as BinaryExpr;

 

       if (unary != null && unary.Op == UnaryOpExpr.Opcode.Not) {

-        foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, e); }

+        foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return Not(e); }

       } else if (binary != null && binary.Op == separator) {

         foreach (var e in SplitExpr(binary.E0, separator)) { yield return e; }

         foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; }

       } else if (binary != null && binary.Op == BinaryExpr.Opcode.Imp && separator == BinaryExpr.Opcode.Or) {

-        foreach (var e in SplitExpr(new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, binary.E0), separator)) { yield return e; }

+        foreach (var e in SplitExpr(Not(binary.E0), separator)) { yield return e; }

         foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; }

+      } else {

+        yield return expr;

       }

     }

 

     internal static IEnumerable<Expression> SplitAndStich(BinaryExpr pair, BinaryExpr.Opcode separator) {

-      foreach (var e1 in SplitExpr(pair.E1, separator)) { 

-        yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1);

+      foreach (var e1 in SplitExpr(pair.E1, separator)) {

+        yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1) { ResolvedOp = pair.ResolvedOp, Type = pair.Type };

       }

     }

 

     internal static IEnumerable<Expression> SplitQuantifier(QuantifierExpr quantifier) {

-      var body = quantifier.LogicalBody();

+      var body = quantifier.Term;

       var binary = body as BinaryExpr;

 

       if (quantifier is ForallExpr) {

@@ -55,7 +62,7 @@ namespace Microsoft.Dafny.Triggers {
           stream = SplitExpr(body, BinaryExpr.Opcode.And);

         }

         foreach (var e in stream) {

-          yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes);

+          yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type };

         }

       } else if (quantifier is ExistsExpr) {

         IEnumerable<Expression> stream;

@@ -65,17 +72,18 @@ namespace Microsoft.Dafny.Triggers {
           stream = SplitExpr(body, BinaryExpr.Opcode.Or);

         }

         foreach (var e in stream) {

-          yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes);

+          yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type };

         }

       } else {

         yield return quantifier;

       }

     }

         

-    protected override void VisitOneExpr(Expression expr) { //FIXME: This doesn't save the rewritten quantifier

+    protected override void VisitOneExpr(Expression expr) {

       var quantifier = expr as QuantifierExpr;

       if (quantifier != null) {

-        var rew = SplitQuantifier(quantifier);

+        var split = SplitQuantifier(quantifier).ToList();

+        quantifier.SplitQuantifier = split;

         //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| "));

       }

     }