diff options
author | 2011-05-14 01:35:57 -0700 | |
---|---|---|
committer | 2011-05-14 01:35:57 -0700 | |
commit | 5d983730fba0b12bd5520be075e1a46d48b644a3 (patch) | |
tree | 5f1dd296d4625e53e23c4cf8ff6df3d5afbb4778 | |
parent | f2c2a579f9db4f012d79f25469563204f8fb285e (diff) |
Dafny: fixed bug in quantifier bounds discovery
-rw-r--r-- | Source/Dafny/Resolver.cs | 106 |
1 files changed, 54 insertions, 52 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 37b80894..6c2f6c38 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2398,12 +2398,11 @@ namespace Microsoft.Dafny { }
var e0 = c.E0;
var e1 = c.E1;
- var op = c.ResolvedOp;
- int whereIsBv = SanitizeForBoundDiscovery(e.BoundVars, j, ref op, ref e0, ref e1);
+ int whereIsBv = SanitizeForBoundDiscovery(e.BoundVars, j, c.ResolvedOp, ref e0, ref e1);
if (whereIsBv < 0) {
goto CHECK_NEXT_CONJUNCT;
}
- switch (op) {
+ switch (c.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.InSet:
if (whereIsBv == 0) {
bounds.Add(new QuantifierExpr.SetBoundedPool(e1));
@@ -2412,7 +2411,7 @@ namespace Microsoft.Dafny { break;
case BinaryExpr.ResolvedOpcode.InSeq:
if (whereIsBv == 0) {
- bounds.Add(new QuantifierExpr.SetBoundedPool(e1));
+ bounds.Add(new QuantifierExpr.SeqBoundedPool(e1));
goto CHECK_NEXT_BOUND_VARIABLE;
}
break;
@@ -2425,7 +2424,7 @@ namespace Microsoft.Dafny { break;
case BinaryExpr.ResolvedOpcode.Gt:
case BinaryExpr.ResolvedOpcode.Ge:
- Contract.Assert(false); throw new cce.UnreachableException(); // promised by postconditions of NormalizedConjunct and SanitizeForBoundDiscovery
+ Contract.Assert(false); throw new cce.UnreachableException(); // promised by postconditions of NormalizedConjunct
case BinaryExpr.ResolvedOpcode.Lt:
if (whereIsBv == 0 && upperBound == null) {
upperBound = e1; // bv < E
@@ -2462,14 +2461,13 @@ namespace Microsoft.Dafny { }
/// <summary>
- /// If the return value is negative, the resulting "op", "e0", and "e1" should not be used.
+ /// If the return value is negative, the resulting "e0" and "e1" should not be used.
/// Otherwise, the following is true on return:
/// The new "e0 op e1" is equivalent to the old "e0 op e1".
/// One of "e0" and "e1" is the identifier "boundVars[bvi]"; the return value is either 0 or 1, and indicates which.
/// The other of "e0" and "e1" is an expression whose free variables are not among "boundVars[bvi..]".
- /// Requires the initial value of "op" not to be Gt or Ge, and ensures the same about the final value of "op".
/// </summary>
- int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, ref BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1)
+ int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1)
{
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
@@ -2499,54 +2497,57 @@ namespace Microsoft.Dafny { }
// Next, clean up the side where bv is by adjusting both sides of the expression
- while (true) {
- switch (op) {
- case BinaryExpr.ResolvedOpcode.EqCommon:
- case BinaryExpr.ResolvedOpcode.NeqCommon:
- case BinaryExpr.ResolvedOpcode.Gt:
- case BinaryExpr.ResolvedOpcode.Ge:
- case BinaryExpr.ResolvedOpcode.Le:
- case BinaryExpr.ResolvedOpcode.Lt:
+ switch (op) {
+ case BinaryExpr.ResolvedOpcode.EqCommon:
+ case BinaryExpr.ResolvedOpcode.NeqCommon:
+ case BinaryExpr.ResolvedOpcode.Gt:
+ case BinaryExpr.ResolvedOpcode.Ge:
+ case BinaryExpr.ResolvedOpcode.Le:
+ case BinaryExpr.ResolvedOpcode.Lt:
+ // Repeatedly move additive or subtractive terms from thisSide to thatSide
+ while (true) {
var bin = thisSide as BinaryExpr;
- if (bin != null) {
- if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add) {
- // Change "A+B op C" into either "A op C-B" or "B op C-A", depending on where we find bv among A and B.
- if (!FreeVariables(bin.E1).Contains(bv)) {
- thisSide = bin.E0;
- thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E1);
- } else {
- thisSide = bin.E1;
- thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E0);
- }
+ if (bin == null) {
+ break; // done simplifying
+
+ } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add) {
+ // Change "A+B op C" into either "A op C-B" or "B op C-A", depending on where we find bv among A and B.
+ if (!FreeVariables(bin.E1).Contains(bv)) {
+ thisSide = bin.E0;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E1);
+ } else {
+ thisSide = bin.E1;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E0);
+ }
+ ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
+ thatSide.Type = bin.Type;
+
+ } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub) {
+ // Change "A-B op C" in a similar way.
+ if (!FreeVariables(bin.E1).Contains(bv)) {
+ // change to "A op C+B"
+ thisSide = bin.E0;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Add, thatSide, bin.E1);
+ ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Add;
+ } else {
+ // In principle, change to "-B op C-A" and then to "B dualOp A-C". But since we don't want
+ // to change "op", we instead end with "A-C op B" and switch the mapping of thisSide/thatSide
+ // to e0/e1 (by inverting "whereIsBv").
+ thisSide = bin.E1;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, bin.E0, thatSide);
((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
- thatSide.Type = bin.Type;
- continue; // continue simplifying
-
- } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub) {
- // Change "A-B op C" in a similar way.
- if (!FreeVariables(bin.E1).Contains(bv)) {
- // change to "A op C+B"
- thisSide = bin.E0;
- thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Add, thatSide, bin.E1);
- ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Add;
- } else {
- // In principle, change to "-B op C-A" and then to "B dualOp A-C". But since we don't want
- // to return with the operator being > or >=, we instead end with "A-C op B" and switch the
- // mapping of thisSide/thatSide to e0/e1 (by inverting "whereIsBv").
- thisSide = bin.E1;
- thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, bin.E0, thatSide);
- ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
- whereIsBv = 1 - whereIsBv;
- }
- thatSide.Type = bin.Type;
- continue; // continue simplifying
+ whereIsBv = 1 - whereIsBv;
}
+ thatSide.Type = bin.Type;
+
+ } else {
+ break; // done simplifying
}
- break; // done simplifying
- default:
- break; // done simplifying
- }
- break; // done simplifying
+ }
+ break;
+
+ default:
+ break;
}
// Now, see if the interesting side is simply bv itself
@@ -2675,6 +2676,7 @@ namespace Microsoft.Dafny { b.ResolvedOp = newROp;
b.Type = Type.Bool;
yield return b;
+ yield break;
}
}
JUST_RETURN_IT: ;
|