From d3c2801fd211c69c61fcc85e3c3f1a18c3d0f187 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 23 Jul 2013 21:00:37 -0700 Subject: Removed the remaining pure collections. --- Source/Core/Core.csproj | 1 - Source/Core/DeadVarElim.cs | 1 - Source/Core/Parser.cs | 1 - Source/Core/PureCollections.cs | 923 ----------------------------------------- Source/VCGeneration/VC.cs | 32 +- 5 files changed, 26 insertions(+), 932 deletions(-) delete mode 100644 Source/Core/PureCollections.cs diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index f3db4f9a..6d5b7bd9 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -167,7 +167,6 @@ - diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 356ff272..9d20c15e 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -1,7 +1,6 @@ using System; using System.Collections.Generic; using Microsoft.Boogie.GraphUtil; -using PureCollections; using System.Diagnostics.Contracts; diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index fa15b100..310e3cc0 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1,4 +1,3 @@ -using PureCollections; using System.Collections; using System.Collections.Generic; using System.IO; diff --git a/Source/Core/PureCollections.cs b/Source/Core/PureCollections.cs deleted file mode 100644 index 8eafd73f..00000000 --- a/Source/Core/PureCollections.cs +++ /dev/null @@ -1,923 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- - -//--------------------------------------------------------------------- -// PureCollections.cs -// - Mostly pure functions for tuples, sets, maps, Sequences -// Version 1.0, WS, 3/23/2002 -//--------------------------------------------------------------------- - - -using System; -using System.Collections; -using System.Diagnostics.Contracts; - -namespace PureCollections { - //------------------------------------------------------------------- - // General types - //------------------------------------------------------------------- - - public class MissingCase : Exception { - } - - public struct Capacity { - public int capacity; - public Capacity(int i) { - capacity = i; - } - } - - abstract public class Coll { - public object[] elems; // null is used to show empty spots! - protected int card; - protected Coll() { - } - protected Coll(object[] elems, int card) { - this.elems = elems; - this.card = card; - } - protected Coll(Coll c) { - Contract.Requires(c != null); - Contract.Requires(c.elems != null); - this.elems = (object[])c.elems.Clone(); - this.card = c.card; - } - } - - - // ------------------------------------------------------------------ - // Tuple - // ------------------------------------------------------------------ - - public class Tuple : Coll, IComparable { - //public object[] elems; - - //invariant this.elems != null; - - // Constructor - - - - - - - - - - - - - - - - - - - - - - - - - - - public Tuple(params object[] ts) { - Contract.Requires(ts != null); - elems = ts; - card = ts.Length; - } - public Tuple(Capacity c) { - elems = new object[c.capacity]; - card = c.capacity; - } - - //Equality - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object o) { - Contract.Assert(this.elems != null); - if (o == null || !(o is Tuple) || elems.Length != (cce.NonNull((Tuple)o).elems).Length) - return false; - - Tuple s = (Tuple)o; - for (int i = 0; i < elems.Length; i++) - if (!Equals(this.elems[i], s.elems[i])) - return false; - return true; - } - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML - public static bool operator ==(Tuple s, Tuple t) { - return s == null ? t == null : s.Equals(t); - } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML - public static bool operator !=(Tuple s, Tuple t) { - return !(t == s); - } - - [Pure] - public override int GetHashCode() { - int h = 0; - Contract.Assume(this.elems != null); - for (int i = 0; i < elems.Length; i++) { - object elem = elems[i]; - if (elem != null) - h += elem.GetHashCode(); - } - return h; - } - - //Compare - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - int IComparable.CompareTo(object o) { - Contract.Assert(this.elems != null); - if (o == null || !(o is Tuple) || elems.Length != (cce.NonNull((Tuple)o).elems).Length) - throw new MissingCase(); - - Tuple t = (Tuple)o; - for (int i = 0; i < elems.Length; i++) { - int c = cce.NonNull((IComparable)elems[i]).CompareTo(t.elems[i]); - if (c < 0) - return -1; - else if (c > 0) - return +1; - } - return 0; - } - - public static bool operator <=(Tuple s, Tuple t) { - return s == null ? t == null : ((IComparable)s).CompareTo(t) <= 0; - } - public static bool operator <(Tuple s, Tuple t) { - return s == null ? false : ((IComparable)s).CompareTo(t) < 0; - } - public static bool operator >=(Tuple s, Tuple t) { - return t <= s; - } - public static bool operator >(Tuple s, Tuple t) { - return t < s; - } - - //Select and Update - - - - - - - - - - - - - - - - - - - - - - - - - public object this[int index] { - get { - Contract.Assert(this.elems != null); - return elems[index]; - } - set { - Contract.Assert(this.elems != null); - elems[index] = value; - } - } - - //ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - Contract.Assert(this.elems != null); - if (elems.Length == 0) - return "()"; - - string s = "("; - for (int i = 0; i < elems.Length - 1; i++) - s += cce.NonNull(elems[i]).ToString() + ", "; - return s + cce.NonNull(elems[elems.Length - 1]).ToString() + ")"; - } - } - - // ------------------------------------------------------------------ - // Pair - public class Pair : Tuple { - protected Pair() { - } - public Pair(object first, object second) { - elems = new object[] { first, second }; - } - public object First { - get { - Contract.Assert(this.elems != null); - return elems[0]; - } - set { - Contract.Assert(this.elems != null); - elems[0] = value; - } - } - public object Second { - get { - Contract.Assert(this.elems != null); - return elems[1]; - } - set { - Contract.Assert(this.elems != null); - elems[1] = value; - } - } - } - - // -------------------------------------------------------------------- - // Map - // -------------------------------------------------------------------- - - public class MapEnumerator : IEnumerator { - private Map/*!*/ map; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(map != null); - } - - private int index = -1; - public MapEnumerator(Map m) { - Contract.Requires(m != null); - map = m; - } - public bool MoveNext() { - do { - index++; - Contract.Assert(map.elems != null); - } while (index < map.elems.Length && map.elems[index] == null); - return index < map.elems.Length; - } - public object Current { - get { - Contract.Assert(map.elems != null); - return new Pair(map.elems[index], map.vals[index]); - } - } - public void Reset() { - index = -1; - } - } - - public class Map : Coll, IEnumerable, IComparable { - public Object[]/*!*/ vals; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(vals != null); - } - - - //invariant this.elems != null; - - // constructors - - - - - - - - - - - - - - - - - - - - - - - - - - - - public Map(Capacity c) { - elems = new Object[c.capacity * 2]; - vals = new Object[c.capacity * 2]; - card = 0; - } - - [NotDelayed] - public Map(params Pair[] ps) - : base() { - Contract.Requires(ps != null); - elems = new Object[ps.Length * 2]; - vals = new Object[ps.Length * 2]; - card = 0; - for (int i = 0; i < ps.Length; i++) - Insert(cce.NonNull(ps[i]).First, cce.NonNull(ps[i]).Second); - } - - // iterators - - - - - - - - - - - - - - - - - - - - - - - - - - - - [Pure] - [GlobalAccess(false)] - [Escapes(true, false)] - public IEnumerator GetEnumerator() { - Contract.Ensures(Contract.Result() != null); - return new MapEnumerator(this); - } - public Pair[] ToArray() { - Pair[] n = new Pair[card]; - int ct = 0; - Contract.Assert(this.elems != null); - for (int i = 0; i < elems.Length; i++) - if (elems[i] != null) - n[ct++] = new Pair(elems[i], vals[i]); - return n; - } - - //(ASM) Update- - - - - - - - - - - - - - - - - - - - - - - - - - - - public Map Update(object k, object v) { - Map n = new Map(new Capacity(card + 1)); - Contract.Assert(this.elems != null); - for (int i = 0; i < elems.Length; i++) - if (elems[i] != null && !Equals(elems[i], k)) - n.Insert(elems[i], vals[i]); - n.Insert(k, v); - return n; - } - - //In place Update (and Remove)- - - - - - - - - - - - - - - - - - - - public object this[object index] { - get { - return this.Apply(index); - } - set { - this.Insert(index, value); - } - } - - public void Remove(object o) { - Contract.Requires(o != null); - Contract.Assert(this.elems != null); - int h = Math.Abs(o.GetHashCode()) % elems.Length; - for (int i = 0; i < elems.Length; i++) { - int j = (i + h) % elems.Length; - if (elems[j] == null) { - break; - } else if (Equals(elems[j], o)) { - elems[j] = null; - vals[j] = null; - break; - } - } - } - - public void Insert(Object key, Object val) { - if (key == null) - throw new MissingCase(); - - Contract.Assert(this.elems != null); - if (elems.Length == 0 || 2 * card >= elems.Length) { - int m = card * 2; - if (m < 4) - m = 4; - object[] newElems = new object[m]; - object[] newVals = new object[m]; - for (int k = 0; k < elems.Length; k++) { - object elem = elems[k]; - if (elem != null) { - int newHash = Math.Abs(elem.GetHashCode()) % newElems.Length; - for (int i = 0; i < newElems.Length; i++) { - int j = (i + newHash) % newElems.Length; - if (newElems[j] == null) { - newElems[j] = elem; - newVals[j] = vals[k]; - break; - } - } - } - } - elems = newElems; - vals = newVals; - } - int h = Math.Abs(key.GetHashCode()) % elems.Length; - for (int i = 0; i < elems.Length; i++) { - int j = (i + h) % elems.Length; - if (elems[j] == null) { - elems[j] = key; - vals[j] = val; - card++; - return; - } else if (key.Equals(elems[j])) { - vals[j] = val; - return; - } - } - } - - //ToString - - - - - - - - - - - - - - - - - - - - - - - - - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - if (card == 0) - return "{|->}"; - else { - string s = "{"; - int ct = 0; - Contract.Assert(this.elems != null); - for (int i = 0; i < elems.Length; i++) { - object elem = elems[i]; - if (elem != null) { - s += elem.ToString() + "|->" + cce.NonNull(vals[i]).ToString(); - s += (ct != card - 1) ? ", " : ""; - ct++; - } - } - return s + "}"; - } - } - - // Subset operations - - - - - - - - - - - - - - - - - - - - - - - - // View Map as Set of Pairs - - int IComparable.CompareTo(object o) { - if (o == null || !(o is Map)) - throw new MissingCase(); - // WS Improve performance! - Map t = (Map)o; - if (this < t) - return -1; - else if (this > t) - return +1; - else - return 0; - } - public static bool operator <=(Map s, Map t) { - if (s == null) - return t == null; - if (t == null) - return false; - Contract.Assert(s.elems != null); - for (int i = 0; i < s.elems.Length; i++) - if (s.elems[i] != null) { - object o = t.Apply(s.elems[i]); - if (o == null || !o.Equals(s.vals[i])) - return false; - } - return true; - } - public static bool operator <(Map s, Map t) { - return s == null || t == null ? false : s.card < t.card && s <= t; - } - public static bool operator >=(Map s, Map t) { - return t <= s; - } - public static bool operator >(Map s, Map t) { - return t < s; - } - - // Equality - - - - - - - - - - - - - - - - - - - - - - - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(Object t) { - return t != null && t is Map && card == ((Map)t).card && this <= ((Map)t); - } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML - public static bool operator ==(Map s, Map t) { - if ((object)s == null) - if ((object)t == null) - return true; - else - return t.Equals(s); - else - return s.Equals(t); - } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML - public static bool operator !=(Map s, Map t) { - return !(t == s); - } - [Pure] - public override int GetHashCode() { - int h = 0; - Contract.Assert(this.elems != null); - for (int i = 0; i < elems.Length; i++) { - object elem = elems[i]; - if (elem != null) { - h += elem.GetHashCode() + cce.NonNull(vals[i]).GetHashCode(); - } - } - return h; - } - - //Ordinary map operations- - - - - - - - - - - - - - - - - - - - - - - - - - [Pure] - public bool Has(Object x) { - if (x == null) - throw new MissingCase(); - - Contract.Assert(this.elems != null); - if (elems.Length == 0) - return false; - int h = Math.Abs(x.GetHashCode()) % elems.Length; - for (int i = 0; i < elems.Length; i++) { - int j = (i + h) % elems.Length; - if (x.Equals(elems[j])) - return true; - } - return false; - } - - public object Apply(object x) { - if (x == null) - throw new MissingCase(); - Contract.Assert(this.elems != null); - if (elems.Length == 0) - return null; - int h = Math.Abs(x.GetHashCode()) % elems.Length; - for (int i = 0; i < elems.Length; i++) { - int j = (i + h) % elems.Length; - if (elems[j] != null && x.Equals(elems[j])) - return vals[j]; - } - return null; - } - - public static Map Override(Map s, Map t) { - Contract.Requires(t != null); - Contract.Requires(s != null); - Map m = new Map(new Capacity(s.card + t.card)); - Contract.Assert(s.elems != null); - for (int i = 0; i < s.elems.Length; i++) - if (s.elems[i] != null) - m.Insert(s.elems[i], s.vals[i]); - Contract.Assert(t.elems != null); - for (int i = 0; i < t.elems.Length; i++) - if (t.elems[i] != null) - m.Insert(t.elems[i], t.vals[i]); - return m; - } - } - - // -------------------------------------------------------------------- - // Sequence - - public class SequenceEnumerator : IEnumerator { - [Peer] - private Sequence/*!*/ seq; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(seq != null); - } - - private int index = -1; - [Captured] - public SequenceEnumerator(Sequence s) { - Contract.Requires(s != null); - seq = s; - } - public bool MoveNext() { - index++; - //while (index < seq.elems.Length); // Sequences allow nils ... && seq.elems[index] == null); - return index < seq.Count; - } - public object Current { - get { - Contract.Assert(seq.elems != null); - return seq.elems[index]; - } - } - public void Reset() { - index = -1; - } - } - - public class Sequence : Coll, IEnumerable, IComparable { - public Sequence() { - elems = new object[4]; - } - - //invariant this.elems != null; - - //constructors - - - - - - - - - - - - - - - - - - - - - - - - - - - - public Sequence(params object[] ds) { - Contract.Requires(ds != null); - card = ds.Length; - elems = ds; - } - public Sequence(Sequence seq) - : base(seq) { - Contract.Requires(seq != null); - } - public Sequence(Capacity c) { - elems = new object[c.capacity]; - } - - // Iterators - - - - - - - - - - - - - - - - - - - - - - - - - - - - [Pure] - [GlobalAccess(false)] - [Escapes(true, false)] - public IEnumerator/*!*/ GetEnumerator() { - Contract.Ensures(cce.Owner.Same(Contract.Result(), this)); - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(cce.IsNew(Contract.Result())); - return new SequenceEnumerator(this); - } - - public object[] ToArray() { - object[] n = new object[card]; - int ct = 0; - Contract.Assert(this.elems != null); - for (int i = 0; i < card; i++) - n[ct++] = elems[i]; - return n; - } - - //ASM Update - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - public Sequence Update(int i, object v) { - Sequence n = new Sequence(new Capacity(card + 1)); - Contract.Assert(this.elems != null); - Contract.Assert(n.elems != null); - for (int j = 0; j < elems.Length; j++) - n.elems[j] = elems[j]; - if (i >= 0 && i < card) { - n.elems[i] = v; - n.card = card; - return n; - } else if (i == card) { - n.elems[i] = v; - n.card = card + 1; - return n; - } else - throw new Exception("Sequence Update out of range"); - } - - //In place Update (and Remove) and Length - - - - - - - - - - - - - - - - public int Count { - get { - return this.card; - } - } - - public object this[int index] { - get { - Contract.Assert(this.elems != null); - return this.elems[index]; - } - set { - Contract.Assert(this.elems != null); - this.elems[index] = value; - } - } - - public void Add(object o) { - Contract.Assert(this.elems != null); - int n = this.elems.Length; - int i = this.card++; - if (i == n) { - int m = n * 2; - if (m < 4) - m = 4; - object[] newElems = new object[m]; - for (int j = 0; j < n; j++) - newElems[j] = elems[j]; - elems = newElems; - } - elems[i] = o; - } - - public void AddRange(Sequence seq) { - Contract.Requires(seq != null); - foreach (object o in seq) { - Add(o); - } - } - - //ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - string s = ""; - if (this.elems == null) - return "(null)"; - Contract.Assert(this.elems != null); - if (card > 0 && elems[0] is Char) { - for (int i = 0; i < card; i++) { - object elem = elems[i]; - if (elem != null) { - s += elem.ToString(); - } - } - return s; - } else { - s = "["; - for (int i = 0; i < card - 1; i++) { - object elem = elems[i]; - if (elem != null) { - s += elem.ToString() + ", "; - } - } - if (card > 0) { - object last = elems[card - 1]; - if (last != null) { - s += last.ToString(); - } - } - s += "]"; - return s; - } - } - //Equality- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object that) { - return that != null && that is Sequence && ((Sequence)this == (Sequence)that); - } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML - public static bool operator ==(Sequence s, Sequence t) { - if ((object)s == (object)t) { - return true; - } else if ((object)s == null || (object)t == null) { - return false; - } - if (s.card != t.card) - return false; - Contract.Assert(s.elems != null); - Contract.Assert(t.elems != null); - for (int i = 0; i < s.card; i++) - if (!Equals(s.elems[i], t.elems[i])) - return false; - return true; - } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML - public static bool operator !=(Sequence s, Sequence t) { - return !(s == t); - } - [Pure] - public override int GetHashCode() { - int h = 0; - for (int i = 0; i < card; i++) { - Contract.Assert(this.elems != null); - object elem = elems[i]; - if (elem != null) { - h += elem.GetHashCode(); - } - } - return h; - } - //Subset- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - // View Sequence of T as Set of (Integer,T) - int IComparable.CompareTo(object o) { - if (o == null || !(o is Sequence)) - throw new MissingCase(); - // WS Improve performance! - Sequence t = (Sequence)o; - if (this < t) - return -1; - else if (this > t) - return +1; - else - return 0; - } - - public static bool operator <(Sequence s, Sequence t) { - if (s == null) - throw new ArgumentNullException("s"); - if (t == null) - throw new ArgumentNullException("t"); - if (s.card >= t.card) - return false; - Contract.Assert(s.elems != null); - Contract.Assert(t.elems != null); - for (int i = 0; i < s.card; i++) - if (!Equals(s.elems[i], t.elems[i])) - return false; - return true; - } - public static bool operator <=(Sequence s, Sequence t) { - if (s == null) - throw new ArgumentNullException("s"); - if (t == null) - throw new ArgumentNullException("t"); - if (s.card > t.card) - return false; - Contract.Assert(s.elems != null); - Contract.Assert(t.elems != null); - for (int i = 0; i < s.card; i++) - if (!Equals(s.elems[i], t.elems[i])) - return false; - return true; - } - public static bool operator >(Sequence s, Sequence t) { - return t < s; - } - public static bool operator >=(Sequence s, Sequence t) { - return t <= s; - } - - //pure--------------------------------------------------------------- - [Pure] - public bool Contains(object x) { // WS translate to tailrecursion - if (x == null) - throw new MissingCase(); - Contract.Assert(this.elems != null); - for (int i = 0; i < card; i++) - if (x.Equals(elems[i])) - return true; - return false; - } - - // the index of the first occurrence of x in this sequence, - // or -1 if x does not occur - [Pure] - public int IndexOf(object x) { - if (x == null) - throw new MissingCase(); - Contract.Assert(this.elems != null); - for (int i = 0; i < card; i++) - if (x.Equals(elems[i])) - return i; - return -1; - } - - // the index of the last occurrence of x in this sequence, - // or -1 if x does not occur - [Pure] - public int LastIndexOf(object x) { - if (x == null) - throw new MissingCase(); - Contract.Assert(this.elems != null); - for (int i = card - 1; i >= 0; i--) - if (x.Equals(elems[i])) - return i; - return -1; - } - - public object Head() { - Contract.Assert(this.elems != null); - return elems[0]; - } - public object Last() { - Contract.Assert(this.elems != null); - return elems[card - 1]; - } - - public static Sequence Tail(Sequence s) { - Contract.Requires(s != null); - Sequence n = new Sequence(new Capacity(s.card - 1)); - Contract.Assert(n.elems != null); - Contract.Assert(s.elems != null); - for (int i = 1; i < s.card; i++) - n.elems[n.card++] = s.elems[i]; - return n; - } - - public static Sequence Front(Sequence s) { - Contract.Requires(s != null); - Sequence n = new Sequence(new Capacity(s.card - 1)); - Contract.Assert(n.elems != null); - Contract.Assert(s.elems != null); - for (int i = 0; i < s.card - 1; i++) - n.elems[n.card++] = s.elems[i]; - return n; - } - public static Sequence Concat(Sequence s) { - Contract.Requires(s != null); - Sequence n = new Sequence(new Capacity(s.card)); - Contract.Assert(n.elems != null); - Contract.Assert(s.elems != null); - for (int i = 0; i < s.card; i++) { - Sequence t = (Sequence)cce.NonNull(s.elems[i]); - Contract.Assert(t.elems != null); - for (int j = 0; j < t.card; j++) - n.Add(t.elems[j]); - } - return n; - } - - public static Sequence Reverse(Sequence s) { - Contract.Requires(s != null); - Sequence n = new Sequence(new Capacity(s.card)); - Contract.Assert(n.elems != null); - Contract.Assert(s.elems != null); - for (int i = s.card - 1; i >= 0; i--) - n.elems[n.card++] = s.elems[i]; - return n; - } - - public static Sequence operator +(Sequence s, Sequence t) { - if (s == null) - throw new ArgumentNullException("s"); - if (t == null) - throw new ArgumentNullException("t"); - return Append(t, s); - } - - public static Sequence Append(Sequence s, Sequence t) { - Contract.Requires(t != null); - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); - Sequence n = new Sequence(new Capacity(s.card + t.card)); - Contract.Assert(n != null); - Contract.Assert(n.elems != null); - Contract.Assert(s.elems != null); - Contract.Assert(t.elems != null); - for (int i = 0; i < s.card; i++) - n.elems[n.card++] = s.elems[i]; - for (int i = 0; i < t.card; i++) - n.elems[n.card++] = t.elems[i]; - return n; - } - public static Sequence Zip(Sequence s, Sequence t) { - Contract.Requires(t != null); - Contract.Requires(s != null); - int min = s.card < t.card ? s.card : t.card; - Sequence n = new Sequence(new Capacity(min)); - Contract.Assert(n.elems != null); - Contract.Assert(s.elems != null); - Contract.Assert(t.elems != null); - for (int i = 0; i < min; i++) - n.elems[n.card++] = new Tuple(s.elems[i], t.elems[i]); - return n; - } - public static Tuple Unzip(Sequence s) { - Contract.Requires(s != null); - Sequence n0 = new Sequence(new Capacity(s.card)); - Sequence n1 = new Sequence(new Capacity(s.card)); - Contract.Assert(s.elems != null); - Contract.Assert(n0.elems != null); - Contract.Assert(n1.elems != null); - for (int i = 0; i < s.card; i++) { - n0.elems[n0.card++] = (cce.NonNull((Tuple)s.elems[i]).elems)[0]; - n1.elems[n1.card++] = (cce.NonNull((Tuple)s.elems[i]).elems)[1]; - } - return new Tuple(n0, n1); - } - - public static Sequence FromTo(int from, int to) { //WS hash the result! - if (from > to) - return new Sequence(); - Sequence n = new Sequence(new Capacity(to - from + 1)); - Contract.Assert(n.elems != null); - for (int i = from; i <= to; i++) - n.elems[n.card++] = i; - return n; - } - - public static Sequence FromStepTo(int from, int step, int to) { - Sequence n = new Sequence(); - int incr = step - from; - if (incr > 0) - for (int i = from; i <= to; i += incr) - n.Add(i); - else if (incr < 0) - for (int i = to; i >= from; i -= incr) - n.Add(i); - return n; - } - - } -} \ No newline at end of file diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 92d1fd14..fd7a4f72 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1120,7 +1120,7 @@ namespace VC { ss.Add(s0.blocks[0]); ss.Add(s1.blocks[0]); try { - best.SoundnessCheck(new HashSet(), best.blocks[0], ss); + best.SoundnessCheck(new HashSet>(new BlockListComparer()), best.blocks[0], ss); } catch (System.Exception e) { Console.WriteLine(e); best.DumpDot(-1); @@ -1149,6 +1149,28 @@ namespace VC { return res; } + class BlockListComparer : IEqualityComparer> + { + public bool Equals(List x, List y) + { + return x == y || x.SequenceEqual(y); + } + + public int GetHashCode(List obj) + { + int h = 0; + Contract.Assume(obj != null); + foreach (var b in obj) + { + if (b != null) + { + h += b.GetHashCode(); + } + } + return h; + } + } + public Checker Checker { get { Contract.Ensures(Contract.Result() != null); @@ -1296,17 +1318,15 @@ namespace VC { checker.BeginCheck(desc, vc, reporter); } - private void SoundnessCheck(HashSet/*!*/ cache, Block/*!*/ orig, List/*!*/ copies) { + private void SoundnessCheck(HashSet/*!*/>/*!*/ cache, Block/*!*/ orig, List/*!*/ copies) { Contract.Requires(cce.NonNull(cache)); Contract.Requires(orig != null); Contract.Requires(copies != null); { - PureCollections.Tuple t = new PureCollections.Tuple(new PureCollections.Capacity(1 + copies.Count)); - int i = 0; - t[i++] = orig; + var t = new List { orig }; foreach (Block b in copies) { Contract.Assert(b != null); - t[i++] = b; + t.Add(b); } if (cache.Contains(t)) { return; -- cgit v1.2.3