From 461d6b17aed0bd81adc86d4ce2148c0f1d790bbc Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 29 Oct 2015 16:08:48 -0700
Subject: Fix issue 91 - Change how we compute the bounds of quantified
 variables so that it does not depend on the order they appeared.

---
 Source/Dafny/Resolver.cs | 42 +++++++++++++++++++++++++++++++-----------
 1 file changed, 31 insertions(+), 11 deletions(-)

(limited to 'Source')

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 74ff60e7..21476ede 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -9715,8 +9715,28 @@ namespace Microsoft.Dafny
         var c = GetImpliedTypeConstraint(bv, bv.Type, null);
         expr = polarity ? Expression.CreateAnd(c, expr) : Expression.CreateImplies(c, expr);
       }
-      var all = DiscoverAllBounds_Aux_MultipleVars(bvars, expr, polarity);
-      var bests = all.ConvertAll(tup => ComprehensionExpr.BoundedPool.GetBest(tup.Item2, onlyFiniteBounds));
+      List<ComprehensionExpr.BoundedPool> knownBounds = null;
+      var orgCount = bvars.Count;
+      var bests = new List<ComprehensionExpr.BoundedPool>();
+      bool changed = true;
+      // compute the bounds of the BV until no new information is obtained.
+      while (changed) {
+        changed = false;
+        var all = DiscoverAllBounds_Aux_MultipleVars(bvars, expr, polarity, knownBounds);
+        bests = all.ConvertAll(tup => ComprehensionExpr.BoundedPool.GetBest(tup.Item2, onlyFiniteBounds));
+        // check to see if we found new bounds in this iteration
+        int count = 0;
+        for (int i = 0; i < bests.Count; i++) {
+          if (bests[i] == null) {
+            count++;
+          }
+        }
+        if (count >0 && count != orgCount) {
+          changed = true;
+          knownBounds = bests;
+          orgCount = count;
+        }
+      }
       missingBounds = new List<VT>();
       for (var i = 0; i < bvars.Count; i++) {
         if (bests[i] == null) {
@@ -9728,24 +9748,24 @@ namespace Microsoft.Dafny
 
     public static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_SingleVar<VT>(VT v, Expression expr) where VT : IVariable {
       expr = Expression.CreateAnd(GetImpliedTypeConstraint(v, v.Type, null), expr);
-      return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true);
+      return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true, null);
     }
 
-    private static List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>> DiscoverAllBounds_Aux_MultipleVars<VT>(List<VT> bvars, Expression expr, bool polarity) where VT : IVariable {
+    private static List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>> DiscoverAllBounds_Aux_MultipleVars<VT>(List<VT> bvars, Expression expr, bool polarity, List<ComprehensionExpr.BoundedPool> knownBounds) where VT : IVariable {
       Contract.Requires(bvars != null);
       Contract.Requires(expr != null);
       var bb = new List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>();
       for (var j = 0; j < bvars.Count; j++) {
-        var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity);
+        var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity, knownBounds);
         bb.Add(new Tuple<VT, List<ComprehensionExpr.BoundedPool>>(bvars[j], bounds));
       }
       return bb;
     }
 
     /// <summary>
-    /// Returns a list of (possibly partial) bounds for "bvars[j]", each of which can be written without mentioning any variable in "bvars[j..]".
+    /// Returns a list of (possibly partial) bounds for "bvars[j]", each of which can be written without mentioning any variable in "bvars[j..]" that is not bounded.
     /// </summary>
-    private static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_Aux_SingleVar<VT>(List<VT> bvars, int j, Expression expr, bool polarity) where VT : IVariable {
+    private static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_Aux_SingleVar<VT>(List<VT> bvars, int j, Expression expr, bool polarity, List<ComprehensionExpr.BoundedPool> knownBounds) where VT : IVariable {
       Contract.Requires(bvars != null);
       Contract.Requires(0 <= j && j < bvars.Count);
       Contract.Requires(expr != null);
@@ -9774,7 +9794,7 @@ namespace Microsoft.Dafny
         }
         var e0 = c.E0;
         var e1 = c.E1;
-        int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, ref e0, ref e1);
+        int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, knownBounds, ref e0, ref e1);
         if (whereIsBv < 0) {
           continue;
         }
@@ -9870,7 +9890,7 @@ namespace Microsoft.Dafny
     /// The other of "e0" and "e1" is an expression whose free variables are not among "boundVars[bvi..]".
     /// Ensures that the resulting "e0" and "e1" are not ConcreteSyntaxExpression's.
     /// </summary>
-    static int SanitizeForBoundDiscovery<VT>(List<VT> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) where VT : IVariable {
+    static int SanitizeForBoundDiscovery<VT>(List<VT> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, List<ComprehensionExpr.BoundedPool> knownBounds, ref Expression e0, ref Expression e1) where VT : IVariable {
       Contract.Requires(e0 != null);
       Contract.Requires(e1 != null);
       Contract.Requires(boundVars != null);
@@ -9965,10 +9985,10 @@ namespace Microsoft.Dafny
       }
 
       // Finally, check that the other side does not contain "bv" or any of the bound variables
-      // listed after "bv" in the quantifier.
+      // listed after "bv" in the quantifier that is not bounded.
       var fv = FreeVariables(thatSide);
       for (int i = bvi; i < boundVars.Count; i++) {
-        if (fv.Contains(boundVars[i])) {
+        if (fv.Contains(boundVars[i]) && (knownBounds == null || knownBounds[i] == null)) {
           return -1;
         }
       }
-- 
cgit v1.2.3