diff options
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 72 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 12 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 12 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 8 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 6 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 6 |
6 files changed, 94 insertions, 22 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index ac688143..2d17af99 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -7,7 +7,6 @@ namespace Dafny public class Set<T>
{
Dictionary<T, bool> dict;
- public Set() { }
Set(Dictionary<T, bool> d) {
dict = d;
}
@@ -34,6 +33,35 @@ namespace Dafny return dict.Keys;
}
}
+ /// <summary>
+ /// This is an inefficient iterator for producing all subsets of "this". Each set returned is the same
+ /// Set<T> object (but this Set<T> object is fresh; in particular, it is not "this").
+ /// </summary>
+ public IEnumerable<Set<T>> AllSubsets {
+ get {
+ // Start by putting all set elements into a list
+ var elmts = new List<T>();
+ elmts.AddRange(dict.Keys);
+ var n = elmts.Count;
+ var which = new bool[n];
+ var s = new Set<T>(new Dictionary<T, bool>(0));
+ while (true) {
+ yield return s;
+ // "add 1" to "which", as if doing a carry chain. For every digit changed, change the membership of the corresponding element in "s".
+ int i = 0;
+ for (; i < n && which[i]; i++) {
+ which[i] = false;
+ s.dict.Remove(elmts[i]);
+ }
+ if (i == n) {
+ // we have cycled through all the subsets
+ break;
+ }
+ which[i] = true;
+ s.dict.Add(elmts[i], true);
+ }
+ }
+ }
public bool Equals(Set<T> other) {
return dict.Count == other.dict.Count && IsSubsetOf(other);
}
@@ -43,6 +71,15 @@ namespace Dafny public override int GetHashCode() {
return dict.GetHashCode();
}
+ public override string ToString() {
+ var s = "{";
+ var sep = "";
+ foreach (var t in dict.Keys) {
+ s += sep + t.ToString();
+ sep = ", ";
+ }
+ return s + "}";
+ }
public bool IsProperSubsetOf(Set<T> other) {
return dict.Count < other.dict.Count && IsSubsetOf(other);
}
@@ -136,7 +173,6 @@ namespace Dafny public class MultiSet<T>
{
Dictionary<T, int> dict;
- public MultiSet() { }
MultiSet(Dictionary<T, int> d) {
dict = d;
}
@@ -195,6 +231,18 @@ namespace Dafny public override int GetHashCode() {
return dict.GetHashCode();
}
+ public override string ToString() {
+ var s = "multiset{";
+ var sep = "";
+ foreach (var kv in dict) {
+ var t = kv.Key.ToString();
+ for (int i = 0; i < kv.Value; i++) {
+ s += sep + t.ToString();
+ sep = ", ";
+ }
+ }
+ return s + "}";
+ }
public bool IsProperSubsetOf(MultiSet<T> other) {
return !Equals(other) && IsSubsetOf(other);
}
@@ -293,7 +341,6 @@ namespace Dafny public class Map<U, V>
{
Dictionary<U, V> dict;
- public Map() { }
Map(Dictionary<U, V> d) {
dict = d;
}
@@ -342,6 +389,15 @@ namespace Dafny public override int GetHashCode() {
return dict.GetHashCode();
}
+ public override string ToString() {
+ var s = "map[";
+ var sep = "";
+ foreach (var kv in dict) {
+ s += sep + kv.Key.ToString() + " := " + kv.Value.ToString();
+ sep = ", ";
+ }
+ return s + "]";
+ }
public bool IsDisjointFrom(Map<U, V> other) {
foreach (U u in dict.Keys) {
if (other.dict.ContainsKey(u))
@@ -373,7 +429,6 @@ namespace Dafny public class Sequence<T>
{
T[] elmts;
- public Sequence() { }
public Sequence(T[] ee) {
elmts = ee;
}
@@ -417,6 +472,15 @@ namespace Dafny public override int GetHashCode() {
return elmts.GetHashCode();
}
+ public override string ToString() {
+ var s = "[";
+ var sep = "";
+ foreach (var t in elmts) {
+ s += sep + t.ToString();
+ sep = ", ";
+ }
+ return s + "]";
+ }
bool EqualUntil(Sequence<T> other, int n) {
for (int i = 0; i < n; i++) {
if (!elmts[i].Equals(other.elmts[i]))
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 66d8900c..29bcb4ff 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1068,9 +1068,12 @@ namespace Microsoft.Dafny { } else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
- if (s.MissingBounds != null) {
+ if (s.AssumeToken != null) {
+ // Note, a non-ghost AssignSuchThatStmt may contain an assume
+ Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);
+ } else if (s.MissingBounds != null) {
foreach (var bv in s.MissingBounds) {
- Error("this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", bv.Name, bv.Tok.line);
+ Error("this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", bv.Name, s.Tok.line);
}
} else {
Contract.Assume(s.Bounds != null);
@@ -1128,6 +1131,11 @@ namespace Microsoft.Dafny { wr.Write("foreach (var {0} in (", tmpVar);
TrExpr(b.Set);
wr.WriteLine(").Elements) {{ @{0} = {1};", bv.CompileName, tmpVar);
+ } else if (bound is ComprehensionExpr.SubSetBoundedPool) {
+ var b = (ComprehensionExpr.SubSetBoundedPool)bound;
+ wr.Write("foreach (var {0} in (", tmpVar);
+ TrExpr(b.UpperBound);
+ wr.WriteLine(").AllSubsets) {{ @{0} = {1};", bv.CompileName, tmpVar);
} else if (bound is ComprehensionExpr.MapBoundedPool) {
var b = (ComprehensionExpr.MapBoundedPool)bound;
wr.Write("foreach (var {0} in (", tmpVar);
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ce0ea857..7ee244cf 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4362,6 +4362,9 @@ namespace Microsoft.Dafny { public readonly Attributes Attributes;
public abstract class BoundedPool { }
+ public class BoolBoundedPool : BoundedPool
+ {
+ }
public class IntBoundedPool : BoundedPool
{
public readonly Expression LowerBound;
@@ -4376,10 +4379,10 @@ namespace Microsoft.Dafny { public readonly Expression Set;
public SetBoundedPool(Expression set) { Set = set; }
}
- public class SuperSetBoundedPool : BoundedPool
+ public class SubSetBoundedPool : BoundedPool
{
- public readonly Expression LowerBound;
- public SuperSetBoundedPool(Expression set) { LowerBound = set; }
+ public readonly Expression UpperBound;
+ public SubSetBoundedPool(Expression set) { UpperBound = set; }
}
public class MapBoundedPool : BoundedPool
{
@@ -4391,9 +4394,6 @@ namespace Microsoft.Dafny { public readonly Expression Seq;
public SeqBoundedPool(Expression seq) { Seq = seq; }
}
- public class BoolBoundedPool : BoundedPool
- {
- }
public class DatatypeBoundedPool : BoundedPool
{
public readonly DatatypeDecl Decl;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 1188fa94..c70c039d 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6344,7 +6344,7 @@ namespace Microsoft.Dafny /// 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 SuperSetBoundedPool is returned
+ /// -- no SubSetBoundedPool is returned
/// If "returnAllBounds" is true, then:
/// -- a variable may give rise to several BoundedPool's
/// -- IntBoundedPool bounds may have just one component
@@ -6410,8 +6410,8 @@ namespace Microsoft.Dafny }
break;
case BinaryExpr.ResolvedOpcode.Subset:
- if (returnAllBounds && whereIsBv == 1) {
- bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(e0));
+ if (returnAllBounds && whereIsBv == 0) {
+ bounds.Add(new ComprehensionExpr.SubSetBoundedPool(e1));
foundBoundsForBv = true;
}
break;
@@ -6444,7 +6444,7 @@ namespace Microsoft.Dafny if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
} else if (returnAllBounds && bv.Type is SetType) {
var otherOperand = whereIsBv == 0 ? e1 : e0;
- bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(otherOperand));
+ bounds.Add(new ComprehensionExpr.SubSetBoundedPool(otherOperand));
foundBoundsForBv = true;
}
break;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index bda97426..8acc14d0 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5119,9 +5119,9 @@ namespace Microsoft.Dafny { var bnd = (ComprehensionExpr.IntBoundedPool)bound;
if (bnd.LowerBound != null) yield return bnd.LowerBound;
if (bnd.UpperBound != null) yield return Resolver.Minus(bnd.UpperBound, 1);
- } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {
- var bnd = (ComprehensionExpr.SuperSetBoundedPool)bound;
- yield return bnd.LowerBound;
+ } else if (bound is ComprehensionExpr.SubSetBoundedPool) {
+ var bnd = (ComprehensionExpr.SubSetBoundedPool)bound;
+ yield return bnd.UpperBound;
} else if (bound is ComprehensionExpr.SetBoundedPool) {
var st = ((ComprehensionExpr.SetBoundedPool)bound).Set.Resolved;
if (st is DisplayExpression) {
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 7b88d0d4..75a42200 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -584,8 +584,8 @@ method AssignSuchThat6() }
method AssignSuchThat7<T>(A: set<T>, x: T) {
- var B :| A <= B;
- assert x in A ==> x in B;
+ var B :| B <= A;
+ assert x in B ==> x in A;
}
method AssignSuchThat8(n: int) returns (x: int, y: Lindgren) {
@@ -625,7 +625,7 @@ method LetSuchThat0(ghost g: int) method LetSuchThat1<T>(A: set<T>)
{
- ghost var C := var B :| A <= B; A - B;
+ ghost var C := var B :| B <= A; B - A;
assert C == {};
}
|