Refactored and improved bounds discovery

5 files changed, 242 insertions, 279 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index f02f7861..619638ac 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2978,6 +2978,7 @@ namespace Microsoft.Dafny {
           TrExpr(b.Seq);

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

         } else {

+          // TODO: handle ComprehensionExpr.SubSetBoundedPool

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

         }

         wr.Write("if (");

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 1b2af648..b998aa47 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -6688,24 +6688,56 @@ namespace Microsoft.Dafny {
       }

       public abstract int Preference(); // higher is better

       

-      public static BoundedPool GetBest(List<BoundedPool> bounds) {

-        Contract.Requires(bounds != null && bounds.Count > 0);

-        var ret = bounds[0];

+      public static BoundedPool GetBest(List<BoundedPool> bounds, bool onlyFiniteBounds) {

+        Contract.Requires(bounds != null);

+        bounds = CombineIntegerBounds(bounds);

+        BoundedPool best = null;

         foreach (var bound in bounds) {

-          if (bound.Preference() > ret.Preference()) {

-            ret = bound;

-          } else {            

-            var retInt = ret as ComprehensionExpr.IntBoundedPool;

-            if (retInt != null && (retInt.LowerBound == null || retInt.UpperBound == null)) {

-              var boundInt = bound as ComprehensionExpr.IntBoundedPool;

-              if (boundInt != null) {

-                ret = new ComprehensionExpr.IntBoundedPool(retInt.LowerBound ?? boundInt.LowerBound, 

-                                                           retInt.UpperBound ?? boundInt.UpperBound);

-              }

-            }         

+          if (!onlyFiniteBounds || bound.IsFinite) {

+            if (best == null || bound.Preference() > best.Preference()) {

+              best = bound;

+            }

+          }

+        }

+        return best;

+      }

+      static List<BoundedPool> CombineIntegerBounds(List<BoundedPool> bounds) {

+        var lowerBounds = new List<IntBoundedPool>();

+        var upperBounds = new List<IntBoundedPool>();

+        var others = new List<BoundedPool>();

+        foreach (var b in bounds) {

+          var ib = b as IntBoundedPool;

+          if (ib != null && ib.UpperBound == null) {

+            lowerBounds.Add(ib);

+          } else if (ib != null && ib.LowerBound == null) {

+            upperBounds.Add(ib);

+          } else {

+            others.Add(b);

           }

         }

-        return ret;

+        // pair up the bounds

+        var n = Math.Min(lowerBounds.Count, upperBounds.Count);

+        for (var i = 0; i < n; i++) {

+          others.Add(new IntBoundedPool(lowerBounds[i].LowerBound, upperBounds[i].UpperBound));

+        }

+        for (var i = n; i < lowerBounds.Count; i++) {

+          others.Add(lowerBounds[i]);

+        }

+        for (var i = n; i < upperBounds.Count; i++) {

+          others.Add(upperBounds[i]);

+        }

+        return others;

+      }

+    }

+    public class ExactBoundedPool : BoundedPool

+    {

+      public readonly Expression E;

+      public ExactBoundedPool(Expression e) {

+        Contract.Requires(e != null);

+        E = e;

+      }

+      public override int Preference() {

+        return 20;  // the best of all bounds

       }

     }

     public class BoolBoundedPool : BoundedPool

@@ -6754,6 +6786,9 @@ namespace Microsoft.Dafny {
       public override int Preference() {

         return 0;

       }

+      public override bool IsFinite {

+        get { return false; }

+      }

     }

     public class MapBoundedPool : BoundedPool

     {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1bf96d7d..cd531cf1 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1477,13 +1477,15 @@ namespace Microsoft.Dafny
 

       if (ErrorCount == prevErrorCount) {

         foreach (var e in needFiniteBoundsChecks_SetComprehension) {

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

           CheckTypeInference(e.Range);  // we need to resolve operators before the call to DiscoverBounds

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

+          List<BoundVar> missingBounds;

+          e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds);

           if (missingBounds.Count != 0) {

             e.MissingBounds = missingBounds;

-            foreach (var bv in e.MissingBounds) {

-              Error(e, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

+            if (e.Finite) {

+              foreach (var bv in e.MissingBounds) {

+                Error(e, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

+              }

             }

           }

         }

@@ -1491,21 +1493,17 @@ namespace Microsoft.Dafny
           Contract.Assert(!e.Exact);  // only let-such-that expressions are ever added to the list

           Contract.Assert(e.RHSs.Count == 1);  // if we got this far, the resolver will have checked this condition successfully

           var constraint = e.RHSs[0];

-          var missingBounds = new List<IVariable>();

           CheckTypeInference(constraint);  // we need to resolve operators before the call to DiscoverBounds

-          var allBounds = DiscoverBoundsAux(e.tok, new List<IVariable>(e.BoundVars), constraint, true, true, true, missingBounds);

+          List<IVariable> missingBounds;

+          var vars = new List<IVariable>(e.BoundVars);

+          var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds);

           if (missingBounds.Count != 0) {

             e.Constraint_MissingBounds = missingBounds;

             foreach (var bv in e.Constraint_MissingBounds) {

               Error(e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

             }

           } else {

-            e.Constraint_Bounds = new List<ComprehensionExpr.BoundedPool>();

-            foreach (var pair in allBounds) {

-              Contract.Assert(1 <= pair.Item2.Count);

-              // TODO: The following could be improved by picking the bound that is most likely to give rise to an efficient compiled program

-              e.Constraint_Bounds.Add(pair.Item2[0]);

-            }

+            e.Constraint_Bounds = bestBounds;

           }

         }

       }

@@ -1578,38 +1576,34 @@ namespace Microsoft.Dafny
                 }

                 return null;

               };

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

-              var bounds = DiscoverBounds(dd.Constraint.tok, new List<BoundVar> { dd.Var }, dd.Constraint,

-                true, true, missingBounds);

+              var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint);

               List<NativeType> potentialNativeTypes =

                 (stringNativeType != null) ? new List<NativeType> { stringNativeType } :

                 (boolNativeType == false) ? new List<NativeType>() :

                 NativeTypes;

               foreach (var nt in potentialNativeTypes) {

-                if (missingBounds.Count == 0) {

-                  bool lowerOk = false;

-                  bool upperOk = false;

-                  foreach (var bound in bounds) {

-                    if (bound is ComprehensionExpr.IntBoundedPool) {

-                      var bnd = (ComprehensionExpr.IntBoundedPool)bound;

-                      if (bnd.LowerBound != null) {

-                        BigInteger? lower = GetConst(bnd.LowerBound);

-                        if (lower != null && nt.LowerBound <= lower) {

-                          lowerOk = true;

-                        }

+                bool lowerOk = false;

+                bool upperOk = false;

+                foreach (var bound in bounds) {

+                  if (bound is ComprehensionExpr.IntBoundedPool) {

+                    var bnd = (ComprehensionExpr.IntBoundedPool)bound;

+                    if (bnd.LowerBound != null) {

+                      BigInteger? lower = GetConst(bnd.LowerBound);

+                      if (lower != null && nt.LowerBound <= lower) {

+                        lowerOk = true;

                       }

-                      if (bnd.UpperBound != null) {

-                        BigInteger? upper = GetConst(bnd.UpperBound);

-                        if (upper != null && upper <= nt.UpperBound) {

-                          upperOk = true;

-                        }

+                    }

+                    if (bnd.UpperBound != null) {

+                      BigInteger? upper = GetConst(bnd.UpperBound);

+                      if (upper != null && upper <= nt.UpperBound) {

+                        upperOk = true;

                       }

                     }

                   }

-                  if (lowerOk && upperOk) {

-                    dd.NativeType = nt;

-                    break;

-                  }

+                }

+                if (lowerOk && upperOk) {

+                  dd.NativeType = nt;

+                  break;

                 }

               }

               if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) {

@@ -5262,9 +5256,9 @@ namespace Microsoft.Dafny
 

         bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == ErrorCount && UsesSpecFeatures(s.Range));

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

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

           CheckTypeInference(s.Range);  // we need to resolve operators before the call to DiscoverBounds

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

+          List<BoundVar> missingBounds;

+          s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, true, out missingBounds);

           if (missingBounds.Count != 0) {

             bodyMustBeSpecOnly = true;

           }

@@ -6082,18 +6076,14 @@ namespace Microsoft.Dafny
       if (ec == ErrorCount && !s.IsGhost && s.AssumeToken == null && !specContextOnly) {

         CheckIsNonGhost(s.Expr);

 

-        var missingBounds = new List<IVariable>();

         CheckTypeInference(s.Expr);  // we need to resolve operators before the call to DiscoverBoundsAux

-        var allBounds = DiscoverBoundsAux(s.Tok, varLhss, s.Expr, true, true, true, missingBounds);

+        List<IVariable> missingBounds;

+        var bestBounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, false, out missingBounds);

         if (missingBounds.Count != 0) {

           s.MissingBounds = missingBounds;  // so that an error message can be produced during compilation

         } else {

-          Contract.Assert(allBounds != null);

-          s.Bounds = new List<ComprehensionExpr.BoundedPool>();

-          foreach (var pair in allBounds) {

-            Contract.Assert(1 <= pair.Item2.Count);                                             

-            s.Bounds.Add(ComprehensionExpr.BoundedPool.GetBest(pair.Item2));

-          }

+          Contract.Assert(bestBounds != null);

+          s.Bounds = bestBounds;

         }

       }

     }

@@ -7694,7 +7684,7 @@ namespace Microsoft.Dafny
         if (e.Contract != null) ResolveExpression(e.Contract, opts);

         e.Type = e.Body.Type;

       } else if (expr is QuantifierExpr) {

-        QuantifierExpr e = (QuantifierExpr)expr;

+        var e = (QuantifierExpr)expr;

         int prevErrorCount = ErrorCount;

         bool _val = true;

         bool typeQuantifier = Attributes.ContainsBool(e.Attributes, "typeQuantifier", ref _val) && _val;

@@ -7729,9 +7719,9 @@ namespace Microsoft.Dafny
         expr.Type = Type.Bool;

 

         if (prevErrorCount == ErrorCount) {

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

           CheckTypeInference(e.LogicalBody());  // we need to resolve operators before the call to DiscoverBounds

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

+          List<BoundVar> missingBounds;

+          e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.LogicalBody(), e is ExistsExpr, true, out missingBounds);

           if (missingBounds.Count != 0) {

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

             var mb = missingBounds;

@@ -7801,9 +7791,9 @@ namespace Microsoft.Dafny
         expr.Type = new MapType(e.Finite, e.BoundVars[0].Type, e.Term.Type);

 

         if (prevErrorCount == ErrorCount) {

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

           CheckTypeInference(e.Range);  // we need to resolve operators before the call to DiscoverBounds

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

+          List<BoundVar> missingBounds;

+          e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds);

           if (missingBounds.Count != 0) {

             e.MissingBounds = missingBounds;

             if (e.Finite) {

@@ -9408,202 +9398,138 @@ namespace Microsoft.Dafny
     }

 

     /// <summary>

-    /// For a description, see DiscoverBoundsAux.

-    /// </summary>

-    public static List<ComprehensionExpr.BoundedPool> DiscoverBounds<VT>(IToken tok, List<VT> bvars, Expression expr, bool polarity, bool returnAllBounds, List<VT> missingBounds) where VT : IVariable {

-      var pairs = DiscoverBoundsAux(tok, bvars, expr, polarity, returnAllBounds, false, missingBounds);

-      if (pairs == null) {

-        return null;

-      }

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

-      foreach (var pr in pairs) {

-        Contract.Assert(1 <= pr.Item2.Count);

-        bounds.AddRange(pr.Item2);

-      }

-      return bounds;

-    }

-

-    /// <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 SubSetBoundedPool or SuperSetBoundedPool is returned

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

-    ///   -- a variable may give rise to several 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.

-    /// If "allowAnyIntegers", then integer variables will always be given a bound, but this bound may be WiggleWaggle if

-    /// there is no better bound.

+    /// For a list of variables "bvars", returns a list of best bounds for each respective variable.  If no bound is found for a variable "v", then the bound for

+    /// "v" in the returned list is set to "null" and "v" is added to "missingBounds".

     /// </summary>

-    public static List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>> DiscoverBoundsAux<VT>(IToken tok, List<VT> bvars, Expression expr, bool polarity, bool returnAllBounds, bool allowAnyIntegers, List<VT> missingBounds) where VT : IVariable {

-      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(

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

-        (!returnAllBounds &&

-         Contract.Result<List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>>() != null &&

-         Contract.Result<List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>>().Count == bvars.Count &&

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

-        (!returnAllBounds &&

-         Contract.Result<List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>>() == null &&

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

-

-      var allBounds = new List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>>();

-      bool foundError = false;

+    public static List<ComprehensionExpr.BoundedPool> DiscoverBestBounds_MultipleVars<VT>(List<VT> bvars, Expression expr, bool polarity, bool onlyFiniteBounds, out List<VT> missingBounds) where VT : IVariable {

       foreach (var bv in bvars) {

         var c = TypeConstraint(bv, bv.Type);

         expr = polarity ? Expression.CreateAnd(c, expr) : Expression.CreateImplies(c, expr);

       }

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

-        VT bv;

-        List<ComprehensionExpr.BoundedPool> bounds;

-        foundError = DiscoverAuxSingle<VT>(bvars, expr, polarity, returnAllBounds, true, allowAnyIntegers, missingBounds, foundError, j, out bv, out bounds);

-        if (!returnAllBounds && bounds.Count > 1) {

-          var best = ComprehensionExpr.BoundedPool.GetBest(bounds);

-          bounds = new List<ComprehensionExpr.BoundedPool>() { best };

+      var all = DiscoverAllBounds_Aux_MultipleVars(bvars, expr, polarity);

+      var bests = all.ConvertAll(tup => ComprehensionExpr.BoundedPool.GetBest(tup.Item2, onlyFiniteBounds));

+      missingBounds = new List<VT>();

+      for (var i = 0; i < bvars.Count; i++) {

+        if (bests[i] == null) {

+          missingBounds.Add(bvars[i]);

         }

+      }

+      return bests;

+    }

 

-        allBounds.Add(new Tuple<VT, List<ComprehensionExpr.BoundedPool>>(bv, bounds));

+    public static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_SingleVar<VT>(VT v, Expression expr) where VT : IVariable {

+      expr = Expression.CreateAnd(TypeConstraint(v, v.Type), expr);

+      return DiscoverAllBounds_Aux_SingleVar(new List<VT> { v }, 0, expr, true);

+    }

+

+    private static List<Tuple<VT, List<ComprehensionExpr.BoundedPool>>> DiscoverAllBounds_Aux_MultipleVars<VT>(List<VT> bvars, Expression expr, bool polarity) 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);

+        bb.Add(new Tuple<VT, List<ComprehensionExpr.BoundedPool>>(bvars[j], bounds));

       }

-      return foundError ? null : allBounds;

+      return bb;

     }

 

-    private static bool DiscoverAuxSingle<VT>(List<VT> bvars, Expression expr, bool polarity, bool allowPartialBounds, bool returnAllBounds, bool allowAnyIntegers, List<VT> missingBounds, bool foundError, int j, out VT bv, out List<ComprehensionExpr.BoundedPool> bounds) where VT : IVariable {

-      bv = bvars[j];

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

+    /// <summary>

+    /// Returns a list of (possibly partial) bounds for "bvars[j]", each of which can be written without mentioning any variable in "bvars[j..]".

+    /// </summary>

+    private static List<ComprehensionExpr.BoundedPool> DiscoverAllBounds_Aux_SingleVar<VT>(List<VT> bvars, int j, Expression expr, bool polarity) where VT : IVariable {

+      Contract.Requires(bvars != null);

+      Contract.Requires(0 <= j && j < bvars.Count);

+      Contract.Requires(expr != null);

+      var bv = bvars[j];

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

+

+      // Maybe the type itself gives a bound

       if (bv.Type.IsBoolType) {

         // easy

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

-      } else {

-        bool foundBoundsForBv = false;

-        if (bv.Type.IsIndDatatype && bv.Type.AsIndDatatype.HasFinitePossibleValues) {

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

-          foundBoundsForBv = true;

-        }

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

-        Expression lowerBound = null;

-        Expression upperBound = null;

-        if ((allowPartialBounds || returnAllBounds) && 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) {

-            goto CHECK_NEXT_CONJUNCT;

-          }

-          var e0 = c.E0;

-          var e1 = c.E1;

-          int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, ref e0, ref e1);

-          if (whereIsBv < 0) {

-            goto CHECK_NEXT_CONJUNCT;

-          }

-          switch (c.ResolvedOp) {

-            case BinaryExpr.ResolvedOpcode.InSet:

-              if (whereIsBv == 0) {

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

-                foundBoundsForBv = true;

-                if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

-              }

-              break;

-            case BinaryExpr.ResolvedOpcode.Subset:

-              if (returnAllBounds) {

-                if (whereIsBv == 0) {

-                  bounds.Add(new ComprehensionExpr.SubSetBoundedPool(e1));

-                } else {

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

-                }

-                foundBoundsForBv = true;

-              }

-              break;

-            case BinaryExpr.ResolvedOpcode.InMultiSet:

-              if (whereIsBv == 0) {

-                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 ComprehensionExpr.SeqBoundedPool(e1));

-                foundBoundsForBv = true;

-                if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

-              }

-              break;

-            case BinaryExpr.ResolvedOpcode.InMap:

-              if (whereIsBv == 0 && e1.Type.AsMapType.Finite) {

-                bounds.Add(new ComprehensionExpr.MapBoundedPool(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 ComprehensionExpr.IntBoundedPool(otherOperand, Expression.CreateIncrement(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.SubSetBoundedPool(otherOperand));

-                foundBoundsForBv = true;

-              }

-              break;

-            case BinaryExpr.ResolvedOpcode.Gt:

-            case BinaryExpr.ResolvedOpcode.Ge:

-              Contract.Assert(false); throw new cce.UnreachableException();  // promised by postconditions of NormalizedConjunct

-            case BinaryExpr.ResolvedOpcode.Lt:

-              if (e0.Type.IsNumericBased(Type.NumericPersuation.Int)) {

-                if (whereIsBv == 0 && upperBound == null) {

-                  upperBound = e1;  // bv < E

-                } else if (whereIsBv == 1 && lowerBound == null) {

-                  lowerBound = Expression.CreateIncrement(e0, 1);  // E < bv

-                }

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

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

+      } else if (bv.Type.IsNumericBased(Type.NumericPersuation.Int)) {

+        bounds.Add(new AssignSuchThatStmt.WiggleWaggleBound());

+      }

+

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

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

+        var c = conjunct as BinaryExpr;

+        if (c == null) {

+          // We only know what to do with binary expressions

+          continue;

+        }

+        var e0 = c.E0;

+        var e1 = c.E1;

+        int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, ref e0, ref e1);

+        if (whereIsBv < 0) {

+          continue;

+        }

+        switch (c.ResolvedOp) {

+          case BinaryExpr.ResolvedOpcode.InSet:

+            if (whereIsBv == 0 && e1.Type.AsSetType.Finite) {

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

+            }

+            break;

+          case BinaryExpr.ResolvedOpcode.Subset:

+            if (whereIsBv == 0) {

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

+            } else {

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

+            }

+            break;

+          case BinaryExpr.ResolvedOpcode.InMultiSet:

+            if (whereIsBv == 0) {

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

+            }

+            break;

+          case BinaryExpr.ResolvedOpcode.InSeq:

+            if (whereIsBv == 0) {

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

+            }

+            break;

+          case BinaryExpr.ResolvedOpcode.InMap:

+            if (whereIsBv == 0 && e1.Type.AsMapType.Finite) {

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

+            }

+            break;

+          case BinaryExpr.ResolvedOpcode.EqCommon:

+            // TODO: Use the new ComprehensionExpr.ExactBoundedPool

+            if (bv.Type.IsNumericBased(Type.NumericPersuation.Int)) {

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

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

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

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

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

+            }

+            break;

+          case BinaryExpr.ResolvedOpcode.Gt:

+          case BinaryExpr.ResolvedOpcode.Ge:

+            Contract.Assert(false); throw new cce.UnreachableException();  // promised by postconditions of NormalizedConjunct

+          case BinaryExpr.ResolvedOpcode.Lt:

+            if (e0.Type.IsNumericBased(Type.NumericPersuation.Int)) {

+              if (whereIsBv == 0) {  // bv < E

+                bounds.Add(new ComprehensionExpr.IntBoundedPool(null, e1));

+              } else {  // E < bv

+                bounds.Add(new ComprehensionExpr.IntBoundedPool(Expression.CreateIncrement(e0, 1), null));

               }

-              break;

-            case BinaryExpr.ResolvedOpcode.Le:

-              if (e0.Type.IsNumericBased(Type.NumericPersuation.Int)) {

-                if (whereIsBv == 0 && upperBound == null) {

-                  upperBound = Expression.CreateIncrement(e1, 1);  // bv <= E

-                } else if (whereIsBv == 1 && lowerBound == null) {

-                  lowerBound = e0;  // E <= bv

-                }

+            }

+            break;

+          case BinaryExpr.ResolvedOpcode.Le:

+            if (e0.Type.IsNumericBased(Type.NumericPersuation.Int)) {

+              if (whereIsBv == 0) {  // bv <= E

+                bounds.Add(new ComprehensionExpr.IntBoundedPool(null, Expression.CreateIncrement(e1, 1)));

+              } else {  // E <= bv

+                bounds.Add(new ComprehensionExpr.IntBoundedPool(e0, null));

               }

-              break;

-            default:

-              break;

-          }

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

-              (allowPartialBounds && (lowerBound != null || upperBound != null))) {

-            // we have found two halves (or, in the case of returnAllBounds, we have found some bound)

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

-            lowerBound = null;

-            upperBound = null;

-            foundBoundsForBv = true;

-            if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

-          }

-        CHECK_NEXT_CONJUNCT: ;

-        }

-        if (!foundBoundsForBv) {

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

-          if (allowAnyIntegers && bv.Type is IntType) {

-            bounds.Add(new AssignSuchThatStmt.WiggleWaggleBound());

-          } else {

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

-            foundError = true;

-          }

+            }

+            break;

+          default:

+            break;

         }

       }

-    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)

-      return foundError;

+      return bounds;

     }

 

     static Expression TypeConstraint(IVariable bv, Type ty) {

@@ -10241,7 +10167,7 @@ namespace Microsoft.Dafny
       } else if (expr is NamedExpr) {

         return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body);

       } else if (expr is ComprehensionExpr) {

-        if (expr is QuantifierExpr && ((QuantifierExpr)expr).Bounds == null) {

+        if (expr is QuantifierExpr && ((QuantifierExpr)expr).Bounds.Contains(null)) {

           return true;  // the quantifier cannot be compiled if the resolver found no bounds

         }

         return Contract.Exists(expr.SubExpressions, se => UsesSpecFeatures(se));

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 59d93347..2ae03412 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -7653,39 +7653,37 @@ namespace Microsoft.Dafny {
       }

 

       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 Expression.CreateDecrement(bnd.UpperBound, 1);

-          } else if (bound is ComprehensionExpr.SubSetBoundedPool) {

-            var bnd = (ComprehensionExpr.SubSetBoundedPool)bound;

-            yield return bnd.UpperBound;

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

-            var bnd = (ComprehensionExpr.SuperSetBoundedPool)bound;

-            yield return bnd.LowerBound;

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

-            var st = ((ComprehensionExpr.SetBoundedPool)bound).Set.Resolved;

-            if (st is DisplayExpression) {

-              var display = (DisplayExpression)st;

-              foreach (var el in display.Elements) {

-                yield return el;

-              }

-            } else if (st is MapDisplayExpr) {

-              var display = (MapDisplayExpr)st;

-              foreach (var maplet in display.Elements) {

-                yield return maplet.A;

-              }

+      var bounds = Resolver.DiscoverAllBounds_SingleVar(x, expr);

+      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 Expression.CreateDecrement(bnd.UpperBound, 1);

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

+          var bnd = (ComprehensionExpr.SubSetBoundedPool)bound;

+          yield return bnd.UpperBound;

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

+          var bnd = (ComprehensionExpr.SuperSetBoundedPool)bound;

+          yield return bnd.LowerBound;

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

+          var st = ((ComprehensionExpr.SetBoundedPool)bound).Set.Resolved;

+          if (st is DisplayExpression) {

+            var display = (DisplayExpression)st;

+            foreach (var el in display.Elements) {

+              yield return el;

             }

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

-            var sq = ((ComprehensionExpr.SeqBoundedPool)bound).Seq.Resolved;

-            var display = sq as DisplayExpression;

-            if (display != null) {

-              foreach (var el in display.Elements) {

-                yield return el;

-              }

+          } else if (st is MapDisplayExpr) {

+            var display = (MapDisplayExpr)st;

+            foreach (var maplet in display.Elements) {

+              yield return maplet.A;

+            }

+          }

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

+          var sq = ((ComprehensionExpr.SeqBoundedPool)bound).Seq.Resolved;

+          var display = sq as DisplayExpression;

+          if (display != null) {

+            foreach (var el in display.Elements) {

+              yield return el;

             }

           }

         }

@@ -11603,8 +11601,8 @@ namespace Microsoft.Dafny {
 

         } else if (expr is LambdaExpr) {

           var e = (LambdaExpr)expr;

-

           return TrLambdaExpr(e);

+

         } else if (expr is StmtExpr) {

           var e = (StmtExpr)expr;

           return TrExpr(e.E);

diff --git a/Test/dafny0/ISets.dfy b/Test/dafny0/ISets.dfy
index bb0230f4..703039c8 100644
--- a/Test/dafny0/ISets.dfy
+++ b/Test/dafny0/ISets.dfy
@@ -4,7 +4,7 @@
 ghost method M()

 {

    ghost var s := iset{2};

-   // test "in

+   // test "in"

    if(2 in s)

    {

    }

@@ -35,6 +35,9 @@ ghost method m1() {
  assert s2 - s3 == iset{3}; // set difference

 

  assert (iset x | x in s2 :: x+1) == iset{2,3,4}; // set comprehension

+ assert 17 in (iset x: int | true :: x); // set comprehension

+

+ assert (imap x: int | true :: x+1)[14] == 15;

 }