diff options
| author |  Rustan Leino <unknown> | 2015-08-19 20:05:47 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-08-19 20:05:47 -0700 |
| commit | 69c320b225825eb2adf2ae899f88588a10fd27fe (patch) | |
| tree | 8d9fe5b99e481291f656718e29c81fc2cd04ab92 /Source/Dafny/DafnyAst.cs | |
| parent | 747e2d218f49683605d52f70dbb372f37d9f304b (diff) | |
Refactored and improved bounds discovery
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 65 |
1 files changed, 50 insertions, 15 deletions
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
{
|