summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/DafnyPrelude.bpl104
-rw-r--r--Binaries/DafnyRuntime.cs2238
-rw-r--r--Binaries/System.Collections.Immutable.dllbin0 -> 149752 bytes
-rwxr-xr-xBinaries/dafny16
-rwxr-xr-xBinaries/dafny-server16
-rw-r--r--Binaries/z3.exebin6343680 -> 10647552 bytes
6 files changed, 1458 insertions, 916 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 74bdb63e..2ca10f73 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -20,6 +20,7 @@ const unique TInt : Ty;
const unique TNat : Ty;
const unique TReal : Ty;
function TSet(Ty) : Ty;
+function TISet(Ty) : Ty;
function TMultiSet(Ty) : Ty;
function TSeq(Ty) : Ty;
function TMap(Ty, Ty) : Ty;
@@ -27,6 +28,8 @@ function TIMap(Ty, Ty) : Ty;
function Inv0_TSet(Ty) : Ty;
axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t);
+function Inv0_TISet(Ty) : Ty;
+axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t);
function Inv0_TSeq(Ty) : Ty;
axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t);
function Inv0_TMultiSet(Ty) : Ty;
@@ -52,6 +55,7 @@ const unique TagInt : TyTag;
const unique TagNat : TyTag;
const unique TagReal : TyTag;
const unique TagSet : TyTag;
+const unique TagISet : TyTag;
const unique TagMultiSet : TyTag;
const unique TagSeq : TyTag;
const unique TagMap : TyTag;
@@ -64,6 +68,7 @@ axiom Tag(TInt) == TagInt;
axiom Tag(TNat) == TagNat;
axiom Tag(TReal) == TagReal;
axiom (forall t: Ty :: { TSet(t) } Tag(TSet(t)) == TagSet);
+axiom (forall t: Ty :: { TISet(t) } Tag(TISet(t)) == TagISet);
axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet);
axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq);
axiom (forall t, u: Ty :: { TMap(t,u) } Tag(TMap(t,u)) == TagMap);
@@ -138,6 +143,9 @@ axiom (forall bx : Box, t : Ty ::
{ $IsBox(bx, TSet(t)) }
( $IsBox(bx, TSet(t)) ==> $Box($Unbox(bx) : Set Box) == bx && $Is($Unbox(bx) : Set Box, TSet(t))));
axiom (forall bx : Box, t : Ty ::
+ { $IsBox(bx, TISet(t)) }
+ ( $IsBox(bx, TISet(t)) ==> $Box($Unbox(bx) : ISet Box) == bx && $Is($Unbox(bx) : ISet Box, TISet(t))));
+axiom (forall bx : Box, t : Ty ::
{ $IsBox(bx, TMultiSet(t)) }
( $IsBox(bx, TMultiSet(t)) ==> $Box($Unbox(bx) : MultiSet Box) == bx && $Is($Unbox(bx) : MultiSet Box, TMultiSet(t))));
axiom (forall bx : Box, t : Ty ::
@@ -187,6 +195,10 @@ axiom (forall v: Set Box, t0: Ty :: { $Is(v, TSet(t0)) }
$Is(v, TSet(t0)) <==>
(forall bx: Box :: { v[bx] }
v[bx] ==> $IsBox(bx, t0)));
+axiom (forall v: ISet Box, t0: Ty :: { $Is(v, TISet(t0)) }
+ $Is(v, TISet(t0)) <==>
+ (forall bx: Box :: { v[bx] }
+ v[bx] ==> $IsBox(bx, t0)));
axiom (forall v: MultiSet Box, t0: Ty :: { $Is(v, TMultiSet(t0)) }
$Is(v, TMultiSet(t0)) <==>
(forall bx: Box :: { v[bx] }
@@ -202,6 +214,10 @@ axiom (forall v: Set Box, t0: Ty, h: Heap :: { $IsAlloc(v, TSet(t0), h) }
$IsAlloc(v, TSet(t0), h) <==>
(forall bx: Box :: { v[bx] }
v[bx] ==> $IsAllocBox(bx, t0, h)));
+axiom (forall v: ISet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TISet(t0), h) }
+ $IsAlloc(v, TISet(t0), h) <==>
+ (forall bx: Box :: { v[bx] }
+ v[bx] ==> $IsAllocBox(bx, t0, h)));
axiom (forall v: MultiSet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TMultiSet(t0), h) }
$IsAlloc(v, TMultiSet(t0), h) <==>
(forall bx: Box :: { v[bx] }
@@ -257,6 +273,8 @@ const unique class._System.set: ClassName;
const unique class._System.seq: ClassName;
const unique class._System.multiset: ClassName;
+function Tclass._System.object(): Ty;
+
function /*{:never_pattern true}*/ dtype(ref): Ty; // changed from ClassName to Ty
function TypeTuple(a: ClassName, b: ClassName): ClassName;
@@ -271,6 +289,12 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }
type HandleType;
+function SetRef_to_SetBox(s: [ref]bool): Set Box;
+axiom (forall s: [ref]bool, bx: Box :: { SetRef_to_SetBox(s)[bx] }
+ SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]);
+axiom (forall s: [ref]bool :: { SetRef_to_SetBox(s) }
+ $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object())));
+
// ---------------------------------------------------------------
// -- Datatypes --------------------------------------------------
// ---------------------------------------------------------------
@@ -382,7 +406,8 @@ function {:inline true} read<alpha>(H:Heap, r:ref, f:Field alpha): alpha { H[r,
function {:inline true} update<alpha>(H:Heap, r:ref, f:Field alpha, v:alpha): Heap { H[r,f := v] }
function $IsGoodHeap(Heap): bool;
-var $Heap: Heap where $IsGoodHeap($Heap);
+function $IsHeapAnchor(Heap): bool;
+var $Heap: Heap where $IsGoodHeap($Heap) && $IsHeapAnchor($Heap);
function $HeapSucc(Heap, Heap): bool;
axiom (forall<alpha> h: Heap, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) }
@@ -545,6 +570,81 @@ axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a,b) }
Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));
// ---------------------------------------------------------------
+// -- Axiomatization of isets -------------------------------------
+// ---------------------------------------------------------------
+
+type ISet T = [T]bool;
+
+function ISet#Empty<T>(): Set T;
+axiom (forall<T> o: T :: { ISet#Empty()[o] } !ISet#Empty()[o]);
+
+// the empty set could be of anything
+//axiom (forall<T> t: Ty :: { $Is(ISet#Empty() : [T]bool, TISet(t)) } $Is(ISet#Empty() : [T]bool, TISet(t)));
+
+
+function ISet#UnionOne<T>(ISet T, T): ISet T;
+axiom (forall<T> a: ISet T, x: T, o: T :: { ISet#UnionOne(a,x)[o] }
+ ISet#UnionOne(a,x)[o] <==> o == x || a[o]);
+axiom (forall<T> a: ISet T, x: T :: { ISet#UnionOne(a, x) }
+ ISet#UnionOne(a, x)[x]);
+axiom (forall<T> a: ISet T, x: T, y: T :: { ISet#UnionOne(a, x), a[y] }
+ a[y] ==> ISet#UnionOne(a, x)[y]);
+
+function ISet#Union<T>(ISet T, ISet T): ISet T;
+axiom (forall<T> a: ISet T, b: ISet T, o: T :: { ISet#Union(a,b)[o] }
+ ISet#Union(a,b)[o] <==> a[o] || b[o]);
+axiom (forall<T> a, b: ISet T, y: T :: { ISet#Union(a, b), a[y] }
+ a[y] ==> ISet#Union(a, b)[y]);
+axiom (forall<T> a, b: Set T, y: T :: { ISet#Union(a, b), b[y] }
+ b[y] ==> ISet#Union(a, b)[y]);
+axiom (forall<T> a, b: ISet T :: { ISet#Union(a, b) }
+ ISet#Disjoint(a, b) ==>
+ ISet#Difference(ISet#Union(a, b), a) == b &&
+ ISet#Difference(ISet#Union(a, b), b) == a);
+// Follows from the general union axiom, but might be still worth including, because disjoint union is a common case:
+// axiom (forall<T> a, b: ISet T :: { ISet#Card(ISet#Union(a, b)) }
+// ISet#Disjoint(a, b) ==>
+// ISet#Card(ISet#Union(a, b)) == ISet#Card(a) + ISet#Card(b));
+
+function ISet#Intersection<T>(ISet T, ISet T): ISet T;
+axiom (forall<T> a: ISet T, b: ISet T, o: T :: { ISet#Intersection(a,b)[o] }
+ ISet#Intersection(a,b)[o] <==> a[o] && b[o]);
+
+axiom (forall<T> a, b: ISet T :: { ISet#Union(ISet#Union(a, b), b) }
+ ISet#Union(ISet#Union(a, b), b) == ISet#Union(a, b));
+axiom (forall<T> a, b: Set T :: { ISet#Union(a, ISet#Union(a, b)) }
+ ISet#Union(a, ISet#Union(a, b)) == ISet#Union(a, b));
+axiom (forall<T> a, b: ISet T :: { ISet#Intersection(ISet#Intersection(a, b), b) }
+ ISet#Intersection(ISet#Intersection(a, b), b) == ISet#Intersection(a, b));
+axiom (forall<T> a, b: ISet T :: { ISet#Intersection(a, ISet#Intersection(a, b)) }
+ ISet#Intersection(a, ISet#Intersection(a, b)) == ISet#Intersection(a, b));
+
+
+function ISet#Difference<T>(ISet T, ISet T): ISet T;
+axiom (forall<T> a: ISet T, b: ISet T, o: T :: { ISet#Difference(a,b)[o] }
+ ISet#Difference(a,b)[o] <==> a[o] && !b[o]);
+axiom (forall<T> a, b: ISet T, y: T :: { ISet#Difference(a, b), b[y] }
+ b[y] ==> !ISet#Difference(a, b)[y] );
+
+function ISet#Subset<T>(ISet T, ISet T): bool;
+axiom(forall<T> a: ISet T, b: ISet T :: { ISet#Subset(a,b) }
+ ISet#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o]));
+// axiom(forall<T> a: ISet T, b: ISet T ::
+// { ISet#Subset(a,b), ISet#Card(a), ISet#Card(b) } // very restrictive trigger
+// ISet#Subset(a,b) ==> ISet#Card(a) <= ISet#Card(b));
+
+
+function ISet#Equal<T>(ISet T, ISet T): bool;
+axiom(forall<T> a: ISet T, b: ISet T :: { ISet#Equal(a,b) }
+ ISet#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o]));
+axiom(forall<T> a: ISet T, b: ISet T :: { ISet#Equal(a,b) } // extensionality axiom for sets
+ ISet#Equal(a,b) ==> a == b);
+
+function ISet#Disjoint<T>(ISet T, ISet T): bool;
+axiom (forall<T> a: ISet T, b: ISet T :: { ISet#Disjoint(a,b) }
+ ISet#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));
+
+// ---------------------------------------------------------------
// -- Axiomatization of multisets --------------------------------
// ---------------------------------------------------------------
@@ -745,7 +845,7 @@ function Seq#Contains<T>(Seq T, T): bool;
axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
Seq#Contains(s,x) <==>
(exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));
-axiom (forall x: ref ::
+axiom (forall<T> x: T ::
{ Seq#Contains(Seq#Empty(), x) }
!Seq#Contains(Seq#Empty(), x));
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index fd680a0b..587d5159 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -1,914 +1,1324 @@
-using System; // for Func
-using System.Numerics;
-
-namespace Dafny
-{
- using System.Collections.Generic;
-
- public class Set<T>
- {
- Dictionary<T, bool> dict;
- Set(Dictionary<T, bool> d) {
- dict = d;
- }
- public static Set<T> Empty {
- get {
- return new Set<T>(new Dictionary<T, bool>(0));
- }
- }
- public static Set<T> FromElements(params T[] values) {
- Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
- foreach (T t in values)
- d[t] = true;
- return new Set<T>(d);
- }
- public static Set<T> FromCollection(ICollection<T> values) {
- Dictionary<T, bool> d = new Dictionary<T, bool>();
- foreach (T t in values)
- d[t] = true;
- return new Set<T>(d);
- }
- public int Length {
- get { return dict.Count; }
- }
- public long LongLength {
- get { return dict.Count; }
- }
- public IEnumerable<T> Elements {
- get {
- 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);
- }
- public override bool Equals(object other) {
- return other is Set<T> && Equals((Set<T>)other);
- }
- public override int GetHashCode() {
- var hashCode = 1;
- foreach (var t in dict.Keys) {
- hashCode = hashCode * (t.GetHashCode()+3);
- }
- return hashCode;
- }
- 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);
- }
- public bool IsSubsetOf(Set<T> other) {
- if (other.dict.Count < dict.Count)
- return false;
- foreach (T t in dict.Keys) {
- if (!other.dict.ContainsKey(t))
- return false;
- }
- return true;
- }
- public bool IsSupersetOf(Set<T> other) {
- return other.IsSubsetOf(this);
- }
- public bool IsProperSupersetOf(Set<T> other) {
- return other.IsProperSubsetOf(this);
- }
- public bool IsDisjointFrom(Set<T> other) {
- Dictionary<T, bool> a, b;
- if (dict.Count < other.dict.Count) {
- a = dict; b = other.dict;
- } else {
- a = other.dict; b = dict;
- }
- foreach (T t in a.Keys) {
- if (b.ContainsKey(t))
- return false;
- }
- return true;
- }
- public bool Contains(T t) {
- return dict.ContainsKey(t);
- }
- public Set<T> Union(Set<T> other) {
- if (dict.Count == 0)
- return other;
- else if (other.dict.Count == 0)
- return this;
- Dictionary<T, bool> a, b;
- if (dict.Count < other.dict.Count) {
- a = dict; b = other.dict;
- } else {
- a = other.dict; b = dict;
- }
- Dictionary<T, bool> r = new Dictionary<T, bool>();
- foreach (T t in b.Keys)
- r[t] = true;
- foreach (T t in a.Keys)
- r[t] = true;
- return new Set<T>(r);
- }
- public Set<T> Intersect(Set<T> other) {
- if (dict.Count == 0)
- return this;
- else if (other.dict.Count == 0)
- return other;
- Dictionary<T, bool> a, b;
- if (dict.Count < other.dict.Count) {
- a = dict; b = other.dict;
- } else {
- a = other.dict; b = dict;
- }
- var r = new Dictionary<T, bool>();
- foreach (T t in a.Keys) {
- if (b.ContainsKey(t))
- r.Add(t, true);
- }
- return new Set<T>(r);
- }
- public Set<T> Difference(Set<T> other) {
- if (dict.Count == 0)
- return this;
- else if (other.dict.Count == 0)
- return this;
- var r = new Dictionary<T, bool>();
- foreach (T t in dict.Keys) {
- if (!other.dict.ContainsKey(t))
- r.Add(t, true);
- }
- return new Set<T>(r);
- }
- }
- public class MultiSet<T>
- {
- Dictionary<T, int> dict;
- MultiSet(Dictionary<T, int> d) {
- dict = d;
- }
- public static MultiSet<T> Empty {
- get {
- return new MultiSet<T>(new Dictionary<T, int>(0));
- }
- }
- public static MultiSet<T> FromElements(params T[] values) {
- Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
- foreach (T t in values) {
- var i = 0;
- if (!d.TryGetValue(t, out i)) {
- i = 0;
- }
- d[t] = i + 1;
- }
- return new MultiSet<T>(d);
- }
- public static MultiSet<T> FromCollection(ICollection<T> values) {
- Dictionary<T, int> d = new Dictionary<T, int>();
- foreach (T t in values) {
- var i = 0;
- if (!d.TryGetValue(t, out i)) {
- i = 0;
- }
- d[t] = i + 1;
- }
- return new MultiSet<T>(d);
- }
- public static MultiSet<T> FromSeq(Sequence<T> values) {
- Dictionary<T, int> d = new Dictionary<T, int>();
- foreach (T t in values.Elements) {
- var i = 0;
- if (!d.TryGetValue(t, out i)) {
- i = 0;
- }
- d[t] = i + 1;
- }
- return new MultiSet<T>(d);
- }
- public static MultiSet<T> FromSet(Set<T> values) {
- Dictionary<T, int> d = new Dictionary<T, int>();
- foreach (T t in values.Elements) {
- d[t] = 1;
- }
- return new MultiSet<T>(d);
- }
-
- public bool Equals(MultiSet<T> other) {
- return other.IsSubsetOf(this) && this.IsSubsetOf(other);
- }
- public override bool Equals(object other) {
- return other is MultiSet<T> && Equals((MultiSet<T>)other);
- }
- public override int GetHashCode() {
- var hashCode = 1;
- foreach (var kv in dict) {
- var key = kv.Key.GetHashCode();
- key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
- hashCode = hashCode * (key + 3);
- }
- return hashCode;
- }
- 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);
- }
- public bool IsSubsetOf(MultiSet<T> other) {
- foreach (T t in dict.Keys) {
- if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
- return false;
- }
- return true;
- }
- public bool IsSupersetOf(MultiSet<T> other) {
- return other.IsSubsetOf(this);
- }
- public bool IsProperSupersetOf(MultiSet<T> other) {
- return other.IsProperSubsetOf(this);
- }
- public bool IsDisjointFrom(MultiSet<T> other) {
- foreach (T t in dict.Keys) {
- if (other.dict.ContainsKey(t))
- return false;
- }
- foreach (T t in other.dict.Keys) {
- if (dict.ContainsKey(t))
- return false;
- }
- return true;
- }
- public bool Contains(T t) {
- return dict.ContainsKey(t);
- }
- public MultiSet<T> Union(MultiSet<T> other) {
- if (dict.Count == 0)
- return other;
- else if (other.dict.Count == 0)
- return this;
- var r = new Dictionary<T, int>();
- foreach (T t in dict.Keys) {
- var i = 0;
- if (!r.TryGetValue(t, out i)) {
- i = 0;
- }
- r[t] = i + dict[t];
- }
- foreach (T t in other.dict.Keys) {
- var i = 0;
- if (!r.TryGetValue(t, out i)) {
- i = 0;
- }
- r[t] = i + other.dict[t];
- }
- return new MultiSet<T>(r);
- }
- public MultiSet<T> Intersect(MultiSet<T> other) {
- if (dict.Count == 0)
- return this;
- else if (other.dict.Count == 0)
- return other;
- var r = new Dictionary<T, int>();
- foreach (T t in dict.Keys) {
- if (other.dict.ContainsKey(t)) {
- r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
- }
- }
- return new MultiSet<T>(r);
- }
- public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
- if (dict.Count == 0)
- return this;
- else if (other.dict.Count == 0)
- return this;
- var r = new Dictionary<T, int>();
- foreach (T t in dict.Keys) {
- if (!other.dict.ContainsKey(t)) {
- r.Add(t, dict[t]);
- } else if (other.dict[t] < dict[t]) {
- r.Add(t, dict[t] - other.dict[t]);
- }
- }
- return new MultiSet<T>(r);
- }
- public IEnumerable<T> Elements {
- get {
- List<T> l = new List<T>();
- foreach (T t in dict.Keys) {
- int n;
- dict.TryGetValue(t, out n);
- for (int i = 0; i < n; i ++) {
- l.Add(t);
- }
- }
- return l;
- }
- }
- }
-
- public class Map<U, V>
- {
- Dictionary<U, V> dict;
- Map(Dictionary<U, V> d) {
- dict = d;
- }
- public static Map<U, V> Empty {
- get {
- return new Map<U, V>(new Dictionary<U,V>());
- }
- }
- public static Map<U, V> FromElements(params Pair<U, V>[] values) {
- Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
- foreach (Pair<U, V> p in values) {
- d[p.Car] = p.Cdr;
- }
- return new Map<U, V>(d);
- }
- public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
- Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
- foreach (Pair<U, V> p in values) {
- d[p.Car] = p.Cdr;
- }
- return new Map<U, V>(d);
- }
- public int Length {
- get { return dict.Count; }
- }
- public long LongLength {
- get { return dict.Count; }
- }
- public bool Equals(Map<U, V> other) {
- foreach (U u in dict.Keys) {
- V v1, v2;
- if (!dict.TryGetValue(u, out v1)) {
- return false; // this shouldn't happen
- }
- if (!other.dict.TryGetValue(u, out v2)) {
- return false; // other dictionary does not contain this element
- }
- if (!v1.Equals(v2)) {
- return false;
- }
- }
- foreach (U u in other.dict.Keys) {
- if (!dict.ContainsKey(u)) {
- return false; // this shouldn't happen
- }
- }
- return true;
- }
- public override bool Equals(object other) {
- return other is Map<U, V> && Equals((Map<U, V>)other);
- }
- public override int GetHashCode() {
- var hashCode = 1;
- foreach (var kv in dict) {
- var key = kv.Key.GetHashCode();
- key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
- hashCode = hashCode * (key + 3);
- }
- return hashCode;
- }
- 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))
- return false;
- }
- foreach (U u in other.dict.Keys) {
- if (dict.ContainsKey(u))
- return false;
- }
- return true;
- }
- public bool Contains(U u) {
- return dict.ContainsKey(u);
- }
- public V Select(U index) {
- return dict[index];
- }
- public Map<U, V> Update(U index, V val) {
- Dictionary<U, V> d = new Dictionary<U, V>(dict);
- d[index] = val;
- return new Map<U, V>(d);
- }
- public IEnumerable<U> Domain {
- get {
- return dict.Keys;
- }
- }
- }
- public class Sequence<T>
- {
- T[] elmts;
- public Sequence(T[] ee) {
- elmts = ee;
- }
- public static Sequence<T> Empty {
- get {
- return new Sequence<T>(new T[0]);
- }
- }
- public static Sequence<T> FromElements(params T[] values) {
- return new Sequence<T>(values);
- }
- public static Sequence<char> FromString(string s) {
- return new Sequence<char>(s.ToCharArray());
- }
- public int Length {
- get { return elmts.Length; }
- }
- public long LongLength {
- get { return elmts.LongLength; }
- }
- public T[] Elements {
- get {
- return elmts;
- }
- }
- public IEnumerable<T> UniqueElements {
- get {
- var st = Set<T>.FromElements(elmts);
- return st.Elements;
- }
- }
- public T Select(ulong index) {
- return elmts[index];
- }
- public T Select(long index) {
- return elmts[index];
- }
- public T Select(uint index) {
- return elmts[index];
- }
- public T Select(int index) {
- return elmts[index];
- }
- public T Select(BigInteger index) {
- return elmts[(int)index];
- }
- public Sequence<T> Update(long index, T t) {
- T[] a = (T[])elmts.Clone();
- a[index] = t;
- return new Sequence<T>(a);
- }
- public Sequence<T> Update(ulong index, T t) {
- return Update((long)index, t);
- }
- public Sequence<T> Update(BigInteger index, T t) {
- return Update((long)index, t);
- }
- public bool Equals(Sequence<T> other) {
- int n = elmts.Length;
- return n == other.elmts.Length && EqualUntil(other, n);
- }
- public override bool Equals(object other) {
- return other is Sequence<T> && Equals((Sequence<T>)other);
- }
- public override int GetHashCode() {
- if (elmts == null || elmts.Length == 0)
- return 0;
- var hashCode = 0;
- for (var i = 0; i < elmts.Length; i++) {
- hashCode = (hashCode << 3) | (hashCode >> 29) ^ elmts[i].GetHashCode();
- }
- return hashCode;
- }
- public override string ToString() {
- if (elmts is char[]) {
- var s = "";
- foreach (var t in elmts) {
- s += t.ToString();
- }
- return s;
- } else {
- 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]))
- return false;
- }
- return true;
- }
- public bool IsProperPrefixOf(Sequence<T> other) {
- int n = elmts.Length;
- return n < other.elmts.Length && EqualUntil(other, n);
- }
- public bool IsPrefixOf(Sequence<T> other) {
- int n = elmts.Length;
- return n <= other.elmts.Length && EqualUntil(other, n);
- }
- public Sequence<T> Concat(Sequence<T> other) {
- if (elmts.Length == 0)
- return other;
- else if (other.elmts.Length == 0)
- return this;
- T[] a = new T[elmts.Length + other.elmts.Length];
- System.Array.Copy(elmts, 0, a, 0, elmts.Length);
- System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
- return new Sequence<T>(a);
- }
- public bool Contains(T t) {
- int n = elmts.Length;
- for (int i = 0; i < n; i++) {
- if (t.Equals(elmts[i]))
- return true;
- }
- return false;
- }
- public Sequence<T> Take(long m) {
- if (elmts.LongLength == m)
- return this;
- T[] a = new T[m];
- System.Array.Copy(elmts, a, m);
- return new Sequence<T>(a);
- }
- public Sequence<T> Take(ulong n) {
- return Take((long)n);
- }
- public Sequence<T> Take(BigInteger n) {
- return Take((long)n);
- }
- public Sequence<T> Drop(long m) {
- if (m == 0)
- return this;
- T[] a = new T[elmts.Length - m];
- System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
- return new Sequence<T>(a);
- }
- public Sequence<T> Drop(ulong n) {
- return Drop((long)n);
- }
- public Sequence<T> Drop(BigInteger n) {
- if (n.IsZero)
- return this;
- return Drop((long)n);
- }
- }
- public struct Pair<A, B>
- {
- public readonly A Car;
- public readonly B Cdr;
- public Pair(A a, B b) {
- this.Car = a;
- this.Cdr = b;
- }
- }
- public partial class Helpers {
- // Computing forall/exists quantifiers
- public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
- if (frall) {
- return pred(false) && pred(true);
- } else {
- return pred(false) || pred(true);
- }
- }
- public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
- for (BigInteger i = lo; i < hi; i++) {
- if (pred(i) != frall) { return !frall; }
- }
- return frall;
- }
- public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
- foreach (var u in set.Elements) {
- if (pred(u) != frall) { return !frall; }
- }
- return frall;
- }
- public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
- foreach (var u in map.Domain) {
- if (pred(u) != frall) { return !frall; }
- }
- return frall;
- }
- public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
- foreach (var u in seq.Elements) {
- if (pred(u) != frall) { return !frall; }
- }
- return frall;
- }
- public static bool QuantDatatype<U>(IEnumerable<U> set, bool frall, System.Predicate<U> pred) {
- foreach (var u in set) {
- if (pred(u) != frall) { return !frall; }
- }
- return frall;
- }
- // Enumerating other collections
- public delegate Dafny.Set<T> ComprehensionDelegate<T>();
- public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
- public static IEnumerable<bool> AllBooleans {
- get {
- yield return false;
- yield return true;
- }
- }
- public static IEnumerable<BigInteger> AllIntegers {
- get {
- yield return new BigInteger(0);
- for (var j = new BigInteger(1);; j++) {
- yield return j;
- yield return -j;
- }
- }
- }
- // pre: b != 0
- // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
- public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) {
- return (sbyte)EuclideanDivision_int(a, b);
- }
- public static short EuclideanDivision_short(short a, short b) {
- return (short)EuclideanDivision_int(a, b);
- }
- public static int EuclideanDivision_int(int a, int b) {
- if (0 <= a) {
- if (0 <= b) {
- // +a +b: a/b
- return (int)(((uint)(a)) / ((uint)(b)));
- } else {
- // +a -b: -(a/(-b))
- return -((int)(((uint)(a)) / ((uint)(unchecked(-b)))));
- }
- } else {
- if (0 <= b) {
- // -a +b: -((-a-1)/b) - 1
- return -((int)(((uint)(-(a + 1))) / ((uint)(b)))) - 1;
- } else {
- // -a -b: ((-a-1)/(-b)) + 1
- return ((int)(((uint)(-(a + 1))) / ((uint)(unchecked(-b))))) + 1;
- }
- }
- }
- public static long EuclideanDivision_long(long a, long b) {
- if (0 <= a) {
- if (0 <= b) {
- // +a +b: a/b
- return (long)(((ulong)(a)) / ((ulong)(b)));
- } else {
- // +a -b: -(a/(-b))
- return -((long)(((ulong)(a)) / ((ulong)(unchecked(-b)))));
- }
- } else {
- if (0 <= b) {
- // -a +b: -((-a-1)/b) - 1
- return -((long)(((ulong)(-(a + 1))) / ((ulong)(b)))) - 1;
- } else {
- // -a -b: ((-a-1)/(-b)) + 1
- return ((long)(((ulong)(-(a + 1))) / ((ulong)(unchecked(-b))))) + 1;
- }
- }
- }
- public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
- if (0 <= a.Sign) {
- if (0 <= b.Sign) {
- // +a +b: a/b
- return BigInteger.Divide(a, b);
- } else {
- // +a -b: -(a/(-b))
- return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
- }
- } else {
- if (0 <= b.Sign) {
- // -a +b: -((-a-1)/b) - 1
- return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
- } else {
- // -a -b: ((-a-1)/(-b)) + 1
- return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
- }
- }
- }
- // pre: b != 0
- // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
- public static sbyte EuclideanModulus_sbyte(sbyte a, sbyte b) {
- return (sbyte)EuclideanModulus_int(a, b);
- }
- public static short EuclideanModulus_short(short a, short b) {
- return (short)EuclideanModulus_int(a, b);
- }
- public static int EuclideanModulus_int(int a, int b) {
- uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b));
- if (0 <= a) {
- // +a: a % b'
- return (int)(((uint)a) % bp);
- } else {
- // c = ((-a) % b')
- // -a: b' - c if c > 0
- // -a: 0 if c == 0
- uint c = ((uint)(unchecked(-a))) % bp;
- return (int)(c == 0 ? c : bp - c);
- }
- }
- public static long EuclideanModulus_long(long a, long b) {
- ulong bp = (0 <= b) ? (ulong)b : (ulong)(unchecked(-b));
- if (0 <= a) {
- // +a: a % b'
- return (long)(((ulong)a) % bp);
- } else {
- // c = ((-a) % b')
- // -a: b' - c if c > 0
- // -a: 0 if c == 0
- ulong c = ((ulong)(unchecked(-a))) % bp;
- return (long)(c == 0 ? c : bp - c);
- }
- }
- public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
- var bp = BigInteger.Abs(b);
- if (0 <= a.Sign) {
- // +a: a % b'
- return BigInteger.Remainder(a, bp);
- } else {
- // c = ((-a) % b')
- // -a: b' - c if c > 0
- // -a: 0 if c == 0
- var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
- return c.IsZero ? c : BigInteger.Subtract(bp, c);
- }
- }
- public static Sequence<T> SeqFromArray<T>(T[] array) {
- return new Sequence<T>(array);
- }
- // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
- // method if possible. Method "ExpressionSequence" would be a good candidate for it:
- // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
- public static U ExpressionSequence<T, U>(T t, U u)
- {
- return u;
- }
-
- public static U Let<T, U>(T t, Func<T,U> f) {
- return f(t);
- }
-
- public delegate Result Function<Input,Result>(Input input);
-
- public static A Id<A>(A a) {
- return a;
- }
- }
-
- public struct BigRational
- {
- public static readonly BigRational ZERO = new BigRational(0);
-
- BigInteger num, den; // invariant 1 <= den
- public override string ToString() {
- return string.Format("({0}.0 / {1}.0)", num, den);
- }
- public BigRational(int n) {
- num = new BigInteger(n);
- den = BigInteger.One;
- }
- public BigRational(BigInteger n, BigInteger d) {
- // requires 1 <= d
- num = n;
- den = d;
- }
- public BigInteger ToBigInteger() {
- if (0 <= num) {
- return num / den;
- } else {
- return (num - den + 1) / den;
- }
- }
- /// <summary>
- /// Returns values such that aa/dd == a and bb/dd == b.
- /// </summary>
- private static void Normalize(BigRational a, BigRational b, out BigInteger aa, out BigInteger bb, out BigInteger dd) {
- var gcd = BigInteger.GreatestCommonDivisor(a.den, b.den);
- var xx = a.den / gcd;
- var yy = b.den / gcd;
- // We now have a == a.num / (xx * gcd) and b == b.num / (yy * gcd).
- aa = a.num * yy;
- bb = b.num * xx;
- dd = a.den * yy;
- }
- public int CompareTo(BigRational that) {
- // simple things first
- int asign = this.num.Sign;
- int bsign = that.num.Sign;
- if (asign < 0 && 0 <= bsign) {
- return 1;
- } else if (asign <= 0 && 0 < bsign) {
- return 1;
- } else if (bsign < 0 && 0 <= asign) {
- return -1;
- } else if (bsign <= 0 && 0 < asign) {
- return -1;
- }
- BigInteger aa, bb, dd;
- Normalize(this, that, out aa, out bb, out dd);
- return aa.CompareTo(bb);
- }
- public override int GetHashCode() {
- return num.GetHashCode() + 29 * den.GetHashCode();
- }
- public override bool Equals(object obj) {
- if (obj is BigRational) {
- return this == (BigRational)obj;
- } else {
- return false;
- }
- }
- public static bool operator ==(BigRational a, BigRational b) {
- return a.CompareTo(b) == 0;
- }
- public static bool operator !=(BigRational a, BigRational b) {
- return a.CompareTo(b) != 0;
- }
- public static bool operator >(BigRational a, BigRational b) {
- return 0 < a.CompareTo(b);
- }
- public static bool operator >=(BigRational a, BigRational b) {
- return 0 <= a.CompareTo(b);
- }
- public static bool operator <(BigRational a, BigRational b) {
- return a.CompareTo(b) < 0;
- }
- public static bool operator <=(BigRational a, BigRational b) {
- return a.CompareTo(b) <= 0;
- }
- public static BigRational operator +(BigRational a, BigRational b) {
- BigInteger aa, bb, dd;
- Normalize(a, b, out aa, out bb, out dd);
- return new BigRational(aa + bb, dd);
- }
- public static BigRational operator -(BigRational a, BigRational b) {
- BigInteger aa, bb, dd;
- Normalize(a, b, out aa, out bb, out dd);
- return new BigRational(aa - bb, dd);
- }
- public static BigRational operator -(BigRational a) {
- return new BigRational(-a.num, a.den);
- }
- public static BigRational operator *(BigRational a, BigRational b) {
- return new BigRational(a.num * b.num, a.den * b.den);
- }
- public static BigRational operator /(BigRational a, BigRational b) {
- // Compute the reciprocal of b
- BigRational bReciprocal;
- if (0 < b.num) {
- bReciprocal = new BigRational(b.den, b.num);
- } else {
- // this is the case b.num < 0
- bReciprocal = new BigRational(-b.den, -b.num);
- }
- return a * bReciprocal;
- }
- }
-}
+using System; // for Func
+using System.Numerics;
+
+namespace Dafny
+{
+ using System.Collections.Generic;
+// set this option if you want to use System.Collections.Immutable and if you know what you're doing.
+#if DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE
+ using System.Collections.Immutable;
+ using System.Linq;
+
+ public class Set<T>
+ {
+ readonly ImmutableHashSet<T> setImpl;
+ Set(ImmutableHashSet<T> d) {
+ this.setImpl = d;
+ }
+ public static readonly Set<T> Empty = new Set<T>(ImmutableHashSet<T>.Empty);
+ public static Set<T> FromElements(params T[] values) {
+ return FromElements((IEnumerable<T>)values);
+ }
+ public static Set<T> FromElements(IEnumerable<T> values) {
+ var d = ImmutableHashSet<T>.Empty.ToBuilder();
+ foreach (T t in values)
+ d.Add(t);
+ return new Set<T>(d.ToImmutable());
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ var d = ImmutableHashSet<T>.Empty.ToBuilder();
+ foreach (T t in values)
+ d.Add(t);
+ return new Set<T>(d.ToImmutable());
+ }
+ public int Length {
+ get { return this.setImpl.Count; }
+ }
+ public long LongLength {
+ get { return this.setImpl.Count; }
+ }
+ public IEnumerable<T> Elements {
+ get {
+ return this.setImpl;
+ }
+ }
+ /// <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(this.setImpl);
+ var n = elmts.Count;
+ var which = new bool[n];
+ var s = ImmutableHashSet<T>.Empty.ToBuilder();
+ while (true) {
+ yield return new Set<T>(s.ToImmutable());
+ // "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.Remove(elmts[i]);
+ }
+ if (i == n) {
+ // we have cycled through all the subsets
+ break;
+ }
+ which[i] = true;
+ s.Add(elmts[i]);
+ }
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return this.setImpl.SetEquals(other.setImpl);
+ }
+ public override bool Equals(object other) {
+ var otherSet = other as Set<T>;
+ return otherSet != null && this.Equals(otherSet);
+ }
+ public override int GetHashCode() {
+ var hashCode = 1;
+ foreach (var t in this.setImpl) {
+ hashCode = hashCode * (t.GetHashCode()+3);
+ }
+ return hashCode;
+ }
+ public override string ToString() {
+ var s = "{";
+ var sep = "";
+ foreach (var t in this.setImpl) {
+ s += sep + t.ToString();
+ sep = ", ";
+ }
+ return s + "}";
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return IsProperSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ return IsSubsetOf(other);
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSupersetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSupersetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ ImmutableHashSet<T> a, b;
+ if (this.setImpl.Count < other.setImpl.Count) {
+ a = this.setImpl; b = other.setImpl;
+ } else {
+ a = other.setImpl; b = this.setImpl;
+ }
+ foreach (T t in a) {
+ if (b.Contains(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return this.setImpl.Contains(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ return new Set<T>(this.setImpl.Union(other.setImpl));
+ }
+ public Set<T> Intersect(Set<T> other) {
+ return new Set<T>(this.setImpl.Intersect(other.setImpl));
+ }
+ public Set<T> Difference(Set<T> other) {
+ return new Set<T>(this.setImpl.Except(other.setImpl));
+ }
+ }
+ public partial class MultiSet<T>
+ {
+
+ readonly ImmutableDictionary<T, int> dict;
+ MultiSet(ImmutableDictionary<T, int> d) {
+ dict = d;
+ }
+ public static readonly MultiSet<T> Empty = new MultiSet<T>(ImmutableDictionary<T, int>.Empty);
+ public static MultiSet<T> FromElements(params T[] values) {
+ var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d.ToImmutable());
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d.ToImmutable());
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d.ToImmutable());
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d.ToImmutable());
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ var hashCode = 1;
+ foreach (var kv in dict) {
+ var key = kv.Key.GetHashCode();
+ key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+ hashCode = hashCode * (key + 3);
+ }
+ return hashCode;
+ }
+ 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);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r.ToImmutable());
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r[t] = other.dict[t] < dict[t] ? other.dict[t] : dict[t];
+ }
+ }
+ return new MultiSet<T>(r.ToImmutable());
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r[t] = dict[t];
+ } else if (other.dict[t] < dict[t]) {
+ r[t] = dict[t] - other.dict[t];
+ }
+ }
+ return new MultiSet<T>(r.ToImmutable());
+ }
+ public IEnumerable<T> Elements {
+ get {
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ yield return t;
+ }
+ }
+ }
+ }
+ }
+
+ public partial class Map<U, V>
+ {
+ readonly ImmutableDictionary<U, V> dict;
+ Map(ImmutableDictionary<U, V> d) {
+ dict = d;
+ }
+ public static readonly Map<U, V> Empty = new Map<U, V>(ImmutableDictionary<U, V>.Empty);
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ var d = ImmutableDictionary<U, V>.Empty.ToBuilder();
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d.ToImmutable());
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ var d = ImmutableDictionary<U, V>.Empty.ToBuilder();
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d.ToImmutable());
+ }
+ public int Length {
+ get { return dict.Count; }
+ }
+ public long LongLength {
+ get { return dict.Count; }
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ var hashCode = 1;
+ foreach (var kv in dict) {
+ var key = kv.Key.GetHashCode();
+ key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+ hashCode = hashCode * (key + 3);
+ }
+ return hashCode;
+ }
+ 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))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ return new Map<U, V>(dict.SetItem(index, val));
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+#else // !def DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE
+ public class Set<T>
+ {
+ HashSet<T> set;
+ Set(HashSet<T> s) {
+ this.set = s;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new HashSet<T>());
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ var s = new HashSet<T>();
+ foreach (T t in values)
+ s.Add(t);
+ return new Set<T>(s);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ HashSet<T> s = new HashSet<T>();
+ foreach (T t in values)
+ s.Add(t);
+ return new Set<T>(s);
+ }
+ public int Length {
+ get { return this.set.Count; }
+ }
+ public long LongLength {
+ get { return this.set.Count; }
+ }
+ public IEnumerable<T> Elements {
+ get {
+ return this.set;
+ }
+ }
+ /// <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(this.set);
+ var n = elmts.Count;
+ var which = new bool[n];
+ var s = new Set<T>(new HashSet<T>());
+ 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.set.Remove(elmts[i]);
+ }
+ if (i == n) {
+ // we have cycled through all the subsets
+ break;
+ }
+ which[i] = true;
+ s.set.Add(elmts[i]);
+ }
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return this.set.Count == other.set.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ var hashCode = 1;
+ foreach (var t in this.set) {
+ hashCode = hashCode * (t.GetHashCode()+3);
+ }
+ return hashCode;
+ }
+ public override string ToString() {
+ var s = "{";
+ var sep = "";
+ foreach (var t in this.set) {
+ s += sep + t.ToString();
+ sep = ", ";
+ }
+ return s + "}";
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return this.set.Count < other.set.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.set.Count < this.set.Count)
+ return false;
+ foreach (T t in this.set) {
+ if (!other.set.Contains(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ HashSet<T> a, b;
+ if (this.set.Count < other.set.Count) {
+ a = this.set; b = other.set;
+ } else {
+ a = other.set; b = this.set;
+ }
+ foreach (T t in a) {
+ if (b.Contains(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return this.set.Contains(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (this.set.Count == 0)
+ return other;
+ else if (other.set.Count == 0)
+ return this;
+ HashSet<T> a, b;
+ if (this.set.Count < other.set.Count) {
+ a = this.set; b = other.set;
+ } else {
+ a = other.set; b = this.set;
+ }
+ var r = new HashSet<T>();
+ foreach (T t in b)
+ r.Add(t);
+ foreach (T t in a)
+ r.Add(t);
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (this.set.Count == 0)
+ return this;
+ else if (other.set.Count == 0)
+ return other;
+ HashSet<T> a, b;
+ if (this.set.Count < other.set.Count) {
+ a = this.set; b = other.set;
+ } else {
+ a = other.set; b = this.set;
+ }
+ var r = new HashSet<T>();
+ foreach (T t in a) {
+ if (b.Contains(t))
+ r.Add(t);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (this.set.Count == 0)
+ return this;
+ else if (other.set.Count == 0)
+ return this;
+ var r = new HashSet<T>();
+ foreach (T t in this.set) {
+ if (!other.set.Contains(t))
+ r.Add(t);
+ }
+ return new Set<T>(r);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ var hashCode = 1;
+ foreach (var kv in dict) {
+ var key = kv.Key.GetHashCode();
+ key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+ hashCode = hashCode * (key + 3);
+ }
+ return hashCode;
+ }
+ 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);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public int Length {
+ get { return dict.Count; }
+ }
+ public long LongLength {
+ get { return dict.Count; }
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ var hashCode = 1;
+ foreach (var kv in dict) {
+ var key = kv.Key.GetHashCode();
+ key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+ hashCode = hashCode * (key + 3);
+ }
+ return hashCode;
+ }
+ 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))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+#endif
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public static Sequence<char> FromString(string s) {
+ return new Sequence<char>(s.ToCharArray());
+ }
+ public int Length {
+ get { return elmts.Length; }
+ }
+ public long LongLength {
+ get { return elmts.LongLength; }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(ulong index) {
+ return elmts[index];
+ }
+ public T Select(long index) {
+ return elmts[index];
+ }
+ public T Select(uint index) {
+ return elmts[index];
+ }
+ public T Select(int index) {
+ return elmts[index];
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(long index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[index] = t;
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Update(ulong index, T t) {
+ return Update((long)index, t);
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ return Update((long)index, t);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ if (elmts == null || elmts.Length == 0)
+ return 0;
+ var hashCode = 0;
+ for (var i = 0; i < elmts.Length; i++) {
+ hashCode = (hashCode << 3) | (hashCode >> 29) ^ elmts[i].GetHashCode();
+ }
+ return hashCode;
+ }
+ public override string ToString() {
+ if (elmts is char[]) {
+ var s = "";
+ foreach (var t in elmts) {
+ s += t.ToString();
+ }
+ return s;
+ } else {
+ 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]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(long m) {
+ if (elmts.LongLength == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Take(ulong n) {
+ return Take((long)n);
+ }
+ public Sequence<T> Take(BigInteger n) {
+ return Take((long)n);
+ }
+ public Sequence<T> Drop(long m) {
+ if (m == 0)
+ return this;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(ulong n) {
+ return Drop((long)n);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ return Drop((long)n);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
+ if (frall) {
+ return pred(false) && pred(true);
+ } else {
+ return pred(false) || pred(true);
+ }
+ }
+ public static bool QuantChar(bool frall, System.Predicate<char> pred) {
+ for (int i = 0; i < 0x10000; i++) {
+ if (pred((char)i) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
+ for (BigInteger i = lo; i < hi; i++) {
+ if (pred(i) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantDatatype<U>(IEnumerable<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ public static IEnumerable<char> AllChars {
+ get {
+ for (int i = 0; i < 0x10000; i++) {
+ yield return (char)i;
+ }
+ }
+ }
+ public static IEnumerable<BigInteger> AllIntegers {
+ get {
+ yield return new BigInteger(0);
+ for (var j = new BigInteger(1);; j++) {
+ yield return j;
+ yield return -j;
+ }
+ }
+ }
+ public static IEnumerable<BigInteger> IntegerRange(BigInteger lo, BigInteger hi) {
+ for (var j = lo; j < hi; j++) {
+ yield return j;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) {
+ return (sbyte)EuclideanDivision_int(a, b);
+ }
+ public static short EuclideanDivision_short(short a, short b) {
+ return (short)EuclideanDivision_int(a, b);
+ }
+ public static int EuclideanDivision_int(int a, int b) {
+ if (0 <= a) {
+ if (0 <= b) {
+ // +a +b: a/b
+ return (int)(((uint)(a)) / ((uint)(b)));
+ } else {
+ // +a -b: -(a/(-b))
+ return -((int)(((uint)(a)) / ((uint)(unchecked(-b)))));
+ }
+ } else {
+ if (0 <= b) {
+ // -a +b: -((-a-1)/b) - 1
+ return -((int)(((uint)(-(a + 1))) / ((uint)(b)))) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return ((int)(((uint)(-(a + 1))) / ((uint)(unchecked(-b))))) + 1;
+ }
+ }
+ }
+ public static long EuclideanDivision_long(long a, long b) {
+ if (0 <= a) {
+ if (0 <= b) {
+ // +a +b: a/b
+ return (long)(((ulong)(a)) / ((ulong)(b)));
+ } else {
+ // +a -b: -(a/(-b))
+ return -((long)(((ulong)(a)) / ((ulong)(unchecked(-b)))));
+ }
+ } else {
+ if (0 <= b) {
+ // -a +b: -((-a-1)/b) - 1
+ return -((long)(((ulong)(-(a + 1))) / ((ulong)(b)))) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return ((long)(((ulong)(-(a + 1))) / ((ulong)(unchecked(-b))))) + 1;
+ }
+ }
+ }
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static sbyte EuclideanModulus_sbyte(sbyte a, sbyte b) {
+ return (sbyte)EuclideanModulus_int(a, b);
+ }
+ public static short EuclideanModulus_short(short a, short b) {
+ return (short)EuclideanModulus_int(a, b);
+ }
+ public static int EuclideanModulus_int(int a, int b) {
+ uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b));
+ if (0 <= a) {
+ // +a: a % b'
+ return (int)(((uint)a) % bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ uint c = ((uint)(unchecked(-a))) % bp;
+ return (int)(c == 0 ? c : bp - c);
+ }
+ }
+ public static long EuclideanModulus_long(long a, long b) {
+ ulong bp = (0 <= b) ? (ulong)b : (ulong)(unchecked(-b));
+ if (0 <= a) {
+ // +a: a % b'
+ return (long)(((ulong)a) % bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ ulong c = ((ulong)(unchecked(-a))) % bp;
+ return (long)(c == 0 ? c : bp - c);
+ }
+ }
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>((T[])array.Clone());
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+
+ public static U Let<T, U>(T t, Func<T,U> f) {
+ return f(t);
+ }
+
+ public delegate Result Function<Input,Result>(Input input);
+
+ public static A Id<A>(A a) {
+ return a;
+ }
+ }
+
+ public struct BigRational
+ {
+ public static readonly BigRational ZERO = new BigRational(0);
+
+ BigInteger num, den; // invariant 1 <= den
+ public override string ToString() {
+ return string.Format("({0}.0 / {1}.0)", num, den);
+ }
+ public BigRational(int n) {
+ num = new BigInteger(n);
+ den = BigInteger.One;
+ }
+ public BigRational(BigInteger n, BigInteger d) {
+ // requires 1 <= d
+ num = n;
+ den = d;
+ }
+ public BigInteger ToBigInteger() {
+ if (0 <= num) {
+ return num / den;
+ } else {
+ return (num - den + 1) / den;
+ }
+ }
+ /// <summary>
+ /// Returns values such that aa/dd == a and bb/dd == b.
+ /// </summary>
+ private static void Normalize(BigRational a, BigRational b, out BigInteger aa, out BigInteger bb, out BigInteger dd) {
+ var gcd = BigInteger.GreatestCommonDivisor(a.den, b.den);
+ var xx = a.den / gcd;
+ var yy = b.den / gcd;
+ // We now have a == a.num / (xx * gcd) and b == b.num / (yy * gcd).
+ aa = a.num * yy;
+ bb = b.num * xx;
+ dd = a.den * yy;
+ }
+ public int CompareTo(BigRational that) {
+ // simple things first
+ int asign = this.num.Sign;
+ int bsign = that.num.Sign;
+ if (asign < 0 && 0 <= bsign) {
+ return -1;
+ } else if (asign <= 0 && 0 < bsign) {
+ return -1;
+ } else if (bsign < 0 && 0 <= asign) {
+ return 1;
+ } else if (bsign <= 0 && 0 < asign) {
+ return 1;
+ }
+ BigInteger aa, bb, dd;
+ Normalize(this, that, out aa, out bb, out dd);
+ return aa.CompareTo(bb);
+ }
+ public override int GetHashCode() {
+ return num.GetHashCode() + 29 * den.GetHashCode();
+ }
+ public override bool Equals(object obj) {
+ if (obj is BigRational) {
+ return this == (BigRational)obj;
+ } else {
+ return false;
+ }
+ }
+ public static bool operator ==(BigRational a, BigRational b) {
+ return a.CompareTo(b) == 0;
+ }
+ public static bool operator !=(BigRational a, BigRational b) {
+ return a.CompareTo(b) != 0;
+ }
+ public static bool operator >(BigRational a, BigRational b) {
+ return 0 < a.CompareTo(b);
+ }
+ public static bool operator >=(BigRational a, BigRational b) {
+ return 0 <= a.CompareTo(b);
+ }
+ public static bool operator <(BigRational a, BigRational b) {
+ return a.CompareTo(b) < 0;
+ }
+ public static bool operator <=(BigRational a, BigRational b) {
+ return a.CompareTo(b) <= 0;
+ }
+ public static BigRational operator +(BigRational a, BigRational b) {
+ BigInteger aa, bb, dd;
+ Normalize(a, b, out aa, out bb, out dd);
+ return new BigRational(aa + bb, dd);
+ }
+ public static BigRational operator -(BigRational a, BigRational b) {
+ BigInteger aa, bb, dd;
+ Normalize(a, b, out aa, out bb, out dd);
+ return new BigRational(aa - bb, dd);
+ }
+ public static BigRational operator -(BigRational a) {
+ return new BigRational(-a.num, a.den);
+ }
+ public static BigRational operator *(BigRational a, BigRational b) {
+ return new BigRational(a.num * b.num, a.den * b.den);
+ }
+ public static BigRational operator /(BigRational a, BigRational b) {
+ // Compute the reciprocal of b
+ BigRational bReciprocal;
+ if (0 < b.num) {
+ bReciprocal = new BigRational(b.den, b.num);
+ } else {
+ // this is the case b.num < 0
+ bReciprocal = new BigRational(-b.den, -b.num);
+ }
+ return a * bReciprocal;
+ }
+ }
+}
diff --git a/Binaries/System.Collections.Immutable.dll b/Binaries/System.Collections.Immutable.dll
new file mode 100644
index 00000000..bcf23fe5
--- /dev/null
+++ b/Binaries/System.Collections.Immutable.dll
Binary files differ
diff --git a/Binaries/dafny b/Binaries/dafny
new file mode 100755
index 00000000..889ebc81
--- /dev/null
+++ b/Binaries/dafny
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+MONO=$(which mono)
+DAFNY=$(dirname "${BASH_SOURCE[0]}")/Dafny.exe
+
+if [[ ! -x "$MONO" ]]; then
+ echo "Error: Dafny requires Mono to run on non-Windows systems."
+ exit 1
+fi
+
+if [[ ! -x "$DAFNY" ]]; then
+ echo "Error: Dafny.exe not found at $DAFNY."
+ exit 1
+fi
+
+"$MONO" "$DAFNY" "$@"
diff --git a/Binaries/dafny-server b/Binaries/dafny-server
new file mode 100755
index 00000000..2fd0d202
--- /dev/null
+++ b/Binaries/dafny-server
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+MONO=$(which mono)
+DAFNYSERVER=$(dirname "${BASH_SOURCE[0]}")/DafnyServer.exe
+
+if [[ ! -x "$MONO" ]]; then
+ echo "Error: Dafny requires Mono to run on non-Windows systems."
+ exit 1
+fi
+
+if [[ ! -x "$DAFNYSERVER" ]]; then
+ echo "Error: DafnyServer.exe not found at $DAFNYSERVER."
+ exit 1
+fi
+
+"$MONO" "$DAFNYSERVER" "$@"
diff --git a/Binaries/z3.exe b/Binaries/z3.exe
index 72aa6ccd..21c6d85b 100644
--- a/Binaries/z3.exe
+++ b/Binaries/z3.exe
Binary files differ
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 15:22:51 +0000