Normalise line endings using a .gitattributes file. Unfortunately

this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.

1 files changed, 959 insertions, 959 deletions

diff --git a/Source/AIFramework/Lattice.cs b/Source/AIFramework/Lattice.cs
index ab10be9a..1796f1f6 100644
--- a/Source/AIFramework/Lattice.cs
+++ b/Source/AIFramework/Lattice.cs
@@ -1,960 +1,960 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-namespace Microsoft.AbstractInterpretationFramework {

-  using System;

-  using System.Diagnostics.Contracts;

-  using System.Collections;

-  using G = System.Collections.Generic;

-  using System.Diagnostics;

-  using Microsoft.AbstractInterpretationFramework.Collections;

-  using Microsoft.Boogie;

-

+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.AbstractInterpretationFramework {
+  using System;
+  using System.Diagnostics.Contracts;
+  using System.Collections;
+  using G = System.Collections.Generic;
+  using System.Diagnostics;
+  using Microsoft.AbstractInterpretationFramework.Collections;
+  using Microsoft.Boogie;
+
   using ArraySet = Microsoft.Boogie.GSet<object>;
-  using IMutableSet = Microsoft.Boogie.GSet<object>; 

-  using HashSet = Microsoft.Boogie.GSet<object>;

-  using ISet = Microsoft.Boogie.GSet<object>;

-  using Set = Microsoft.Boogie.GSet<object>;

-

-

-  /// <summary>

-  ///  Specifies the operations (e.g., join) on a mathematical lattice that depend

-  ///  only on the elements of the lattice.

-  /// </summary>

-  [ContractClass(typeof(MathematicalLatticeContracts))]

-  public abstract class MathematicalLattice {

-    #region Element

-    /// <summary>

-    ///  An element of the lattice.  This class should be derived from in any

-    ///  implementation of MathematicalLattice.

-    /// </summary>

-    [ContractClass(typeof(ElementContracts))]

-    public abstract class Element : System.ICloneable {

-      /// <summary>

-      /// Print out a debug-useful representation of the internal data structure of the lattice element.

-      /// </summary>

-      public virtual void Dump(string/*!*/ msg) {

-        Contract.Requires(msg != null);

-        System.Console.WriteLine("Dump({0}) = {1}", msg, this);

-      }

-

-      public abstract Element/*!*/ Clone();

-      object/*!*/ System.ICloneable.Clone() {

-        return this.Clone();

-      }

-

-      public abstract G.ICollection<IVariable/*!*/>/*!*/ FreeVariables();

-

-    }

-    [ContractClassFor(typeof(Element))]

-    public abstract class ElementContracts : Element {

-      public override Element Clone() {

-        Contract.Ensures(Contract.Result<Element>() != null);

-        throw new NotImplementedException();

-

-      }

-

-      public override System.Collections.Generic.ICollection<IVariable> FreeVariables() {

-        Contract.Ensures(cce.NonNullElements(Contract.Result<G.ICollection<IVariable>>()));

-        Contract.Ensures(Contract.Result<System.Collections.Generic.ICollection<IVariable>>().IsReadOnly);

-        throw new System.NotImplementedException();

-      }

-    }

-    #endregion

-

-    public abstract Element/*!*/ Top {

-      get;

-    }

-    public abstract Element/*!*/ Bottom {

-      get;

-    }

-

-    public abstract bool IsTop(Element/*!*/ e);

-    public abstract bool IsBottom(Element/*!*/ e);

-

-    /// <summary>

-    /// Returns true if a &lt;= this.

-    /// </summary>

-    protected abstract bool AtMost(Element/*!*/ a, Element/*!*/ b);

-    /* The following cases are handled elsewhere and need not be considered in subclass. */

-    //  requires a.GetType() == b.GetType();

-    //  requires ! a.IsTop;

-    //  requires ! a.IsBottom;

-    //  requires ! b.IsTop;

-    //  requires ! b.IsBottom;

-

-

-    protected Answer TrivialLowerThan(Element/*!*/ a, Element/*!*/ b) {

-      Contract.Requires(b != null);

-      Contract.Requires(a != null);

-      if (a.GetType() != b.GetType()) {

-        throw new System.InvalidOperationException(

-          "operands to <= must be of same Element type"

-          );

-      }

-      if (IsBottom(a)) {

-        return Answer.Yes;

-      }

-      if (IsTop(b)) {

-        return Answer.Yes;

-      }

-      if (IsTop(a)) {

-        return Answer.No;

-      }

-      if (IsBottom(b)) {

-        return Answer.No;

-      }

-

-      return Answer.Maybe;

-    }

-

-    // Is 'a' better information than 'b'?

-    //

-    public bool LowerThan(Element/*!*/ a, Element/*!*/ b) {

-      Contract.Requires(b != null);

-      Contract.Requires(a != null);

-      Answer ans = TrivialLowerThan(a, b);

-      return ans != Answer.Maybe ? ans == Answer.Yes : AtMost(a, b);

-    }

-

-    // Is 'a' worse information than 'b'?

-    //

-    public bool HigherThan(Element/*!*/ a, Element/*!*/ b) {

-      Contract.Requires(b != null);

-      Contract.Requires(a != null);

-      return LowerThan(b, a);

-    }

-

-    // Are 'a' and 'b' equivalent?

-    //

-    public bool Equivalent(Element/*!*/ a, Element/*!*/ b) {

-      Contract.Requires(b != null);

-      Contract.Requires(a != null);

-      return LowerThan(a, b) && LowerThan(b, a);

-    }

-

-    public abstract Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b);

-    /* The following cases are handled elsewhere and need not be considered in subclass. */

-    //  requires a.GetType() == b.GetType();

-    //  requires ! a.IsTop;

-    //  requires ! a.IsBottom;

-    //  requires ! b.IsTop;

-    //  requires ! b.IsBottom;

-

-

-    protected Element/*?*/ TrivialJoin(Element/*!*/ a, Element/*!*/ b) {

-      Contract.Requires(b != null);

-      Contract.Requires(a != null);

-      if (a.GetType() != b.GetType()) {

-        throw new System.InvalidOperationException(

-          "operands to Join must be of same Lattice.Element type"

-          );

-      }

-      if (IsTop(a)) {

-        return a;

-      }

-      if (IsTop(b)) {

-        return b;

-      }

-      if (IsBottom(a)) {

-        return b;

-      }

-      if (IsBottom(b)) {

-        return a;

-      }

-

-      return null;

-    }

-

-    public Element/*!*/ Join(Element/*!*/ a, Element/*!*/ b) {

-      Contract.Requires(b != null);

-      Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      Element/*?*/ r = TrivialJoin(a, b);

-      return r != null ? r : NontrivialJoin(a, b);

-    }

-

-    public abstract Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b)

-      /* The following cases are handled elsewhere and need not be considered in subclass. */

-      //  requires a.GetType() == b.GetType();

-      //  requires ! a.IsTop;

-      //  requires ! a.IsBottom;

-      //  requires ! b.IsTop;

-      //  requires ! b.IsBottom;

-    ;

-

-    protected Element/*?*/ TrivialMeet(Element/*!*/ a, Element/*!*/ b) {

-      Contract.Requires(b != null);

-      Contract.Requires(a != null);

-      if (a.GetType() != b.GetType()) {

-        throw new System.InvalidOperationException(

-          "operands to Meet must be of same Lattice.Element type"

-          );

-      }

-      if (IsTop(a)) {

-        return b;

-      }

-      if (IsTop(b)) {

-        return a;

-      }

-      if (IsBottom(a)) {

-        return a;

-      }

-      if (IsBottom(b)) {

-        return b;

-      }

-

-      return null;

-    }

-

-    public Element/*!*/ Meet(Element/*!*/ a, Element/*!*/ b) {

-      Contract.Requires(b != null);

-      Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      Element/*?*/ r = TrivialMeet(a, b);

-      return r != null ? r : NontrivialMeet(a, b);

-    }

-

-    public abstract Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b);

-

-    public virtual void Validate() {

-      Debug.Assert(IsTop(Top));

-      Debug.Assert(IsBottom(Bottom));

-      Debug.Assert(!IsBottom(Top));

-      Debug.Assert(!IsTop(Bottom));

-

-      Debug.Assert(LowerThan(Top, Top));

-      Debug.Assert(LowerThan(Bottom, Top));

-      Debug.Assert(LowerThan(Bottom, Bottom));

-

-      Debug.Assert(IsTop(Join(Top, Top)));

-      Debug.Assert(IsBottom(Join(Bottom, Bottom)));

-    }

-  }

-  [ContractClassFor(typeof(MathematicalLattice))]

-  public abstract class MathematicalLatticeContracts : MathematicalLattice {

-    public override MathematicalLattice.Element Top {

-      get {

-        Contract.Ensures(Contract.Result<Element>() != null);

-        throw new NotImplementedException();

-      }

-    }

-

-    public override MathematicalLattice.Element Bottom {

-      get {

-        Contract.Ensures(Contract.Result<Element>() != null);

-        throw new NotImplementedException();

-      }

-    }

-

-    public override bool IsTop(MathematicalLattice.Element e) {

-      Contract.Requires(e != null);

-      throw new NotImplementedException();

-    }

-

-    public override bool IsBottom(MathematicalLattice.Element e) {

-      Contract.Requires(e != null);

-      throw new NotImplementedException();

-    }

-

-    protected override bool AtMost(MathematicalLattice.Element a, MathematicalLattice.Element b) {

-      Contract.Requires(a != null);

-      Contract.Requires(b != null);

-      throw new NotImplementedException();

-    }

-

-    public override MathematicalLattice.Element NontrivialJoin(MathematicalLattice.Element a, MathematicalLattice.Element b) {

-      Contract.Requires(a != null);

-      Contract.Requires(b != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      throw new NotImplementedException();

-    }

-

-    public override MathematicalLattice.Element NontrivialMeet(MathematicalLattice.Element a, MathematicalLattice.Element b) {

-      Contract.Requires(a != null);

-      Contract.Requires(b != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      throw new NotImplementedException();

-    }

-

-    public override MathematicalLattice.Element Widen(MathematicalLattice.Element a, MathematicalLattice.Element b) {

-      Contract.Requires(a != null);

-      Contract.Requires(b != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      throw new NotImplementedException();

-    }

-  }

-

-

-  /// <summary>

-  ///  Provides an abstract interface for the operations of a lattice specific

-  ///  to abstract interpretation (i.e., that deals with the expression language).

-  /// </summary>

-  [ContractClass(typeof(LatticeContracts))]

-  public abstract class Lattice : MathematicalLattice {

-    internal readonly IValueExprFactory/*!*/ valueExprFactory;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(valueExprFactory != null);

-    }

-

-

-    public Lattice(IValueExprFactory/*!*/ valueExprFactory) {

-      Contract.Requires(valueExprFactory != null);

-      this.valueExprFactory = valueExprFactory;

-      // base();

-    }

-

-    #region Primitives that commands translate into

-

-    public abstract Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable);

-

-    public abstract Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName);

-

-    public abstract Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr);

-

-    #endregion

-

-

-    //        TODO keep this?

-    //        public Element! Eliminate(Element! e, VariableSeq! variables)

-    //        {

-    //            Lattice.Element result = e;

-    //            foreach (IVariable var in variables)

-    //            {

-    //                result = this.Eliminate(result, var);

-    //            }

-    //            return result;

-    //        }

-

-

-    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

-    // Note!

-    // 

-    // Concrete classes that implement Lattice must implement one of the AtMost

-    // overloads.  We provide here a default implementation for one given a "real"

-    // implementation of the other.  Otherwise, there will be an infinite loop!

-    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

-

-    protected override bool AtMost(Element/*!*/ a, Element/*!*/ b) {

-      //Contract.Requires(b != null);

-      //Contract.Requires(a != null);

-      return AtMost(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map);

-    }

-

-    protected virtual bool AtMost(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {

-      Contract.Requires(bToResult != null);

-      Contract.Requires(b != null);

-      Contract.Requires(aToResult != null);

-      Contract.Requires(a != null);

-      return AtMost(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult));

-    }

-

-    public bool LowerThan(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {

-      Contract.Requires(bToResult != null);

-      Contract.Requires(b != null);

-      Contract.Requires(aToResult != null);

-      Contract.Requires(a != null);

-      Answer ans = TrivialLowerThan(a, b);

-      return ans != Answer.Maybe ? ans == Answer.Yes : AtMost(a, aToResult, b, bToResult);

-    }

-

-    public bool HigherThan(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {

-      Contract.Requires(bToResult != null);

-      Contract.Requires(b != null);

-      Contract.Requires(aToResult != null);

-      Contract.Requires(a != null);

-      return LowerThan(b, bToResult, a, aToResult);

-    }

-

-

-    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

-    // Note!

-    // 

-    // Concrete classes that implement Lattice must implement one of the NontrivialJoin

-    // overloads.  We provide here a default implementation for one given a "real"

-    // implementation of the other.  Otherwise, there will be an infinite loop!

-    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

-

-    public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) {

-      //Contract.Requires(b != null);

-      //Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      return NontrivialJoin(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map);

-    }

-

-    public virtual Element/*!*/ NontrivialJoin(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {

-      Contract.Requires(bToResult != null);

-      Contract.Requires(b != null);

-      Contract.Requires(aToResult != null);

-      Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      return NontrivialJoin(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult));

-    }

-

-    public Element/*!*/ Join(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {

-      Contract.Requires(bToResult != null);

-      Contract.Requires(b != null);

-      Contract.Requires(aToResult != null);

-      Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      Element/*?*/ r = TrivialJoin(a, b);

-      return r != null ? r : NontrivialJoin(a, aToResult, b, bToResult);

-    }

-

-

-    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

-    // Note!

-    // 

-    // Concrete classes that implement Lattice must implement one of the Widen

-    // overloads.  We provide here a default implementation for one given a "real"

-    // implementation of the other.  Otherwise, there will be an infinite loop!

-    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

-

-    public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) {

-      //Contract.Requires(b != null);

-      //Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      return Widen(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map);

-    }

-

-    public virtual Element/*!*/ Widen(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {

-      Contract.Requires(bToResult != null);

-      Contract.Requires(b != null);

-      Contract.Requires(aToResult != null);

-      Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      return Widen(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult));

-    }

-

-

-

-    /// <summary>

-    ///  A default implementation of the <see cref="CheckVariableDisequality"/> given

-    ///  the appropriate expression factories by calling CheckPredicate.

-    /// </summary>

-    protected Answer DefaultCheckVariableDisequality(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valExprFactory, Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {

-      Contract.Requires(propExprFactory != null);

-      Contract.Requires(valExprFactory != null);

-      Contract.Requires(e != null);

-      Contract.Requires(var1 != null);

-      Contract.Requires(var2 != null);

-      return this.CheckPredicate(e, propExprFactory.Not(valExprFactory.Eq(var1, var2)));

-    }

-

-    private Element/*!*/ ApplyCombineNameMap(Element/*!*/ e, ICombineNameMap/*!*/ eToResult) {

-      Contract.Requires(eToResult != null);

-      Contract.Requires(e != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      Element/*!*/ result = e;

-

-      foreach (G.KeyValuePair<IVariable/*!*/, ISet/*<IVariable!>*//*!*/> entry in eToResult.GetSourceToResult()) {

-        IVariable/*!*/ sourceName = entry.Key;

-        Contract.Assert(sourceName != null);

-        ISet/*<IVariable!*//*!*/ resultNames = entry.Value;

-        Contract.Assert(resultNames != null);

-        // Renaming s to r is okay if

-        //       (1) s is not used in the result

-        //   and (2) s has not been renamed already

-        bool renameOkay = !resultNames.Contains(sourceName);

-        IVariable/*!*/ representative = sourceName;

-        Contract.Assert(representative != null);

-

-        foreach (IVariable/*!*/ rname in resultNames) {

-          Contract.Assert(rname != null);

-          // skip if sourceName and rname are the same

-          if (object.Equals(sourceName, rname)) {

-            continue;

-          }

-

-          if (renameOkay) {

-            result = this.Rename(result, sourceName, rname);

-            representative = rname; // representative now rname

-            renameOkay = false;  // no longer okay to rename

-          } else {

-            result = this.Constrain(result, valueExprFactory.Eq(representative, rname));

-          }

-        }

-      }

-

-      return result;

-    }

-

-    private sealed class IdentityCombineNameMap : ICombineNameMap {

-      public static readonly IdentityCombineNameMap/*!*/ Map = new IdentityCombineNameMap();

-

-      private static readonly G.Dictionary<IVariable/*!*/, ISet/*<IVariable!>*//*!*/>/*!*/ emptyDictionary1 = new G.Dictionary<IVariable/*!*/, ISet/*<IVariable!>*//*!*/>();

-      private static readonly G.Dictionary<IVariable/*!*/, IVariable/*!*/>/*!*/ emptyDictionary2 = new G.Dictionary<IVariable/*!*/, IVariable/*!*/>();

-      [ContractInvariantMethod]

-      void ObjectInvariant() {

-        Contract.Invariant(Map != null);

-        Contract.Invariant(cce.NonNullDictionaryAndValues(emptyDictionary1) && Contract.ForAll(emptyDictionary1.Values, set =>/*cce.NonNullElements(set)*/set != null));

-        Contract.Invariant(cce.NonNullDictionaryAndValues(emptyDictionary2));

-        Contract.Invariant(indexMap != null);

-        Contract.Invariant(reverseIndexMap != null);

-

-      }

-

-

-      public ISet/*<IVariable!>*//*?*/ GetResultNames(IVariable/*!*/ srcname) {

-        //Contract.Requires(srcname != null);

-        ArraySet a = new ArraySet();

-        a.Add(srcname);

-        return a;

-      }

-

-      public IVariable/*?*/ GetSourceName(IVariable/*!*/ resname) {

-        //Contract.Requires(resname != null);

-        return resname;

-      }

-

-      //TODO: uncomment when works in compiler

-      //public G.IEnumerable<G.KeyValuePair<IVariable!,ISet/*<IVariable!>*/!>> GetSourceToResult()

-      public IEnumerable/*!*/ GetSourceToResult() {

-        Contract.Ensures(Contract.Result<IEnumerable>() != null);

-        return emptyDictionary1;

-      }

-

-      //public G.IEnumerable<G.KeyValuePair<IVariable!,IVariable!>> GetResultToSource()

-      public IEnumerable/*!*/ GetResultToSource() {

-        Contract.Ensures(Contract.Result<IEnumerable>() != null);

-        return emptyDictionary2;

-      }

-

-      private IdentityCombineNameMap() {

-      }

-    }

-

-    #region Support for MultiLattice to uniquely number every subclass of Lattice

-

-

-    private static Hashtable/*<System.Type,int>*//*!*/ indexMap = new Hashtable();

-    private static Hashtable/*<int,Lattice>*//*!*/ reverseIndexMap = new Hashtable();

-    private static int globalCount = 0;

-

-    protected virtual object/*!*/ UniqueId {

-      get {

-        Contract.Ensures(Contract.Result<object>() != null);

-        return cce.NonNull(this.GetType());

-      }

-    }

-

-    public int Index {

-      get {

-        object unique = this.UniqueId;

-        if (indexMap.ContainsKey(unique)) {

-          object index = indexMap[unique];

-          Contract.Assert(index != null); // this does nothing for nonnull analysis

-          if (index != null) {

-            return (int)index;

-          }

-          return 0;

-        } else {

-          int myIndex = globalCount++;

-          indexMap[unique] = myIndex;

-          reverseIndexMap[myIndex] = this;

-          return myIndex;

-        }

-      }

-    }

-

-    public static Lattice GetGlobalLattice(int i) {

-      return reverseIndexMap[i] as Lattice;

-    }

-    #endregion

-

-    public static bool LogSwitch = false;

-    /// <summary>

-    ///  Returns the predicate that corresponds to the given lattice element.

-    /// </summary>

-    public abstract IExpr/*!*/ ToPredicate(Element/*!*/ e);

-

-    /// <summary>

-    ///  Allows the lattice to specify whether it understands a particular function symbol.

-    /// 

-    ///  The lattice is always allowed to return "true" even when it really can't do anything

-    ///  with such functions; however, it is advantageous to say "false" when possible to

-    ///  avoid being called to do certain things.

-    /// 

-    ///  The arguments to a function are provided for context so that the lattice can say

-    ///  true or false for the same function symbol in different situations.  For example,

-    ///  a lattice may understand the multiplication of a variable and a constant but not

-    ///  of two variables.  The implementation of a lattice should not hold on to the

-    ///  arguments.

-    /// </summary>

-    /// <param name="f">The function symbol.</param>

-    /// <param name="args">The argument context.</param>

-    /// <returns>True if it may understand f, false if it does not understand f.</returns>

-    public abstract bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args);

-

-    /// <summary>

-    ///  Return an expression that is equivalent to the given expression that does not

-    ///  contain the given variable according to the lattice element and queryable.

-    /// </summary>

-    /// <param name="e">The lattice element.</param>

-    /// <param name="q">A queryable for asking addtional information.</param>

-    /// <param name="expr">The expression to find an equivalent expression.</param>

-    /// <param name="var">The variable to eliminate.</param>

-    /// <param name="prohibitedVars">The set of variables that can't be used in the resulting expression.</param>

-    /// <returns>

-    /// An equivalent expression to <paramref name="expr"/> without <paramref name="var"/>

-    /// or null if not possible.

-    /// </returns>

-    public abstract IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, Set/*<IVariable!>*//*!*/ prohibitedVars);

-

-    /// <summary>

-    ///  Answers a query about whether the given predicate holds given the lattice element.

-    /// </summary>

-    /// <param name="e">The lattice element.</param>

-    /// <param name="pred">The predicate.</param>

-    /// <returns>Yes, No, or Maybe.</returns>

-    public abstract Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred);

-

-    /// <summary>

-    ///  Answers a disequality about two variables.  The same information could be obtained

-    ///  by asking CheckPredicate, but a different implementation may be simpler and more

-    ///  efficient.

-    /// </summary>

-    /// <param name="e">The lattice element.</param>

-    /// <param name="var1">The first variable.</param>

-    /// <param name="var2">The second variable.</param>

-    /// <returns>Yes, No, or Maybe.</returns>

-    public abstract Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2);

-

-    public abstract string/*!*/ ToString(Element/*!*/ e); // for debugging

-

-  }

-  [ContractClassFor(typeof(Lattice))]

-  abstract class LatticeContracts : Lattice {

-    public LatticeContracts()

-      : base(null) {

-    }

-    public override IExpr ToPredicate(MathematicalLattice.Element e) {

-      Contract.Requires(e != null);

-      Contract.Ensures(Contract.Result<IExpr>() != null);

-      throw new NotImplementedException();

-    }

-    public override bool Understands(IFunctionSymbol f, IList args) {

-      Contract.Requires(f != null);

-      Contract.Requires(args != null);

-      throw new NotImplementedException();

-    }

-    public override IExpr EquivalentExpr(MathematicalLattice.Element e, IQueryable q, IExpr expr, IVariable var, Set prohibitedVars) {

-      Contract.Requires(e != null);

-      Contract.Requires(q != null);

-      Contract.Requires(expr != null);

-      Contract.Requires(var != null);

-      Contract.Requires(prohibitedVars != null);

-      Contract.Ensures(Contract.Result<IExpr>() != null);

-      throw new NotImplementedException();

-    }

-    public override Answer CheckPredicate(MathematicalLattice.Element e, IExpr pred) {

-      Contract.Requires(e != null);

-      Contract.Requires(pred != null);

-      throw new NotImplementedException();

-    }

-    public override Answer CheckVariableDisequality(MathematicalLattice.Element e, IVariable var1, IVariable var2) {

-      Contract.Requires(e != null);

-      Contract.Requires(var1 != null);

-      Contract.Requires(var2 != null);

-      throw new NotImplementedException();

-    }

-    public override string ToString(Element e) {

-      Contract.Requires(e != null);

-      Contract.Ensures(Contract.Result<string>() != null);

-      throw new NotImplementedException();

-    }

-    public override MathematicalLattice.Element Eliminate(MathematicalLattice.Element e, IVariable variable) {

-      Contract.Requires(e != null);

-      Contract.Requires(variable != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      throw new NotImplementedException();

-    }

-    public override MathematicalLattice.Element Rename(MathematicalLattice.Element e, IVariable oldName, IVariable newName) {

-      Contract.Requires(e != null);

-      Contract.Requires(oldName != null);

-      Contract.Requires(newName != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      throw new NotImplementedException();

-    }

-    public override MathematicalLattice.Element Constrain(MathematicalLattice.Element e, IExpr expr) {

-      Contract.Requires(e != null);

-      Contract.Requires(expr != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      throw new NotImplementedException();

-    }

-  }

-

-  /// <summary>

-  ///   Defines the relation between names used in the respective input lattice elements to the

-  ///   various combination operators (Join,Widen,Meet,AtMost) and the names that should be used

-  ///   in the resulting lattice element.

-  /// </summary>

-  [ContractClass(typeof(ICombineNameMapContracts))]

-  public interface ICombineNameMap {

-    ISet/*<IVariable!>*//*?*/ GetResultNames(IVariable/*!*/ srcname);

-    IVariable/*?*/ GetSourceName(IVariable/*!*/ resname);

-

-    //TODO: uncommet when works in compiler

-    //G.IEnumerable<G.KeyValuePair<IVariable!,ISet/*<IVariable!>*/!>> GetSourceToResult();

-    IEnumerable/*!*/ GetSourceToResult();

-    //G.IEnumerable<G.KeyValuePair<IVariable!,IVariable!>> GetResultToSource();

-    IEnumerable/*!*/ GetResultToSource();

-  }

-  [ContractClassFor(typeof(ICombineNameMap))]

-  public abstract class ICombineNameMapContracts : ICombineNameMap {

-    #region ICombineNameMap Members

-

-    public Set GetResultNames(IVariable srcname) {

-      Contract.Requires(srcname != null);

-      throw new NotImplementedException();

-    }

-

-    public IVariable GetSourceName(IVariable resname) {

-      Contract.Requires(resname != null);

-      throw new NotImplementedException();

-    }

-

-    public IEnumerable GetSourceToResult() {

-      Contract.Ensures(Contract.Result<IEnumerable>() != null);

-      throw new NotImplementedException();

-    }

-

-    public IEnumerable GetResultToSource() {

-      Contract.Ensures(Contract.Result<IEnumerable>() != null);

-      throw new NotImplementedException();

-    }

-

-    #endregion

-  }

-

-  /// <summary>

-  ///   Provides statistics on the number of times an operation is performed

-  ///   and forwards the real operations to the given lattice in the constructor.

-  /// </summary>

-  public class StatisticsLattice : Lattice {

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(lattice != null);

-    }

-

-    readonly Lattice/*!*/ lattice;

-    int eliminateCount;

-    int renameCount;

-    int constrainCount;

-    int toPredicateCount;

-    int atMostCount;

-    int topCount;

-    int bottomCount;

-    int isTopCount;

-    int isBottomCount;

-    int joinCount;

-    int meetCount;

-    int widenCount;

-    int understandsCount;

-    int equivalentExprCount;

-    int checkPredicateCount;

-    int checkVariableDisequalityCount;

-

-    public StatisticsLattice(Lattice/*!*/ lattice)

-      : base(lattice.valueExprFactory) {

-      Contract.Requires(lattice != null);

-      this.lattice = lattice;

-      // base(lattice.valueExprFactory);

-    }

-

-    public override Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable) {

-      //Contract.Requires(variable != null);

-      //Contract.Requires(e != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      eliminateCount++;

-      return lattice.Eliminate(e, variable);

-    }

-

-    public override Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName) {

-      //Contract.Requires(newName != null);

-      //Contract.Requires(oldName != null);

-      //Contract.Requires(e != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      renameCount++;

-      return lattice.Rename(e, oldName, newName);

-    }

-

-    public override Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr) {

-      //Contract.Requires(expr != null);

-      //Contract.Requires(e != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      constrainCount++;

-      return lattice.Constrain(e, expr);

-    }

-

-

-    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {

-      //Contract.Requires(args != null);

-      //Contract.Requires(f != null);

-      understandsCount++;

-      return lattice.Understands(f, args);

-    }

-

-

-    public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars) {

-      //Contract.Requires(prohibitedVars != null);

-      //Contract.Requires(var != null);

-      //Contract.Requires(expr != null);

-      //Contract.Requires(q != null);

-      //Contract.Requires(e != null);

-      equivalentExprCount++;

-      return lattice.EquivalentExpr(e, q, expr, var, prohibitedVars);

-    }

-

-

-    public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {

-      //Contract.Requires(pred != null);

-      //Contract.Requires(e != null);

-      checkPredicateCount++;

-      return lattice.CheckPredicate(e, pred);

-    }

-

-

-    public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {

-      //Contract.Requires(var2 != null);

-      //Contract.Requires(var1 != null);

-      //Contract.Requires(e != null);

-      checkVariableDisequalityCount++;

-      return lattice.CheckVariableDisequality(e, var1, var2);

-    }

-

-

-

-    public override IExpr/*!*/ ToPredicate(Element/*!*/ e) {

-      //Contract.Requires(e != null);

-      Contract.Ensures(Contract.Result<IExpr>() != null);

-      toPredicateCount++;

-      return lattice.ToPredicate(e);

-    }

-

-    public override string/*!*/ ToString(Element/*!*/ e) {

-      //Contract.Requires(e != null);

-      Contract.Ensures(Contract.Result<string>() != null);

-      return lattice.ToString(e);

-    }

-

-    [Pure]

-    public override string/*!*/ ToString() {

-      Contract.Ensures(Contract.Result<string>() != null);

-      return string.Format(

-        "StatisticsLattice: #Eliminate={0} #Rename={1} #Constrain={2} #ToPredicate={3} " +

-        "#Understands={4} #EquivalentExpr={5} #CheckPredicate={6} #CheckVariableDisequality={7} " +

-        "#AtMost={8} #Top={9} #Bottom={9} #IsTop={10} #IsBottom={11} " +

-        "#NonTrivialJoin={12} #NonTrivialMeet={13} #Widen={14}",

-        eliminateCount, renameCount, constrainCount, toPredicateCount,

-        understandsCount, equivalentExprCount, checkPredicateCount, checkVariableDisequalityCount,

-        atMostCount, topCount, bottomCount, isTopCount, isBottomCount,

-        joinCount, meetCount, widenCount);

-    }

-

-    protected override bool AtMost(Element/*!*/ a, Element/*!*/ b) {

-      //Contract.Requires(b != null);

-      //Contract.Requires(a != null);

-      atMostCount++;

-      return lattice.LowerThan(a, b);

-    }

-

-    public override Element/*!*/ Top {

-      get {

-        Contract.Ensures(Contract.Result<Element>() != null);

-        topCount++;

-        return lattice.Top;

-      }

-    }

-    public override Element/*!*/ Bottom {

-      get {

-        Contract.Ensures(Contract.Result<Element>() != null);

-        bottomCount++;

-        return lattice.Bottom;

-      }

-    }

-

-    public override bool IsTop(Element/*!*/ e) {

-      //Contract.Requires(e != null);

-      isTopCount++;

-      return lattice.IsTop(e);

-    }

-

-    public override bool IsBottom(Element/*!*/ e) {

-      //Contract.Requires(e != null);

-      isBottomCount++;

-      return lattice.IsBottom(e);

-    }

-

-    public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) {

-      //Contract.Requires(b != null);

-      //Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      joinCount++;

-      return lattice.NontrivialJoin(a, b);

-    }

-

-    public override Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b) {

-      //Contract.Requires(b != null);

-      //Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      meetCount++;

-      return lattice.NontrivialMeet(a, b);

-    }

-

-    public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) {

-      //Contract.Requires(b != null);

-      //Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<Element>() != null);

-      widenCount++;

-      return lattice.Widen(a, b);

-    }

-

-    public override void Validate() {

-      base.Validate();

-      lattice.Validate();

-    }

-

-    protected override object/*!*/ UniqueId {

-      get {

-        Contract.Ensures(Contract.Result<object>() != null);

-        // use the base id, not the underlying-lattice id (is that the right thing to do?)

-        return base.UniqueId;

-      }

-    }

-  }

-

-

-  public sealed class LatticeQueryable : IQueryable {

-    private Lattice/*!*/ lattice;

-    private Lattice.Element/*!*/ element;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(lattice != null);

-      Contract.Invariant(element != null);

-    }

-

-

-    public LatticeQueryable(Lattice/*!*/ lattice, Lattice.Element/*!*/ element) {

-      Contract.Requires(element != null);

-      Contract.Requires(lattice != null);

-      this.lattice = lattice;

-      this.element = element;

-      // base();

-    }

-

-    public Answer CheckPredicate(IExpr/*!*/ pred) {

-      //Contract.Requires(pred != null);

-      return lattice.CheckPredicate(element, pred);

-    }

-

-    public Answer CheckVariableDisequality(IVariable/*!*/ var1, IVariable/*!*/ var2) {

-      //Contract.Requires(var2 != null);

-      //Contract.Requires(var1 != null);

-      return lattice.CheckVariableDisequality(element, var1, var2);

-    }

-  }

-}

+  using IMutableSet = Microsoft.Boogie.GSet<object>; 
+  using HashSet = Microsoft.Boogie.GSet<object>;
+  using ISet = Microsoft.Boogie.GSet<object>;
+  using Set = Microsoft.Boogie.GSet<object>;
+
+
+  /// <summary>
+  ///  Specifies the operations (e.g., join) on a mathematical lattice that depend
+  ///  only on the elements of the lattice.
+  /// </summary>
+  [ContractClass(typeof(MathematicalLatticeContracts))]
+  public abstract class MathematicalLattice {
+    #region Element
+    /// <summary>
+    ///  An element of the lattice.  This class should be derived from in any
+    ///  implementation of MathematicalLattice.
+    /// </summary>
+    [ContractClass(typeof(ElementContracts))]
+    public abstract class Element : System.ICloneable {
+      /// <summary>
+      /// Print out a debug-useful representation of the internal data structure of the lattice element.
+      /// </summary>
+      public virtual void Dump(string/*!*/ msg) {
+        Contract.Requires(msg != null);
+        System.Console.WriteLine("Dump({0}) = {1}", msg, this);
+      }
+
+      public abstract Element/*!*/ Clone();
+      object/*!*/ System.ICloneable.Clone() {
+        return this.Clone();
+      }
+
+      public abstract G.ICollection<IVariable/*!*/>/*!*/ FreeVariables();
+
+    }
+    [ContractClassFor(typeof(Element))]
+    public abstract class ElementContracts : Element {
+      public override Element Clone() {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        throw new NotImplementedException();
+
+      }
+
+      public override System.Collections.Generic.ICollection<IVariable> FreeVariables() {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<G.ICollection<IVariable>>()));
+        Contract.Ensures(Contract.Result<System.Collections.Generic.ICollection<IVariable>>().IsReadOnly);
+        throw new System.NotImplementedException();
+      }
+    }
+    #endregion
+
+    public abstract Element/*!*/ Top {
+      get;
+    }
+    public abstract Element/*!*/ Bottom {
+      get;
+    }
+
+    public abstract bool IsTop(Element/*!*/ e);
+    public abstract bool IsBottom(Element/*!*/ e);
+
+    /// <summary>
+    /// Returns true if a &lt;= this.
+    /// </summary>
+    protected abstract bool AtMost(Element/*!*/ a, Element/*!*/ b);
+    /* The following cases are handled elsewhere and need not be considered in subclass. */
+    //  requires a.GetType() == b.GetType();
+    //  requires ! a.IsTop;
+    //  requires ! a.IsBottom;
+    //  requires ! b.IsTop;
+    //  requires ! b.IsBottom;
+
+
+    protected Answer TrivialLowerThan(Element/*!*/ a, Element/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      if (a.GetType() != b.GetType()) {
+        throw new System.InvalidOperationException(
+          "operands to <= must be of same Element type"
+          );
+      }
+      if (IsBottom(a)) {
+        return Answer.Yes;
+      }
+      if (IsTop(b)) {
+        return Answer.Yes;
+      }
+      if (IsTop(a)) {
+        return Answer.No;
+      }
+      if (IsBottom(b)) {
+        return Answer.No;
+      }
+
+      return Answer.Maybe;
+    }
+
+    // Is 'a' better information than 'b'?
+    //
+    public bool LowerThan(Element/*!*/ a, Element/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Answer ans = TrivialLowerThan(a, b);
+      return ans != Answer.Maybe ? ans == Answer.Yes : AtMost(a, b);
+    }
+
+    // Is 'a' worse information than 'b'?
+    //
+    public bool HigherThan(Element/*!*/ a, Element/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      return LowerThan(b, a);
+    }
+
+    // Are 'a' and 'b' equivalent?
+    //
+    public bool Equivalent(Element/*!*/ a, Element/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      return LowerThan(a, b) && LowerThan(b, a);
+    }
+
+    public abstract Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b);
+    /* The following cases are handled elsewhere and need not be considered in subclass. */
+    //  requires a.GetType() == b.GetType();
+    //  requires ! a.IsTop;
+    //  requires ! a.IsBottom;
+    //  requires ! b.IsTop;
+    //  requires ! b.IsBottom;
+
+
+    protected Element/*?*/ TrivialJoin(Element/*!*/ a, Element/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      if (a.GetType() != b.GetType()) {
+        throw new System.InvalidOperationException(
+          "operands to Join must be of same Lattice.Element type"
+          );
+      }
+      if (IsTop(a)) {
+        return a;
+      }
+      if (IsTop(b)) {
+        return b;
+      }
+      if (IsBottom(a)) {
+        return b;
+      }
+      if (IsBottom(b)) {
+        return a;
+      }
+
+      return null;
+    }
+
+    public Element/*!*/ Join(Element/*!*/ a, Element/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Element/*?*/ r = TrivialJoin(a, b);
+      return r != null ? r : NontrivialJoin(a, b);
+    }
+
+    public abstract Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b)
+      /* The following cases are handled elsewhere and need not be considered in subclass. */
+      //  requires a.GetType() == b.GetType();
+      //  requires ! a.IsTop;
+      //  requires ! a.IsBottom;
+      //  requires ! b.IsTop;
+      //  requires ! b.IsBottom;
+    ;
+
+    protected Element/*?*/ TrivialMeet(Element/*!*/ a, Element/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      if (a.GetType() != b.GetType()) {
+        throw new System.InvalidOperationException(
+          "operands to Meet must be of same Lattice.Element type"
+          );
+      }
+      if (IsTop(a)) {
+        return b;
+      }
+      if (IsTop(b)) {
+        return a;
+      }
+      if (IsBottom(a)) {
+        return a;
+      }
+      if (IsBottom(b)) {
+        return b;
+      }
+
+      return null;
+    }
+
+    public Element/*!*/ Meet(Element/*!*/ a, Element/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Element/*?*/ r = TrivialMeet(a, b);
+      return r != null ? r : NontrivialMeet(a, b);
+    }
+
+    public abstract Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b);
+
+    public virtual void Validate() {
+      Debug.Assert(IsTop(Top));
+      Debug.Assert(IsBottom(Bottom));
+      Debug.Assert(!IsBottom(Top));
+      Debug.Assert(!IsTop(Bottom));
+
+      Debug.Assert(LowerThan(Top, Top));
+      Debug.Assert(LowerThan(Bottom, Top));
+      Debug.Assert(LowerThan(Bottom, Bottom));
+
+      Debug.Assert(IsTop(Join(Top, Top)));
+      Debug.Assert(IsBottom(Join(Bottom, Bottom)));
+    }
+  }
+  [ContractClassFor(typeof(MathematicalLattice))]
+  public abstract class MathematicalLatticeContracts : MathematicalLattice {
+    public override MathematicalLattice.Element Top {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        throw new NotImplementedException();
+      }
+    }
+
+    public override MathematicalLattice.Element Bottom {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        throw new NotImplementedException();
+      }
+    }
+
+    public override bool IsTop(MathematicalLattice.Element e) {
+      Contract.Requires(e != null);
+      throw new NotImplementedException();
+    }
+
+    public override bool IsBottom(MathematicalLattice.Element e) {
+      Contract.Requires(e != null);
+      throw new NotImplementedException();
+    }
+
+    protected override bool AtMost(MathematicalLattice.Element a, MathematicalLattice.Element b) {
+      Contract.Requires(a != null);
+      Contract.Requires(b != null);
+      throw new NotImplementedException();
+    }
+
+    public override MathematicalLattice.Element NontrivialJoin(MathematicalLattice.Element a, MathematicalLattice.Element b) {
+      Contract.Requires(a != null);
+      Contract.Requires(b != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      throw new NotImplementedException();
+    }
+
+    public override MathematicalLattice.Element NontrivialMeet(MathematicalLattice.Element a, MathematicalLattice.Element b) {
+      Contract.Requires(a != null);
+      Contract.Requires(b != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      throw new NotImplementedException();
+    }
+
+    public override MathematicalLattice.Element Widen(MathematicalLattice.Element a, MathematicalLattice.Element b) {
+      Contract.Requires(a != null);
+      Contract.Requires(b != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      throw new NotImplementedException();
+    }
+  }
+
+
+  /// <summary>
+  ///  Provides an abstract interface for the operations of a lattice specific
+  ///  to abstract interpretation (i.e., that deals with the expression language).
+  /// </summary>
+  [ContractClass(typeof(LatticeContracts))]
+  public abstract class Lattice : MathematicalLattice {
+    internal readonly IValueExprFactory/*!*/ valueExprFactory;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(valueExprFactory != null);
+    }
+
+
+    public Lattice(IValueExprFactory/*!*/ valueExprFactory) {
+      Contract.Requires(valueExprFactory != null);
+      this.valueExprFactory = valueExprFactory;
+      // base();
+    }
+
+    #region Primitives that commands translate into
+
+    public abstract Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable);
+
+    public abstract Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName);
+
+    public abstract Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr);
+
+    #endregion
+
+
+    //        TODO keep this?
+    //        public Element! Eliminate(Element! e, VariableSeq! variables)
+    //        {
+    //            Lattice.Element result = e;
+    //            foreach (IVariable var in variables)
+    //            {
+    //                result = this.Eliminate(result, var);
+    //            }
+    //            return result;
+    //        }
+
+
+    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+    // Note!
+    // 
+    // Concrete classes that implement Lattice must implement one of the AtMost
+    // overloads.  We provide here a default implementation for one given a "real"
+    // implementation of the other.  Otherwise, there will be an infinite loop!
+    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+
+    protected override bool AtMost(Element/*!*/ a, Element/*!*/ b) {
+      //Contract.Requires(b != null);
+      //Contract.Requires(a != null);
+      return AtMost(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map);
+    }
+
+    protected virtual bool AtMost(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {
+      Contract.Requires(bToResult != null);
+      Contract.Requires(b != null);
+      Contract.Requires(aToResult != null);
+      Contract.Requires(a != null);
+      return AtMost(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult));
+    }
+
+    public bool LowerThan(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {
+      Contract.Requires(bToResult != null);
+      Contract.Requires(b != null);
+      Contract.Requires(aToResult != null);
+      Contract.Requires(a != null);
+      Answer ans = TrivialLowerThan(a, b);
+      return ans != Answer.Maybe ? ans == Answer.Yes : AtMost(a, aToResult, b, bToResult);
+    }
+
+    public bool HigherThan(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {
+      Contract.Requires(bToResult != null);
+      Contract.Requires(b != null);
+      Contract.Requires(aToResult != null);
+      Contract.Requires(a != null);
+      return LowerThan(b, bToResult, a, aToResult);
+    }
+
+
+    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+    // Note!
+    // 
+    // Concrete classes that implement Lattice must implement one of the NontrivialJoin
+    // overloads.  We provide here a default implementation for one given a "real"
+    // implementation of the other.  Otherwise, there will be an infinite loop!
+    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+
+    public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) {
+      //Contract.Requires(b != null);
+      //Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      return NontrivialJoin(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map);
+    }
+
+    public virtual Element/*!*/ NontrivialJoin(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {
+      Contract.Requires(bToResult != null);
+      Contract.Requires(b != null);
+      Contract.Requires(aToResult != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      return NontrivialJoin(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult));
+    }
+
+    public Element/*!*/ Join(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {
+      Contract.Requires(bToResult != null);
+      Contract.Requires(b != null);
+      Contract.Requires(aToResult != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Element/*?*/ r = TrivialJoin(a, b);
+      return r != null ? r : NontrivialJoin(a, aToResult, b, bToResult);
+    }
+
+
+    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+    // Note!
+    // 
+    // Concrete classes that implement Lattice must implement one of the Widen
+    // overloads.  We provide here a default implementation for one given a "real"
+    // implementation of the other.  Otherwise, there will be an infinite loop!
+    //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+
+    public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) {
+      //Contract.Requires(b != null);
+      //Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      return Widen(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map);
+    }
+
+    public virtual Element/*!*/ Widen(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {
+      Contract.Requires(bToResult != null);
+      Contract.Requires(b != null);
+      Contract.Requires(aToResult != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      return Widen(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult));
+    }
+
+
+
+    /// <summary>
+    ///  A default implementation of the <see cref="CheckVariableDisequality"/> given
+    ///  the appropriate expression factories by calling CheckPredicate.
+    /// </summary>
+    protected Answer DefaultCheckVariableDisequality(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valExprFactory, Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
+      Contract.Requires(propExprFactory != null);
+      Contract.Requires(valExprFactory != null);
+      Contract.Requires(e != null);
+      Contract.Requires(var1 != null);
+      Contract.Requires(var2 != null);
+      return this.CheckPredicate(e, propExprFactory.Not(valExprFactory.Eq(var1, var2)));
+    }
+
+    private Element/*!*/ ApplyCombineNameMap(Element/*!*/ e, ICombineNameMap/*!*/ eToResult) {
+      Contract.Requires(eToResult != null);
+      Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      Element/*!*/ result = e;
+
+      foreach (G.KeyValuePair<IVariable/*!*/, ISet/*<IVariable!>*//*!*/> entry in eToResult.GetSourceToResult()) {
+        IVariable/*!*/ sourceName = entry.Key;
+        Contract.Assert(sourceName != null);
+        ISet/*<IVariable!*//*!*/ resultNames = entry.Value;
+        Contract.Assert(resultNames != null);
+        // Renaming s to r is okay if
+        //       (1) s is not used in the result
+        //   and (2) s has not been renamed already
+        bool renameOkay = !resultNames.Contains(sourceName);
+        IVariable/*!*/ representative = sourceName;
+        Contract.Assert(representative != null);
+
+        foreach (IVariable/*!*/ rname in resultNames) {
+          Contract.Assert(rname != null);
+          // skip if sourceName and rname are the same
+          if (object.Equals(sourceName, rname)) {
+            continue;
+          }
+
+          if (renameOkay) {
+            result = this.Rename(result, sourceName, rname);
+            representative = rname; // representative now rname
+            renameOkay = false;  // no longer okay to rename
+          } else {
+            result = this.Constrain(result, valueExprFactory.Eq(representative, rname));
+          }
+        }
+      }
+
+      return result;
+    }
+
+    private sealed class IdentityCombineNameMap : ICombineNameMap {
+      public static readonly IdentityCombineNameMap/*!*/ Map = new IdentityCombineNameMap();
+
+      private static readonly G.Dictionary<IVariable/*!*/, ISet/*<IVariable!>*//*!*/>/*!*/ emptyDictionary1 = new G.Dictionary<IVariable/*!*/, ISet/*<IVariable!>*//*!*/>();
+      private static readonly G.Dictionary<IVariable/*!*/, IVariable/*!*/>/*!*/ emptyDictionary2 = new G.Dictionary<IVariable/*!*/, IVariable/*!*/>();
+      [ContractInvariantMethod]
+      void ObjectInvariant() {
+        Contract.Invariant(Map != null);
+        Contract.Invariant(cce.NonNullDictionaryAndValues(emptyDictionary1) && Contract.ForAll(emptyDictionary1.Values, set =>/*cce.NonNullElements(set)*/set != null));
+        Contract.Invariant(cce.NonNullDictionaryAndValues(emptyDictionary2));
+        Contract.Invariant(indexMap != null);
+        Contract.Invariant(reverseIndexMap != null);
+
+      }
+
+
+      public ISet/*<IVariable!>*//*?*/ GetResultNames(IVariable/*!*/ srcname) {
+        //Contract.Requires(srcname != null);
+        ArraySet a = new ArraySet();
+        a.Add(srcname);
+        return a;
+      }
+
+      public IVariable/*?*/ GetSourceName(IVariable/*!*/ resname) {
+        //Contract.Requires(resname != null);
+        return resname;
+      }
+
+      //TODO: uncomment when works in compiler
+      //public G.IEnumerable<G.KeyValuePair<IVariable!,ISet/*<IVariable!>*/!>> GetSourceToResult()
+      public IEnumerable/*!*/ GetSourceToResult() {
+        Contract.Ensures(Contract.Result<IEnumerable>() != null);
+        return emptyDictionary1;
+      }
+
+      //public G.IEnumerable<G.KeyValuePair<IVariable!,IVariable!>> GetResultToSource()
+      public IEnumerable/*!*/ GetResultToSource() {
+        Contract.Ensures(Contract.Result<IEnumerable>() != null);
+        return emptyDictionary2;
+      }
+
+      private IdentityCombineNameMap() {
+      }
+    }
+
+    #region Support for MultiLattice to uniquely number every subclass of Lattice
+
+
+    private static Hashtable/*<System.Type,int>*//*!*/ indexMap = new Hashtable();
+    private static Hashtable/*<int,Lattice>*//*!*/ reverseIndexMap = new Hashtable();
+    private static int globalCount = 0;
+
+    protected virtual object/*!*/ UniqueId {
+      get {
+        Contract.Ensures(Contract.Result<object>() != null);
+        return cce.NonNull(this.GetType());
+      }
+    }
+
+    public int Index {
+      get {
+        object unique = this.UniqueId;
+        if (indexMap.ContainsKey(unique)) {
+          object index = indexMap[unique];
+          Contract.Assert(index != null); // this does nothing for nonnull analysis
+          if (index != null) {
+            return (int)index;
+          }
+          return 0;
+        } else {
+          int myIndex = globalCount++;
+          indexMap[unique] = myIndex;
+          reverseIndexMap[myIndex] = this;
+          return myIndex;
+        }
+      }
+    }
+
+    public static Lattice GetGlobalLattice(int i) {
+      return reverseIndexMap[i] as Lattice;
+    }
+    #endregion
+
+    public static bool LogSwitch = false;
+    /// <summary>
+    ///  Returns the predicate that corresponds to the given lattice element.
+    /// </summary>
+    public abstract IExpr/*!*/ ToPredicate(Element/*!*/ e);
+
+    /// <summary>
+    ///  Allows the lattice to specify whether it understands a particular function symbol.
+    /// 
+    ///  The lattice is always allowed to return "true" even when it really can't do anything
+    ///  with such functions; however, it is advantageous to say "false" when possible to
+    ///  avoid being called to do certain things.
+    /// 
+    ///  The arguments to a function are provided for context so that the lattice can say
+    ///  true or false for the same function symbol in different situations.  For example,
+    ///  a lattice may understand the multiplication of a variable and a constant but not
+    ///  of two variables.  The implementation of a lattice should not hold on to the
+    ///  arguments.
+    /// </summary>
+    /// <param name="f">The function symbol.</param>
+    /// <param name="args">The argument context.</param>
+    /// <returns>True if it may understand f, false if it does not understand f.</returns>
+    public abstract bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args);
+
+    /// <summary>
+    ///  Return an expression that is equivalent to the given expression that does not
+    ///  contain the given variable according to the lattice element and queryable.
+    /// </summary>
+    /// <param name="e">The lattice element.</param>
+    /// <param name="q">A queryable for asking addtional information.</param>
+    /// <param name="expr">The expression to find an equivalent expression.</param>
+    /// <param name="var">The variable to eliminate.</param>
+    /// <param name="prohibitedVars">The set of variables that can't be used in the resulting expression.</param>
+    /// <returns>
+    /// An equivalent expression to <paramref name="expr"/> without <paramref name="var"/>
+    /// or null if not possible.
+    /// </returns>
+    public abstract IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, Set/*<IVariable!>*//*!*/ prohibitedVars);
+
+    /// <summary>
+    ///  Answers a query about whether the given predicate holds given the lattice element.
+    /// </summary>
+    /// <param name="e">The lattice element.</param>
+    /// <param name="pred">The predicate.</param>
+    /// <returns>Yes, No, or Maybe.</returns>
+    public abstract Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred);
+
+    /// <summary>
+    ///  Answers a disequality about two variables.  The same information could be obtained
+    ///  by asking CheckPredicate, but a different implementation may be simpler and more
+    ///  efficient.
+    /// </summary>
+    /// <param name="e">The lattice element.</param>
+    /// <param name="var1">The first variable.</param>
+    /// <param name="var2">The second variable.</param>
+    /// <returns>Yes, No, or Maybe.</returns>
+    public abstract Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2);
+
+    public abstract string/*!*/ ToString(Element/*!*/ e); // for debugging
+
+  }
+  [ContractClassFor(typeof(Lattice))]
+  abstract class LatticeContracts : Lattice {
+    public LatticeContracts()
+      : base(null) {
+    }
+    public override IExpr ToPredicate(MathematicalLattice.Element e) {
+      Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      throw new NotImplementedException();
+    }
+    public override bool Understands(IFunctionSymbol f, IList args) {
+      Contract.Requires(f != null);
+      Contract.Requires(args != null);
+      throw new NotImplementedException();
+    }
+    public override IExpr EquivalentExpr(MathematicalLattice.Element e, IQueryable q, IExpr expr, IVariable var, Set prohibitedVars) {
+      Contract.Requires(e != null);
+      Contract.Requires(q != null);
+      Contract.Requires(expr != null);
+      Contract.Requires(var != null);
+      Contract.Requires(prohibitedVars != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      throw new NotImplementedException();
+    }
+    public override Answer CheckPredicate(MathematicalLattice.Element e, IExpr pred) {
+      Contract.Requires(e != null);
+      Contract.Requires(pred != null);
+      throw new NotImplementedException();
+    }
+    public override Answer CheckVariableDisequality(MathematicalLattice.Element e, IVariable var1, IVariable var2) {
+      Contract.Requires(e != null);
+      Contract.Requires(var1 != null);
+      Contract.Requires(var2 != null);
+      throw new NotImplementedException();
+    }
+    public override string ToString(Element e) {
+      Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<string>() != null);
+      throw new NotImplementedException();
+    }
+    public override MathematicalLattice.Element Eliminate(MathematicalLattice.Element e, IVariable variable) {
+      Contract.Requires(e != null);
+      Contract.Requires(variable != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      throw new NotImplementedException();
+    }
+    public override MathematicalLattice.Element Rename(MathematicalLattice.Element e, IVariable oldName, IVariable newName) {
+      Contract.Requires(e != null);
+      Contract.Requires(oldName != null);
+      Contract.Requires(newName != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      throw new NotImplementedException();
+    }
+    public override MathematicalLattice.Element Constrain(MathematicalLattice.Element e, IExpr expr) {
+      Contract.Requires(e != null);
+      Contract.Requires(expr != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      throw new NotImplementedException();
+    }
+  }
+
+  /// <summary>
+  ///   Defines the relation between names used in the respective input lattice elements to the
+  ///   various combination operators (Join,Widen,Meet,AtMost) and the names that should be used
+  ///   in the resulting lattice element.
+  /// </summary>
+  [ContractClass(typeof(ICombineNameMapContracts))]
+  public interface ICombineNameMap {
+    ISet/*<IVariable!>*//*?*/ GetResultNames(IVariable/*!*/ srcname);
+    IVariable/*?*/ GetSourceName(IVariable/*!*/ resname);
+
+    //TODO: uncommet when works in compiler
+    //G.IEnumerable<G.KeyValuePair<IVariable!,ISet/*<IVariable!>*/!>> GetSourceToResult();
+    IEnumerable/*!*/ GetSourceToResult();
+    //G.IEnumerable<G.KeyValuePair<IVariable!,IVariable!>> GetResultToSource();
+    IEnumerable/*!*/ GetResultToSource();
+  }
+  [ContractClassFor(typeof(ICombineNameMap))]
+  public abstract class ICombineNameMapContracts : ICombineNameMap {
+    #region ICombineNameMap Members
+
+    public Set GetResultNames(IVariable srcname) {
+      Contract.Requires(srcname != null);
+      throw new NotImplementedException();
+    }
+
+    public IVariable GetSourceName(IVariable resname) {
+      Contract.Requires(resname != null);
+      throw new NotImplementedException();
+    }
+
+    public IEnumerable GetSourceToResult() {
+      Contract.Ensures(Contract.Result<IEnumerable>() != null);
+      throw new NotImplementedException();
+    }
+
+    public IEnumerable GetResultToSource() {
+      Contract.Ensures(Contract.Result<IEnumerable>() != null);
+      throw new NotImplementedException();
+    }
+
+    #endregion
+  }
+
+  /// <summary>
+  ///   Provides statistics on the number of times an operation is performed
+  ///   and forwards the real operations to the given lattice in the constructor.
+  /// </summary>
+  public class StatisticsLattice : Lattice {
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(lattice != null);
+    }
+
+    readonly Lattice/*!*/ lattice;
+    int eliminateCount;
+    int renameCount;
+    int constrainCount;
+    int toPredicateCount;
+    int atMostCount;
+    int topCount;
+    int bottomCount;
+    int isTopCount;
+    int isBottomCount;
+    int joinCount;
+    int meetCount;
+    int widenCount;
+    int understandsCount;
+    int equivalentExprCount;
+    int checkPredicateCount;
+    int checkVariableDisequalityCount;
+
+    public StatisticsLattice(Lattice/*!*/ lattice)
+      : base(lattice.valueExprFactory) {
+      Contract.Requires(lattice != null);
+      this.lattice = lattice;
+      // base(lattice.valueExprFactory);
+    }
+
+    public override Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable) {
+      //Contract.Requires(variable != null);
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      eliminateCount++;
+      return lattice.Eliminate(e, variable);
+    }
+
+    public override Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+      //Contract.Requires(newName != null);
+      //Contract.Requires(oldName != null);
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      renameCount++;
+      return lattice.Rename(e, oldName, newName);
+    }
+
+    public override Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr) {
+      //Contract.Requires(expr != null);
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      constrainCount++;
+      return lattice.Constrain(e, expr);
+    }
+
+
+    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
+      //Contract.Requires(args != null);
+      //Contract.Requires(f != null);
+      understandsCount++;
+      return lattice.Understands(f, args);
+    }
+
+
+    public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars) {
+      //Contract.Requires(prohibitedVars != null);
+      //Contract.Requires(var != null);
+      //Contract.Requires(expr != null);
+      //Contract.Requires(q != null);
+      //Contract.Requires(e != null);
+      equivalentExprCount++;
+      return lattice.EquivalentExpr(e, q, expr, var, prohibitedVars);
+    }
+
+
+    public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
+      //Contract.Requires(pred != null);
+      //Contract.Requires(e != null);
+      checkPredicateCount++;
+      return lattice.CheckPredicate(e, pred);
+    }
+
+
+    public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
+      //Contract.Requires(var2 != null);
+      //Contract.Requires(var1 != null);
+      //Contract.Requires(e != null);
+      checkVariableDisequalityCount++;
+      return lattice.CheckVariableDisequality(e, var1, var2);
+    }
+
+
+
+    public override IExpr/*!*/ ToPredicate(Element/*!*/ e) {
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      toPredicateCount++;
+      return lattice.ToPredicate(e);
+    }
+
+    public override string/*!*/ ToString(Element/*!*/ e) {
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<string>() != null);
+      return lattice.ToString(e);
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return string.Format(
+        "StatisticsLattice: #Eliminate={0} #Rename={1} #Constrain={2} #ToPredicate={3} " +
+        "#Understands={4} #EquivalentExpr={5} #CheckPredicate={6} #CheckVariableDisequality={7} " +
+        "#AtMost={8} #Top={9} #Bottom={9} #IsTop={10} #IsBottom={11} " +
+        "#NonTrivialJoin={12} #NonTrivialMeet={13} #Widen={14}",
+        eliminateCount, renameCount, constrainCount, toPredicateCount,
+        understandsCount, equivalentExprCount, checkPredicateCount, checkVariableDisequalityCount,
+        atMostCount, topCount, bottomCount, isTopCount, isBottomCount,
+        joinCount, meetCount, widenCount);
+    }
+
+    protected override bool AtMost(Element/*!*/ a, Element/*!*/ b) {
+      //Contract.Requires(b != null);
+      //Contract.Requires(a != null);
+      atMostCount++;
+      return lattice.LowerThan(a, b);
+    }
+
+    public override Element/*!*/ Top {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        topCount++;
+        return lattice.Top;
+      }
+    }
+    public override Element/*!*/ Bottom {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        bottomCount++;
+        return lattice.Bottom;
+      }
+    }
+
+    public override bool IsTop(Element/*!*/ e) {
+      //Contract.Requires(e != null);
+      isTopCount++;
+      return lattice.IsTop(e);
+    }
+
+    public override bool IsBottom(Element/*!*/ e) {
+      //Contract.Requires(e != null);
+      isBottomCount++;
+      return lattice.IsBottom(e);
+    }
+
+    public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) {
+      //Contract.Requires(b != null);
+      //Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      joinCount++;
+      return lattice.NontrivialJoin(a, b);
+    }
+
+    public override Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b) {
+      //Contract.Requires(b != null);
+      //Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      meetCount++;
+      return lattice.NontrivialMeet(a, b);
+    }
+
+    public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) {
+      //Contract.Requires(b != null);
+      //Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      widenCount++;
+      return lattice.Widen(a, b);
+    }
+
+    public override void Validate() {
+      base.Validate();
+      lattice.Validate();
+    }
+
+    protected override object/*!*/ UniqueId {
+      get {
+        Contract.Ensures(Contract.Result<object>() != null);
+        // use the base id, not the underlying-lattice id (is that the right thing to do?)
+        return base.UniqueId;
+      }
+    }
+  }
+
+
+  public sealed class LatticeQueryable : IQueryable {
+    private Lattice/*!*/ lattice;
+    private Lattice.Element/*!*/ element;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(lattice != null);
+      Contract.Invariant(element != null);
+    }
+
+
+    public LatticeQueryable(Lattice/*!*/ lattice, Lattice.Element/*!*/ element) {
+      Contract.Requires(element != null);
+      Contract.Requires(lattice != null);
+      this.lattice = lattice;
+      this.element = element;
+      // base();
+    }
+
+    public Answer CheckPredicate(IExpr/*!*/ pred) {
+      //Contract.Requires(pred != null);
+      return lattice.CheckPredicate(element, pred);
+    }
+
+    public Answer CheckVariableDisequality(IVariable/*!*/ var1, IVariable/*!*/ var2) {
+      //Contract.Requires(var2 != null);
+      //Contract.Requires(var1 != null);
+      return lattice.CheckVariableDisequality(element, var1, var2);
+    }
+  }
+}