Merge

6 files changed, 264 insertions, 86 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 57623068..18721cf3 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1160,11 +1160,11 @@ namespace Microsoft.Dafny {
           var ind = indent + i * IndentAmount;

           var bound = s.Bounds[i];

           var bv = s.BoundVars[i];

-          if (bound is QuantifierExpr.BoolBoundedPool) {

+          if (bound is ComprehensionExpr.BoolBoundedPool) {

             Indent(ind);

             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);

-          } else if (bound is QuantifierExpr.IntBoundedPool) {

-            var b = (QuantifierExpr.IntBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.IntBoundedPool) {

+            var b = (ComprehensionExpr.IntBoundedPool)bound;

             SpillLetVariableDecls(b.LowerBound, ind);

             SpillLetVariableDecls(b.UpperBound, ind);

             Indent(ind);

@@ -1173,22 +1173,22 @@ namespace Microsoft.Dafny {
             wr.Write("; @{0} < ", bv.CompileName);

             TrExpr(b.UpperBound);

             wr.Write("; @{0}++) {{ ", bv.CompileName);

-          } else if (bound is QuantifierExpr.SetBoundedPool) {

-            var b = (QuantifierExpr.SetBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SetBoundedPool) {

+            var b = (ComprehensionExpr.SetBoundedPool)bound;

             SpillLetVariableDecls(b.Set, ind);

             Indent(ind);

             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Set);

             wr.Write(").Elements) { ");

-          } else if (bound is QuantifierExpr.SeqBoundedPool) {

-            var b = (QuantifierExpr.SeqBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SeqBoundedPool) {

+            var b = (ComprehensionExpr.SeqBoundedPool)bound;

             SpillLetVariableDecls(b.Seq, ind);

             Indent(ind);

             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Seq);

             wr.Write(").UniqueElements) { ");

-          } else if (bound is QuantifierExpr.DatatypeBoundedPool) {

-            var b = (QuantifierExpr.DatatypeBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

+            var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

             wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));

           } else {

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

@@ -2053,32 +2053,32 @@ namespace Microsoft.Dafny {
           var bound = e.Bounds[i];

           var bv = e.BoundVars[i];

           // emit:  Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)

-          if (bound is QuantifierExpr.BoolBoundedPool) {

+          if (bound is ComprehensionExpr.BoolBoundedPool) {

             wr.Write("Dafny.Helpers.QuantBool(");

-          } else if (bound is QuantifierExpr.IntBoundedPool) {

-            var b = (QuantifierExpr.IntBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.IntBoundedPool) {

+            var b = (ComprehensionExpr.IntBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantInt(");

             TrExpr(b.LowerBound);

             wr.Write(", ");

             TrExpr(b.UpperBound);

             wr.Write(", ");

-          } else if (bound is QuantifierExpr.SetBoundedPool) {

-            var b = (QuantifierExpr.SetBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SetBoundedPool) {

+            var b = (ComprehensionExpr.SetBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantSet(");

             TrExpr(b.Set);

             wr.Write(", ");

-          } else if (bound is QuantifierExpr.MapBoundedPool) {

-            var b = (QuantifierExpr.MapBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.MapBoundedPool) {

+            var b = (ComprehensionExpr.MapBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantMap(");

             TrExpr(b.Map);

             wr.Write(", ");

-          } else if (bound is QuantifierExpr.SeqBoundedPool) {

-            var b = (QuantifierExpr.SeqBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SeqBoundedPool) {

+            var b = (ComprehensionExpr.SeqBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantSeq(");

             TrExpr(b.Seq);

             wr.Write(", ");

-          } else if (bound is QuantifierExpr.DatatypeBoundedPool) {

-            var b = (QuantifierExpr.DatatypeBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

+            var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantDatatype(");

 

             wr.Write("{0}.AllSingletonConstructors, ", DtName(b.Decl));

@@ -2120,32 +2120,32 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < n; i++) {

           var bound = e.Bounds[i];

           var bv = e.BoundVars[i];

-          if (bound is QuantifierExpr.BoolBoundedPool) {

+          if (bound is ComprehensionExpr.BoolBoundedPool) {

             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);

-          } else if (bound is QuantifierExpr.IntBoundedPool) {

-            var b = (QuantifierExpr.IntBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.IntBoundedPool) {

+            var b = (ComprehensionExpr.IntBoundedPool)bound;

             wr.Write("for (var @{0} = ", bv.CompileName);

             TrExpr(b.LowerBound);

             wr.Write("; @{0} < ", bv.CompileName);

             TrExpr(b.UpperBound);

             wr.Write("; @{0}++) {{ ", bv.CompileName);

-          } else if (bound is QuantifierExpr.SetBoundedPool) {

-            var b = (QuantifierExpr.SetBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SetBoundedPool) {

+            var b = (ComprehensionExpr.SetBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Set);

             wr.Write(").Elements) { ");

-          } else if (bound is QuantifierExpr.MapBoundedPool) {

-            var b = (QuantifierExpr.MapBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.MapBoundedPool) {

+            var b = (ComprehensionExpr.MapBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Map);

             wr.Write(").Domain) { ");

-          } else if (bound is QuantifierExpr.SeqBoundedPool) {

-            var b = (QuantifierExpr.SeqBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SeqBoundedPool) {

+            var b = (ComprehensionExpr.SeqBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Seq);

             wr.Write(").Elements) { ");

-          } else if (bound is QuantifierExpr.DatatypeBoundedPool) {

-            var b = (QuantifierExpr.DatatypeBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

+            var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

             wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));

           } else {

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

@@ -2189,27 +2189,27 @@ namespace Microsoft.Dafny {
         Contract.Assert(e.Bounds.Count == n && n == 1);

         var bound = e.Bounds[0];

         var bv = e.BoundVars[0];

-        if (bound is QuantifierExpr.BoolBoundedPool) {

+        if (bound is ComprehensionExpr.BoolBoundedPool) {

           wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);

-        } else if (bound is QuantifierExpr.IntBoundedPool) {

-          var b = (QuantifierExpr.IntBoundedPool)bound;

+        } else if (bound is ComprehensionExpr.IntBoundedPool) {

+          var b = (ComprehensionExpr.IntBoundedPool)bound;

           wr.Write("for (var @{0} = ", bv.CompileName);

           TrExpr(b.LowerBound);

           wr.Write("; @{0} < ", bv.CompileName);

           TrExpr(b.UpperBound);

           wr.Write("; @{0}++) {{ ", bv.CompileName);

-        } else if (bound is QuantifierExpr.SetBoundedPool) {

-          var b = (QuantifierExpr.SetBoundedPool)bound;

+        } else if (bound is ComprehensionExpr.SetBoundedPool) {

+          var b = (ComprehensionExpr.SetBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

           TrExpr(b.Set);

           wr.Write(").Elements) { ");

-        } else if (bound is QuantifierExpr.MapBoundedPool) {

-          var b = (QuantifierExpr.MapBoundedPool)bound;

+        } else if (bound is ComprehensionExpr.MapBoundedPool) {

+          var b = (ComprehensionExpr.MapBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

           TrExpr(b.Map);

           wr.Write(").Domain) { ");

-        } else if (bound is QuantifierExpr.SeqBoundedPool) {

-          var b = (QuantifierExpr.SeqBoundedPool)bound;

+        } else if (bound is ComprehensionExpr.SeqBoundedPool) {

+          var b = (ComprehensionExpr.SeqBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

           TrExpr(b.Seq);

           wr.Write(").Elements) { ");

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index ebf01c4c..d8d95079 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -17,6 +17,7 @@ COMPILER Dafny
 static ModuleDecl theModule;

 static BuiltIns theBuiltIns;

 static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);

+static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null);

 static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);

 static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);

 static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");

@@ -849,12 +850,13 @@ UpdateStmt<out Statement/*!*/ s>
   .)

   .

 Rhs<out AssignmentRhs r, Expression receiverForInitCall>

-= (. IToken/*!*/ x, newToken;  Expression/*!*/ e;

+= (. Contract.Ensures(Contract.ValueAtReturn<AssignmentRhs>(out r) != null);

+     IToken/*!*/ x, newToken;  Expression/*!*/ e;

      List<Expression> ee = null;

      Type ty = null;

      CallStmt initCall = null;

      List<Expression> args;

-     r = null;  // to please compiler

+     r = dummyRhs;  // to please compiler

      Attributes attrs = null;

   .)

   ( "new"                              (. newToken = t; .)

@@ -899,7 +901,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
   | "*"                                (. r = new HavocRhs(t); .)

   | Expression<out e>                  (. r = new ExprRhs(e); .)

   )

-  { Attribute<ref attrs> }             (. if (r != null) r.Attributes = attrs; .)

+  { Attribute<ref attrs> }             (. r.Attributes = attrs; .)

   .

 VarDeclStatement<.out Statement/*!*/ s.>

 = (. IToken x = null, assignTok = null;  bool isGhost = false;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 98319473..1c43a530 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3490,6 +3490,11 @@ namespace Microsoft.Dafny {
       public readonly Expression Set;

       public SetBoundedPool(Expression set) { Set = set; }

     }

+    public class SuperSetBoundedPool : BoundedPool

+    {

+      public readonly Expression LowerBound;

+      public SuperSetBoundedPool(Expression set) { LowerBound = set; }

+    }

     public class MapBoundedPool : BoundedPool

     {

       public readonly Expression Map;

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d01fe161..a81b256e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -37,6 +37,7 @@ public class Parser {
 static ModuleDecl theModule;

 static BuiltIns theBuiltIns;

 static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);

+static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null);

 static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);

 static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);

 static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");

@@ -1638,12 +1639,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void Rhs(out AssignmentRhs r, Expression receiverForInitCall) {

+		Contract.Ensures(Contract.ValueAtReturn<AssignmentRhs>(out r) != null);

 		IToken/*!*/ x, newToken;  Expression/*!*/ e;

 		List<Expression> ee = null;

 		Type ty = null;

 		CallStmt initCall = null;

 		List<Expression> args;

-		r = null;  // to please compiler

+		r = dummyRhs;  // to please compiler

 		Attributes attrs = null;

 		

 		if (la.kind == 61) {

@@ -1712,7 +1714,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

-		if (r != null) r.Attributes = attrs; 

+		r.Attributes = attrs; 

 	}

 

 	void Lhs(out Expression e) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 17f35b1e..6534d2ba 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2870,7 +2870,7 @@ namespace Microsoft.Dafny
         bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == ErrorCount && UsesSpecFeatures(s.Range));

         if (!bodyMustBeSpecOnly && prevErrorCount == ErrorCount) {

           var missingBounds = new List<BoundVar>();

-          s.Bounds = DiscoverBounds(s.Tok, s.BoundVars, s.Range, true, missingBounds);

+          s.Bounds = DiscoverBounds(s.Tok, s.BoundVars, s.Range, true, false, missingBounds);

           if (missingBounds.Count != 0) {

             bodyMustBeSpecOnly = true;

           }

@@ -4198,7 +4198,7 @@ namespace Microsoft.Dafny
 

         if (prevErrorCount == ErrorCount) {

           var missingBounds = new List<BoundVar>();

-          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, missingBounds);

+          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, false, missingBounds);

           if (missingBounds.Count != 0) {

             // Report errors here about quantifications that depend on the allocation state.

             var mb = missingBounds;

@@ -4242,7 +4242,7 @@ namespace Microsoft.Dafny
 

         if (prevErrorCount == ErrorCount) {

           var missingBounds = new List<BoundVar>();

-          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, missingBounds);

+          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);

           if (missingBounds.Count != 0) {

             e.MissingBounds = missingBounds;

             foreach (var bv in e.MissingBounds) {

@@ -4278,7 +4278,7 @@ namespace Microsoft.Dafny
 

         if (prevErrorCount == ErrorCount) {

           var missingBounds = new List<BoundVar>();

-          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, missingBounds);

+          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);

           if (missingBounds.Count != 0) {

             e.MissingBounds = missingBounds;

             foreach (var bv in e.MissingBounds) {

@@ -4990,34 +4990,52 @@ namespace Microsoft.Dafny
     /// <summary>

     /// Tries to find a bounded pool for each of the bound variables "bvars" of "expr".  If this process

     /// fails, then "null" is returned and the bound variables for which the process fails are added to "missingBounds".

+    /// If "returnAllBounds" is false, then:

+    ///   -- at most one BoundedPool per variable is returned

+    ///   -- every IntBoundedPool returned has both a lower and an upper bound

+    ///   -- no SuperSetBoundedPool is returned

+    /// If "returnAllBounds" is true, then:

+    ///   -- a variable may give rise to BoundedPool's

+    ///   -- IntBoundedPool bounds may have just one component

+    ///   -- a non-null return value means that some bound were found for each variable (but, for example, perhaps one

+    ///      variable only has lower bounds, no upper bounds)

     /// Requires "expr" to be successfully resolved.

     /// </summary>

-    List<QuantifierExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, List<BoundVar> missingBounds) {

+    public static List<ComprehensionExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, bool returnAllBounds, List<BoundVar> missingBounds) {

       Contract.Requires(tok != null);

       Contract.Requires(bvars != null);

       Contract.Requires(missingBounds != null);

       Contract.Requires(expr != null);

       Contract.Requires(expr.Type != null);  // a sanity check (but not a complete proof) that "expr" has been resolved

       Contract.Ensures(

-        (Contract.Result<List<QuantifierExpr.BoundedPool>>() != null &&

-         Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == bvars.Count &&

+        (returnAllBounds && Contract.OldValue(missingBounds.Count) <= missingBounds.Count) ||

+        (!returnAllBounds &&

+         Contract.Result<List<ComprehensionExpr.BoundedPool>>() != null &&

+         Contract.Result<List<ComprehensionExpr.BoundedPool>>().Count == bvars.Count &&

          Contract.OldValue(missingBounds.Count) == missingBounds.Count) ||

-        (Contract.Result<List<QuantifierExpr.BoundedPool>>() == null &&

+        (!returnAllBounds &&

+         Contract.Result<List<ComprehensionExpr.BoundedPool>>() == null &&

          Contract.OldValue(missingBounds.Count) < missingBounds.Count));

 

-      var bounds = new List<QuantifierExpr.BoundedPool>();

+      var bounds = new List<ComprehensionExpr.BoundedPool>();

       bool foundError = false;

       for (int j = 0; j < bvars.Count; j++) {

         var bv = bvars[j];

         if (bv.Type is BoolType) {

           // easy

-          bounds.Add(new QuantifierExpr.BoolBoundedPool());

+          bounds.Add(new ComprehensionExpr.BoolBoundedPool());

         } else if (bv.Type.IsIndDatatype && (bv.Type.AsIndDatatype).HasFinitePossibleValues) {

-          bounds.Add(new QuantifierExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));

+          bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));

         } else {

           // Go through the conjuncts of the range expression to look for bounds.

           Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;

           Expression upperBound = null;

+          bool foundBoundsForBv = false;

+          if (lowerBound != null) {

+            bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

+            lowerBound = null;

+            foundBoundsForBv = true;

+          }

           foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {

             var c = conjunct as BinaryExpr;

             if (c == null) {

@@ -5032,33 +5050,48 @@ namespace Microsoft.Dafny
             switch (c.ResolvedOp) {

               case BinaryExpr.ResolvedOpcode.InSet:

                 if (whereIsBv == 0) {

-                  bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

-                  goto CHECK_NEXT_BOUND_VARIABLE;

+                  bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

+                  foundBoundsForBv = true;

+                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

+                }

+                break;

+              case BinaryExpr.ResolvedOpcode.Subset:

+                if (returnAllBounds && whereIsBv == 1) {

+                  bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(e0));

+                  foundBoundsForBv = true;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.InMultiSet:

                 if (whereIsBv == 0) {

-                  bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

-                  goto CHECK_NEXT_BOUND_VARIABLE;

+                  bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

+                  foundBoundsForBv = true;

+                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.InSeq:

                 if (whereIsBv == 0) {

-                  bounds.Add(new QuantifierExpr.SeqBoundedPool(e1));

-                  goto CHECK_NEXT_BOUND_VARIABLE;

+                  bounds.Add(new ComprehensionExpr.SeqBoundedPool(e1));

+                  foundBoundsForBv = true;

+                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.InMap:

                 if (whereIsBv == 0) {

-                  bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

-                  goto CHECK_NEXT_BOUND_VARIABLE;

+                  bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

+                  foundBoundsForBv = true;

+                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.EqCommon:

                 if (bv.Type is IntType) {

                   var otherOperand = whereIsBv == 0 ? e1 : e0;

-                  bounds.Add(new QuantifierExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));

-                  goto CHECK_NEXT_BOUND_VARIABLE;

+                  bounds.Add(new ComprehensionExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));

+                  foundBoundsForBv = true;

+                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

+                } else if (returnAllBounds && bv.Type is SetType) {

+                  var otherOperand = whereIsBv == 0 ? e1 : e0;

+                  bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(otherOperand));

+                  foundBoundsForBv = true;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.Gt:

@@ -5081,16 +5114,22 @@ namespace Microsoft.Dafny
               default:

                 break;

             }

-            if (lowerBound != null && upperBound != null) {

+            if ((lowerBound != null && upperBound != null) ||

+                (returnAllBounds && (lowerBound != null || upperBound != null))) {

               // we have found two halves

-              bounds.Add(new QuantifierExpr.IntBoundedPool(lowerBound, upperBound));

-              goto CHECK_NEXT_BOUND_VARIABLE;

+                  bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

+              lowerBound = null;

+              upperBound = null;

+              foundBoundsForBv = true;

+              if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

             }

           CHECK_NEXT_CONJUNCT: ;

           }

-          // we have checked every conjunct in the range expression and still have not discovered good bounds

-          missingBounds.Add(bv);  // record failing bound variable

-          foundError = true;

+          if (!foundBoundsForBv) {

+            // we have checked every conjunct in the range expression and still have not discovered good bounds

+            missingBounds.Add(bv);  // record failing bound variable

+            foundError = true;

+          }

         }

       CHECK_NEXT_BOUND_VARIABLE: ;  // should goto here only if the bound for the current variable has been discovered (otherwise, return with null from this method)

       }

@@ -5105,7 +5144,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>

-    int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) {

+    static int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

       Contract.Requires(boundVars != null);

@@ -5229,7 +5268,7 @@ namespace Microsoft.Dafny
     /// Requires "expr" to be successfully resolved.

     /// Ensures that what is returned is not a ConcreteSyntaxExpression.

     /// </summary>

-    IEnumerable<Expression> NormalizedConjuncts(Expression expr, bool polarity) {

+    static IEnumerable<Expression> NormalizedConjuncts(Expression expr, bool polarity) {

       // We consider 5 cases.  To describe them, define P(e)=Conjuncts(e,true) and N(e)=Conjuncts(e,false).

       //   *  X ==> Y    is treated as a shorthand for !X || Y, and so is described by the remaining cases

       //   *  X && Y     P(_) = P(X),P(Y)    and    N(_) = !(X && Y)

@@ -5332,7 +5371,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    Expression Plus(Expression e, int n) {

+    public static Expression Plus(Expression e, int n) {

       Contract.Requires(0 <= n);

 

       var nn = new LiteralExpr(e.tok, n);

@@ -5343,12 +5382,23 @@ namespace Microsoft.Dafny
       return p;

     }

 

+    public static Expression Minus(Expression e, int n) {

+      Contract.Requires(0 <= n);

+

+      var nn = new LiteralExpr(e.tok, n);

+      nn.Type = Type.Int;

+      var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Sub, e, nn);

+      p.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;

+      p.Type = Type.Int;

+      return p;

+    }

+

     /// <summary>

     /// Returns the set of free variables in "expr".

     /// Requires "expr" to be successfully resolved.

     /// Ensures that the set returned has no aliases.

     /// </summary>

-    ISet<IVariable> FreeVariables(Expression expr) {

+    static ISet<IVariable> FreeVariables(Expression expr) {

       Contract.Requires(expr != null);

       Contract.Ensures(expr.Type != null);

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2e322029..1b8a23ee 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2154,6 +2154,20 @@ namespace Microsoft.Dafny {
       }

     }

 

+    Bpl.Expr BplOr(Bpl.Expr a, Bpl.Expr b) {

+      Contract.Requires(a != null);

+      Contract.Requires(b != null);

+      Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+

+      if (a == Bpl.Expr.False) {

+        return b;

+      } else if (b == Bpl.Expr.False) {

+        return a;

+      } else {

+        return Bpl.Expr.Or(a, b);

+      }

+    }

+

     Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -2161,6 +2175,8 @@ namespace Microsoft.Dafny {
 

       if (a == Bpl.Expr.True || b == Bpl.Expr.True) {

         return b;

+      } else if (a == Bpl.Expr.False) {

+        return Bpl.Expr.True;

       } else {

         return Bpl.Expr.Imp(a, b);

       }

@@ -3791,11 +3807,19 @@ namespace Microsoft.Dafny {
               Contract.Assume(false);  // unexpected case

             }

           }

-          var bvs = new VariableSeq();

-          var typeAntecedent = etran.TrBoundVariables(bvars, bvs);

-          var substE = etran.TrExpr(Substitute(s.Expr, null, substMap));

-          var ex = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, substE));

-          builder.Add(Assert(s.Tok, ex, "cannot establish the existence of LHS values that satisfy the such-that predicate"));

+

+          List<Tuple<List<BoundVar>, Expression>> partialGuesses = GeneratePartialGuesses(bvars, Substitute(s.Expr, null, substMap));

+          Bpl.Expr w = Bpl.Expr.False;

+          foreach (var tup in partialGuesses) {

+            var body = etran.TrExpr(tup.Item2);

+            if (tup.Item1.Count != 0) {

+              var bvs = new VariableSeq();

+              var typeAntecedent = etran.TrBoundVariables(tup.Item1, bvs);

+              body = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, body));

+            }

+            w = BplOr(body, w);

+          }

+          builder.Add(Assert(s.Tok, w, "cannot establish the existence of LHS values that satisfy the such-that predicate"));

         }

         // End by doing the assume

         builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Expr)));

@@ -4025,6 +4049,103 @@ namespace Microsoft.Dafny {
       }

     }

 

+    List<Tuple<List<BoundVar>, Expression>> GeneratePartialGuesses(List<BoundVar> bvars, Expression expression) {

+      if (bvars.Count == 0) {

+        var tup = new Tuple<List<BoundVar>, Expression>(new List<BoundVar>(), expression);

+        return new List<Tuple<List<BoundVar>, Expression>>() { tup };

+      }

+      var result = new List<Tuple<List<BoundVar>, Expression>>();

+      var x = bvars[0];

+      var otherBvars = bvars.GetRange(1, bvars.Count - 1);

+      foreach (var tup in GeneratePartialGuesses(otherBvars, expression)) {

+        // in the special case that x does not even occur in expression, we can just ignore x

+        if (!ContainsFreeVariable(tup.Item2, false, x)) {

+          result.Add(tup);

+          continue;

+        }

+        // one possible result is to quantify over all the variables

+        var vs = new List<BoundVar>() { x };

+        vs.AddRange(tup.Item1);

+        result.Add(new Tuple<List<BoundVar>, Expression>(vs, tup.Item2));

+        // other possibilities involve guessing a value for x

+        foreach (var guess in GuessWitnesses(x, tup.Item2)) {

+          var substMap = new Dictionary<IVariable, Expression>();

+          substMap.Add(x, guess);

+          result.Add(new Tuple<List<BoundVar>, Expression>(tup.Item1, Substitute(tup.Item2, null, substMap)));

+        }

+      }

+      return result;

+    }

+

+    IEnumerable<Expression> GuessWitnesses(BoundVar x, Expression expr) {

+      Contract.Requires(x != null);

+      Contract.Requires(expr != null);

+      var lookForBounds = false;

+      if (x.Type is BoolType) {

+        var lit = new LiteralExpr(x.tok, false);

+        lit.Type = Type.Bool;  // resolve here

+        yield return lit;

+        lit = new LiteralExpr(x.tok, true);

+        lit.Type = Type.Bool;  // resolve here

+        yield return lit;

+      } else if (x.Type.IsRefType) {

+        var lit = new LiteralExpr(x.tok);

+        lit.Type = x.Type;

+        yield return lit;

+      } else if (x.Type.IsIndDatatype) {

+        var dt = x.Type.AsIndDatatype;

+        Expression zero = Zero(x.tok, x.Type);

+        if (zero != null) {

+          yield return zero;

+        }

+      } else if (x.Type is SetType) {

+        var empty = new SetDisplayExpr(x.tok, new List<Expression>());

+        empty.Type = x.Type;

+        yield return empty;

+        lookForBounds = true;

+      } else if (x.Type is MultiSetType) {

+        var empty = new MultiSetDisplayExpr(x.tok, new List<Expression>());

+        empty.Type = x.Type;

+        yield return empty;

+        lookForBounds = true;

+      } else if (x.Type is SeqType) {

+        var empty = new SeqDisplayExpr(x.tok, new List<Expression>());

+        empty.Type = x.Type;

+        yield return empty;

+        lookForBounds = true;

+      } else if (x.Type is IntType) {

+        var lit = new LiteralExpr(x.tok, 0);

+        lit.Type = Type.Int;  // resolve here

+        yield return lit;

+        lookForBounds = true;

+      }

+      if (lookForBounds) {

+        var missingBounds = new List<BoundVar>();

+        var bounds = Resolver.DiscoverBounds(x.tok, new List<BoundVar>() { x }, expr, true, true, missingBounds);

+        if (missingBounds.Count == 0) {

+          foreach (var bound in bounds) {

+            if (bound is ComprehensionExpr.IntBoundedPool) {

+              var bnd = (ComprehensionExpr.IntBoundedPool)bound;

+              if (bnd.LowerBound != null) yield return bnd.LowerBound;

+              if (bnd.UpperBound != null) yield return Resolver.Minus(bnd.UpperBound, 1);

+            } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {

+              var bnd = (ComprehensionExpr.SuperSetBoundedPool)bound;

+              yield return bnd.LowerBound;

+            }

+          }

+        }

+      }

+    }

+

+    /// <summary>

+    /// Return a zero-equivalent value for "typ", or return null (for any reason whatsoever).

+    /// </summary>

+    Expression Zero(Bpl.IToken tok, Type typ) {

+      Contract.Requires(tok != null);

+      Contract.Requires(typ != null);

+      return null;  // TODO: this can be improved

+    }

+

     void TrParallelAssign(ParallelStmt s, AssignStmt s0,

       Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder updater, Bpl.VariableSeq locals, ExpressionTranslator etran) {

       // The statement:

@@ -4804,12 +4925,10 @@ namespace Microsoft.Dafny {
     }

 

     static Expression CreateIntSub(IToken tok, Expression e0, Expression e1)

-     {

+    {

       Contract.Requires(tok != null);

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-

-

       Contract.Requires(e0.Type is IntType && e1.Type is IntType);

       Contract.Ensures(Contract.Result<Expression>() != null);

       BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1);

@@ -4819,7 +4938,7 @@ namespace Microsoft.Dafny {
     }

 

     static Expression CreateIntITE(IToken tok, Expression test, Expression e0, Expression e1)

-     {

+    {

       Contract.Requires(tok != null);

       Contract.Requires(test != null);

       Contract.Requires(e0 != null);

@@ -4833,7 +4952,7 @@ namespace Microsoft.Dafny {
     }

 

     public IEnumerable<Expression> Conjuncts(Expression expr)

-     {

+    {

       Contract.Requires(expr != null);

       Contract.Requires(expr.Type is BoolType);

       Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));