diff options
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 1 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 65 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 386 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 64 |
4 files changed, 238 insertions, 278 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);
|