From 10a8896ae40fd918abbb8caa616ac6ee0876ac1d Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 29 May 2015 16:29:15 -0700 Subject: Add an infinite set collection type. --- Test/dafny0/ISets.dfy | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 Test/dafny0/ISets.dfy (limited to 'Test/dafny0/ISets.dfy') diff --git a/Test/dafny0/ISets.dfy b/Test/dafny0/ISets.dfy new file mode 100644 index 00000000..bb0230f4 --- /dev/null +++ b/Test/dafny0/ISets.dfy @@ -0,0 +1,40 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +ghost method M() +{ + ghost var s := iset{2}; + // test "in + if(2 in s) + { + } + else + { assert false; } + // test "!in" + if(3 !in s) + { + } + else + { assert false; } + + if(s == iset{2}) + { + } + else + { assert false; } +} + +ghost method m1() { + var s1:iset := iset{}; // the empty set + var s2 := iset{1, 2, 3}; // set contains exactly 1, 2, and 3 + assert s2 == iset{1,1,2,3,3,3,3}; // same as before + var s3, s4 := iset{1,2}, iset{1,4}; + + assert s2 + s4 == iset{1,2,3,4}; // set union + assert s2 * s3 == iset{1,2} && s2 * s4 == iset{1}; // set intersection + assert s2 - s3 == iset{3}; // set difference + + assert (iset x | x in s2 :: x+1) == iset{2,3,4}; // set comprehension +} + + -- cgit v1.2.3 From 69c320b225825eb2adf2ae899f88588a10fd27fe Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 19 Aug 2015 20:05:47 -0700 Subject: Refactored and improved bounds discovery --- Source/Dafny/Compiler.cs | 1 + Source/Dafny/DafnyAst.cs | 65 ++++++-- Source/Dafny/Resolver.cs | 386 ++++++++++++++++++--------------------------- Source/Dafny/Translator.cs | 64 ++++---- Test/dafny0/ISets.dfy | 5 +- 5 files changed, 242 insertions(+), 279 deletions(-) (limited to 'Test/dafny0/ISets.dfy') 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 bounds) { - Contract.Requires(bounds != null && bounds.Count > 0); - var ret = bounds[0]; + public static BoundedPool GetBest(List 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 CombineIntegerBounds(List bounds) { + var lowerBounds = new List(); + var upperBounds = new List(); + var others = new List(); + 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(); 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 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(); CheckTypeInference(constraint); // we need to resolve operators before the call to DiscoverBounds - var allBounds = DiscoverBoundsAux(e.tok, new List(e.BoundVars), constraint, true, true, true, missingBounds); + List missingBounds; + var vars = new List(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(); - 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(); - var bounds = DiscoverBounds(dd.Constraint.tok, new List { dd.Var }, dd.Constraint, - true, true, missingBounds); + var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint); List potentialNativeTypes = (stringNativeType != null) ? new List { stringNativeType } : (boolNativeType == false) ? new List() : 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(); 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 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(); 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 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(); - 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(); 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 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(); 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 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 } /// - /// For a description, see DiscoverBoundsAux. - /// - public static List DiscoverBounds(IToken tok, List bvars, Expression expr, bool polarity, bool returnAllBounds, List missingBounds) where VT : IVariable { - var pairs = DiscoverBoundsAux(tok, bvars, expr, polarity, returnAllBounds, false, missingBounds); - if (pairs == null) { - return null; - } - var bounds = new List(); - foreach (var pr in pairs) { - Contract.Assert(1 <= pr.Item2.Count); - bounds.AddRange(pr.Item2); - } - return bounds; - } - - /// - /// 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". /// - public static List>> DiscoverBoundsAux(IToken tok, List bvars, Expression expr, bool polarity, bool returnAllBounds, bool allowAnyIntegers, List 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>>>() != null && - Contract.Result>>>().Count == bvars.Count && - Contract.OldValue(missingBounds.Count) == missingBounds.Count) || - (!returnAllBounds && - Contract.Result>>>() == null && - Contract.OldValue(missingBounds.Count) < missingBounds.Count)); - - var allBounds = new List>>(); - bool foundError = false; + public static List DiscoverBestBounds_MultipleVars(List bvars, Expression expr, bool polarity, bool onlyFiniteBounds, out List 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 bounds; - foundError = DiscoverAuxSingle(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() { best }; + var all = DiscoverAllBounds_Aux_MultipleVars(bvars, expr, polarity); + var bests = all.ConvertAll(tup => ComprehensionExpr.BoundedPool.GetBest(tup.Item2, onlyFiniteBounds)); + missingBounds = new List(); + for (var i = 0; i < bvars.Count; i++) { + if (bests[i] == null) { + missingBounds.Add(bvars[i]); } + } + return bests; + } - allBounds.Add(new Tuple>(bv, bounds)); + public static List DiscoverAllBounds_SingleVar(VT v, Expression expr) where VT : IVariable { + expr = Expression.CreateAnd(TypeConstraint(v, v.Type), expr); + return DiscoverAllBounds_Aux_SingleVar(new List { v }, 0, expr, true); + } + + private static List>> DiscoverAllBounds_Aux_MultipleVars(List bvars, Expression expr, bool polarity) where VT : IVariable { + Contract.Requires(bvars != null); + Contract.Requires(expr != null); + var bb = new List>>(); + for (var j = 0; j < bvars.Count; j++) { + var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity); + bb.Add(new Tuple>(bvars[j], bounds)); } - return foundError ? null : allBounds; + return bb; } - private static bool DiscoverAuxSingle(List bvars, Expression expr, bool polarity, bool allowPartialBounds, bool returnAllBounds, bool allowAnyIntegers, List missingBounds, bool foundError, int j, out VT bv, out List bounds) where VT : IVariable { - bv = bvars[j]; - bounds = new List(); + /// + /// Returns a list of (possibly partial) bounds for "bvars[j]", each of which can be written without mentioning any variable in "bvars[j..]". + /// + private static List DiscoverAllBounds_Aux_SingleVar(List 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(); + + // 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(); - var bounds = Resolver.DiscoverBounds(x.tok, new List() { 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; } -- cgit v1.2.3