using System; // for Func using System.Numerics; namespace Dafny { using System.Collections.Generic; public class Set { Dictionary dict; Set(Dictionary d) { dict = d; } public static Set Empty { get { return new Set(new Dictionary(0)); } } public static Set FromElements(params T[] values) { Dictionary d = new Dictionary(values.Length); foreach (T t in values) d[t] = true; return new Set(d); } public static Set FromCollection(ICollection values) { Dictionary d = new Dictionary(); foreach (T t in values) d[t] = true; return new Set(d); } public IEnumerable Elements { get { return dict.Keys; } } /// /// This is an inefficient iterator for producing all subsets of "this". Each set returned is the same /// Set object (but this Set object is fresh; in particular, it is not "this"). /// public IEnumerable> AllSubsets { get { // Start by putting all set elements into a list var elmts = new List(); elmts.AddRange(dict.Keys); var n = elmts.Count; var which = new bool[n]; var s = new Set(new Dictionary(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 other) { return dict.Count == other.dict.Count && IsSubsetOf(other); } public override bool Equals(object other) { return other is Set && Equals((Set)other); } 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 other) { return dict.Count < other.dict.Count && IsSubsetOf(other); } public bool IsSubsetOf(Set 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 other) { return other.IsSubsetOf(this); } public bool IsProperSupersetOf(Set other) { return other.IsProperSubsetOf(this); } public bool IsDisjointFrom(Set other) { Dictionary 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 Union(Set other) { if (dict.Count == 0) return other; else if (other.dict.Count == 0) return this; Dictionary a, b; if (dict.Count < other.dict.Count) { a = dict; b = other.dict; } else { a = other.dict; b = dict; } Dictionary r = new Dictionary(); foreach (T t in b.Keys) r[t] = true; foreach (T t in a.Keys) r[t] = true; return new Set(r); } public Set Intersect(Set other) { if (dict.Count == 0) return this; else if (other.dict.Count == 0) return other; Dictionary a, b; if (dict.Count < other.dict.Count) { a = dict; b = other.dict; } else { a = other.dict; b = dict; } var r = new Dictionary(); foreach (T t in a.Keys) { if (b.ContainsKey(t)) r.Add(t, true); } return new Set(r); } public Set Difference(Set other) { if (dict.Count == 0) return this; else if (other.dict.Count == 0) return this; var r = new Dictionary(); foreach (T t in dict.Keys) { if (!other.dict.ContainsKey(t)) r.Add(t, true); } return new Set(r); } } public class MultiSet { Dictionary dict; MultiSet(Dictionary d) { dict = d; } public static MultiSet Empty { get { return new MultiSet(new Dictionary(0)); } } public static MultiSet FromElements(params T[] values) { Dictionary d = new Dictionary(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(d); } public static MultiSet FromCollection(ICollection values) { Dictionary d = new Dictionary(); foreach (T t in values) { var i = 0; if (!d.TryGetValue(t, out i)) { i = 0; } d[t] = i + 1; } return new MultiSet(d); } public static MultiSet FromSeq(Sequence values) { Dictionary d = new Dictionary(); foreach (T t in values.Elements) { var i = 0; if (!d.TryGetValue(t, out i)) { i = 0; } d[t] = i + 1; } return new MultiSet(d); } public static MultiSet FromSet(Set values) { Dictionary d = new Dictionary(); foreach (T t in values.Elements) { d[t] = 1; } return new MultiSet(d); } public bool Equals(MultiSet other) { return other.IsSubsetOf(this) && this.IsSubsetOf(other); } public override bool Equals(object other) { return other is MultiSet && Equals((MultiSet)other); } 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 other) { return !Equals(other) && IsSubsetOf(other); } public bool IsSubsetOf(MultiSet 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 other) { return other.IsSubsetOf(this); } public bool IsProperSupersetOf(MultiSet other) { return other.IsProperSubsetOf(this); } public bool IsDisjointFrom(MultiSet 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 Union(MultiSet other) { if (dict.Count == 0) return other; else if (other.dict.Count == 0) return this; var r = new Dictionary(); 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(r); } public MultiSet Intersect(MultiSet other) { if (dict.Count == 0) return this; else if (other.dict.Count == 0) return other; var r = new Dictionary(); 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(r); } public MultiSet Difference(MultiSet other) { // \result == this - other if (dict.Count == 0) return this; else if (other.dict.Count == 0) return this; var r = new Dictionary(); 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(r); } public IEnumerable Elements { get { List l = new List(); 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 { Dictionary dict; Map(Dictionary d) { dict = d; } public static Map Empty { get { return new Map(new Dictionary()); } } public static Map FromElements(params Pair[] values) { Dictionary d = new Dictionary(values.Length); foreach (Pair p in values) { d[p.Car] = p.Cdr; } return new Map(d); } public static Map FromCollection(List> values) { Dictionary d = new Dictionary(values.Count); foreach (Pair p in values) { d[p.Car] = p.Cdr; } return new Map(d); } public bool Equals(Map 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 && Equals((Map)other); } 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 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 Update(U index, V val) { Dictionary d = new Dictionary(dict); d[index] = val; return new Map(d); } public IEnumerable Domain { get { return dict.Keys; } } } public class Sequence { T[] elmts; public Sequence(T[] ee) { elmts = ee; } public static Sequence Empty { get { return new Sequence(new T[0]); } } public static Sequence FromElements(params T[] values) { return new Sequence(values); } public static Sequence FromString(string s) { return new Sequence(s.ToCharArray()); } public int Length { get { return elmts.Length; } } public long LongLength { get { return elmts.LongLength; } } public T[] Elements { get { return elmts; } } public IEnumerable UniqueElements { get { var st = Set.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 Update(long index, T t) { T[] a = (T[])elmts.Clone(); a[index] = t; return new Sequence(a); } public Sequence Update(ulong index, T t) { return Update((long)index, t); } public Sequence Update(BigInteger index, T t) { return Update((long)index, t); } public bool Equals(Sequence other) { int n = elmts.Length; return n == other.elmts.Length && EqualUntil(other, n); } public override bool Equals(object other) { return other is Sequence && Equals((Sequence)other); } public override int GetHashCode() { return elmts.GetHashCode(); } 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 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 other) { int n = elmts.Length; return n < other.elmts.Length && EqualUntil(other, n); } public bool IsPrefixOf(Sequence other) { int n = elmts.Length; return n <= other.elmts.Length && EqualUntil(other, n); } public Sequence Concat(Sequence 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(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 Take(long m) { if (elmts.LongLength == m) return this; T[] a = new T[m]; System.Array.Copy(elmts, a, m); return new Sequence(a); } public Sequence Take(ulong n) { return Take((long)n); } public Sequence Take(BigInteger n) { return Take((long)n); } public Sequence 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(a); } public Sequence Drop(ulong n) { return Drop((long)n); } public Sequence Drop(BigInteger n) { if (n.IsZero) return this; return Drop((long)n); } } public struct Pair { 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 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 pred) { for (BigInteger i = lo; i < hi; i++) { if (pred(i) != frall) { return !frall; } } return frall; } public static bool QuantSet(Dafny.Set set, bool frall, System.Predicate pred) { foreach (var u in set.Elements) { if (pred(u) != frall) { return !frall; } } return frall; } public static bool QuantMap(Dafny.Map map, bool frall, System.Predicate pred) { foreach (var u in map.Domain) { if (pred(u) != frall) { return !frall; } } return frall; } public static bool QuantSeq(Dafny.Sequence seq, bool frall, System.Predicate pred) { foreach (var u in seq.Elements) { if (pred(u) != frall) { return !frall; } } return frall; } public static bool QuantDatatype(IEnumerable set, bool frall, System.Predicate pred) { foreach (var u in set) { if (pred(u) != frall) { return !frall; } } return frall; } // Enumerating other collections public delegate Dafny.Set ComprehensionDelegate(); public delegate Dafny.Map MapComprehensionDelegate(); public static IEnumerable AllBooleans { get { yield return false; yield return true; } } public static IEnumerable 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 SeqFromArray(T[] array) { return new Sequence(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 t, U u) { return u; } public static U Let(T t, Func f) { return f(t); } public delegate Result Function(Input input); public static A Id(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; } } /// /// Returns values such that aa/dd == a and bb/dd == b. /// 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; } } }