4 files changed, 3691 insertions, 3691 deletions
diff --git a/Source/AIFramework/Polyhedra/LinearConstraint.cs b/Source/AIFramework/Polyhedra/LinearConstraint.cs
index ab5e14f8..82264364 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraint.cs
+++ b/Source/AIFramework/Polyhedra/LinearConstraint.cs
@@ -1,545 +1,545 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework {
-  using System;
-  //using System.Compiler;
-  using System.Collections;
-  using Microsoft.Basetypes;
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System.Diagnostics.Contracts;
+namespace Microsoft.AbstractInterpretationFramework {
+  using System;
+  //using System.Compiler;
+  using System.Collections;
+  using Microsoft.Basetypes;
   using Set = Microsoft.Boogie.GSet<object>;
-  using IMutableSet = Microsoft.Boogie.GSet<object>; 
-  using HashSet = Microsoft.Boogie.GSet<object>;
-  using ISet = Microsoft.Boogie.GSet<object>;
-
-
-  /// <summary>
-  /// Represents a single linear constraint, coefficients are stored as Rationals.
-  /// </summary>
-  public class LinearConstraint {
-
-    public enum ConstraintRelation {
-      EQ,    // equal
-      LE,    // less-than or equal
-    }
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(coefficients != null);
-    }
-
-    public readonly ConstraintRelation Relation;
-    internal Hashtable /*IVariable->Rational*//*!*/ coefficients = new Hashtable /*IVariable->Rational*/ ();
-    internal Rational rhs;
-
-    public LinearConstraint(ConstraintRelation rel) {
-      Relation = rel;
-    }
-
-    [Pure]
-    public override string/*!*/ ToString() {
-      Contract.Ensures(Contract.Result<string>() != null);
-      string s = null;
-      foreach (DictionaryEntry /*IVariable->Rational*/ entry in coefficients) {
-        if (s == null) {
-          s = "";
-        } else {
-          s += " + ";
-        }
-        s += String.Format("{0}*{1}", entry.Value, entry.Key);
-      }
-      System.Diagnostics.Debug.Assert(s != null, "malformed LinearConstraint: no variables");
-      s += String.Format(" {0} {1}", Relation == ConstraintRelation.EQ ? "==" : "<=", rhs);
-      return s;
-    }
-
-
-#if DONT_KNOW_HOW_TO_TAKE_THE_TYPE_OF_AN_IVARIABLE_YET
-        public bool IsOverIntegers 
-        {
-            get
-            {
-                foreach (DictionaryEntry /*IVariable->Rational*/ entry in coefficients) 
-                {
-                    IVariable var = (IVariable)entry.Key;
-                    if ( ! var.TypedIdent.Type.IsInt) { return false; }
-                }
-                return true;
-            }
-        }
-#endif
-
-
-    /// <summary>
-    /// Note: This method requires that all dimensions are of type Variable, something that's
-    /// not required elsewhere in this class.
-    /// </summary>
-    /// <returns></returns>
-    public IExpr/*!*/ ConvertToExpression(ILinearExprFactory/*!*/ factory) {
-      Contract.Requires(factory != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      IExpr leftSum = null;
-      IExpr rightSum = null;
-      foreach (DictionaryEntry /*object->Rational*/ entry in coefficients) {
-        IVariable var = (IVariable)entry.Key;
-        Rational coeff = (Rational)(cce.NonNull(entry.Value));
-        if (coeff.IsPositive) {
-          leftSum = AddTerm(factory, leftSum, coeff, var);
-        } else if (coeff.IsNegative) {
-          rightSum = AddTerm(factory, rightSum, -coeff, var);
-        } else {
-          // ignore the term is coeff==0
-        }
-      }
-
-      if (leftSum == null && rightSum == null) {
-        // there are no variables in this constraint
-        if (Relation == ConstraintRelation.EQ ? rhs.IsZero : rhs.IsNonNegative) {
-          return factory.True;
-        } else {
-          return factory.False;
-        }
-      }
-
-      if (leftSum == null || (rightSum != null && rhs.IsNegative)) {
-        // show the constant on the left side
-        leftSum = AddTerm(factory, leftSum, -rhs, null);
-      } else if (rightSum == null || rhs.IsPositive) {
-        // show the constant on the right side
-        rightSum = AddTerm(factory, rightSum, rhs, null);
-      }
-
-      Contract.Assert(leftSum != null);
-      Contract.Assert(rightSum != null);
-      return Relation == ConstraintRelation.EQ ? factory.Eq(leftSum, rightSum) : factory.AtMost(leftSum, rightSum);
-    }
-
-    /// <summary>
-    /// Returns an expression that denotes sum + r*x.
-    /// If sum==null, drops the "sum +".
-    /// If x==null, drops the "*x".
-    /// if x!=null and r==1, drops the "r*".
-    /// </summary>
-    /// <param name="factory"></param>
-    /// <param name="sum"></param>
-    /// <param name="r"></param>
-    /// <param name="x"></param>
-    static IExpr/*!*/ AddTerm(ILinearExprFactory/*!*/ factory, /*MayBeNull*/ IExpr sum, Rational r, /*MayBeNull*/ IVariable x) {
-      Contract.Requires(factory != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      IExpr/*!*/ product = factory.Term(r, x);
-      Contract.Assert(product != null);
-      if (sum == null) {
-        return product;
-      } else {
-        return factory.Add(sum, product);
-      }
-    }
-    public System.Collections.Generic.IEnumerable<IVariable> GetDefinedDimensionsGeneric() {
-      Contract.Ensures(Contract.Result<System.Collections.Generic.IEnumerable<IVariable>>() != null);
-      foreach (IVariable/*!*/ dim in coefficients.Keys) {
-        Contract.Assert(dim != null);
-        yield return dim;
-      }
-    }
-    public ISet /*IVariable!*//*!*/ GetDefinedDimensions() {
-      Contract.Ensures(Contract.Result<ISet>() != null);
-      HashSet /*IVariable!*/ dims = new HashSet /*IVariable!*/ (coefficients.Count);
-      int j = 0;
-      foreach (IVariable/*!*/ dim in coefficients.Keys) {
-        Contract.Assert(dim != null);
-        dims.Add(dim);
-        j++;
-      }
-      System.Diagnostics.Debug.Assert(j == coefficients.Count);
-      return dims;
-    }
-
-    /// <summary>
-    /// Returns true iff all of the coefficients in the constraint are 0.  In that
-    /// case, the constraint has the form 0 &lt;= C for some constant C; hence, the
-    /// constraint is either unsatisfiable or trivially satisfiable.
-    /// </summary>
-    /// <returns></returns>
-    public bool IsConstant() {
-      foreach (Rational coeff in coefficients.Values) {
-        if (coeff.IsNonZero) {
-          return false;
-        }
-      }
-      return true;
-    }
-
-    /// <summary>
-    /// For an equality constraint, returns 0 == rhs.
-    /// For an inequality constraint, returns 0 &lt;= rhs.
-    /// </summary>
-    public bool IsConstantSatisfiable() {
-      if (Relation == ConstraintRelation.EQ) {
-        return rhs.IsZero;
-      } else {
-        return rhs.IsNonNegative;
-      }
-    }
-
-    /// <summary>
-    /// Returns 0 if "this" and "c" are not equivalent constraints.  If "this" and "c"
-    /// are equivalent constraints, the non-0 return value "m" satisfies "this == m*c".
-    /// </summary>
-    /// <param name="c"></param>
-    /// <returns></returns>
-    public Rational IsEquivalent(LinearConstraint/*!*/ c) {
-      Contract.Requires(c != null);
-      // "m" is the scale factor.  If it is 0, it hasn't been used yet.  If it
-      // is non-0, it will remain that value throughout, and it then says that
-      // for every dimension "d", "this[d] == m * c[d]".
-      Rational m = Rational.ZERO;
-
-      ArrayList /*IVariable*/ dd = new ArrayList /*IVariable*/ ();
-      foreach (IVariable/*!*/ d in this.GetDefinedDimensions()) {
-        Contract.Assert(d != null);
-        if (!dd.Contains(d)) {
-          dd.Add(d);
-        }
-      }
-      foreach (IVariable/*!*/ d in c.GetDefinedDimensions()) {
-        Contract.Assert(d != null);
-        if (!dd.Contains(d)) {
-          dd.Add(d);
-        }
-      }
-
-      foreach (IVariable/*!*/ d in dd) {
-        Contract.Assert(d != null);
-        Rational a = this[d];
-        Rational b = c[d];
-
-        if (a.IsZero || b.IsZero) {
-          if (a.IsNonZero || b.IsNonZero) {
-            return Rational.ZERO;  // not equivalent
-          }
-        } else if (m.IsZero) {
-          m = a / b;
-        } else if (a != m * b) {
-          return Rational.ZERO;  // not equivalent
-        }
-      }
-
-      // we expect there to have been some non-zero coefficient, so "m" should have been used by now
-      System.Diagnostics.Debug.Assert(m.IsNonZero);
-
-      // finally, check the rhs
-      if (this.rhs == m * c.rhs) {
-        return m;  // equivalent
-      } else {
-        return Rational.ZERO;  // not equivalent
-      }
-    }
-
-    /// <summary>
-    /// Splits an equality constraint into two inequality constraints, the conjunction of
-    /// which equals the equality constraint.  Assumes "this" is a equality constraint.
-    /// </summary>
-    /// <param name="a"></param>
-    /// <param name="b"></param>
-    public void GenerateInequalityConstraints(out LinearConstraint a, out LinearConstraint b) {
-      System.Diagnostics.Debug.Assert(this.Relation == ConstraintRelation.EQ);
-
-      a = new LinearConstraint(ConstraintRelation.LE);
-      a.coefficients = (Hashtable)this.coefficients.Clone();
-      a.rhs = this.rhs;
-
-      b = new LinearConstraint(ConstraintRelation.LE);
-      b.coefficients = new Hashtable /*IVariable->Rational*/ ();
-      foreach (DictionaryEntry entry in this.coefficients) {
-        b.coefficients[entry.Key] = -(Rational)(cce.NonNull(entry.Value));
-      }
-      b.rhs = -this.rhs;
-    }
-
-    public void SetCoefficient(IVariable/*!*/ dimension, Rational coefficient) {
-      Contract.Requires(dimension != null);
-      coefficients[dimension] = coefficient;
-    }
-
-    /// <summary>
-    /// Removes dimension "dim" from the constraint.  Only dimensions with coefficient 0 can
-    /// be removed.
-    /// </summary>
-    /// <param name="dim"></param>
-    public void RemoveDimension(IVariable/*!*/ dim) {
-      Contract.Requires(dim != null);
-      object val = coefficients[dim];
-      if (val != null) {
-#if FIXED_SERIALIZER            
-                Contract.Assert(((Rational)val).IsZero);
-#endif
-        coefficients.Remove(dim);
-      }
-    }
-
-    /// <summary>
-    /// The getter returns 0 if the dimension is not present.
-    /// </summary>
-    public Rational this[IVariable/*!*/ dimension] {
-      get {
-        Contract.Requires(dimension != null);
-
-
-        object z = coefficients[dimension];
-        if (z == null) {
-          return Rational.ZERO;
-        } else {
-          return (Rational)z;
-        }
-      }
-      set {
-        SetCoefficient(dimension, value);
-      }
-    }
-
-    public LinearConstraint Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName) {
-      Contract.Requires(newName != null);
-      Contract.Requires(oldName != null);
-      object /*Rational*/ z = coefficients[oldName];
-      if (z == null) {
-        return this;
-      } else {
-        System.Diagnostics.Debug.Assert(z is Rational);
-        Hashtable /*IVariable->Rational*/ newCoeffs = (Hashtable/*!*/ /*IVariable->Rational*/)cce.NonNull(coefficients.Clone());
-        newCoeffs.Remove(oldName);
-        newCoeffs.Add(newName, z);
-
-        LinearConstraint lc = new LinearConstraint(this.Relation);
-        lc.coefficients = newCoeffs;
-        lc.rhs = this.rhs;
-        return lc;
-      }
-    }
-
-    public LinearConstraint Clone() {
-      LinearConstraint z = new LinearConstraint(Relation);
-      z.coefficients = (Hashtable /*IVariable->Rational*/)this.coefficients.Clone();
-      z.rhs = this.rhs;
-      return z;
-    }
-
-    /// <summary>
-    /// Returns a constraint like "this", but with the given relation "r".
-    /// </summary>
-    /// <returns></returns>
-    public LinearConstraint/*!*/ ChangeRelation(ConstraintRelation rel) {
-      Contract.Ensures(Contract.Result<LinearConstraint>() != null);
-      if (Relation == rel) {
-        return this;
-      } else {
-        LinearConstraint z = new LinearConstraint(rel);
-        z.coefficients = (Hashtable)this.coefficients.Clone();
-        z.rhs = this.rhs;
-        return z;
-      }
-    }
-
-    /// <summary>
-    /// Returns a constraint like "this", but, conceptually, with the inequality relation >=.
-    /// </summary>
-    /// <returns></returns>
-    public LinearConstraint/*!*/ ChangeRelationToAtLeast() {
-      Contract.Ensures(Contract.Result<LinearConstraint>() != null);
-      LinearConstraint z = new LinearConstraint(ConstraintRelation.LE);
-      foreach (DictionaryEntry /*IVariable->Rational*/ entry in this.coefficients) {
-        z.coefficients.Add(entry.Key, -(Rational)(cce.NonNull(entry.Value)));
-      }
-      z.rhs = -this.rhs;
-      return z;
-    }
-
-    /// <summary>
-    /// Returns the left-hand side of the constraint evaluated at the point "v".
-    /// Any coordinate not present in "v" is treated as if it were 0.
-    /// Stated differently, this routine treats the left-hand side of the constraint
-    /// as a row vector and "v" as a column vector, and then returns the dot-product
-    /// of the two.
-    /// </summary>
-    /// <param name="v"></param>
-    /// <returns></returns>
-    public Rational EvaluateLhs(FrameElement/*!*/ v) {
-      Contract.Requires(v != null);
-      Rational q = Rational.ZERO;
-      foreach (DictionaryEntry /*IVariable,Rational*/ term in coefficients) {
-        IVariable dim = (IVariable/*!*/)cce.NonNull(term.Key);
-        Rational a = (Rational)(cce.NonNull(term.Value));
-        Rational x = v[dim];
-        q += a * x;
-      }
-      return q;
-    }
-
-    /// <summary>
-    /// Determines whether or not a given vertex or ray saturates the constraint.
-    /// </summary>
-    /// <param name="fe"></param>
-    /// <param name="vertex">true if "fe" is a vertex; false if "fe" is a ray</param>
-    /// <returns></returns>
-    public bool IsSaturatedBy(FrameElement/*!*/ fe, bool vertex) {
-      Contract.Requires(fe != null);
-      Rational lhs = EvaluateLhs(fe);
-      Rational rhs = vertex ? this.rhs : Rational.ZERO;
-      return lhs == rhs;
-    }
-
-    /// <summary>
-    /// Changes the current constraint A*X &lt;= B into (A + m*aa)*X &lt;= B + m*bb,
-    /// where "cc" is the constraint aa*X &lt;= bb.
-    /// </summary>
-    /// <param name="m"></param>
-    /// <param name="cc"></param>
-    /// <returns></returns>
-    public void AddMultiple(Rational m, LinearConstraint/*!*/ cc) {
-      Contract.Requires(cc != null);
-      foreach (DictionaryEntry /*IVariable->Rational*/ entry in cc.coefficients) {
-        IVariable dim = (IVariable)entry.Key;
-        Rational d = m * (Rational)(cce.NonNull(entry.Value));
-        if (d.IsNonZero) {
-          object prev = coefficients[dim];
-          if (prev == null) {
-            coefficients[dim] = d;
-          } else {
-            coefficients[dim] = (Rational)prev + d;
-          }
-        }
-      }
-      rhs += m * cc.rhs;
-    }
-
-    /// <summary>
-    /// Try to reduce the magnitude of the coefficients used.
-    /// Has a side effect on the coefficients, but leaves the meaning of the linear constraint
-    /// unchanged.
-    /// </summary>
-    public void Normalize() {
-      // compute the gcd of the numerators and the gcd of the denominators
-      Rational gcd = rhs;
-      foreach (Rational r in coefficients.Values) {
-        gcd = Rational.Gcd(gcd, r);
-      }
-      // Change all coefficients, to divide their numerators with gcdNum and to
-      // divide their denominators with gcdDen.
-      Hashtable /*IVariable->Rational*/ newCoefficients = new Hashtable /*IVariable->Rational*/ (coefficients.Count);
-      foreach (DictionaryEntry /*IVarianble->Rational*/ e in coefficients) {
-        Rational r = (Rational)(cce.NonNull(e.Value));
-        if (r.IsNonZero) {
-          newCoefficients.Add(e.Key, Rational.FromBignums(r.Numerator / gcd.Numerator, r.Denominator / gcd.Denominator));
-        } else {
-          newCoefficients.Add(e.Key, r);
-        }
-      }
-
-      coefficients = newCoefficients;
-      rhs = rhs.IsNonZero ? Rational.FromBignums(rhs.Numerator / gcd.Numerator, rhs.Denominator / gcd.Denominator) : rhs;
-    }
-  }
-
-  /// <summary>
-  /// Represents a frame element (vector of dimension/value tuples).  Used only
-  /// internally in class LinearConstraintSystem and its communication with class
-  /// LinearConstraint.
-  /// </summary>
-  public class FrameElement {
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(terms != null);
-    }
-
-    Hashtable /*IVariable->Rational*//*!*/ terms = new Hashtable /*IVariable->Rational*/ ();
-
-    /// <summary>
-    /// Constructs an empty FrameElement.  To add dimensions, call AddCoordinate after construction.
-    /// </summary>
-    public FrameElement() {
-    }
-
-    /// <summary>
-    /// This method is to be thought of as being part of the FrameElement object's construction process.
-    /// Assumes "dimension" is not already in FrameElement.
-    /// </summary>
-    /// <param name="dimension"></param>
-    /// <param name="value"></param>
-    public void AddCoordinate(IVariable/*!*/ dimension, Rational value) {
-      Contract.Requires(dimension != null);
-      terms.Add(dimension, value);
-    }
-
-    [Pure]
-    public override string/*!*/ ToString() {
-      Contract.Ensures(Contract.Result<string>() != null);
-      string s = null;
-      foreach (DictionaryEntry item in terms) {
-        if (s == null) {
-          s = "(";
-        } else {
-          s += ", ";
-        }
-        s += String.Format("<{0},{1}>", item.Key, (Rational)(cce.NonNull(item.Value)));
-      }
-      if (s == null) {
-        s = "(";
-      }
-      return s + ")";
-    }
-
-    public IMutableSet /*IVariable!*//*!*/ GetDefinedDimensions() {
-      Contract.Ensures(Contract.Result<IMutableSet>() != null);
-      HashSet /*IVariable!*//*!*/ dims = new HashSet /*IVariable!*/ (terms.Count);
-      foreach (IVariable/*!*/ dim in terms.Keys) {
-        Contract.Assert(dim != null);
-        dims.Add(dim);
-      }
-      System.Diagnostics.Debug.Assert(dims.Count == terms.Count);
-      return dims;
-    }
-
-    /// <summary>
-    /// The getter returns the value at the given dimension, or 0 if that dimension is not defined.
-    /// </summary>
-    public Rational this[IVariable/*!*/ dimension] {
-      get {
-        //Contract.Ensures(Contract.Result<Rational>() != null);
-        object z = terms[dimension];
-        if (z == null) {
-          return Rational.ZERO;
-        } else {
-          return (Rational)z;
-        }
-      }
-      set {
-        terms[dimension] = value;
-      }
-    }
-
-    public FrameElement Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName) {
-      Contract.Requires(newName != null);
-      Contract.Requires(oldName != null);
-      object /*Rational*/ z = terms[oldName];
-      if (z == null) {
-        return this;
-      } else {
-        System.Diagnostics.Debug.Assert(z is Rational);
-        Hashtable /*IVariable->Rational*/ newTerms = (Hashtable/*!*/ /*IVariable->Rational*/)cce.NonNull(terms.Clone());
-        newTerms.Remove(oldName);
-        newTerms.Add(newName, z);
-
-        FrameElement fe = new FrameElement();
-        fe.terms = newTerms;
-        return fe;
-      }
-    }
-
-    public FrameElement Clone() {
-      FrameElement z = new FrameElement();
-      z.terms = (Hashtable /*IVariable->Rational*/)this.terms.Clone();
-      return z;
-    }
-  }
-}
+  using IMutableSet = Microsoft.Boogie.GSet<object>; 
+  using HashSet = Microsoft.Boogie.GSet<object>;
+  using ISet = Microsoft.Boogie.GSet<object>;
+
+
+  /// <summary>
+  /// Represents a single linear constraint, coefficients are stored as Rationals.
+  /// </summary>
+  public class LinearConstraint {
+
+    public enum ConstraintRelation {
+      EQ,    // equal
+      LE,    // less-than or equal
+    }
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(coefficients != null);
+    }
+
+    public readonly ConstraintRelation Relation;
+    internal Hashtable /*IVariable->Rational*//*!*/ coefficients = new Hashtable /*IVariable->Rational*/ ();
+    internal Rational rhs;
+
+    public LinearConstraint(ConstraintRelation rel) {
+      Relation = rel;
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      string s = null;
+      foreach (DictionaryEntry /*IVariable->Rational*/ entry in coefficients) {
+        if (s == null) {
+          s = "";
+        } else {
+          s += " + ";
+        }
+        s += String.Format("{0}*{1}", entry.Value, entry.Key);
+      }
+      System.Diagnostics.Debug.Assert(s != null, "malformed LinearConstraint: no variables");
+      s += String.Format(" {0} {1}", Relation == ConstraintRelation.EQ ? "==" : "<=", rhs);
+      return s;
+    }
+
+
+#if DONT_KNOW_HOW_TO_TAKE_THE_TYPE_OF_AN_IVARIABLE_YET
+        public bool IsOverIntegers 
+        {
+            get
+            {
+                foreach (DictionaryEntry /*IVariable->Rational*/ entry in coefficients) 
+                {
+                    IVariable var = (IVariable)entry.Key;
+                    if ( ! var.TypedIdent.Type.IsInt) { return false; }
+                }
+                return true;
+            }
+        }
+#endif
+
+
+    /// <summary>
+    /// Note: This method requires that all dimensions are of type Variable, something that's
+    /// not required elsewhere in this class.
+    /// </summary>
+    /// <returns></returns>
+    public IExpr/*!*/ ConvertToExpression(ILinearExprFactory/*!*/ factory) {
+      Contract.Requires(factory != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      IExpr leftSum = null;
+      IExpr rightSum = null;
+      foreach (DictionaryEntry /*object->Rational*/ entry in coefficients) {
+        IVariable var = (IVariable)entry.Key;
+        Rational coeff = (Rational)(cce.NonNull(entry.Value));
+        if (coeff.IsPositive) {
+          leftSum = AddTerm(factory, leftSum, coeff, var);
+        } else if (coeff.IsNegative) {
+          rightSum = AddTerm(factory, rightSum, -coeff, var);
+        } else {
+          // ignore the term is coeff==0
+        }
+      }
+
+      if (leftSum == null && rightSum == null) {
+        // there are no variables in this constraint
+        if (Relation == ConstraintRelation.EQ ? rhs.IsZero : rhs.IsNonNegative) {
+          return factory.True;
+        } else {
+          return factory.False;
+        }
+      }
+
+      if (leftSum == null || (rightSum != null && rhs.IsNegative)) {
+        // show the constant on the left side
+        leftSum = AddTerm(factory, leftSum, -rhs, null);
+      } else if (rightSum == null || rhs.IsPositive) {
+        // show the constant on the right side
+        rightSum = AddTerm(factory, rightSum, rhs, null);
+      }
+
+      Contract.Assert(leftSum != null);
+      Contract.Assert(rightSum != null);
+      return Relation == ConstraintRelation.EQ ? factory.Eq(leftSum, rightSum) : factory.AtMost(leftSum, rightSum);
+    }
+
+    /// <summary>
+    /// Returns an expression that denotes sum + r*x.
+    /// If sum==null, drops the "sum +".
+    /// If x==null, drops the "*x".
+    /// if x!=null and r==1, drops the "r*".
+    /// </summary>
+    /// <param name="factory"></param>
+    /// <param name="sum"></param>
+    /// <param name="r"></param>
+    /// <param name="x"></param>
+    static IExpr/*!*/ AddTerm(ILinearExprFactory/*!*/ factory, /*MayBeNull*/ IExpr sum, Rational r, /*MayBeNull*/ IVariable x) {
+      Contract.Requires(factory != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      IExpr/*!*/ product = factory.Term(r, x);
+      Contract.Assert(product != null);
+      if (sum == null) {
+        return product;
+      } else {
+        return factory.Add(sum, product);
+      }
+    }
+    public System.Collections.Generic.IEnumerable<IVariable> GetDefinedDimensionsGeneric() {
+      Contract.Ensures(Contract.Result<System.Collections.Generic.IEnumerable<IVariable>>() != null);
+      foreach (IVariable/*!*/ dim in coefficients.Keys) {
+        Contract.Assert(dim != null);
+        yield return dim;
+      }
+    }
+    public ISet /*IVariable!*//*!*/ GetDefinedDimensions() {
+      Contract.Ensures(Contract.Result<ISet>() != null);
+      HashSet /*IVariable!*/ dims = new HashSet /*IVariable!*/ (coefficients.Count);
+      int j = 0;
+      foreach (IVariable/*!*/ dim in coefficients.Keys) {
+        Contract.Assert(dim != null);
+        dims.Add(dim);
+        j++;
+      }
+      System.Diagnostics.Debug.Assert(j == coefficients.Count);
+      return dims;
+    }
+
+    /// <summary>
+    /// Returns true iff all of the coefficients in the constraint are 0.  In that
+    /// case, the constraint has the form 0 &lt;= C for some constant C; hence, the
+    /// constraint is either unsatisfiable or trivially satisfiable.
+    /// </summary>
+    /// <returns></returns>
+    public bool IsConstant() {
+      foreach (Rational coeff in coefficients.Values) {
+        if (coeff.IsNonZero) {
+          return false;
+        }
+      }
+      return true;
+    }
+
+    /// <summary>
+    /// For an equality constraint, returns 0 == rhs.
+    /// For an inequality constraint, returns 0 &lt;= rhs.
+    /// </summary>
+    public bool IsConstantSatisfiable() {
+      if (Relation == ConstraintRelation.EQ) {
+        return rhs.IsZero;
+      } else {
+        return rhs.IsNonNegative;
+      }
+    }
+
+    /// <summary>
+    /// Returns 0 if "this" and "c" are not equivalent constraints.  If "this" and "c"
+    /// are equivalent constraints, the non-0 return value "m" satisfies "this == m*c".
+    /// </summary>
+    /// <param name="c"></param>
+    /// <returns></returns>
+    public Rational IsEquivalent(LinearConstraint/*!*/ c) {
+      Contract.Requires(c != null);
+      // "m" is the scale factor.  If it is 0, it hasn't been used yet.  If it
+      // is non-0, it will remain that value throughout, and it then says that
+      // for every dimension "d", "this[d] == m * c[d]".
+      Rational m = Rational.ZERO;
+
+      ArrayList /*IVariable*/ dd = new ArrayList /*IVariable*/ ();
+      foreach (IVariable/*!*/ d in this.GetDefinedDimensions()) {
+        Contract.Assert(d != null);
+        if (!dd.Contains(d)) {
+          dd.Add(d);
+        }
+      }
+      foreach (IVariable/*!*/ d in c.GetDefinedDimensions()) {
+        Contract.Assert(d != null);
+        if (!dd.Contains(d)) {
+          dd.Add(d);
+        }
+      }
+
+      foreach (IVariable/*!*/ d in dd) {
+        Contract.Assert(d != null);
+        Rational a = this[d];
+        Rational b = c[d];
+
+        if (a.IsZero || b.IsZero) {
+          if (a.IsNonZero || b.IsNonZero) {
+            return Rational.ZERO;  // not equivalent
+          }
+        } else if (m.IsZero) {
+          m = a / b;
+        } else if (a != m * b) {
+          return Rational.ZERO;  // not equivalent
+        }
+      }
+
+      // we expect there to have been some non-zero coefficient, so "m" should have been used by now
+      System.Diagnostics.Debug.Assert(m.IsNonZero);
+
+      // finally, check the rhs
+      if (this.rhs == m * c.rhs) {
+        return m;  // equivalent
+      } else {
+        return Rational.ZERO;  // not equivalent
+      }
+    }
+
+    /// <summary>
+    /// Splits an equality constraint into two inequality constraints, the conjunction of
+    /// which equals the equality constraint.  Assumes "this" is a equality constraint.
+    /// </summary>
+    /// <param name="a"></param>
+    /// <param name="b"></param>
+    public void GenerateInequalityConstraints(out LinearConstraint a, out LinearConstraint b) {
+      System.Diagnostics.Debug.Assert(this.Relation == ConstraintRelation.EQ);
+
+      a = new LinearConstraint(ConstraintRelation.LE);
+      a.coefficients = (Hashtable)this.coefficients.Clone();
+      a.rhs = this.rhs;
+
+      b = new LinearConstraint(ConstraintRelation.LE);
+      b.coefficients = new Hashtable /*IVariable->Rational*/ ();
+      foreach (DictionaryEntry entry in this.coefficients) {
+        b.coefficients[entry.Key] = -(Rational)(cce.NonNull(entry.Value));
+      }
+      b.rhs = -this.rhs;
+    }
+
+    public void SetCoefficient(IVariable/*!*/ dimension, Rational coefficient) {
+      Contract.Requires(dimension != null);
+      coefficients[dimension] = coefficient;
+    }
+
+    /// <summary>
+    /// Removes dimension "dim" from the constraint.  Only dimensions with coefficient 0 can
+    /// be removed.
+    /// </summary>
+    /// <param name="dim"></param>
+    public void RemoveDimension(IVariable/*!*/ dim) {
+      Contract.Requires(dim != null);
+      object val = coefficients[dim];
+      if (val != null) {
+#if FIXED_SERIALIZER            
+                Contract.Assert(((Rational)val).IsZero);
+#endif
+        coefficients.Remove(dim);
+      }
+    }
+
+    /// <summary>
+    /// The getter returns 0 if the dimension is not present.
+    /// </summary>
+    public Rational this[IVariable/*!*/ dimension] {
+      get {
+        Contract.Requires(dimension != null);
+
+
+        object z = coefficients[dimension];
+        if (z == null) {
+          return Rational.ZERO;
+        } else {
+          return (Rational)z;
+        }
+      }
+      set {
+        SetCoefficient(dimension, value);
+      }
+    }
+
+    public LinearConstraint Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+      Contract.Requires(newName != null);
+      Contract.Requires(oldName != null);
+      object /*Rational*/ z = coefficients[oldName];
+      if (z == null) {
+        return this;
+      } else {
+        System.Diagnostics.Debug.Assert(z is Rational);
+        Hashtable /*IVariable->Rational*/ newCoeffs = (Hashtable/*!*/ /*IVariable->Rational*/)cce.NonNull(coefficients.Clone());
+        newCoeffs.Remove(oldName);
+        newCoeffs.Add(newName, z);
+
+        LinearConstraint lc = new LinearConstraint(this.Relation);
+        lc.coefficients = newCoeffs;
+        lc.rhs = this.rhs;
+        return lc;
+      }
+    }
+
+    public LinearConstraint Clone() {
+      LinearConstraint z = new LinearConstraint(Relation);
+      z.coefficients = (Hashtable /*IVariable->Rational*/)this.coefficients.Clone();
+      z.rhs = this.rhs;
+      return z;
+    }
+
+    /// <summary>
+    /// Returns a constraint like "this", but with the given relation "r".
+    /// </summary>
+    /// <returns></returns>
+    public LinearConstraint/*!*/ ChangeRelation(ConstraintRelation rel) {
+      Contract.Ensures(Contract.Result<LinearConstraint>() != null);
+      if (Relation == rel) {
+        return this;
+      } else {
+        LinearConstraint z = new LinearConstraint(rel);
+        z.coefficients = (Hashtable)this.coefficients.Clone();
+        z.rhs = this.rhs;
+        return z;
+      }
+    }
+
+    /// <summary>
+    /// Returns a constraint like "this", but, conceptually, with the inequality relation >=.
+    /// </summary>
+    /// <returns></returns>
+    public LinearConstraint/*!*/ ChangeRelationToAtLeast() {
+      Contract.Ensures(Contract.Result<LinearConstraint>() != null);
+      LinearConstraint z = new LinearConstraint(ConstraintRelation.LE);
+      foreach (DictionaryEntry /*IVariable->Rational*/ entry in this.coefficients) {
+        z.coefficients.Add(entry.Key, -(Rational)(cce.NonNull(entry.Value)));
+      }
+      z.rhs = -this.rhs;
+      return z;
+    }
+
+    /// <summary>
+    /// Returns the left-hand side of the constraint evaluated at the point "v".
+    /// Any coordinate not present in "v" is treated as if it were 0.
+    /// Stated differently, this routine treats the left-hand side of the constraint
+    /// as a row vector and "v" as a column vector, and then returns the dot-product
+    /// of the two.
+    /// </summary>
+    /// <param name="v"></param>
+    /// <returns></returns>
+    public Rational EvaluateLhs(FrameElement/*!*/ v) {
+      Contract.Requires(v != null);
+      Rational q = Rational.ZERO;
+      foreach (DictionaryEntry /*IVariable,Rational*/ term in coefficients) {
+        IVariable dim = (IVariable/*!*/)cce.NonNull(term.Key);
+        Rational a = (Rational)(cce.NonNull(term.Value));
+        Rational x = v[dim];
+        q += a * x;
+      }
+      return q;
+    }
+
+    /// <summary>
+    /// Determines whether or not a given vertex or ray saturates the constraint.
+    /// </summary>
+    /// <param name="fe"></param>
+    /// <param name="vertex">true if "fe" is a vertex; false if "fe" is a ray</param>
+    /// <returns></returns>
+    public bool IsSaturatedBy(FrameElement/*!*/ fe, bool vertex) {
+      Contract.Requires(fe != null);
+      Rational lhs = EvaluateLhs(fe);
+      Rational rhs = vertex ? this.rhs : Rational.ZERO;
+      return lhs == rhs;
+    }
+
+    /// <summary>
+    /// Changes the current constraint A*X &lt;= B into (A + m*aa)*X &lt;= B + m*bb,
+    /// where "cc" is the constraint aa*X &lt;= bb.
+    /// </summary>
+    /// <param name="m"></param>
+    /// <param name="cc"></param>
+    /// <returns></returns>
+    public void AddMultiple(Rational m, LinearConstraint/*!*/ cc) {
+      Contract.Requires(cc != null);
+      foreach (DictionaryEntry /*IVariable->Rational*/ entry in cc.coefficients) {
+        IVariable dim = (IVariable)entry.Key;
+        Rational d = m * (Rational)(cce.NonNull(entry.Value));
+        if (d.IsNonZero) {
+          object prev = coefficients[dim];
+          if (prev == null) {
+            coefficients[dim] = d;
+          } else {
+            coefficients[dim] = (Rational)prev + d;
+          }
+        }
+      }
+      rhs += m * cc.rhs;
+    }
+
+    /// <summary>
+    /// Try to reduce the magnitude of the coefficients used.
+    /// Has a side effect on the coefficients, but leaves the meaning of the linear constraint
+    /// unchanged.
+    /// </summary>
+    public void Normalize() {
+      // compute the gcd of the numerators and the gcd of the denominators
+      Rational gcd = rhs;
+      foreach (Rational r in coefficients.Values) {
+        gcd = Rational.Gcd(gcd, r);
+      }
+      // Change all coefficients, to divide their numerators with gcdNum and to
+      // divide their denominators with gcdDen.
+      Hashtable /*IVariable->Rational*/ newCoefficients = new Hashtable /*IVariable->Rational*/ (coefficients.Count);
+      foreach (DictionaryEntry /*IVarianble->Rational*/ e in coefficients) {
+        Rational r = (Rational)(cce.NonNull(e.Value));
+        if (r.IsNonZero) {
+          newCoefficients.Add(e.Key, Rational.FromBignums(r.Numerator / gcd.Numerator, r.Denominator / gcd.Denominator));
+        } else {
+          newCoefficients.Add(e.Key, r);
+        }
+      }
+
+      coefficients = newCoefficients;
+      rhs = rhs.IsNonZero ? Rational.FromBignums(rhs.Numerator / gcd.Numerator, rhs.Denominator / gcd.Denominator) : rhs;
+    }
+  }
+
+  /// <summary>
+  /// Represents a frame element (vector of dimension/value tuples).  Used only
+  /// internally in class LinearConstraintSystem and its communication with class
+  /// LinearConstraint.
+  /// </summary>
+  public class FrameElement {
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(terms != null);
+    }
+
+    Hashtable /*IVariable->Rational*//*!*/ terms = new Hashtable /*IVariable->Rational*/ ();
+
+    /// <summary>
+    /// Constructs an empty FrameElement.  To add dimensions, call AddCoordinate after construction.
+    /// </summary>
+    public FrameElement() {
+    }
+
+    /// <summary>
+    /// This method is to be thought of as being part of the FrameElement object's construction process.
+    /// Assumes "dimension" is not already in FrameElement.
+    /// </summary>
+    /// <param name="dimension"></param>
+    /// <param name="value"></param>
+    public void AddCoordinate(IVariable/*!*/ dimension, Rational value) {
+      Contract.Requires(dimension != null);
+      terms.Add(dimension, value);
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      string s = null;
+      foreach (DictionaryEntry item in terms) {
+        if (s == null) {
+          s = "(";
+        } else {
+          s += ", ";
+        }
+        s += String.Format("<{0},{1}>", item.Key, (Rational)(cce.NonNull(item.Value)));
+      }
+      if (s == null) {
+        s = "(";
+      }
+      return s + ")";
+    }
+
+    public IMutableSet /*IVariable!*//*!*/ GetDefinedDimensions() {
+      Contract.Ensures(Contract.Result<IMutableSet>() != null);
+      HashSet /*IVariable!*//*!*/ dims = new HashSet /*IVariable!*/ (terms.Count);
+      foreach (IVariable/*!*/ dim in terms.Keys) {
+        Contract.Assert(dim != null);
+        dims.Add(dim);
+      }
+      System.Diagnostics.Debug.Assert(dims.Count == terms.Count);
+      return dims;
+    }
+
+    /// <summary>
+    /// The getter returns the value at the given dimension, or 0 if that dimension is not defined.
+    /// </summary>
+    public Rational this[IVariable/*!*/ dimension] {
+      get {
+        //Contract.Ensures(Contract.Result<Rational>() != null);
+        object z = terms[dimension];
+        if (z == null) {
+          return Rational.ZERO;
+        } else {
+          return (Rational)z;
+        }
+      }
+      set {
+        terms[dimension] = value;
+      }
+    }
+
+    public FrameElement Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+      Contract.Requires(newName != null);
+      Contract.Requires(oldName != null);
+      object /*Rational*/ z = terms[oldName];
+      if (z == null) {
+        return this;
+      } else {
+        System.Diagnostics.Debug.Assert(z is Rational);
+        Hashtable /*IVariable->Rational*/ newTerms = (Hashtable/*!*/ /*IVariable->Rational*/)cce.NonNull(terms.Clone());
+        newTerms.Remove(oldName);
+        newTerms.Add(newName, z);
+
+        FrameElement fe = new FrameElement();
+        fe.terms = newTerms;
+        return fe;
+      }
+    }
+
+    public FrameElement Clone() {
+      FrameElement z = new FrameElement();
+      z.terms = (Hashtable /*IVariable->Rational*/)this.terms.Clone();
+      return z;
+    }
+  }
+}
diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
index 74e36eae..59aadb86 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
+++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
@@ -1,1756 +1,1756 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework {
-  using System.Collections;
-  using System.Collections.Generic;
-  using System.Diagnostics;
-  using System;
-  //using Microsoft.SpecSharp.Collections;
-  using System.Diagnostics.Contracts;
-  using Microsoft.Basetypes;
-
-  using IMutableSet = Microsoft.Boogie.GSet<object>;
-  using ISet = Microsoft.Boogie.GSet<object>;
-  using HashSet = Microsoft.Boogie.GSet<object>;
-
-  /// <summary>
-  /// Represents a system of linear constraints (constraint/frame representations).
-  /// </summary>
-  public class LinearConstraintSystem {
-    // --------------------------------------------------------------------------------------------------------
-    // ------------------ Data structure ----------------------------------------------------------------------
-    // --------------------------------------------------------------------------------------------------------
-
-    public /*maybe null*/ ArrayList /*LinearConstraint!*/ Constraints;
-    /*maybe null*/
-    ArrayList /*FrameElement!*/ FrameVertices;
-    /*maybe null*/
-    ArrayList /*FrameElement!*/ FrameRays;
-    IMutableSet/*IVariable!*//*!*/ FrameDimensions;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(FrameDimensions != null);
-    }
-
-    /*maybe null*/
-    ArrayList /*FrameElement!*/ FrameLines;
-    // Invariant:  Either all of Constraints, FrameVertices, FrameRays, and FrameLines are
-    // null, or all are non-null.
-    // Invariant:  Any dimension mentioned in Constraints, FrameVertices, FrameRays, or
-    // FrameLines is mentioned in FrameDimensions.
-    // The meaning of FrameDimensions is that for any dimension x not in FrameDimensions,
-    // there is an implicit line along dimension x (that is, (<x,1>)).
-
-    void CheckInvariant() {
-      if (Constraints == null) {
-        System.Diagnostics.Debug.Assert(FrameVertices == null);
-        System.Diagnostics.Debug.Assert(FrameRays == null);
-        System.Diagnostics.Debug.Assert(FrameLines == null);
-        System.Diagnostics.Debug.Assert(FrameDimensions.Count == 0);
-      } else {
-        System.Diagnostics.Debug.Assert(FrameVertices != null);
-        System.Diagnostics.Debug.Assert(FrameRays != null);
-        System.Diagnostics.Debug.Assert(FrameLines != null);
-
-        foreach (LinearConstraint/*!*/ cc in Constraints) {
-          Contract.Assert(cc != null);
-#if FIXED_DESERIALIZER        
-          Contract.Assert(Contract.ForAll(cc.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
-#endif
-          Contract.Assert(cc.coefficients.Count != 0);
-        }
-        foreach (ArrayList /*FrameElement*//*!*/ FrameComponent in new ArrayList /*FrameElement*/ [] { FrameVertices, FrameRays, FrameLines }) {
-          Contract.Assert(FrameComponent != null);
-          foreach (FrameElement fe in FrameComponent) {
-            if (fe == null)
-              continue;
-#if FIXED_DESERIALIZER        
-            Contract.Assert(Contract.ForAll(fe.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
-#endif
-          }
-        }
-      }
-    }
-
-    // --------------------------------------------------------------------------------------------------------
-    // ------------------ Constructors ------------------------------------------------------------------------
-    // --------------------------------------------------------------------------------------------------------
-
-    /// <summary>
-    /// Creates a LinearConstraintSystem representing the bottom element, that is, representing
-    /// an unsatisfiable system of constraints.
-    /// </summary>
-    [NotDelayed]
-    public LinearConstraintSystem() {
-      FrameDimensions = new HashSet /*IVariable!*/ ();
-      //:base();
-      CheckInvariant();
-    }
-
-    /// <summary>
-    /// Constructs a linear constraint system with constraints "cs".
-    /// The constructor captures all constraints in "cs".
-    /// </summary>
-    /// <param name="cs"></param>
-    [NotDelayed]
-    public LinearConstraintSystem(ArrayList /*LinearConstraint!*//*!*/ cs) {
-      Contract.Requires(cs != null);
-#if BUG_159_HAS_BEEN_FIXED
-      Contract.Requires(Contract.ForAll(cs) , cc=> cc.coefficients.Count != 0);
-#endif
-
-      ArrayList constraints = new ArrayList /*LinearConstraint!*/ (cs.Count);
-      foreach (LinearConstraint/*!*/ cc in cs) {
-        Contract.Assert(cc != null);
-        constraints.Add(cc);
-      }
-      Constraints = constraints;
-      FrameDimensions = new HashSet /*IVariable!*/ ();  // to please compiler; this value will be overridden in the call to GenerateFrameConstraints below
-      //:base();
-
-      GenerateFrameFromConstraints();
-      SimplifyConstraints();
-      CheckInvariant();
-#if DEBUG_PRINT
-      Console.WriteLine("LinearConstraintSystem: constructor produced:");
-      Dump();
-#endif
-    }
-
-    /// <summary>
-    /// Constructs a linear constraint system corresponding to given vertex.  This constructor
-    /// is only used in the test harness--it is not needed for abstract interpretation.
-    /// </summary>
-    /// <param name="v"></param>
-    [NotDelayed]
-    LinearConstraintSystem(FrameElement/*!*/ v) {
-      Contract.Requires(v != null);
-      IMutableSet/*!*/ frameDims = v.GetDefinedDimensions();
-      Contract.Assert(frameDims != null);
-      ArrayList /*LinearConstraint!*/ constraints = new ArrayList /*LinearConstraint!*/ ();
-      foreach (IVariable/*!*/ dim in frameDims) {
-        Contract.Assert(dim != null);
-        LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
-        lc.SetCoefficient(dim, Rational.ONE);
-        lc.rhs = v[dim];
-        constraints.Add(lc);
-      }
-      FrameDimensions = frameDims;
-      Constraints = constraints;
-
-      ArrayList /*FrameElement*/ frameVertices = new ArrayList /*FrameElement*/ ();
-      frameVertices.Add(v);
-      FrameVertices = frameVertices;
-
-      FrameRays = new ArrayList /*FrameElement*/ ();
-      FrameLines = new ArrayList /*FrameElement*/ ();
-
-      //:base();
-      CheckInvariant();
-    }
-
-    void ChangeIntoBottom() {
-      Constraints = null;
-      FrameVertices = null;
-      FrameRays = null;
-      FrameLines = null;
-      FrameDimensions.Clear();  // no implicit lines
-    }
-
-    // --------------------------------------------------------------------------------------------------------
-    // ------------------ Public operations and their support routines ----------------------------------------
-    // --------------------------------------------------------------------------------------------------------
-
-    public bool IsBottom() {
-      return Constraints == null;
-    }
-
-    public bool IsTop() {
-      return Constraints != null && Constraints.Count == 0;
-    }
-
-    [Pure]
-    public override string/*!*/ ToString() {
-      Contract.Ensures(Contract.Result<string>() != null);
-      if (Constraints == null) {
-        return "<bottom>";
-      } else if (Constraints.Count == 0) {
-        return "<top>";
-      } else {
-        string z = null;
-        foreach (LinearConstraint/*!*/ lc in Constraints) {
-          Contract.Assert(lc != null);
-          string s = lc.ToString();
-          if (z == null) {
-            z = s;
-          } else {
-            z += " AND " + s;
-          }
-        }
-        Contract.Assert(z != null);
-        return z;
-      }
-    }
-
-
-    public ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-      Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
-      Contract.Ensures(Contract.Result<ICollection<IVariable>>().IsReadOnly);
-      List<IVariable/*!*/> list = new List<IVariable/*!*/>();
-      foreach (IVariable/*!*/ v in FrameDimensions) {
-        Contract.Assert(v != null);
-        list.Add(v);
-      }
-      return cce.NonNull(list.AsReadOnly());
-    }
-
-    /// <summary>
-    /// Note: This method requires that all dimensions are of type Variable, something that's
-    /// not required elsewhere in this class.
-    /// </summary>
-    /// <returns></returns>
-    public IExpr/*!*/ ConvertToExpression(ILinearExprFactory/*!*/ factory) {
-      Contract.Requires(factory != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      if (this.Constraints == null) {
-        return factory.False;
-      }
-      if (this.Constraints.Count == 0) {
-        return factory.True;
-      }
-
-      IExpr result = null;
-      foreach (LinearConstraint/*!*/ lc in Constraints) {
-        Contract.Assert(lc != null);
-        IExpr conjunct = lc.ConvertToExpression(factory);
-        result = (result == null) ? conjunct : (IExpr)factory.And(conjunct, result);
-      }
-      Contract.Assert(result != null);
-      return result;
-    }
-
-
-    /* IsSubset(): determines if 'lcs' is a subset of 'this'
-     * -- See Cousot/Halbwachs 1978, section 
-     */
-    public bool IsSubset(LinearConstraintSystem/*!*/ lcs) {
-      Contract.Requires(lcs != null);
-      if (lcs.IsBottom()) {
-        return true;
-      } else if (this.IsBottom()) {
-        return false;
-#if DEBUG
-#else
-      } else if (this.IsTop()) {  // optimization -- this case not needed for correctness
-        return true;
-      } else if (lcs.IsTop()) {  // optimization -- this case not needed for correctness
-        return false;
-#endif
-      } else {
-        // phase 0: check if frame dimensions are a superset of the constraint dimensions
-        ISet /*IVariable!*//*!*/ frameDims = lcs.GetDefinedDimensions();
-        Contract.Assert(frameDims != null);
-#if DEBUG_PRINT
-        Console.WriteLine("DEBUG: IsSubset:");
-        Console.WriteLine("  --- this:");
-        this.Dump();
-        Console.WriteLine("  --- lcs:");
-        lcs.Dump();
-        Console.WriteLine("  ---");
-#endif
-        foreach (LinearConstraint/*!*/ cc in cce.NonNull(this.Constraints)) {
-          Contract.Assert(cc != null);
-#if DEBUG_PRINT
-          Console.WriteLine("   cc: {0}", cc);
-          Console.WriteLine("   cc.GetDefinedDimensions(): {0}", cc.GetDefinedDimensions());
-#endif
-
-          if (!Contract.ForAll(cc.GetDefinedDimensionsGeneric(), var => frameDims.Contains(var))) {
-#if DEBUG_PRINT
-            Console.WriteLine("  ---> phase 0 subset violated, return false from IsSubset");
-#endif
-            return false;
-          }
-        }
-      }
-
-      // phase 1: check frame vertices against each constraint...
-      foreach (FrameElement/*!*/ v in cce.NonNull(lcs.FrameVertices)) {
-        Contract.Assert(v != null);
-        foreach (LinearConstraint/*!*/ cc in this.Constraints) {
-          Contract.Assert(cc != null);
-          Rational q = cc.EvaluateLhs(v);
-          if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
-            if (!(q <= cc.rhs)) {
-#if DEBUG_PRINT
-              Console.WriteLine("  ---> phase 1a subset violated, return false from IsSubset");
-#endif
-              return false;
-            }
-          } else {
-            if (!(q == cc.rhs)) {
-#if DEBUG_PRINT
-              Console.WriteLine("  ---> phase 1b subset violated, return false from IsSubset");
-#endif
-              return false;
-            }
-          }
-        }
-      }
-
-      // phase 2: check frame rays against each constraint...
-      // To check if a ray "r" falls within a constraint "cc", we add the vector "r" to
-      // any point "p" on the side of the half-space or plane described by constraint, and
-      // then check if the resulting point satisfies the constraint.  That is, we check (for
-      // an inequality constraint with coefficients a1,a2,...,an and right-hand side
-      // constant C):
-      //     a1*(r1+p1) + a2*(r2+p2) + ... + an*(rn+pn) <= C
-      // Equivalently:
-      //     a1*r1 + a2*r2 + ... + an*rn + a1*p1 + a2*p2 + ... + an*pn <= C
-      // To find a point "p", we can pick out a coordinate, call it 1, with a non-zero
-      // coefficient in the constraint, and then choose "p" as the point that has the
-      // value C/a1 in coordinate 1 and has 0 in all other coordinates.  We then check:
-      //     a1*r1 + a2*r2 + ... + an*rn + a1*(C/a1) + a2*0 + ... + an*0 <= C
-      // which simplifies to:
-      //     a1*r1 + a2*r2 + ... + an*rn + C <= C
-      // which in turn simplifies to:
-      //     a1*r1 + a2*r2 + ... + an*rn <= 0
-      // If the constraint is an equality constraint, we simply replace "<=" with "=="
-      // above.
-      foreach (FrameElement/*!*/ r in cce.NonNull(lcs.FrameRays)) {
-        Contract.Assert(r != null);
-        System.Diagnostics.Debug.Assert(r != null, "encountered a null ray...");
-        foreach (LinearConstraint/*!*/ cc in this.Constraints) {
-          Contract.Assert(cc != null);
-          System.Diagnostics.Debug.Assert(cc != null, "encountered an null constraint...");
-          Rational q = cc.EvaluateLhs(r);
-          if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
-            if (q.IsPositive) {
-#if DEBUG_PRINT
-              Console.WriteLine("  ---> phase 2a subset violated, return false from IsSubset");
-#endif
-              return false;
-            }
-          } else {
-            if (q.IsNonZero) {
-#if DEBUG_PRINT
-              Console.WriteLine("  ---> phase 2b subset violated, return false from IsSubset");
-#endif
-              return false;
-            }
-          }
-        }
-      }
-
-      // phase 3: check frame lines against each constraint...
-      // To check if a line "L" falls within a constraint "cc", we check if both the
-      // vector "L" and "-L", interpreted as rays, fall within the constraint.  From
-      // the discussion above, this means we check the following two properties:
-      //     a1*L1 + a2*L2 + ... + an*Ln <= 0                 (*)
-      //     a1*(-L1) + a2*(-L2) + ... + an*(-Ln) <= 0
-      // The second of these lines can be rewritten as:
-      //     - a1*L1 - a2*L2 - ... - an*Ln <= 0
-      // which is equivalent to:
-      //     -1 * (a1*L1 + a2*L2 + ... + an*Ln) <= 0
-      // Multiplying both sides by -1 and flipping the direction of the inequality,
-      // we have:
-      //     a1*L1 + a2*L2 + ... + an*Ln >= 0                 (**)
-      // Putting (*) and (**) together, we conclude that we need to check:
-      //     a1*L1 + a2*L2 + ... + an*Ln == 0
-      // If the constraint is an equality constraint, we end up with the same equation.
-      foreach (FrameElement/*!*/ line in cce.NonNull(lcs.FrameLines)) {
-        Contract.Assert(line != null);
-        System.Diagnostics.Debug.Assert(line != null, "encountered a null line...");
-        foreach (LinearConstraint/*!*/ cc in this.Constraints) {
-          Contract.Assert(cc != null);
-          System.Diagnostics.Debug.Assert(cc != null, "encountered an null constraint...");
-          Rational q = cc.EvaluateLhs(line);
-          if (q.IsNonZero) {
-#if DEBUG_PRINT
-            Console.WriteLine("  ---> phase 3 subset violated, return false from IsSubset");
-#endif
-            return false;
-          }
-        }
-      }
-
-#if DEBUG_PRINT
-      Console.WriteLine("  ---> IsSubset returns true");
-#endif
-      return true;
-    }
-
-    public LinearConstraintSystem/*!*/ Meet(LinearConstraintSystem/*!*/ lcs) {
-      Contract.Requires(lcs != null);
-      Contract.Requires((this.Constraints != null));
-      Contract.Requires((lcs.Constraints != null));
-      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
-      ArrayList /*LinearConstraint*/ clist = new ArrayList(this.Constraints.Count + lcs.Constraints.Count);
-      clist.AddRange(this.Constraints);
-      clist.AddRange(lcs.Constraints);
-      return new LinearConstraintSystem(clist);
-    }
-
-#if DEBUG_PRINT
-    public LinearConstraintSystem Join(LinearConstraintSystem lcs)
-    {
-      Console.WriteLine("===================================================================================");
-      Console.WriteLine("DEBUG: Join");
-      Console.WriteLine("Join: this=");
-      Dump();
-      Console.WriteLine("Join: lcs=");
-      lcs.Dump();
-      LinearConstraintSystem z = JoinX(lcs);
-      Console.WriteLine("----------Join------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>");
-      Console.WriteLine("Join: result=");
-      z.Dump();
-      Console.WriteLine("===================================================================================");
-      return z;
-    }
-#endif
-
-    /// <summary>
-    /// The join is computed as described in section 4.4 in Cousot and Halbwachs.
-    /// </summary>
-    /// <param name="lcs"></param>
-    /// <returns></returns>
-#if DEBUG_PRINT
-    public LinearConstraintSystem JoinX(LinearConstraintSystem lcs) {
-#else
-    public LinearConstraintSystem/*!*/ Join(LinearConstraintSystem/*!*/ lcs) {
-      Contract.Requires(lcs != null);
-      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
-#endif
-
-      if (this.IsBottom()) {
-        return cce.NonNull(lcs.Clone());
-      } else if (lcs.IsBottom()) {
-        return cce.NonNull(this.Clone());
-      } else if (this.IsTop() || lcs.IsTop()) {
-        return new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ());
-      } else {
-        LinearConstraintSystem/*!*/ z;
-        // Start from the "larger" of the two frames (this is just a heuristic measure intended
-        // to save work).
-        Contract.Assume(this.FrameVertices != null);
-        Contract.Assume(this.FrameRays != null);
-        Contract.Assume(this.FrameLines != null);
-        Contract.Assume(lcs.FrameVertices != null);
-        Contract.Assume(lcs.FrameRays != null);
-        Contract.Assume(lcs.FrameLines != null);
-        if (this.FrameVertices.Count + this.FrameRays.Count + this.FrameLines.Count - this.FrameDimensions.Count <
-          lcs.FrameVertices.Count + lcs.FrameRays.Count + lcs.FrameLines.Count - lcs.FrameDimensions.Count) {
-          z = cce.NonNull(lcs.Clone());
-          lcs = this;
-        } else {
-          z = cce.NonNull(this.Clone());
-        }
-#if DEBUG_PRINT
-        Console.WriteLine("DEBUG: LinearConstraintSystem.Join ---------------");
-        Console.WriteLine("z:");
-        z.Dump();
-        Console.WriteLine("lcs:");
-        lcs.Dump();
-#endif
-
-        // Start by explicating the implicit lines of z for the dimensions dims(lcs)-dims(z).
-        foreach (IVariable/*!*/ dim in lcs.FrameDimensions) {
-          Contract.Assert(dim != null);
-          if (!z.FrameDimensions.Contains(dim)) {
-            z.FrameDimensions.Add(dim);
-            FrameElement line = new FrameElement();
-            line.AddCoordinate(dim, Rational.ONE);
-            // Note:  AddLine is not called (because the line already exists in z--it's just that
-            // it was represented implicitly).  Instead, just tack the explicit representation onto
-            // FrameLines.
-            Contract.Assume(z.FrameLines != null);
-            z.FrameLines.Add(line);
-#if DEBUG_PRINT
-            Console.WriteLine("Join: After explicating line: {0}", line);
-            z.Dump();
-#endif
-          }
-        }
-
-        // Now, the vertices, rays, and lines can be added.
-        foreach (FrameElement/*!*/ v in lcs.FrameVertices) {
-          Contract.Assert(v != null);
-          z.AddVertex(v);
-#if DEBUG_PRINT
-          Console.WriteLine("Join: After adding vertex: {0}", v);
-          z.Dump();
-#endif
-        }
-        foreach (FrameElement/*!*/ r in lcs.FrameRays) {
-          Contract.Assert(r != null);
-          z.AddRay(r);
-#if DEBUG_PRINT
-          Console.WriteLine("Join: After adding ray: {0}", r);
-          z.Dump();
-#endif
-        }
-        foreach (FrameElement/*!*/ l in lcs.FrameLines) {
-          Contract.Assert(l != null);
-          z.AddLine(l);
-#if DEBUG_PRINT
-          Console.WriteLine("Join: After adding line: {0}", l);
-          z.Dump();
-#endif
-        }
-        // also add to z the implicit lines of lcs
-        foreach (IVariable/*!*/ dim in z.FrameDimensions) {
-          Contract.Assert(dim != null);
-          if (!lcs.FrameDimensions.Contains(dim)) {
-            // "dim" is a dimension that's explicit in "z" but implicit in "lcs"
-            FrameElement line = new FrameElement();
-            line.AddCoordinate(dim, Rational.ONE);
-            z.AddLine(line);
-#if DEBUG_PRINT
-            Console.WriteLine("Join: After adding lcs's implicit line: {0}", line);
-            z.Dump();
-#endif
-          }
-        }
-
-        z.SimplifyFrame();
-        z.SimplifyConstraints();
-        z.CheckInvariant();
-#if DEBUG_PRINT
-        Console.WriteLine("Join: Returning z:");
-        z.Dump();
-        Console.WriteLine("----------------------------------------");
-#endif
-        return z;
-      }
-    }
-
-#if DEBUG_PRINT
-    public LinearConstraintSystem Widen(LinearConstraintSystem lcs)
-    {
-      Console.WriteLine("===================================================================================");
-      Console.WriteLine("DEBUG: Widen");
-      Console.WriteLine("Widen: this=");
-      Dump();
-      Console.WriteLine("Widen: lcs=");
-      lcs.Dump();
-      LinearConstraintSystem z = WidenX(lcs);
-      Console.WriteLine("----------Widen------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>");
-      Console.WriteLine("Widen: result=");
-      z.Dump();
-      Console.WriteLine("===================================================================================");
-      return z;
-    }
-#endif
-
-#if DEBUG_PRINT
-    public LinearConstraintSystem WidenX(LinearConstraintSystem lcs){
-#else
-    public LinearConstraintSystem/*!*/ Widen(LinearConstraintSystem/*!*/ lcs) {
-      Contract.Requires(lcs != null);
-      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
-#endif
-      if (this.IsBottom()) {
-        return cce.NonNull(lcs.Clone());
-      } else if (lcs.IsBottom()) {
-        return cce.NonNull(this.Clone());
-      } else if (this.IsTop() || lcs.IsTop()) {
-        return new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ());
-      }
-
-      // create new LCS, we will add only verified constraints to this...
-      ArrayList /*LinearConstraint*/ newConstraints = new ArrayList /*LinearConstraint*/ ();
-      Contract.Assume(this.Constraints != null);
-      foreach (LinearConstraint/*!*/ ccX in this.Constraints) {
-        Contract.Assert(ccX != null);
-        LinearConstraint cc = ccX;
-#if DEBUG_PRINT
-        Console.WriteLine("Widen checking: Starting to check constraint: {0}", cc);
-#endif
-        if (cc.IsConstant()) {
-          // (Can this ever occur in the stable state of a LinearConstraintSystem?  --KRML)
-          // constraint is unaffected by the frame components
-#if DEBUG_PRINT
-          Console.WriteLine("Widen checking:   --Adding it!");
-#endif
-          newConstraints.Add(cc);
-          continue;
-        }
-
-        // PHASE I: verify constraints against all frame vertices...
-
-        foreach (FrameElement/*!*/ vertex in cce.NonNull(lcs.FrameVertices)) {
-          Contract.Assert(vertex != null);
-          Rational lhs = cc.EvaluateLhs(vertex);
-          if (lhs > cc.rhs) {
-            // the vertex does not satisfy the inequality <=
-            if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
-#if DEBUG_PRINT
-              Console.WriteLine("Widen checking:   throwing out because of vertex: {0}", vertex);
-#endif
-              goto CHECK_NEXT_CONSTRAINT;
-            } else {
-              // ... but it does satisfy the inequality >=
-#if DEBUG_PRINT
-              Console.WriteLine("Widen checking:   throwing out <= because of vertex: {0}", vertex);
-#endif
-              cc = cc.ChangeRelationToAtLeast();
-#if DEBUG_PRINT
-              Console.WriteLine("Widen checking:   left with constraint: {0}", cc);
-#endif
-            }
-          } else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ && lhs < cc.rhs) {
-            // the vertex does not satisfy the inequality >=, and the constraint is an equality constraint
-#if DEBUG_PRINT
-            Console.WriteLine("Widen checking:   throwing out >= because of vertex: {0}", vertex);
-#endif
-            cc = cc.ChangeRelation(LinearConstraint.ConstraintRelation.LE);
-#if DEBUG_PRINT
-            Console.WriteLine("Widen checking:   left with contraint: {0}", cc);
-#endif
-          }
-        }
-
-        // PHASE II: verify constraints against all frame rays...
-
-        foreach (FrameElement/*!*/ ray in cce.NonNull(lcs.FrameRays)) {
-          Contract.Assert(ray != null);
-          // The following assumes the constraint to have some dimension with a non-zero coefficient
-          Rational lhs = cc.EvaluateLhs(ray);
-          if (lhs.IsPositive) {
-            // the ray does not satisfy the inequality <=
-            if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
-#if DEBUG_PRINT
-              Console.WriteLine("Widen checking:   throwing out because of ray: {0}", ray);
-#endif
-              goto CHECK_NEXT_CONSTRAINT;
-            } else {
-              // ... but it does satisfy the inequality >=
-#if DEBUG_PRINT
-              Console.WriteLine("Widen checking:   throwing out <= because of ray: {0}", ray);
-#endif
-              cc = cc.ChangeRelationToAtLeast();
-#if DEBUG_PRINT
-              Console.WriteLine("Widen checking:   left with contraint: {0}", cc);
-#endif
-            }
-          } else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ && lhs.IsNegative) {
-            // the ray does not satisfy the inequality >=, and the constraint is an equality constraint
-#if DEBUG_PRINT
-            Console.WriteLine("Widen checking:   throwing out >= because of ray: {0}", ray);
-#endif
-            cc = cc.ChangeRelation(LinearConstraint.ConstraintRelation.LE);
-#if DEBUG_PRINT
-            Console.WriteLine("Widen checking:   left with constraint: {0}", cc);
-#endif
-          }
-        }
-
-        // PHASE III: verify constraints against all frame lines...
-
-        foreach (FrameElement/*!*/ line in cce.NonNull(lcs.FrameLines)) {
-          Contract.Assert(line != null);
-          // The following assumes the constraint to have some dimension with a non-zero coefficient
-          Rational lhs = cc.EvaluateLhs(line);
-          if (!lhs.IsZero) {
-            // The line satisfies neither the inequality <= nor the equality ==
-#if DEBUG_PRINT
-            Console.WriteLine("Widen checking:   throwing out because of line: {0}", line);
-#endif
-            goto CHECK_NEXT_CONSTRAINT;
-          }
-        }
-
-        // constraint has been verified, so add to new constraint system
-#if DEBUG_PRINT
-        Console.WriteLine("Widen checking:   --Adding it!");
-#endif
-        newConstraints.Add(cc);
-
-      CHECK_NEXT_CONSTRAINT: {
-        }
-#if DEBUG_PRINT
-        Console.WriteLine("Widen checking: done with that constraint");
-#endif
-      }
-
-      return new LinearConstraintSystem(newConstraints);
-    }
-
-#if DEBUG_PRINT
-    public LinearConstraintSystem Project(IVariable/*!*/ dim){
-Contract.Requires(dim != null);
-      Console.WriteLine("===================================================================================");
-      Console.WriteLine("DEBUG: Project(dim={0})", dim);
-      Console.WriteLine("Project: this=");
-      Dump();
-      LinearConstraintSystem z = ProjectX(dim);
-      Console.WriteLine("----------Project------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>");
-      Console.WriteLine("Project: result=");
-      z.Dump();
-      Console.WriteLine("===================================================================================");
-      return z;
-    }
-#endif
-
-#if DEBUG_PRINT
-    public LinearConstraintSystem ProjectX(IVariable/*!*/ dim){Contract.Requires(dim != null);Contract.Requires(this.Constraints != null);
-#else
-    public LinearConstraintSystem/*!*/ Project(IVariable/*!*/ dim) {
-      Contract.Requires(dim != null);
-      Contract.Requires(this.Constraints != null);
-      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
-#endif
-
-
-      ArrayList /*LinearConstraint!*//*!*/ cc = Project(dim, Constraints);
-      Contract.Assert(cc != null);
-      return new LinearConstraintSystem(cc);
-    }
-
-#if DEBUG_PRINT
-    public LinearConstraintSystem Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName){
-Contract.Requires(newName != null);
-Contract.Requires(oldName != null);
-      Console.WriteLine("===================================================================================");
-      Console.WriteLine("DEBUG: Rename(oldName={0}, newName={1})", oldName, newName);
-      Console.WriteLine("Rename: this=");
-      Dump();
-      LinearConstraintSystem z = RenameX(oldName, newName);
-      Console.WriteLine("----------Rename------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>");
-      Console.WriteLine("Rename: result=");
-      z.Dump();
-      Console.WriteLine("===================================================================================");
-      return z;
-    }
-#endif
-
-#if DEBUG_PRINT
-    public LinearConstraintSystem RenameX(IVariable/*!*/ oldName, IVariable/*!*/ newName){Contract.Requires(oldName != null);Contract.Requires(newName != null);
-#else
-    public LinearConstraintSystem/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName) {
-      Contract.Requires(oldName != null);
-      Contract.Requires(newName != null);
-      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
-#endif
-      if (this.Constraints == null) {
-        System.Diagnostics.Debug.Assert(this.FrameVertices == null);
-        System.Diagnostics.Debug.Assert(this.FrameRays == null);
-        System.Diagnostics.Debug.Assert(this.FrameLines == null);
-        return this;
-      }
-      IMutableSet /*IVariable!*//*!*/ dims = this.FrameDimensions;
-      Contract.Assert(dims != null);
-      if (!dims.Contains(oldName)) {
-        return this;
-      }
-
-      LinearConstraintSystem z = new LinearConstraintSystem();
-      z.FrameDimensions = cce.NonNull((HashSet/*!*/ /*IVariable!*/)dims.Clone());
-      z.FrameDimensions.Remove(oldName);
-      z.FrameDimensions.Add(newName);
-
-      z.Constraints = new ArrayList /*LinearConstraint!*/ (this.Constraints.Count);
-      foreach (LinearConstraint/*!*/ lc in cce.NonNull(this.Constraints)) {
-        Contract.Assert(lc != null);
-        z.Constraints.Add(lc.Rename(oldName, newName));
-      }
-      z.FrameVertices = RenameInFE(cce.NonNull(this.FrameVertices), oldName, newName);
-      z.FrameRays = RenameInFE(cce.NonNull(this.FrameRays), oldName, newName);
-      z.FrameLines = RenameInFE(cce.NonNull(this.FrameLines), oldName, newName);
-      return z;
-    }
-
-    static ArrayList /*FrameElement*/ RenameInFE(ArrayList/*!*/ /*FrameElement*/ list, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
-      Contract.Requires(list != null);
-      Contract.Requires(newName != null);
-      Contract.Requires(oldName != null);
-      ArrayList/*FrameElement!*//*!*/ z = new ArrayList/*FrameElement!*/ (list.Count);
-      Contract.Assert(z != null);
-      foreach (FrameElement/*!*/ fe in list) {
-        Contract.Assert(fe != null);
-        z.Add(fe.Rename(oldName, newName));
-      }
-      System.Diagnostics.Debug.Assert(z.Count == list.Count);
-      return z;
-    }
-
-    // --------------------------------------------------------------------------------------------------------
-    // ------------------ support routines --------------------------------------------------------------------
-    // --------------------------------------------------------------------------------------------------------
-
-    /// <summary>
-    /// Returns a set of constraints that is the given set of constraints with dimension "dim"
-    /// projected out.  See Cousot and Halbwachs, section 3.3.1.1.
-    /// </summary>
-    /// <param name="dim"></param>
-    /// <param name="constraints"></param>
-    /// <returns></returns>
-    static ArrayList /*LinearConstraint!*//*!*/ Project(IVariable/*!*/ dim, ArrayList /*LinearConstraint!*//*!*/ constraints) {
-      Contract.Requires(constraints != null);
-      Contract.Requires(dim != null);
-      Contract.Ensures(Contract.Result<ArrayList>() != null);
-      // Sort the inequality constaints into ones where dimension "dim" is 0, negative, and
-      // positive, respectively.  Put equality constraints with a non-0 "dim" into "eq".
-      ArrayList /*LinearConstraint!*//*!*/ final = new ArrayList /*LinearConstraint!*/ ();
-      ArrayList /*LinearConstraint!*//*!*/ negative = new ArrayList /*LinearConstraint!*/ ();
-      ArrayList /*LinearConstraint!*//*!*/ positive = new ArrayList /*LinearConstraint!*/ ();
-      ArrayList /*LinearConstraint!*//*!*/ eq = new ArrayList /*LinearConstraint!*/ ();
-      foreach (LinearConstraint/*!*/ cc in constraints) {
-        Contract.Assert(cc != null);
-        Rational coeff = cc[dim];
-        if (coeff.IsZero) {
-          LinearConstraint lc = cce.NonNull(cc.Clone());
-          if (!lc.IsConstant()) {
-            lc.RemoveDimension(dim);
-            final.Add(lc);
-          }
-        } else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ) {
-          eq.Add(cc);
-        } else if (coeff.IsNegative) {
-          negative.Add(cc);
-        } else {
-          System.Diagnostics.Debug.Assert(coeff.IsPositive);
-          positive.Add(cc);
-        }
-      }
-
-      if (eq.Count != 0) {
-        LinearConstraint eqConstraint = (LinearConstraint/*!*/)cce.NonNull(eq[eq.Count - 1]);
-        eq.RemoveAt(eq.Count - 1);
-        Rational eqC = -eqConstraint[dim];
-
-        foreach (ArrayList /*LinearConstraint!*/ list in new ArrayList[] { eq, negative, positive }) {
-          Contract.Assert(list != null);
-          foreach (LinearConstraint/*!*/ lcX in list) {
-            Contract.Assert(lcX != null);
-            LinearConstraint lc = cce.NonNull(lcX.Clone());
-            lc.AddMultiple(lc[dim] / eqC, eqConstraint);
-            System.Diagnostics.Debug.Assert(lc[dim].IsZero);
-            if (!lc.IsConstant()) {
-              lc.RemoveDimension(dim);
-              final.Add(lc);
-            } else {
-              System.Diagnostics.Debug.Assert(lc.IsConstantSatisfiable());
-            }
-          }
-        }
-      } else {
-        // Consider all pairs of constraints with (negative,positive) coefficients of "dim".
-        foreach (LinearConstraint/*!*/ cn in negative) {
-          Contract.Assert(cn != null);
-          Rational dn = -cn[dim];
-          System.Diagnostics.Debug.Assert(dn.IsNonNegative);
-          foreach (LinearConstraint/*!*/ cp in positive) {
-            Contract.Assert(cp != null);
-            Rational dp = cp[dim];
-
-            LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
-            lc.AddMultiple(dn, cp);
-            lc.AddMultiple(dp, cn);
-            System.Diagnostics.Debug.Assert(lc[dim].IsZero);
-            if (!lc.IsConstant()) {
-              lc.RemoveDimension(dim);
-              final.Add(lc);
-            } else {
-              System.Diagnostics.Debug.Assert(lc.IsConstantSatisfiable());
-            }
-          }
-        }
-      }
-
-      return final;
-    }
-
-    /// <summary>
-    /// Initializes FrameVertices, FrameRays, FrameLines, and FrameDimensions, see
-    /// Cousot and Halbwachs, section 3.4.  Any previous values of these fields are
-    /// ignored and overwritten.
-    /// 
-    /// If the set of Constraints is unsatisfiable, then "this" is changed into Bottom.
-    /// </summary>
-    void GenerateFrameFromConstraints() {
-      if (Constraints == null) {
-        FrameVertices = null;
-        FrameRays = null;
-        FrameLines = null;
-        FrameDimensions = new HashSet /*IVariable!*/ ();
-        return;
-      }
-
-      // Step 1 (see Cousot and Halbwachs, section 3.4.3):  create a Simplex Tableau.
-#if DEBUG_PRINT
-      Console.WriteLine("DEBUG: --- GenerateFrameFromConstraint ---");
-      Console.WriteLine("Constraints:");
-      foreach (LinearConstraint cc in Constraints) 
-      {
-        Console.WriteLine("  {0}", cc);
-      }
-#endif
-      SimplexTableau tableau = new SimplexTableau(Constraints);
-#if DEBUG_PRINT
-      Console.WriteLine("Initial tableau:");
-      tableau.Dump();
-#endif
-      FrameDimensions = tableau.GetDimensions();
-#if DEBUG_PRINT
-      Console.WriteLine("Dimensions:");
-      foreach (object dim in FrameDimensions) 
-      {
-        Console.Write("  {0}", dim);
-      }
-      Console.WriteLine();
-#endif
-
-      // Step 3 and 2: Put as many initial variables as possible into basis, then check if
-      // we reached a feasible basis
-      tableau.AddInitialVarsToBasis();
-#if DEBUG_PRINT
-      Console.WriteLine("Tableau after Step 3:");
-      tableau.Dump();
-#endif
-      if (!tableau.IsFeasibleBasis) {
-        // The polyhedron is empty (according to Cousot and Halbwachs)
-        ChangeIntoBottom();
-        return;
-      }
-
-      FrameVertices = new ArrayList /*FrameElement*/ ();
-      FrameRays = new ArrayList /*FrameElement*/ ();
-      FrameLines = new ArrayList /*FrameElement*/ ();
-      if (FrameDimensions.Count == 0) {
-        // top element
-        return;
-      }
-
-      if (tableau.AllInitialVarsInBasis) {
-        // All initial variables are in basis; there are no lines.
-#if DEBUG_PRINT
-        Console.WriteLine("Tableau after Steps 2 and 3 (all initial variables in basis):");
-        tableau.Dump();
-#endif
-      } else {
-        // There are lines
-#if DEBUG_PRINT
-        Console.WriteLine("Tableau after Steps 2 and 3 (NOT all initial variables in basis--there are lines):");
-        tableau.Dump();
-#endif
-        // Step 4.2: Pick out the lines, then produce the tableau for a new polyhedron without those lines.
-        ArrayList /*LinearConstraint*/ moreConstraints = cce.NonNull((ArrayList/*!*/ /*LinearConstraint*/)Constraints.Clone());
-        tableau.ProduceLines(FrameLines, moreConstraints);
-        tableau = new SimplexTableau(moreConstraints);
-#if DEBUG_PRINT
-        Console.WriteLine("Lines produced:");
-        foreach (FrameElement line in FrameLines) 
-        {
-          Console.WriteLine("  {0}", line);
-        }
-        Console.WriteLine("The new list of constraints is:");
-        foreach (LinearConstraint c in moreConstraints) 
-        {
-          Console.WriteLine("  {0}", c);
-        }
-        Console.WriteLine("Tableau after producing lines in Step 4.2:");
-        tableau.Dump();
-#endif
-
-        // Repeat step 3 for the new tableau.
-        // Since the new tableau contains no lines, the following call should cause all initial
-        // variables to be in basis (see step 4.2 in section 3.4.3 of Cousot and Halbwachs).
-        tableau.AddInitialVarsToBasis();
-        System.Diagnostics.Debug.Assert(tableau.AllInitialVarsInBasis);
-        System.Diagnostics.Debug.Assert(tableau.IsFeasibleBasis);  // the new tableau represents a set of feasible constraints, so this basis should be found to be feasible
-#if DEBUG_PRINT
-        Console.WriteLine("Tableau after all initial variables have been moved into basis:");
-        tableau.Dump();
-#endif
-      }
-
-      // Step 4.1: One vertex has been found.  Find all others, too.
-      tableau.TraverseVertices(FrameVertices, FrameRays);
-#if DEBUG_PRINT
-      Console.WriteLine("Tableau after vertex traversal:");
-      tableau.Dump();
-#endif
-    }
-
-    class LambdaDimension : IVariable {
-      readonly int id;
-      static int count = 0;
-
-      /// <summary>
-      /// Return the name of the variable
-      /// </summary>
-      public string Name {
-        get {
-          Contract.Ensures(Contract.Result<string>() != null);
-
-          return this.ToString();
-        }
-      }
-
-      public LambdaDimension() {
-        id = count;
-        count++;
-      }
-      [Pure]
-      public override string/*!*/ ToString() {
-        Contract.Ensures(Contract.Result<string>() != null);
-        return "lambda" + id;
-      }
-      [Pure]
-      public object DoVisit(ExprVisitor/*!*/ visitor) {
-        //Contract.Requires(visitor != null);
-        return visitor.VisitVariable(this);
-      }
-    }
-
-    /// <summary>
-    /// Adds a vertex to the frame of "this" and updates Constraints accordingly, see
-    /// Cousot and Halbwachs, section 3.3.1.1.  However, this method does not simplify
-    /// Constraints after the operation; that remains the caller's responsibility (which
-    /// gives the caller the opportunity to make multiple calls to AddVertex, AddRay,
-    /// and AddLine before calling SimplifyConstraints).
-    /// Assumes Constraints (and the frame fields) to be non-null.
-    /// </summary>
-    /// <param name="vertex"></param>
-    void AddVertex(FrameElement/*!*/ vertex) {
-      Contract.Requires(vertex != null);
-      Contract.Requires(this.FrameVertices != null);
-#if DEBUG_PRINT
-      Console.WriteLine("DEBUG: AddVertex called on {0}", vertex);
-      Console.WriteLine("  Initial constraints:");
-      foreach (LinearConstraint cc in Constraints) {
-        Console.WriteLine("    {0}", cc);
-      }
-#endif
-
-      FrameVertices.Add(vertex.Clone());
-#if FIXED_DESERIALIZER      
-      Contract.Assert(Contract.ForAll(vertex.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
-#endif
-
-      // We use a new temporary dimension.
-      IVariable/*!*/ lambda = new LambdaDimension();
-
-      // We change the constraints A*X <= B into
-      //     A*X + (A*vector - B)*lambda <= A*vector.
-      // That means that each row k in A (which corresponds to one LinearConstraint
-      // in Constraints) is changed by adding
-      //     (A*vector - B)[k] * lambda
-      // to row k and changing the right-hand side of row k to
-      //     (A*vector)[k]
-      // Note:
-      //     (A*vector - B)[k]
-      //  =      { vector subtraction is pointwise }
-      //     (A*vector)[k] - B[k]
-      //  =      { A*vector is a row vector whose every row i is the dot-product of
-      //           row i of A with the column vector "vector" }
-      //     A[k]*vector - B[k]
-      foreach (LinearConstraint/*!*/ cc in cce.NonNull(Constraints)) {
-        Contract.Assert(cc != null);
-        Rational d = cc.EvaluateLhs(vertex);
-        cc.SetCoefficient(lambda, d - cc.rhs);
-        cc.rhs = d;
-      }
-
-      // We also add the constraints that lambda lies between 0 ...
-      LinearConstraint la = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
-      la.SetCoefficient(lambda, Rational.MINUS_ONE);
-      la.rhs = Rational.ZERO;
-      Constraints.Add(la);
-      // ... and 1.
-      la = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
-      la.SetCoefficient(lambda, Rational.ONE);
-      la.rhs = Rational.ONE;
-      Constraints.Add(la);
-#if DEBUG_PRINT
-      Console.WriteLine("  Constraints after addition:");
-      foreach (LinearConstraint cc in Constraints) {
-        Console.WriteLine("    {0}", cc);
-      }
-#endif
-
-      // Finally, project out the dummy dimension.
-      Constraints = Project(lambda, Constraints);
-
-#if DEBUG_PRINT
-      Console.WriteLine("  Resulting constraints:");
-      foreach (LinearConstraint cc in Constraints) {
-        Console.WriteLine("    {0}", cc);
-      }
-#endif
-    }
-
-    /// <summary>
-    /// Adds a ray to the frame of "this" and updates Constraints accordingly, see
-    /// Cousot and Halbwachs, section 3.3.1.1.  However, this method does not simplify
-    /// Constraints after the operation; that remains the caller's responsibility (which
-    /// gives the caller the opportunity to make multiple calls to AddVertex, AddRay,
-    /// and AddLine before calling SimplifyConstraints).
-    /// Assumes Constraints (and the frame fields) to be non-null.
-    /// </summary>
-    /// <param name="ray"></param>
-    void AddRay(FrameElement/*!*/ ray) {
-      Contract.Requires(ray != null);
-      Contract.Requires(this.FrameRays != null);
-#if DEBUG_PRINT
-      Console.WriteLine("DEBUG: AddRay called on {0}", ray);
-      Console.WriteLine("  Initial constraints:");
-      foreach (LinearConstraint cc in Constraints) {
-        Console.WriteLine("    {0}", cc);
-      }
-#endif
-
-      FrameRays.Add(ray.Clone());
-#if FIXED_DESERIALIZER      
-      Contract.Assert(Contract.ForAll(ray.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
-#endif
-
-      // We use a new temporary dimension.
-      IVariable/*!*/ lambda = new LambdaDimension();
-
-      // We change the constraints A*X <= B into
-      //     A*X - (A*ray)*lambda <= B.
-      // That means that each row k in A (which corresponds to one LinearConstraint
-      // in Constraints) is changed by subtracting
-      //     (A*ray)[k] * lambda
-      // from row k.
-      // Note:
-      //     (A*ray)[k]
-      //  =      { A*ray is a row vector whose every row i is the dot-product of
-      //           row i of A with the column vector "ray" }
-      //     A[k]*ray
-      foreach (LinearConstraint/*!*/ cc in cce.NonNull(Constraints)) {
-        Contract.Assert(cc != null);
-        Rational d = cc.EvaluateLhs(ray);
-        cc.SetCoefficient(lambda, -d);
-      }
-
-      // We also add the constraints that lambda is at least 0.
-      LinearConstraint la = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
-      la.SetCoefficient(lambda, Rational.MINUS_ONE);
-      la.rhs = Rational.ZERO;
-      Constraints.Add(la);
-#if DEBUG_PRINT
-      Console.WriteLine("  Constraints after addition:");
-      foreach (LinearConstraint cc in Constraints) {
-        Console.WriteLine("    {0}", cc);
-      }
-#endif
-
-      // Finally, project out the dummy dimension.
-      Constraints = Project(lambda, Constraints);
-
-#if DEBUG_PRINT
-      Console.WriteLine("  Resulting constraints:");
-      foreach (LinearConstraint cc in Constraints) {
-        Console.WriteLine("    {0}", cc);
-      }
-#endif
-    }
-
-    /// <summary>
-    /// Adds a line to the frame of "this" and updates Constraints accordingly, see
-    /// Cousot and Halbwachs, section 3.3.1.1.  However, this method does not simplify
-    /// Constraints after the operation; that remains the caller's responsibility (which
-    /// gives the caller the opportunity to make multiple calls to AddVertex, AddRay,
-    /// and AddLine before calling SimplifyConstraints).
-    /// Assumes Constraints (and the frame fields) to be non-null.
-    /// </summary>
-    /// <param name="line"></param>
-    void AddLine(FrameElement/*!*/ line) {
-      Contract.Requires(line != null);
-      Contract.Requires(this.FrameLines != null);
-      // Note:  The code for AddLine is identical to that of AddRay, except the AddLine
-      // does not introduce the constraint 0 <= lambda.  (One could imagine sharing the
-      // code between AddRay and AddLine.)
-#if DEBUG_PRINT
-      Console.WriteLine("DEBUG: AddLine called on {0}", line);
-      Console.WriteLine("  Initial constraints:");
-      foreach (LinearConstraint cc in Constraints) {
-        Console.WriteLine("    {0}", cc);
-      }
-#endif
-
-      FrameLines.Add(line.Clone());
-#if FIXED_DESERIALIZER      
-      Contract.Assert(Contract.ForAll(line.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
-#endif
-
-      // We use a new temporary dimension.
-      IVariable/*!*/ lambda = new LambdaDimension();
-
-      // We change the constraints A*X <= B into
-      //     A*X - (A*line)*lambda <= B.
-      // That means that each row k in A (which corresponds to one LinearConstraint
-      // in Constraints) is changed by subtracting
-      //     (A*line)[k] * lambda
-      // from row k.
-      // Note:
-      //     (A*line)[k]
-      //  =      { A*line is a row vector whose every row i is the dot-product of
-      //           row i of A with the column vector "line" }
-      //     A[k]*line
-      foreach (LinearConstraint/*!*/ cc in cce.NonNull(Constraints)) {
-        Contract.Assert(cc != null);
-        Rational d = cc.EvaluateLhs(line);
-        cc.SetCoefficient(lambda, -d);
-      }
-
-#if DEBUG_PRINT
-      Console.WriteLine("  Constraints after addition:");
-      foreach (LinearConstraint cc in Constraints) {
-        Console.WriteLine("    {0}", cc);
-      }
-#endif
-
-      // Finally, project out the dummy dimension.
-      Constraints = Project(lambda, Constraints);
-
-#if DEBUG_PRINT
-      Console.WriteLine("  Resulting constraints:");
-      foreach (LinearConstraint cc in Constraints) {
-        Console.WriteLine("    {0}", cc);
-      }
-#endif
-    }
-
-    ISet /*IVariable!*//*!*/ GetDefinedDimensions() {
-      Contract.Ensures(Contract.Result<ISet>() != null);
-      HashSet /*IVariable!*//*!*/ dims = new HashSet /*IVariable!*/ ();
-      foreach (ArrayList p in new ArrayList[] { FrameVertices, FrameRays, FrameLines }) {
-        if (p != null) {
-          foreach (FrameElement/*!*/ element in p) {
-            Contract.Assert(element != null);
-            foreach (IVariable/*!*/ dim in element.GetDefinedDimensions()) {
-              Contract.Assert(dim != null);
-              dims.Add(dim);
-            }
-          }
-        }
-      }
-      return dims;
-    }
-
-    // --------------------------------------------------------------------------------------------------------
-    // ------------------ Simplification routines -------------------------------------------------------------
-    // --------------------------------------------------------------------------------------------------------
-
-    /// <summary>
-    /// Uses the Constraints to simplify the frame.  See section 3.4.4 of Cousot and Halbwachs.
-    /// </summary>
-    void SimplifyFrame() {
-      Contract.Requires(this.Constraints != null);
-      SimplificationStatus[]/*!*/ status;
-
-      SimplifyFrameElements(cce.NonNull(FrameVertices), true, Constraints, out status);
-      RemoveIrrelevantFrameElements(FrameVertices, status, null);
-
-      SimplifyFrameElements(cce.NonNull(FrameRays), false, Constraints, out status);
-      RemoveIrrelevantFrameElements(FrameRays, status, FrameLines);
-    }
-
-    enum SimplificationStatus {
-      Irrelevant,
-      Relevant,
-      More
-    };
-
-    /// <summary>
-    /// For each i, sets status[i] to:
-    ///  <ul>
-    ///  <li>Irrelevant if ff[i] is irrelevant</li>
-    ///  <li>Relevant if ff[i] is irrelevant</li>
-    ///  <li>More if vertices is true and ray ff[i] can be replaced by a line ff[i]</li>
-    ///  </ul>
-    /// </summary>
-    /// <param name="ff"></param>
-    /// <param name="vertices">true if "ff" contains vertices; false if "ff" contains rays</param>
-    /// <param name="constraints"></param>
-    /// <param name="status"></param>
-    static void SimplifyFrameElements(ArrayList/*!*/ /*FrameElement*/ ff, bool vertices, ArrayList/*!*/ /*LinearConstraint*/ constraints, out SimplificationStatus[]/*!*/ status) {
-      Contract.Requires(ff != null);
-      Contract.Requires(constraints != null);
-      Contract.Ensures(Contract.ValueAtReturn(out status) != null);
-      status = new SimplificationStatus[ff.Count];
-      bool[,] sat = new bool[ff.Count, constraints.Count];
-      for (int i = 0; i < ff.Count; i++) {
-        FrameElement f = (FrameElement/*!*/)cce.NonNull(ff[i]);
-        int cnt = 0;
-        for (int c = 0; c < constraints.Count; c++) {
-          LinearConstraint lc = (LinearConstraint/*!*/)cce.NonNull(constraints[c]);
-          bool s = lc.IsSaturatedBy(f, vertices);
-          if (s) {
-            sat[i, c] = true;
-            cnt++;
-          }
-        }
-        if (!vertices && cnt == constraints.Count) {
-          status[i] = SimplificationStatus.More;
-        } else {
-          status[i] = SimplificationStatus.Relevant;
-        }
-      }
-
-      CheckPairSimplifications(sat, status);
-    }
-
-    /// <summary>
-    /// Requires sat.GetLength(0) == status.Length.
-    /// </summary>
-    /// <param name="sat"></param>
-    /// <param name="status"></param>
-    static void CheckPairSimplifications(bool[,]/*!*/ sat, SimplificationStatus[]/*!*/ status) {
-      Contract.Requires(status != null);
-      Contract.Requires(sat != null);
-      Contract.Requires(sat.GetLength(0) == status.Length);
-      int M = sat.GetLength(0);
-      int N = sat.GetLength(1);
-
-      for (int i = 0; i < M - 1; i++) {
-        if (status[i] != SimplificationStatus.Relevant) {
-          continue;
-        }
-        for (int j = i + 1; j < M; j++) {
-          if (status[j] != SimplificationStatus.Relevant) {
-            continue;
-          }
-          // check (sat[i,*] <= sat[j,*]) and (sat[i,*] >= sat[j,*])
-          int cmp = 0;  // -1: (sat[i,*] <= sat[j,*]),  0: equal,  1: (sat[i,*] >= sat[j,*])
-          for (int c = 0; c < N; c++) {
-            if (cmp < 0) {
-              if (sat[i, c] && !sat[j, c]) {
-                // incomparable
-                goto NEXT_PAIR;
-              }
-            } else if (0 < cmp) {
-              if (!sat[i, c] && sat[j, c]) {
-                // incomparable
-                goto NEXT_PAIR;
-              }
-            } else if (sat[i, c] != sat[j, c]) {
-              if (!sat[i, c]) {
-                cmp = -1;
-              } else {
-                cmp = 1;
-              }
-            }
-          }
-          if (cmp <= 0) {
-            // sat[i,*] <= sat[j,*] holds, so mark i as irrelevant
-            status[i] = SimplificationStatus.Irrelevant;
-            goto NEXT_OUTER;
-          } else {
-            // sat[i,*] >= sat[j,*] holds, so mark j as irrelevant
-            status[j] = SimplificationStatus.Irrelevant;
-          }
-        NEXT_PAIR: {
-          }
-        }
-      NEXT_OUTER: {
-        }
-      }
-    }
-
-    static void RemoveIrrelevantFrameElements(ArrayList/*!*/ /*FrameElement*/ ff, SimplificationStatus[]/*!*/ status,
-      /*maybe null*/ ArrayList /*FrameElement*/ lines) {
-      Contract.Requires(ff != null);
-      Contract.Requires(status != null);
-      Contract.Requires(ff.Count == status.Length);
-      for (int j = ff.Count - 1; 0 <= j; j--) {
-        switch (status[j]) {
-          case SimplificationStatus.Relevant:
-            break;
-          case SimplificationStatus.Irrelevant:
-#if DEBUG_PRINT
-            Console.WriteLine("Removing irrelevant {0}: {1}", lines == null ? "vertex" : "ray", ff[j]);
-#endif
-            ff.RemoveAt(j);
-            break;
-          case SimplificationStatus.More:
-            System.Diagnostics.Debug.Assert(lines != null);
-            FrameElement f = (FrameElement)ff[j];
-#if DEBUG_PRINT
-            Console.WriteLine("Changing ray into line: {0}", f);
-#endif
-            ff.RemoveAt(j);
-            Contract.Assert(lines != null);
-            lines.Add(f);
-            break;
-        }
-      }
-    }
-
-    /// <summary>
-    /// Uses the frame to simplify Constraints.  See section 3.3.1.2 of Cousot and Halbwachs.
-    /// 
-    /// Note:  This code does not necessarily eliminate all irrelevant equalities; Cousot and
-    /// Halbwachs only claim that the technique eliminates all irrelevant inequalities.
-    /// </summary>
-    void SimplifyConstraints() {
-      if (Constraints == null) {
-        return;
-      }
-      Contract.Assume(this.FrameVertices != null);
-      Contract.Assume(this.FrameRays != null);
-
-      SimplificationStatus[] status = new SimplificationStatus[Constraints.Count];
-      /*readonly*/
-      int feCount = FrameVertices.Count + FrameRays.Count;
-
-      // Create a table that keeps track of which constraints are satisfied by which vertices and rays
-      bool[,] sat = new bool[Constraints.Count, FrameVertices.Count + FrameRays.Count];
-      for (int i = 0; i < Constraints.Count; i++) {
-        status[i] = SimplificationStatus.Relevant;
-        LinearConstraint lc = (LinearConstraint/*!*/)cce.NonNull(Constraints[i]);
-        int cnt = 0;  // number of vertices and rays that saturate lc
-        for (int j = 0; j < FrameVertices.Count; j++) {
-          FrameElement vertex = (FrameElement/*!*/)cce.NonNull(FrameVertices[j]);
-          if (lc.IsSaturatedBy(vertex, true)) {
-            sat[i, j] = true;
-            cnt++;
-          }
-        }
-        if (cnt == 0) {
-          // no vertex saturates the constraint, so the constraint is irrelevant
-          status[i] = SimplificationStatus.Irrelevant;
-          continue;
-        }
-        for (int j = 0; j < FrameRays.Count; j++) {
-          FrameElement ray = (FrameElement/*!*/)cce.NonNull(FrameRays[j]);
-          if (lc.IsSaturatedBy(ray, false)) {
-            sat[i, FrameVertices.Count + j] = true;
-            cnt++;
-          }
-        }
-        if (cnt == feCount) {
-          status[i] = SimplificationStatus.More;
-        } else {
-          // Cousot and Halbwachs says that all equalities are found in the way we just tested.
-          // If I understand that right, then we should not get here if the constraint is an
-          // equality constraint.  The following assertion tests my understanding.  --KRML
-          System.Diagnostics.Debug.Assert(lc.Relation == LinearConstraint.ConstraintRelation.LE);
-        }
-      }
-
-      CheckPairSimplifications(sat, status);
-
-      // Finally, make the changes to the list of constraints
-      for (int i = Constraints.Count - 1; 0 <= i; i--) {
-        switch (status[i]) {
-          case SimplificationStatus.Relevant:
-            break;
-          case SimplificationStatus.Irrelevant:
-#if DEBUG_PRINT
-            Console.WriteLine("Removing irrelevant constraint: {0}", Constraints[i]);
-#endif
-            Constraints.RemoveAt(i);
-            break;
-          case SimplificationStatus.More:
-            LinearConstraint lc = (LinearConstraint/*!*/)cce.NonNull(Constraints[i]);
-            if (lc.Relation == LinearConstraint.ConstraintRelation.LE) {
-#if DEBUG_PRINT
-              Console.WriteLine("Converting the following constraint into an equality: {0}", lc);
-#endif
-              LinearConstraint lcEq = lc.ChangeRelation(LinearConstraint.ConstraintRelation.EQ);
-              Constraints[i] = lcEq;
-            }
-            break;
-        }
-      }
-
-      foreach (LinearConstraint/*!*/ lc in Constraints) {
-        Contract.Assert(lc != null);
-        lc.Normalize();
-      }
-    }
-
-    // --------------------------------------------------------------------------------------------------------
-    // ------------------ Cloning routines --------------------------------------------------------------------
-    // --------------------------------------------------------------------------------------------------------
-
-    public LinearConstraintSystem/*!*/ Clone() {
-      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
-      LinearConstraintSystem z = new LinearConstraintSystem();
-      z.FrameDimensions = (IMutableSet /*IVariable!*//*!*/)cce.NonNull(this.FrameDimensions.Clone());
-      if (this.Constraints != null) {
-        z.Constraints = DeeperListCopy_LC(this.Constraints);
-        z.FrameVertices = DeeperListCopy_FE(cce.NonNull(this.FrameVertices));
-        z.FrameRays = DeeperListCopy_FE(cce.NonNull(this.FrameRays));
-        z.FrameLines = DeeperListCopy_FE(cce.NonNull(this.FrameLines));
-      } else {
-        System.Diagnostics.Debug.Assert(this.FrameVertices == null);
-        System.Diagnostics.Debug.Assert(this.FrameRays == null);
-        System.Diagnostics.Debug.Assert(this.FrameLines == null);
-        // the constructor should already have set these fields of z to null
-        System.Diagnostics.Debug.Assert(z.Constraints == null);
-        System.Diagnostics.Debug.Assert(z.FrameVertices == null);
-        System.Diagnostics.Debug.Assert(z.FrameRays == null);
-        System.Diagnostics.Debug.Assert(z.FrameLines == null);
-      }
-      return z;
-    }
-
-    /// <summary>
-    /// Clones "list" and the elements of "list".
-    /// </summary>
-    /// <param name="list"></param>
-    /// <returns></returns>
-    ArrayList /*LinearConstraint*/ DeeperListCopy_LC(ArrayList/*!*/ /*LinearConstraint*/ list) {
-      Contract.Requires(list != null);
-      ArrayList /*LinearConstraint*/ z = new ArrayList /*LinearConstraint*/ (list.Count);
-      foreach (LinearConstraint/*!*/ lc in list) {
-        Contract.Assert(lc != null);
-        z.Add(lc.Clone());
-      }
-      System.Diagnostics.Debug.Assert(z.Count == list.Count);
-      return z;
-    }
-
-    /// <summary>
-    /// Clones "list" and the elements of "list".
-    /// </summary>
-    /// <param name="list"></param>
-    /// <returns></returns>
-    ArrayList /*FrameElement*/ DeeperListCopy_FE(ArrayList/*!*/ /*FrameElement*/ list) {
-      Contract.Requires(list != null);
-      ArrayList /*FrameElement*/ z = new ArrayList /*FrameElement*/ (list.Count);
-      foreach (FrameElement/*!*/ fe in list) {
-        Contract.Assert(fe != null);
-        z.Add(fe.Clone());
-      }
-      System.Diagnostics.Debug.Assert(z.Count == list.Count);
-      return z;
-    }
-
-    // --------------------------------------------------------------------------------------------------------
-    // ------------------ Debugging and unit test routines ----------------------------------------------------
-    // --------------------------------------------------------------------------------------------------------
-
-    public void Dump() {
-      Console.WriteLine("  Constraints:");
-      if (Constraints == null) {
-        Console.WriteLine("    <bottom>");
-      } else {
-        foreach (LinearConstraint cc in Constraints) {
-          Console.WriteLine("    {0}", cc);
-        }
-      }
-
-      Console.WriteLine("  FrameDimensions: {0}", FrameDimensions);
-
-      Console.WriteLine("  FrameVerticies:");
-      if (FrameVertices == null) {
-        Console.WriteLine("    <null>");
-      } else {
-        foreach (FrameElement fe in FrameVertices) {
-          Console.WriteLine("    {0}", fe);
-        }
-      }
-
-      Console.WriteLine("  FrameRays:");
-      if (FrameRays == null) {
-        Console.WriteLine("    <null>");
-      } else {
-        foreach (FrameElement fe in FrameRays) {
-          Console.WriteLine("    {0}", fe);
-        }
-      }
-
-      Console.WriteLine("  FrameLines:");
-      if (FrameLines == null) {
-        Console.WriteLine("    <null>");
-      } else {
-        foreach (FrameElement fe in FrameLines) {
-          Console.WriteLine("    {0}", fe);
-        }
-      }
-    }
-
-    class TestVariable : IVariable {
-      readonly string/*!*/ name;
-      [ContractInvariantMethod]
-      void ObjectInvariant() {
-        Contract.Invariant(name != null);
-      }
-
-
-      public string/*!*/ Name {
-        get {
-          Contract.Ensures(Contract.Result<string>() != null);
-
-          return name;
-        }
-      }
-
-      public TestVariable(string/*!*/ name) {
-        Contract.Requires(name != null);
-        this.name = name;
-      }
-      [Pure]
-      public object DoVisit(ExprVisitor/*!*/ visitor) {
-        //Contract.Requires(visitor != null);
-        return visitor.VisitVariable(this);
-      }
-    }
-
-    public static void RunValidationA() {
-      IVariable/*!*/ dim1 = new TestVariable("X");
-      IVariable/*!*/ dim2 = new TestVariable("Y");
-      IVariable/*!*/ dim3 = new TestVariable("Z");
-      Contract.Assert(dim1 != null);
-      Contract.Assert(dim2 != null);
-      Contract.Assert(dim3 != null);
-
-      FrameElement s1 = new FrameElement();
-      s1.AddCoordinate(dim1, Rational.ONE);
-      s1.AddCoordinate(dim2, Rational.MINUS_ONE);
-      s1.AddCoordinate(dim3, Rational.ZERO);
-      FrameElement s2 = new FrameElement();
-      s2.AddCoordinate(dim1, Rational.MINUS_ONE);
-      s2.AddCoordinate(dim2, Rational.ONE);
-      s2.AddCoordinate(dim3, Rational.ZERO);
-      FrameElement r1 = new FrameElement();
-      r1.AddCoordinate(dim1, Rational.ZERO);
-      r1.AddCoordinate(dim2, Rational.ZERO);
-      r1.AddCoordinate(dim3, Rational.ONE);
-      FrameElement d1 = new FrameElement();
-      d1.AddCoordinate(dim1, Rational.ONE);
-      d1.AddCoordinate(dim2, Rational.ONE);
-      d1.AddCoordinate(dim3, Rational.ZERO);
-
-      // create lcs from frame -- cf. Cousot/Halbwachs 1978, section 3.3.1.1
-      LinearConstraintSystem lcs = new LinearConstraintSystem(s1);
-      lcs.Dump();
-
-      lcs.AddVertex(s2);
-      lcs.Dump();
-
-      lcs.AddRay(r1);
-      lcs.Dump();
-
-      lcs.AddLine(d1);
-      lcs.Dump();
-
-      lcs.SimplifyConstraints();
-      lcs.Dump();
-
-#if LATER
-      lcs.GenerateFrameFromConstraints(); // should give us back the original frame...
-#endif
-      Console.WriteLine("IsSubset? {0}", lcs.IsSubset(lcs.Clone()));
-      lcs.Dump();
-    }
-
-    /// <summary>
-    /// Tests the example in section 3.4.3 of Cousot and Halbwachs.
-    /// </summary>
-    public static void RunValidationB() {
-      IVariable/*!*/ X = new TestVariable("X");
-      IVariable/*!*/ Y = new TestVariable("Y");
-      IVariable/*!*/ Z = new TestVariable("Z");
-      Contract.Assert(X != null);
-      Contract.Assert(Y != null);
-      Contract.Assert(Z != null);
-      ArrayList /*LinearConstraint*/ cs = new ArrayList /*LinearConstraint*/ ();
-
-      LinearConstraint c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
-      c.SetCoefficient(X, Rational.MINUS_ONE);
-      c.SetCoefficient(Y, Rational.ONE);
-      c.SetCoefficient(Z, Rational.MINUS_ONE);
-      c.rhs = Rational.ZERO;
-      cs.Add(c);
-
-      c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
-      c.SetCoefficient(X, Rational.MINUS_ONE);
-      c.rhs = Rational.MINUS_ONE;
-      cs.Add(c);
-
-      c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
-      c.SetCoefficient(X, Rational.MINUS_ONE);
-      c.SetCoefficient(Y, Rational.MINUS_ONE);
-      c.SetCoefficient(Z, Rational.ONE);
-      c.rhs = Rational.ZERO;
-      cs.Add(c);
-
-      c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
-      c.SetCoefficient(Y, Rational.MINUS_ONE);
-      c.SetCoefficient(Z, Rational.ONE);
-      c.rhs = Rational.FromInt(3);
-      cs.Add(c);
-
-      LinearConstraintSystem lcs = new LinearConstraintSystem(cs);
-      Console.WriteLine("==================== The final linear constraint system ====================");
-      lcs.Dump();
-    }
-
-    public static void RunValidationC() {
-      // Run the example in section 3.4.3 of Cousot and Halbwachs backwards, that is, from
-      // from to constraints.
-      IVariable/*!*/ dim1 = new TestVariable("X");
-      IVariable/*!*/ dim2 = new TestVariable("Y");
-      IVariable/*!*/ dim3 = new TestVariable("Z");
-      Contract.Assert(dim1 != null);
-      Contract.Assert(dim2 != null);
-      Contract.Assert(dim3 != null);
-
-      FrameElement s0 = new FrameElement();
-      s0.AddCoordinate(dim1, Rational.ONE);
-      s0.AddCoordinate(dim2, Rational.FromInts(1, 2));
-      s0.AddCoordinate(dim3, Rational.FromInts(-1, 2));
-
-      FrameElement s1 = new FrameElement();
-      s1.AddCoordinate(dim1, Rational.ONE);
-      s1.AddCoordinate(dim2, Rational.FromInts(-1, 2));
-      s1.AddCoordinate(dim3, Rational.FromInts(1, 2));
-
-      FrameElement s2 = new FrameElement();
-      s2.AddCoordinate(dim1, Rational.FromInt(3));
-      s2.AddCoordinate(dim2, Rational.FromInts(-3, 2));
-      s2.AddCoordinate(dim3, Rational.FromInts(3, 2));
-
-      FrameElement r0 = new FrameElement();
-      r0.AddCoordinate(dim1, Rational.ONE);
-      r0.AddCoordinate(dim2, Rational.FromInts(1, 2));
-      r0.AddCoordinate(dim3, Rational.FromInts(-1, 2));
-
-      FrameElement r1 = new FrameElement();
-      r1.AddCoordinate(dim1, Rational.ONE);
-      r1.AddCoordinate(dim2, Rational.ZERO);
-      r1.AddCoordinate(dim3, Rational.ZERO);
-
-      FrameElement d0 = new FrameElement();
-      d0.AddCoordinate(dim1, Rational.ZERO);
-      d0.AddCoordinate(dim2, Rational.ONE);
-      d0.AddCoordinate(dim3, Rational.ONE);
-
-      LinearConstraintSystem lcs = new LinearConstraintSystem(s0);
-      lcs.Dump();
-
-      lcs.AddVertex(s1);
-      lcs.Dump();
-
-      lcs.AddVertex(s2);
-      lcs.Dump();
-
-      lcs.AddRay(r0);
-      lcs.Dump();
-
-      lcs.AddRay(r1);
-      lcs.Dump();
-
-      lcs.AddLine(d0);
-      lcs.Dump();
-
-      lcs.SimplifyConstraints();
-      lcs.Dump();
-
-#if LATER
-      lcs.GenerateFrameFromConstraints(); // should give us back the original frame...
-#endif
-    }
-  }
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.AbstractInterpretationFramework {
+  using System.Collections;
+  using System.Collections.Generic;
+  using System.Diagnostics;
+  using System;
+  //using Microsoft.SpecSharp.Collections;
+  using System.Diagnostics.Contracts;
+  using Microsoft.Basetypes;
+
+  using IMutableSet = Microsoft.Boogie.GSet<object>;
+  using ISet = Microsoft.Boogie.GSet<object>;
+  using HashSet = Microsoft.Boogie.GSet<object>;
+
+  /// <summary>
+  /// Represents a system of linear constraints (constraint/frame representations).
+  /// </summary>
+  public class LinearConstraintSystem {
+    // --------------------------------------------------------------------------------------------------------
+    // ------------------ Data structure ----------------------------------------------------------------------
+    // --------------------------------------------------------------------------------------------------------
+
+    public /*maybe null*/ ArrayList /*LinearConstraint!*/ Constraints;
+    /*maybe null*/
+    ArrayList /*FrameElement!*/ FrameVertices;
+    /*maybe null*/
+    ArrayList /*FrameElement!*/ FrameRays;
+    IMutableSet/*IVariable!*//*!*/ FrameDimensions;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(FrameDimensions != null);
+    }
+
+    /*maybe null*/
+    ArrayList /*FrameElement!*/ FrameLines;
+    // Invariant:  Either all of Constraints, FrameVertices, FrameRays, and FrameLines are
+    // null, or all are non-null.
+    // Invariant:  Any dimension mentioned in Constraints, FrameVertices, FrameRays, or
+    // FrameLines is mentioned in FrameDimensions.
+    // The meaning of FrameDimensions is that for any dimension x not in FrameDimensions,
+    // there is an implicit line along dimension x (that is, (<x,1>)).
+
+    void CheckInvariant() {
+      if (Constraints == null) {
+        System.Diagnostics.Debug.Assert(FrameVertices == null);
+        System.Diagnostics.Debug.Assert(FrameRays == null);
+        System.Diagnostics.Debug.Assert(FrameLines == null);
+        System.Diagnostics.Debug.Assert(FrameDimensions.Count == 0);
+      } else {
+        System.Diagnostics.Debug.Assert(FrameVertices != null);
+        System.Diagnostics.Debug.Assert(FrameRays != null);
+        System.Diagnostics.Debug.Assert(FrameLines != null);
+
+        foreach (LinearConstraint/*!*/ cc in Constraints) {
+          Contract.Assert(cc != null);
+#if FIXED_DESERIALIZER        
+          Contract.Assert(Contract.ForAll(cc.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
+#endif
+          Contract.Assert(cc.coefficients.Count != 0);
+        }
+        foreach (ArrayList /*FrameElement*//*!*/ FrameComponent in new ArrayList /*FrameElement*/ [] { FrameVertices, FrameRays, FrameLines }) {
+          Contract.Assert(FrameComponent != null);
+          foreach (FrameElement fe in FrameComponent) {
+            if (fe == null)
+              continue;
+#if FIXED_DESERIALIZER        
+            Contract.Assert(Contract.ForAll(fe.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
+#endif
+          }
+        }
+      }
+    }
+
+    // --------------------------------------------------------------------------------------------------------
+    // ------------------ Constructors ------------------------------------------------------------------------
+    // --------------------------------------------------------------------------------------------------------
+
+    /// <summary>
+    /// Creates a LinearConstraintSystem representing the bottom element, that is, representing
+    /// an unsatisfiable system of constraints.
+    /// </summary>
+    [NotDelayed]
+    public LinearConstraintSystem() {
+      FrameDimensions = new HashSet /*IVariable!*/ ();
+      //:base();
+      CheckInvariant();
+    }
+
+    /// <summary>
+    /// Constructs a linear constraint system with constraints "cs".
+    /// The constructor captures all constraints in "cs".
+    /// </summary>
+    /// <param name="cs"></param>
+    [NotDelayed]
+    public LinearConstraintSystem(ArrayList /*LinearConstraint!*//*!*/ cs) {
+      Contract.Requires(cs != null);
+#if BUG_159_HAS_BEEN_FIXED
+      Contract.Requires(Contract.ForAll(cs) , cc=> cc.coefficients.Count != 0);
+#endif
+
+      ArrayList constraints = new ArrayList /*LinearConstraint!*/ (cs.Count);
+      foreach (LinearConstraint/*!*/ cc in cs) {
+        Contract.Assert(cc != null);
+        constraints.Add(cc);
+      }
+      Constraints = constraints;
+      FrameDimensions = new HashSet /*IVariable!*/ ();  // to please compiler; this value will be overridden in the call to GenerateFrameConstraints below
+      //:base();
+
+      GenerateFrameFromConstraints();
+      SimplifyConstraints();
+      CheckInvariant();
+#if DEBUG_PRINT
+      Console.WriteLine("LinearConstraintSystem: constructor produced:");
+      Dump();
+#endif
+    }
+
+    /// <summary>
+    /// Constructs a linear constraint system corresponding to given vertex.  This constructor
+    /// is only used in the test harness--it is not needed for abstract interpretation.
+    /// </summary>
+    /// <param name="v"></param>
+    [NotDelayed]
+    LinearConstraintSystem(FrameElement/*!*/ v) {
+      Contract.Requires(v != null);
+      IMutableSet/*!*/ frameDims = v.GetDefinedDimensions();
+      Contract.Assert(frameDims != null);
+      ArrayList /*LinearConstraint!*/ constraints = new ArrayList /*LinearConstraint!*/ ();
+      foreach (IVariable/*!*/ dim in frameDims) {
+        Contract.Assert(dim != null);
+        LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
+        lc.SetCoefficient(dim, Rational.ONE);
+        lc.rhs = v[dim];
+        constraints.Add(lc);
+      }
+      FrameDimensions = frameDims;
+      Constraints = constraints;
+
+      ArrayList /*FrameElement*/ frameVertices = new ArrayList /*FrameElement*/ ();
+      frameVertices.Add(v);
+      FrameVertices = frameVertices;
+
+      FrameRays = new ArrayList /*FrameElement*/ ();
+      FrameLines = new ArrayList /*FrameElement*/ ();
+
+      //:base();
+      CheckInvariant();
+    }
+
+    void ChangeIntoBottom() {
+      Constraints = null;
+      FrameVertices = null;
+      FrameRays = null;
+      FrameLines = null;
+      FrameDimensions.Clear();  // no implicit lines
+    }
+
+    // --------------------------------------------------------------------------------------------------------
+    // ------------------ Public operations and their support routines ----------------------------------------
+    // --------------------------------------------------------------------------------------------------------
+
+    public bool IsBottom() {
+      return Constraints == null;
+    }
+
+    public bool IsTop() {
+      return Constraints != null && Constraints.Count == 0;
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      if (Constraints == null) {
+        return "<bottom>";
+      } else if (Constraints.Count == 0) {
+        return "<top>";
+      } else {
+        string z = null;
+        foreach (LinearConstraint/*!*/ lc in Constraints) {
+          Contract.Assert(lc != null);
+          string s = lc.ToString();
+          if (z == null) {
+            z = s;
+          } else {
+            z += " AND " + s;
+          }
+        }
+        Contract.Assert(z != null);
+        return z;
+      }
+    }
+
+
+    public ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+      Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
+      Contract.Ensures(Contract.Result<ICollection<IVariable>>().IsReadOnly);
+      List<IVariable/*!*/> list = new List<IVariable/*!*/>();
+      foreach (IVariable/*!*/ v in FrameDimensions) {
+        Contract.Assert(v != null);
+        list.Add(v);
+      }
+      return cce.NonNull(list.AsReadOnly());
+    }
+
+    /// <summary>
+    /// Note: This method requires that all dimensions are of type Variable, something that's
+    /// not required elsewhere in this class.
+    /// </summary>
+    /// <returns></returns>
+    public IExpr/*!*/ ConvertToExpression(ILinearExprFactory/*!*/ factory) {
+      Contract.Requires(factory != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      if (this.Constraints == null) {
+        return factory.False;
+      }
+      if (this.Constraints.Count == 0) {
+        return factory.True;
+      }
+
+      IExpr result = null;
+      foreach (LinearConstraint/*!*/ lc in Constraints) {
+        Contract.Assert(lc != null);
+        IExpr conjunct = lc.ConvertToExpression(factory);
+        result = (result == null) ? conjunct : (IExpr)factory.And(conjunct, result);
+      }
+      Contract.Assert(result != null);
+      return result;
+    }
+
+
+    /* IsSubset(): determines if 'lcs' is a subset of 'this'
+     * -- See Cousot/Halbwachs 1978, section 
+     */
+    public bool IsSubset(LinearConstraintSystem/*!*/ lcs) {
+      Contract.Requires(lcs != null);
+      if (lcs.IsBottom()) {
+        return true;
+      } else if (this.IsBottom()) {
+        return false;
+#if DEBUG
+#else
+      } else if (this.IsTop()) {  // optimization -- this case not needed for correctness
+        return true;
+      } else if (lcs.IsTop()) {  // optimization -- this case not needed for correctness
+        return false;
+#endif
+      } else {
+        // phase 0: check if frame dimensions are a superset of the constraint dimensions
+        ISet /*IVariable!*//*!*/ frameDims = lcs.GetDefinedDimensions();
+        Contract.Assert(frameDims != null);
+#if DEBUG_PRINT
+        Console.WriteLine("DEBUG: IsSubset:");
+        Console.WriteLine("  --- this:");
+        this.Dump();
+        Console.WriteLine("  --- lcs:");
+        lcs.Dump();
+        Console.WriteLine("  ---");
+#endif
+        foreach (LinearConstraint/*!*/ cc in cce.NonNull(this.Constraints)) {
+          Contract.Assert(cc != null);
+#if DEBUG_PRINT
+          Console.WriteLine("   cc: {0}", cc);
+          Console.WriteLine("   cc.GetDefinedDimensions(): {0}", cc.GetDefinedDimensions());
+#endif
+
+          if (!Contract.ForAll(cc.GetDefinedDimensionsGeneric(), var => frameDims.Contains(var))) {
+#if DEBUG_PRINT
+            Console.WriteLine("  ---> phase 0 subset violated, return false from IsSubset");
+#endif
+            return false;
+          }
+        }
+      }
+
+      // phase 1: check frame vertices against each constraint...
+      foreach (FrameElement/*!*/ v in cce.NonNull(lcs.FrameVertices)) {
+        Contract.Assert(v != null);
+        foreach (LinearConstraint/*!*/ cc in this.Constraints) {
+          Contract.Assert(cc != null);
+          Rational q = cc.EvaluateLhs(v);
+          if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
+            if (!(q <= cc.rhs)) {
+#if DEBUG_PRINT
+              Console.WriteLine("  ---> phase 1a subset violated, return false from IsSubset");
+#endif
+              return false;
+            }
+          } else {
+            if (!(q == cc.rhs)) {
+#if DEBUG_PRINT
+              Console.WriteLine("  ---> phase 1b subset violated, return false from IsSubset");
+#endif
+              return false;
+            }
+          }
+        }
+      }
+
+      // phase 2: check frame rays against each constraint...
+      // To check if a ray "r" falls within a constraint "cc", we add the vector "r" to
+      // any point "p" on the side of the half-space or plane described by constraint, and
+      // then check if the resulting point satisfies the constraint.  That is, we check (for
+      // an inequality constraint with coefficients a1,a2,...,an and right-hand side
+      // constant C):
+      //     a1*(r1+p1) + a2*(r2+p2) + ... + an*(rn+pn) <= C
+      // Equivalently:
+      //     a1*r1 + a2*r2 + ... + an*rn + a1*p1 + a2*p2 + ... + an*pn <= C
+      // To find a point "p", we can pick out a coordinate, call it 1, with a non-zero
+      // coefficient in the constraint, and then choose "p" as the point that has the
+      // value C/a1 in coordinate 1 and has 0 in all other coordinates.  We then check:
+      //     a1*r1 + a2*r2 + ... + an*rn + a1*(C/a1) + a2*0 + ... + an*0 <= C
+      // which simplifies to:
+      //     a1*r1 + a2*r2 + ... + an*rn + C <= C
+      // which in turn simplifies to:
+      //     a1*r1 + a2*r2 + ... + an*rn <= 0
+      // If the constraint is an equality constraint, we simply replace "<=" with "=="
+      // above.
+      foreach (FrameElement/*!*/ r in cce.NonNull(lcs.FrameRays)) {
+        Contract.Assert(r != null);
+        System.Diagnostics.Debug.Assert(r != null, "encountered a null ray...");
+        foreach (LinearConstraint/*!*/ cc in this.Constraints) {
+          Contract.Assert(cc != null);
+          System.Diagnostics.Debug.Assert(cc != null, "encountered an null constraint...");
+          Rational q = cc.EvaluateLhs(r);
+          if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
+            if (q.IsPositive) {
+#if DEBUG_PRINT
+              Console.WriteLine("  ---> phase 2a subset violated, return false from IsSubset");
+#endif
+              return false;
+            }
+          } else {
+            if (q.IsNonZero) {
+#if DEBUG_PRINT
+              Console.WriteLine("  ---> phase 2b subset violated, return false from IsSubset");
+#endif
+              return false;
+            }
+          }
+        }
+      }
+
+      // phase 3: check frame lines against each constraint...
+      // To check if a line "L" falls within a constraint "cc", we check if both the
+      // vector "L" and "-L", interpreted as rays, fall within the constraint.  From
+      // the discussion above, this means we check the following two properties:
+      //     a1*L1 + a2*L2 + ... + an*Ln <= 0                 (*)
+      //     a1*(-L1) + a2*(-L2) + ... + an*(-Ln) <= 0
+      // The second of these lines can be rewritten as:
+      //     - a1*L1 - a2*L2 - ... - an*Ln <= 0
+      // which is equivalent to:
+      //     -1 * (a1*L1 + a2*L2 + ... + an*Ln) <= 0
+      // Multiplying both sides by -1 and flipping the direction of the inequality,
+      // we have:
+      //     a1*L1 + a2*L2 + ... + an*Ln >= 0                 (**)
+      // Putting (*) and (**) together, we conclude that we need to check:
+      //     a1*L1 + a2*L2 + ... + an*Ln == 0
+      // If the constraint is an equality constraint, we end up with the same equation.
+      foreach (FrameElement/*!*/ line in cce.NonNull(lcs.FrameLines)) {
+        Contract.Assert(line != null);
+        System.Diagnostics.Debug.Assert(line != null, "encountered a null line...");
+        foreach (LinearConstraint/*!*/ cc in this.Constraints) {
+          Contract.Assert(cc != null);
+          System.Diagnostics.Debug.Assert(cc != null, "encountered an null constraint...");
+          Rational q = cc.EvaluateLhs(line);
+          if (q.IsNonZero) {
+#if DEBUG_PRINT
+            Console.WriteLine("  ---> phase 3 subset violated, return false from IsSubset");
+#endif
+            return false;
+          }
+        }
+      }
+
+#if DEBUG_PRINT
+      Console.WriteLine("  ---> IsSubset returns true");
+#endif
+      return true;
+    }
+
+    public LinearConstraintSystem/*!*/ Meet(LinearConstraintSystem/*!*/ lcs) {
+      Contract.Requires(lcs != null);
+      Contract.Requires((this.Constraints != null));
+      Contract.Requires((lcs.Constraints != null));
+      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
+      ArrayList /*LinearConstraint*/ clist = new ArrayList(this.Constraints.Count + lcs.Constraints.Count);
+      clist.AddRange(this.Constraints);
+      clist.AddRange(lcs.Constraints);
+      return new LinearConstraintSystem(clist);
+    }
+
+#if DEBUG_PRINT
+    public LinearConstraintSystem Join(LinearConstraintSystem lcs)
+    {
+      Console.WriteLine("===================================================================================");
+      Console.WriteLine("DEBUG: Join");
+      Console.WriteLine("Join: this=");
+      Dump();
+      Console.WriteLine("Join: lcs=");
+      lcs.Dump();
+      LinearConstraintSystem z = JoinX(lcs);
+      Console.WriteLine("----------Join------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>");
+      Console.WriteLine("Join: result=");
+      z.Dump();
+      Console.WriteLine("===================================================================================");
+      return z;
+    }
+#endif
+
+    /// <summary>
+    /// The join is computed as described in section 4.4 in Cousot and Halbwachs.
+    /// </summary>
+    /// <param name="lcs"></param>
+    /// <returns></returns>
+#if DEBUG_PRINT
+    public LinearConstraintSystem JoinX(LinearConstraintSystem lcs) {
+#else
+    public LinearConstraintSystem/*!*/ Join(LinearConstraintSystem/*!*/ lcs) {
+      Contract.Requires(lcs != null);
+      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
+#endif
+
+      if (this.IsBottom()) {
+        return cce.NonNull(lcs.Clone());
+      } else if (lcs.IsBottom()) {
+        return cce.NonNull(this.Clone());
+      } else if (this.IsTop() || lcs.IsTop()) {
+        return new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ());
+      } else {
+        LinearConstraintSystem/*!*/ z;
+        // Start from the "larger" of the two frames (this is just a heuristic measure intended
+        // to save work).
+        Contract.Assume(this.FrameVertices != null);
+        Contract.Assume(this.FrameRays != null);
+        Contract.Assume(this.FrameLines != null);
+        Contract.Assume(lcs.FrameVertices != null);
+        Contract.Assume(lcs.FrameRays != null);
+        Contract.Assume(lcs.FrameLines != null);
+        if (this.FrameVertices.Count + this.FrameRays.Count + this.FrameLines.Count - this.FrameDimensions.Count <
+          lcs.FrameVertices.Count + lcs.FrameRays.Count + lcs.FrameLines.Count - lcs.FrameDimensions.Count) {
+          z = cce.NonNull(lcs.Clone());
+          lcs = this;
+        } else {
+          z = cce.NonNull(this.Clone());
+        }
+#if DEBUG_PRINT
+        Console.WriteLine("DEBUG: LinearConstraintSystem.Join ---------------");
+        Console.WriteLine("z:");
+        z.Dump();
+        Console.WriteLine("lcs:");
+        lcs.Dump();
+#endif
+
+        // Start by explicating the implicit lines of z for the dimensions dims(lcs)-dims(z).
+        foreach (IVariable/*!*/ dim in lcs.FrameDimensions) {
+          Contract.Assert(dim != null);
+          if (!z.FrameDimensions.Contains(dim)) {
+            z.FrameDimensions.Add(dim);
+            FrameElement line = new FrameElement();
+            line.AddCoordinate(dim, Rational.ONE);
+            // Note:  AddLine is not called (because the line already exists in z--it's just that
+            // it was represented implicitly).  Instead, just tack the explicit representation onto
+            // FrameLines.
+            Contract.Assume(z.FrameLines != null);
+            z.FrameLines.Add(line);
+#if DEBUG_PRINT
+            Console.WriteLine("Join: After explicating line: {0}", line);
+            z.Dump();
+#endif
+          }
+        }
+
+        // Now, the vertices, rays, and lines can be added.
+        foreach (FrameElement/*!*/ v in lcs.FrameVertices) {
+          Contract.Assert(v != null);
+          z.AddVertex(v);
+#if DEBUG_PRINT
+          Console.WriteLine("Join: After adding vertex: {0}", v);
+          z.Dump();
+#endif
+        }
+        foreach (FrameElement/*!*/ r in lcs.FrameRays) {
+          Contract.Assert(r != null);
+          z.AddRay(r);
+#if DEBUG_PRINT
+          Console.WriteLine("Join: After adding ray: {0}", r);
+          z.Dump();
+#endif
+        }
+        foreach (FrameElement/*!*/ l in lcs.FrameLines) {
+          Contract.Assert(l != null);
+          z.AddLine(l);
+#if DEBUG_PRINT
+          Console.WriteLine("Join: After adding line: {0}", l);
+          z.Dump();
+#endif
+        }
+        // also add to z the implicit lines of lcs
+        foreach (IVariable/*!*/ dim in z.FrameDimensions) {
+          Contract.Assert(dim != null);
+          if (!lcs.FrameDimensions.Contains(dim)) {
+            // "dim" is a dimension that's explicit in "z" but implicit in "lcs"
+            FrameElement line = new FrameElement();
+            line.AddCoordinate(dim, Rational.ONE);
+            z.AddLine(line);
+#if DEBUG_PRINT
+            Console.WriteLine("Join: After adding lcs's implicit line: {0}", line);
+            z.Dump();
+#endif
+          }
+        }
+
+        z.SimplifyFrame();
+        z.SimplifyConstraints();
+        z.CheckInvariant();
+#if DEBUG_PRINT
+        Console.WriteLine("Join: Returning z:");
+        z.Dump();
+        Console.WriteLine("----------------------------------------");
+#endif
+        return z;
+      }
+    }
+
+#if DEBUG_PRINT
+    public LinearConstraintSystem Widen(LinearConstraintSystem lcs)
+    {
+      Console.WriteLine("===================================================================================");
+      Console.WriteLine("DEBUG: Widen");
+      Console.WriteLine("Widen: this=");
+      Dump();
+      Console.WriteLine("Widen: lcs=");
+      lcs.Dump();
+      LinearConstraintSystem z = WidenX(lcs);
+      Console.WriteLine("----------Widen------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>");
+      Console.WriteLine("Widen: result=");
+      z.Dump();
+      Console.WriteLine("===================================================================================");
+      return z;
+    }
+#endif
+
+#if DEBUG_PRINT
+    public LinearConstraintSystem WidenX(LinearConstraintSystem lcs){
+#else
+    public LinearConstraintSystem/*!*/ Widen(LinearConstraintSystem/*!*/ lcs) {
+      Contract.Requires(lcs != null);
+      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
+#endif
+      if (this.IsBottom()) {
+        return cce.NonNull(lcs.Clone());
+      } else if (lcs.IsBottom()) {
+        return cce.NonNull(this.Clone());
+      } else if (this.IsTop() || lcs.IsTop()) {
+        return new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ());
+      }
+
+      // create new LCS, we will add only verified constraints to this...
+      ArrayList /*LinearConstraint*/ newConstraints = new ArrayList /*LinearConstraint*/ ();
+      Contract.Assume(this.Constraints != null);
+      foreach (LinearConstraint/*!*/ ccX in this.Constraints) {
+        Contract.Assert(ccX != null);
+        LinearConstraint cc = ccX;
+#if DEBUG_PRINT
+        Console.WriteLine("Widen checking: Starting to check constraint: {0}", cc);
+#endif
+        if (cc.IsConstant()) {
+          // (Can this ever occur in the stable state of a LinearConstraintSystem?  --KRML)
+          // constraint is unaffected by the frame components
+#if DEBUG_PRINT
+          Console.WriteLine("Widen checking:   --Adding it!");
+#endif
+          newConstraints.Add(cc);
+          continue;
+        }
+
+        // PHASE I: verify constraints against all frame vertices...
+
+        foreach (FrameElement/*!*/ vertex in cce.NonNull(lcs.FrameVertices)) {
+          Contract.Assert(vertex != null);
+          Rational lhs = cc.EvaluateLhs(vertex);
+          if (lhs > cc.rhs) {
+            // the vertex does not satisfy the inequality <=
+            if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
+#if DEBUG_PRINT
+              Console.WriteLine("Widen checking:   throwing out because of vertex: {0}", vertex);
+#endif
+              goto CHECK_NEXT_CONSTRAINT;
+            } else {
+              // ... but it does satisfy the inequality >=
+#if DEBUG_PRINT
+              Console.WriteLine("Widen checking:   throwing out <= because of vertex: {0}", vertex);
+#endif
+              cc = cc.ChangeRelationToAtLeast();
+#if DEBUG_PRINT
+              Console.WriteLine("Widen checking:   left with constraint: {0}", cc);
+#endif
+            }
+          } else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ && lhs < cc.rhs) {
+            // the vertex does not satisfy the inequality >=, and the constraint is an equality constraint
+#if DEBUG_PRINT
+            Console.WriteLine("Widen checking:   throwing out >= because of vertex: {0}", vertex);
+#endif
+            cc = cc.ChangeRelation(LinearConstraint.ConstraintRelation.LE);
+#if DEBUG_PRINT
+            Console.WriteLine("Widen checking:   left with contraint: {0}", cc);
+#endif
+          }
+        }
+
+        // PHASE II: verify constraints against all frame rays...
+
+        foreach (FrameElement/*!*/ ray in cce.NonNull(lcs.FrameRays)) {
+          Contract.Assert(ray != null);
+          // The following assumes the constraint to have some dimension with a non-zero coefficient
+          Rational lhs = cc.EvaluateLhs(ray);
+          if (lhs.IsPositive) {
+            // the ray does not satisfy the inequality <=
+            if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
+#if DEBUG_PRINT
+              Console.WriteLine("Widen checking:   throwing out because of ray: {0}", ray);
+#endif
+              goto CHECK_NEXT_CONSTRAINT;
+            } else {
+              // ... but it does satisfy the inequality >=
+#if DEBUG_PRINT
+              Console.WriteLine("Widen checking:   throwing out <= because of ray: {0}", ray);
+#endif
+              cc = cc.ChangeRelationToAtLeast();
+#if DEBUG_PRINT
+              Console.WriteLine("Widen checking:   left with contraint: {0}", cc);
+#endif
+            }
+          } else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ && lhs.IsNegative) {
+            // the ray does not satisfy the inequality >=, and the constraint is an equality constraint
+#if DEBUG_PRINT
+            Console.WriteLine("Widen checking:   throwing out >= because of ray: {0}", ray);
+#endif
+            cc = cc.ChangeRelation(LinearConstraint.ConstraintRelation.LE);
+#if DEBUG_PRINT
+            Console.WriteLine("Widen checking:   left with constraint: {0}", cc);
+#endif
+          }
+        }
+
+        // PHASE III: verify constraints against all frame lines...
+
+        foreach (FrameElement/*!*/ line in cce.NonNull(lcs.FrameLines)) {
+          Contract.Assert(line != null);
+          // The following assumes the constraint to have some dimension with a non-zero coefficient
+          Rational lhs = cc.EvaluateLhs(line);
+          if (!lhs.IsZero) {
+            // The line satisfies neither the inequality <= nor the equality ==
+#if DEBUG_PRINT
+            Console.WriteLine("Widen checking:   throwing out because of line: {0}", line);
+#endif
+            goto CHECK_NEXT_CONSTRAINT;
+          }
+        }
+
+        // constraint has been verified, so add to new constraint system
+#if DEBUG_PRINT
+        Console.WriteLine("Widen checking:   --Adding it!");
+#endif
+        newConstraints.Add(cc);
+
+      CHECK_NEXT_CONSTRAINT: {
+        }
+#if DEBUG_PRINT
+        Console.WriteLine("Widen checking: done with that constraint");
+#endif
+      }
+
+      return new LinearConstraintSystem(newConstraints);
+    }
+
+#if DEBUG_PRINT
+    public LinearConstraintSystem Project(IVariable/*!*/ dim){
+Contract.Requires(dim != null);
+      Console.WriteLine("===================================================================================");
+      Console.WriteLine("DEBUG: Project(dim={0})", dim);
+      Console.WriteLine("Project: this=");
+      Dump();
+      LinearConstraintSystem z = ProjectX(dim);
+      Console.WriteLine("----------Project------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>");
+      Console.WriteLine("Project: result=");
+      z.Dump();
+      Console.WriteLine("===================================================================================");
+      return z;
+    }
+#endif
+
+#if DEBUG_PRINT
+    public LinearConstraintSystem ProjectX(IVariable/*!*/ dim){Contract.Requires(dim != null);Contract.Requires(this.Constraints != null);
+#else
+    public LinearConstraintSystem/*!*/ Project(IVariable/*!*/ dim) {
+      Contract.Requires(dim != null);
+      Contract.Requires(this.Constraints != null);
+      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
+#endif
+
+
+      ArrayList /*LinearConstraint!*//*!*/ cc = Project(dim, Constraints);
+      Contract.Assert(cc != null);
+      return new LinearConstraintSystem(cc);
+    }
+
+#if DEBUG_PRINT
+    public LinearConstraintSystem Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName){
+Contract.Requires(newName != null);
+Contract.Requires(oldName != null);
+      Console.WriteLine("===================================================================================");
+      Console.WriteLine("DEBUG: Rename(oldName={0}, newName={1})", oldName, newName);
+      Console.WriteLine("Rename: this=");
+      Dump();
+      LinearConstraintSystem z = RenameX(oldName, newName);
+      Console.WriteLine("----------Rename------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>");
+      Console.WriteLine("Rename: result=");
+      z.Dump();
+      Console.WriteLine("===================================================================================");
+      return z;
+    }
+#endif
+
+#if DEBUG_PRINT
+    public LinearConstraintSystem RenameX(IVariable/*!*/ oldName, IVariable/*!*/ newName){Contract.Requires(oldName != null);Contract.Requires(newName != null);
+#else
+    public LinearConstraintSystem/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+      Contract.Requires(oldName != null);
+      Contract.Requires(newName != null);
+      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
+#endif
+      if (this.Constraints == null) {
+        System.Diagnostics.Debug.Assert(this.FrameVertices == null);
+        System.Diagnostics.Debug.Assert(this.FrameRays == null);
+        System.Diagnostics.Debug.Assert(this.FrameLines == null);
+        return this;
+      }
+      IMutableSet /*IVariable!*//*!*/ dims = this.FrameDimensions;
+      Contract.Assert(dims != null);
+      if (!dims.Contains(oldName)) {
+        return this;
+      }
+
+      LinearConstraintSystem z = new LinearConstraintSystem();
+      z.FrameDimensions = cce.NonNull((HashSet/*!*/ /*IVariable!*/)dims.Clone());
+      z.FrameDimensions.Remove(oldName);
+      z.FrameDimensions.Add(newName);
+
+      z.Constraints = new ArrayList /*LinearConstraint!*/ (this.Constraints.Count);
+      foreach (LinearConstraint/*!*/ lc in cce.NonNull(this.Constraints)) {
+        Contract.Assert(lc != null);
+        z.Constraints.Add(lc.Rename(oldName, newName));
+      }
+      z.FrameVertices = RenameInFE(cce.NonNull(this.FrameVertices), oldName, newName);
+      z.FrameRays = RenameInFE(cce.NonNull(this.FrameRays), oldName, newName);
+      z.FrameLines = RenameInFE(cce.NonNull(this.FrameLines), oldName, newName);
+      return z;
+    }
+
+    static ArrayList /*FrameElement*/ RenameInFE(ArrayList/*!*/ /*FrameElement*/ list, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+      Contract.Requires(list != null);
+      Contract.Requires(newName != null);
+      Contract.Requires(oldName != null);
+      ArrayList/*FrameElement!*//*!*/ z = new ArrayList/*FrameElement!*/ (list.Count);
+      Contract.Assert(z != null);
+      foreach (FrameElement/*!*/ fe in list) {
+        Contract.Assert(fe != null);
+        z.Add(fe.Rename(oldName, newName));
+      }
+      System.Diagnostics.Debug.Assert(z.Count == list.Count);
+      return z;
+    }
+
+    // --------------------------------------------------------------------------------------------------------
+    // ------------------ support routines --------------------------------------------------------------------
+    // --------------------------------------------------------------------------------------------------------
+
+    /// <summary>
+    /// Returns a set of constraints that is the given set of constraints with dimension "dim"
+    /// projected out.  See Cousot and Halbwachs, section 3.3.1.1.
+    /// </summary>
+    /// <param name="dim"></param>
+    /// <param name="constraints"></param>
+    /// <returns></returns>
+    static ArrayList /*LinearConstraint!*//*!*/ Project(IVariable/*!*/ dim, ArrayList /*LinearConstraint!*//*!*/ constraints) {
+      Contract.Requires(constraints != null);
+      Contract.Requires(dim != null);
+      Contract.Ensures(Contract.Result<ArrayList>() != null);
+      // Sort the inequality constaints into ones where dimension "dim" is 0, negative, and
+      // positive, respectively.  Put equality constraints with a non-0 "dim" into "eq".
+      ArrayList /*LinearConstraint!*//*!*/ final = new ArrayList /*LinearConstraint!*/ ();
+      ArrayList /*LinearConstraint!*//*!*/ negative = new ArrayList /*LinearConstraint!*/ ();
+      ArrayList /*LinearConstraint!*//*!*/ positive = new ArrayList /*LinearConstraint!*/ ();
+      ArrayList /*LinearConstraint!*//*!*/ eq = new ArrayList /*LinearConstraint!*/ ();
+      foreach (LinearConstraint/*!*/ cc in constraints) {
+        Contract.Assert(cc != null);
+        Rational coeff = cc[dim];
+        if (coeff.IsZero) {
+          LinearConstraint lc = cce.NonNull(cc.Clone());
+          if (!lc.IsConstant()) {
+            lc.RemoveDimension(dim);
+            final.Add(lc);
+          }
+        } else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ) {
+          eq.Add(cc);
+        } else if (coeff.IsNegative) {
+          negative.Add(cc);
+        } else {
+          System.Diagnostics.Debug.Assert(coeff.IsPositive);
+          positive.Add(cc);
+        }
+      }
+
+      if (eq.Count != 0) {
+        LinearConstraint eqConstraint = (LinearConstraint/*!*/)cce.NonNull(eq[eq.Count - 1]);
+        eq.RemoveAt(eq.Count - 1);
+        Rational eqC = -eqConstraint[dim];
+
+        foreach (ArrayList /*LinearConstraint!*/ list in new ArrayList[] { eq, negative, positive }) {
+          Contract.Assert(list != null);
+          foreach (LinearConstraint/*!*/ lcX in list) {
+            Contract.Assert(lcX != null);
+            LinearConstraint lc = cce.NonNull(lcX.Clone());
+            lc.AddMultiple(lc[dim] / eqC, eqConstraint);
+            System.Diagnostics.Debug.Assert(lc[dim].IsZero);
+            if (!lc.IsConstant()) {
+              lc.RemoveDimension(dim);
+              final.Add(lc);
+            } else {
+              System.Diagnostics.Debug.Assert(lc.IsConstantSatisfiable());
+            }
+          }
+        }
+      } else {
+        // Consider all pairs of constraints with (negative,positive) coefficients of "dim".
+        foreach (LinearConstraint/*!*/ cn in negative) {
+          Contract.Assert(cn != null);
+          Rational dn = -cn[dim];
+          System.Diagnostics.Debug.Assert(dn.IsNonNegative);
+          foreach (LinearConstraint/*!*/ cp in positive) {
+            Contract.Assert(cp != null);
+            Rational dp = cp[dim];
+
+            LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+            lc.AddMultiple(dn, cp);
+            lc.AddMultiple(dp, cn);
+            System.Diagnostics.Debug.Assert(lc[dim].IsZero);
+            if (!lc.IsConstant()) {
+              lc.RemoveDimension(dim);
+              final.Add(lc);
+            } else {
+              System.Diagnostics.Debug.Assert(lc.IsConstantSatisfiable());
+            }
+          }
+        }
+      }
+
+      return final;
+    }
+
+    /// <summary>
+    /// Initializes FrameVertices, FrameRays, FrameLines, and FrameDimensions, see
+    /// Cousot and Halbwachs, section 3.4.  Any previous values of these fields are
+    /// ignored and overwritten.
+    /// 
+    /// If the set of Constraints is unsatisfiable, then "this" is changed into Bottom.
+    /// </summary>
+    void GenerateFrameFromConstraints() {
+      if (Constraints == null) {
+        FrameVertices = null;
+        FrameRays = null;
+        FrameLines = null;
+        FrameDimensions = new HashSet /*IVariable!*/ ();
+        return;
+      }
+
+      // Step 1 (see Cousot and Halbwachs, section 3.4.3):  create a Simplex Tableau.
+#if DEBUG_PRINT
+      Console.WriteLine("DEBUG: --- GenerateFrameFromConstraint ---");
+      Console.WriteLine("Constraints:");
+      foreach (LinearConstraint cc in Constraints) 
+      {
+        Console.WriteLine("  {0}", cc);
+      }
+#endif
+      SimplexTableau tableau = new SimplexTableau(Constraints);
+#if DEBUG_PRINT
+      Console.WriteLine("Initial tableau:");
+      tableau.Dump();
+#endif
+      FrameDimensions = tableau.GetDimensions();
+#if DEBUG_PRINT
+      Console.WriteLine("Dimensions:");
+      foreach (object dim in FrameDimensions) 
+      {
+        Console.Write("  {0}", dim);
+      }
+      Console.WriteLine();
+#endif
+
+      // Step 3 and 2: Put as many initial variables as possible into basis, then check if
+      // we reached a feasible basis
+      tableau.AddInitialVarsToBasis();
+#if DEBUG_PRINT
+      Console.WriteLine("Tableau after Step 3:");
+      tableau.Dump();
+#endif
+      if (!tableau.IsFeasibleBasis) {
+        // The polyhedron is empty (according to Cousot and Halbwachs)
+        ChangeIntoBottom();
+        return;
+      }
+
+      FrameVertices = new ArrayList /*FrameElement*/ ();
+      FrameRays = new ArrayList /*FrameElement*/ ();
+      FrameLines = new ArrayList /*FrameElement*/ ();
+      if (FrameDimensions.Count == 0) {
+        // top element
+        return;
+      }
+
+      if (tableau.AllInitialVarsInBasis) {
+        // All initial variables are in basis; there are no lines.
+#if DEBUG_PRINT
+        Console.WriteLine("Tableau after Steps 2 and 3 (all initial variables in basis):");
+        tableau.Dump();
+#endif
+      } else {
+        // There are lines
+#if DEBUG_PRINT
+        Console.WriteLine("Tableau after Steps 2 and 3 (NOT all initial variables in basis--there are lines):");
+        tableau.Dump();
+#endif
+        // Step 4.2: Pick out the lines, then produce the tableau for a new polyhedron without those lines.
+        ArrayList /*LinearConstraint*/ moreConstraints = cce.NonNull((ArrayList/*!*/ /*LinearConstraint*/)Constraints.Clone());
+        tableau.ProduceLines(FrameLines, moreConstraints);
+        tableau = new SimplexTableau(moreConstraints);
+#if DEBUG_PRINT
+        Console.WriteLine("Lines produced:");
+        foreach (FrameElement line in FrameLines) 
+        {
+          Console.WriteLine("  {0}", line);
+        }
+        Console.WriteLine("The new list of constraints is:");
+        foreach (LinearConstraint c in moreConstraints) 
+        {
+          Console.WriteLine("  {0}", c);
+        }
+        Console.WriteLine("Tableau after producing lines in Step 4.2:");
+        tableau.Dump();
+#endif
+
+        // Repeat step 3 for the new tableau.
+        // Since the new tableau contains no lines, the following call should cause all initial
+        // variables to be in basis (see step 4.2 in section 3.4.3 of Cousot and Halbwachs).
+        tableau.AddInitialVarsToBasis();
+        System.Diagnostics.Debug.Assert(tableau.AllInitialVarsInBasis);
+        System.Diagnostics.Debug.Assert(tableau.IsFeasibleBasis);  // the new tableau represents a set of feasible constraints, so this basis should be found to be feasible
+#if DEBUG_PRINT
+        Console.WriteLine("Tableau after all initial variables have been moved into basis:");
+        tableau.Dump();
+#endif
+      }
+
+      // Step 4.1: One vertex has been found.  Find all others, too.
+      tableau.TraverseVertices(FrameVertices, FrameRays);
+#if DEBUG_PRINT
+      Console.WriteLine("Tableau after vertex traversal:");
+      tableau.Dump();
+#endif
+    }
+
+    class LambdaDimension : IVariable {
+      readonly int id;
+      static int count = 0;
+
+      /// <summary>
+      /// Return the name of the variable
+      /// </summary>
+      public string Name {
+        get {
+          Contract.Ensures(Contract.Result<string>() != null);
+
+          return this.ToString();
+        }
+      }
+
+      public LambdaDimension() {
+        id = count;
+        count++;
+      }
+      [Pure]
+      public override string/*!*/ ToString() {
+        Contract.Ensures(Contract.Result<string>() != null);
+        return "lambda" + id;
+      }
+      [Pure]
+      public object DoVisit(ExprVisitor/*!*/ visitor) {
+        //Contract.Requires(visitor != null);
+        return visitor.VisitVariable(this);
+      }
+    }
+
+    /// <summary>
+    /// Adds a vertex to the frame of "this" and updates Constraints accordingly, see
+    /// Cousot and Halbwachs, section 3.3.1.1.  However, this method does not simplify
+    /// Constraints after the operation; that remains the caller's responsibility (which
+    /// gives the caller the opportunity to make multiple calls to AddVertex, AddRay,
+    /// and AddLine before calling SimplifyConstraints).
+    /// Assumes Constraints (and the frame fields) to be non-null.
+    /// </summary>
+    /// <param name="vertex"></param>
+    void AddVertex(FrameElement/*!*/ vertex) {
+      Contract.Requires(vertex != null);
+      Contract.Requires(this.FrameVertices != null);
+#if DEBUG_PRINT
+      Console.WriteLine("DEBUG: AddVertex called on {0}", vertex);
+      Console.WriteLine("  Initial constraints:");
+      foreach (LinearConstraint cc in Constraints) {
+        Console.WriteLine("    {0}", cc);
+      }
+#endif
+
+      FrameVertices.Add(vertex.Clone());
+#if FIXED_DESERIALIZER      
+      Contract.Assert(Contract.ForAll(vertex.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
+#endif
+
+      // We use a new temporary dimension.
+      IVariable/*!*/ lambda = new LambdaDimension();
+
+      // We change the constraints A*X <= B into
+      //     A*X + (A*vector - B)*lambda <= A*vector.
+      // That means that each row k in A (which corresponds to one LinearConstraint
+      // in Constraints) is changed by adding
+      //     (A*vector - B)[k] * lambda
+      // to row k and changing the right-hand side of row k to
+      //     (A*vector)[k]
+      // Note:
+      //     (A*vector - B)[k]
+      //  =      { vector subtraction is pointwise }
+      //     (A*vector)[k] - B[k]
+      //  =      { A*vector is a row vector whose every row i is the dot-product of
+      //           row i of A with the column vector "vector" }
+      //     A[k]*vector - B[k]
+      foreach (LinearConstraint/*!*/ cc in cce.NonNull(Constraints)) {
+        Contract.Assert(cc != null);
+        Rational d = cc.EvaluateLhs(vertex);
+        cc.SetCoefficient(lambda, d - cc.rhs);
+        cc.rhs = d;
+      }
+
+      // We also add the constraints that lambda lies between 0 ...
+      LinearConstraint la = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+      la.SetCoefficient(lambda, Rational.MINUS_ONE);
+      la.rhs = Rational.ZERO;
+      Constraints.Add(la);
+      // ... and 1.
+      la = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+      la.SetCoefficient(lambda, Rational.ONE);
+      la.rhs = Rational.ONE;
+      Constraints.Add(la);
+#if DEBUG_PRINT
+      Console.WriteLine("  Constraints after addition:");
+      foreach (LinearConstraint cc in Constraints) {
+        Console.WriteLine("    {0}", cc);
+      }
+#endif
+
+      // Finally, project out the dummy dimension.
+      Constraints = Project(lambda, Constraints);
+
+#if DEBUG_PRINT
+      Console.WriteLine("  Resulting constraints:");
+      foreach (LinearConstraint cc in Constraints) {
+        Console.WriteLine("    {0}", cc);
+      }
+#endif
+    }
+
+    /// <summary>
+    /// Adds a ray to the frame of "this" and updates Constraints accordingly, see
+    /// Cousot and Halbwachs, section 3.3.1.1.  However, this method does not simplify
+    /// Constraints after the operation; that remains the caller's responsibility (which
+    /// gives the caller the opportunity to make multiple calls to AddVertex, AddRay,
+    /// and AddLine before calling SimplifyConstraints).
+    /// Assumes Constraints (and the frame fields) to be non-null.
+    /// </summary>
+    /// <param name="ray"></param>
+    void AddRay(FrameElement/*!*/ ray) {
+      Contract.Requires(ray != null);
+      Contract.Requires(this.FrameRays != null);
+#if DEBUG_PRINT
+      Console.WriteLine("DEBUG: AddRay called on {0}", ray);
+      Console.WriteLine("  Initial constraints:");
+      foreach (LinearConstraint cc in Constraints) {
+        Console.WriteLine("    {0}", cc);
+      }
+#endif
+
+      FrameRays.Add(ray.Clone());
+#if FIXED_DESERIALIZER      
+      Contract.Assert(Contract.ForAll(ray.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
+#endif
+
+      // We use a new temporary dimension.
+      IVariable/*!*/ lambda = new LambdaDimension();
+
+      // We change the constraints A*X <= B into
+      //     A*X - (A*ray)*lambda <= B.
+      // That means that each row k in A (which corresponds to one LinearConstraint
+      // in Constraints) is changed by subtracting
+      //     (A*ray)[k] * lambda
+      // from row k.
+      // Note:
+      //     (A*ray)[k]
+      //  =      { A*ray is a row vector whose every row i is the dot-product of
+      //           row i of A with the column vector "ray" }
+      //     A[k]*ray
+      foreach (LinearConstraint/*!*/ cc in cce.NonNull(Constraints)) {
+        Contract.Assert(cc != null);
+        Rational d = cc.EvaluateLhs(ray);
+        cc.SetCoefficient(lambda, -d);
+      }
+
+      // We also add the constraints that lambda is at least 0.
+      LinearConstraint la = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+      la.SetCoefficient(lambda, Rational.MINUS_ONE);
+      la.rhs = Rational.ZERO;
+      Constraints.Add(la);
+#if DEBUG_PRINT
+      Console.WriteLine("  Constraints after addition:");
+      foreach (LinearConstraint cc in Constraints) {
+        Console.WriteLine("    {0}", cc);
+      }
+#endif
+
+      // Finally, project out the dummy dimension.
+      Constraints = Project(lambda, Constraints);
+
+#if DEBUG_PRINT
+      Console.WriteLine("  Resulting constraints:");
+      foreach (LinearConstraint cc in Constraints) {
+        Console.WriteLine("    {0}", cc);
+      }
+#endif
+    }
+
+    /// <summary>
+    /// Adds a line to the frame of "this" and updates Constraints accordingly, see
+    /// Cousot and Halbwachs, section 3.3.1.1.  However, this method does not simplify
+    /// Constraints after the operation; that remains the caller's responsibility (which
+    /// gives the caller the opportunity to make multiple calls to AddVertex, AddRay,
+    /// and AddLine before calling SimplifyConstraints).
+    /// Assumes Constraints (and the frame fields) to be non-null.
+    /// </summary>
+    /// <param name="line"></param>
+    void AddLine(FrameElement/*!*/ line) {
+      Contract.Requires(line != null);
+      Contract.Requires(this.FrameLines != null);
+      // Note:  The code for AddLine is identical to that of AddRay, except the AddLine
+      // does not introduce the constraint 0 <= lambda.  (One could imagine sharing the
+      // code between AddRay and AddLine.)
+#if DEBUG_PRINT
+      Console.WriteLine("DEBUG: AddLine called on {0}", line);
+      Console.WriteLine("  Initial constraints:");
+      foreach (LinearConstraint cc in Constraints) {
+        Console.WriteLine("    {0}", cc);
+      }
+#endif
+
+      FrameLines.Add(line.Clone());
+#if FIXED_DESERIALIZER      
+      Contract.Assert(Contract.ForAll(line.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
+#endif
+
+      // We use a new temporary dimension.
+      IVariable/*!*/ lambda = new LambdaDimension();
+
+      // We change the constraints A*X <= B into
+      //     A*X - (A*line)*lambda <= B.
+      // That means that each row k in A (which corresponds to one LinearConstraint
+      // in Constraints) is changed by subtracting
+      //     (A*line)[k] * lambda
+      // from row k.
+      // Note:
+      //     (A*line)[k]
+      //  =      { A*line is a row vector whose every row i is the dot-product of
+      //           row i of A with the column vector "line" }
+      //     A[k]*line
+      foreach (LinearConstraint/*!*/ cc in cce.NonNull(Constraints)) {
+        Contract.Assert(cc != null);
+        Rational d = cc.EvaluateLhs(line);
+        cc.SetCoefficient(lambda, -d);
+      }
+
+#if DEBUG_PRINT
+      Console.WriteLine("  Constraints after addition:");
+      foreach (LinearConstraint cc in Constraints) {
+        Console.WriteLine("    {0}", cc);
+      }
+#endif
+
+      // Finally, project out the dummy dimension.
+      Constraints = Project(lambda, Constraints);
+
+#if DEBUG_PRINT
+      Console.WriteLine("  Resulting constraints:");
+      foreach (LinearConstraint cc in Constraints) {
+        Console.WriteLine("    {0}", cc);
+      }
+#endif
+    }
+
+    ISet /*IVariable!*//*!*/ GetDefinedDimensions() {
+      Contract.Ensures(Contract.Result<ISet>() != null);
+      HashSet /*IVariable!*//*!*/ dims = new HashSet /*IVariable!*/ ();
+      foreach (ArrayList p in new ArrayList[] { FrameVertices, FrameRays, FrameLines }) {
+        if (p != null) {
+          foreach (FrameElement/*!*/ element in p) {
+            Contract.Assert(element != null);
+            foreach (IVariable/*!*/ dim in element.GetDefinedDimensions()) {
+              Contract.Assert(dim != null);
+              dims.Add(dim);
+            }
+          }
+        }
+      }
+      return dims;
+    }
+
+    // --------------------------------------------------------------------------------------------------------
+    // ------------------ Simplification routines -------------------------------------------------------------
+    // --------------------------------------------------------------------------------------------------------
+
+    /// <summary>
+    /// Uses the Constraints to simplify the frame.  See section 3.4.4 of Cousot and Halbwachs.
+    /// </summary>
+    void SimplifyFrame() {
+      Contract.Requires(this.Constraints != null);
+      SimplificationStatus[]/*!*/ status;
+
+      SimplifyFrameElements(cce.NonNull(FrameVertices), true, Constraints, out status);
+      RemoveIrrelevantFrameElements(FrameVertices, status, null);
+
+      SimplifyFrameElements(cce.NonNull(FrameRays), false, Constraints, out status);
+      RemoveIrrelevantFrameElements(FrameRays, status, FrameLines);
+    }
+
+    enum SimplificationStatus {
+      Irrelevant,
+      Relevant,
+      More
+    };
+
+    /// <summary>
+    /// For each i, sets status[i] to:
+    ///  <ul>
+    ///  <li>Irrelevant if ff[i] is irrelevant</li>
+    ///  <li>Relevant if ff[i] is irrelevant</li>
+    ///  <li>More if vertices is true and ray ff[i] can be replaced by a line ff[i]</li>
+    ///  </ul>
+    /// </summary>
+    /// <param name="ff"></param>
+    /// <param name="vertices">true if "ff" contains vertices; false if "ff" contains rays</param>
+    /// <param name="constraints"></param>
+    /// <param name="status"></param>
+    static void SimplifyFrameElements(ArrayList/*!*/ /*FrameElement*/ ff, bool vertices, ArrayList/*!*/ /*LinearConstraint*/ constraints, out SimplificationStatus[]/*!*/ status) {
+      Contract.Requires(ff != null);
+      Contract.Requires(constraints != null);
+      Contract.Ensures(Contract.ValueAtReturn(out status) != null);
+      status = new SimplificationStatus[ff.Count];
+      bool[,] sat = new bool[ff.Count, constraints.Count];
+      for (int i = 0; i < ff.Count; i++) {
+        FrameElement f = (FrameElement/*!*/)cce.NonNull(ff[i]);
+        int cnt = 0;
+        for (int c = 0; c < constraints.Count; c++) {
+          LinearConstraint lc = (LinearConstraint/*!*/)cce.NonNull(constraints[c]);
+          bool s = lc.IsSaturatedBy(f, vertices);
+          if (s) {
+            sat[i, c] = true;
+            cnt++;
+          }
+        }
+        if (!vertices && cnt == constraints.Count) {
+          status[i] = SimplificationStatus.More;
+        } else {
+          status[i] = SimplificationStatus.Relevant;
+        }
+      }
+
+      CheckPairSimplifications(sat, status);
+    }
+
+    /// <summary>
+    /// Requires sat.GetLength(0) == status.Length.
+    /// </summary>
+    /// <param name="sat"></param>
+    /// <param name="status"></param>
+    static void CheckPairSimplifications(bool[,]/*!*/ sat, SimplificationStatus[]/*!*/ status) {
+      Contract.Requires(status != null);
+      Contract.Requires(sat != null);
+      Contract.Requires(sat.GetLength(0) == status.Length);
+      int M = sat.GetLength(0);
+      int N = sat.GetLength(1);
+
+      for (int i = 0; i < M - 1; i++) {
+        if (status[i] != SimplificationStatus.Relevant) {
+          continue;
+        }
+        for (int j = i + 1; j < M; j++) {
+          if (status[j] != SimplificationStatus.Relevant) {
+            continue;
+          }
+          // check (sat[i,*] <= sat[j,*]) and (sat[i,*] >= sat[j,*])
+          int cmp = 0;  // -1: (sat[i,*] <= sat[j,*]),  0: equal,  1: (sat[i,*] >= sat[j,*])
+          for (int c = 0; c < N; c++) {
+            if (cmp < 0) {
+              if (sat[i, c] && !sat[j, c]) {
+                // incomparable
+                goto NEXT_PAIR;
+              }
+            } else if (0 < cmp) {
+              if (!sat[i, c] && sat[j, c]) {
+                // incomparable
+                goto NEXT_PAIR;
+              }
+            } else if (sat[i, c] != sat[j, c]) {
+              if (!sat[i, c]) {
+                cmp = -1;
+              } else {
+                cmp = 1;
+              }
+            }
+          }
+          if (cmp <= 0) {
+            // sat[i,*] <= sat[j,*] holds, so mark i as irrelevant
+            status[i] = SimplificationStatus.Irrelevant;
+            goto NEXT_OUTER;
+          } else {
+            // sat[i,*] >= sat[j,*] holds, so mark j as irrelevant
+            status[j] = SimplificationStatus.Irrelevant;
+          }
+        NEXT_PAIR: {
+          }
+        }
+      NEXT_OUTER: {
+        }
+      }
+    }
+
+    static void RemoveIrrelevantFrameElements(ArrayList/*!*/ /*FrameElement*/ ff, SimplificationStatus[]/*!*/ status,
+      /*maybe null*/ ArrayList /*FrameElement*/ lines) {
+      Contract.Requires(ff != null);
+      Contract.Requires(status != null);
+      Contract.Requires(ff.Count == status.Length);
+      for (int j = ff.Count - 1; 0 <= j; j--) {
+        switch (status[j]) {
+          case SimplificationStatus.Relevant:
+            break;
+          case SimplificationStatus.Irrelevant:
+#if DEBUG_PRINT
+            Console.WriteLine("Removing irrelevant {0}: {1}", lines == null ? "vertex" : "ray", ff[j]);
+#endif
+            ff.RemoveAt(j);
+            break;
+          case SimplificationStatus.More:
+            System.Diagnostics.Debug.Assert(lines != null);
+            FrameElement f = (FrameElement)ff[j];
+#if DEBUG_PRINT
+            Console.WriteLine("Changing ray into line: {0}", f);
+#endif
+            ff.RemoveAt(j);
+            Contract.Assert(lines != null);
+            lines.Add(f);
+            break;
+        }
+      }
+    }
+
+    /// <summary>
+    /// Uses the frame to simplify Constraints.  See section 3.3.1.2 of Cousot and Halbwachs.
+    /// 
+    /// Note:  This code does not necessarily eliminate all irrelevant equalities; Cousot and
+    /// Halbwachs only claim that the technique eliminates all irrelevant inequalities.
+    /// </summary>
+    void SimplifyConstraints() {
+      if (Constraints == null) {
+        return;
+      }
+      Contract.Assume(this.FrameVertices != null);
+      Contract.Assume(this.FrameRays != null);
+
+      SimplificationStatus[] status = new SimplificationStatus[Constraints.Count];
+      /*readonly*/
+      int feCount = FrameVertices.Count + FrameRays.Count;
+
+      // Create a table that keeps track of which constraints are satisfied by which vertices and rays
+      bool[,] sat = new bool[Constraints.Count, FrameVertices.Count + FrameRays.Count];
+      for (int i = 0; i < Constraints.Count; i++) {
+        status[i] = SimplificationStatus.Relevant;
+        LinearConstraint lc = (LinearConstraint/*!*/)cce.NonNull(Constraints[i]);
+        int cnt = 0;  // number of vertices and rays that saturate lc
+        for (int j = 0; j < FrameVertices.Count; j++) {
+          FrameElement vertex = (FrameElement/*!*/)cce.NonNull(FrameVertices[j]);
+          if (lc.IsSaturatedBy(vertex, true)) {
+            sat[i, j] = true;
+            cnt++;
+          }
+        }
+        if (cnt == 0) {
+          // no vertex saturates the constraint, so the constraint is irrelevant
+          status[i] = SimplificationStatus.Irrelevant;
+          continue;
+        }
+        for (int j = 0; j < FrameRays.Count; j++) {
+          FrameElement ray = (FrameElement/*!*/)cce.NonNull(FrameRays[j]);
+          if (lc.IsSaturatedBy(ray, false)) {
+            sat[i, FrameVertices.Count + j] = true;
+            cnt++;
+          }
+        }
+        if (cnt == feCount) {
+          status[i] = SimplificationStatus.More;
+        } else {
+          // Cousot and Halbwachs says that all equalities are found in the way we just tested.
+          // If I understand that right, then we should not get here if the constraint is an
+          // equality constraint.  The following assertion tests my understanding.  --KRML
+          System.Diagnostics.Debug.Assert(lc.Relation == LinearConstraint.ConstraintRelation.LE);
+        }
+      }
+
+      CheckPairSimplifications(sat, status);
+
+      // Finally, make the changes to the list of constraints
+      for (int i = Constraints.Count - 1; 0 <= i; i--) {
+        switch (status[i]) {
+          case SimplificationStatus.Relevant:
+            break;
+          case SimplificationStatus.Irrelevant:
+#if DEBUG_PRINT
+            Console.WriteLine("Removing irrelevant constraint: {0}", Constraints[i]);
+#endif
+            Constraints.RemoveAt(i);
+            break;
+          case SimplificationStatus.More:
+            LinearConstraint lc = (LinearConstraint/*!*/)cce.NonNull(Constraints[i]);
+            if (lc.Relation == LinearConstraint.ConstraintRelation.LE) {
+#if DEBUG_PRINT
+              Console.WriteLine("Converting the following constraint into an equality: {0}", lc);
+#endif
+              LinearConstraint lcEq = lc.ChangeRelation(LinearConstraint.ConstraintRelation.EQ);
+              Constraints[i] = lcEq;
+            }
+            break;
+        }
+      }
+
+      foreach (LinearConstraint/*!*/ lc in Constraints) {
+        Contract.Assert(lc != null);
+        lc.Normalize();
+      }
+    }
+
+    // --------------------------------------------------------------------------------------------------------
+    // ------------------ Cloning routines --------------------------------------------------------------------
+    // --------------------------------------------------------------------------------------------------------
+
+    public LinearConstraintSystem/*!*/ Clone() {
+      Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
+      LinearConstraintSystem z = new LinearConstraintSystem();
+      z.FrameDimensions = (IMutableSet /*IVariable!*//*!*/)cce.NonNull(this.FrameDimensions.Clone());
+      if (this.Constraints != null) {
+        z.Constraints = DeeperListCopy_LC(this.Constraints);
+        z.FrameVertices = DeeperListCopy_FE(cce.NonNull(this.FrameVertices));
+        z.FrameRays = DeeperListCopy_FE(cce.NonNull(this.FrameRays));
+        z.FrameLines = DeeperListCopy_FE(cce.NonNull(this.FrameLines));
+      } else {
+        System.Diagnostics.Debug.Assert(this.FrameVertices == null);
+        System.Diagnostics.Debug.Assert(this.FrameRays == null);
+        System.Diagnostics.Debug.Assert(this.FrameLines == null);
+        // the constructor should already have set these fields of z to null
+        System.Diagnostics.Debug.Assert(z.Constraints == null);
+        System.Diagnostics.Debug.Assert(z.FrameVertices == null);
+        System.Diagnostics.Debug.Assert(z.FrameRays == null);
+        System.Diagnostics.Debug.Assert(z.FrameLines == null);
+      }
+      return z;
+    }
+
+    /// <summary>
+    /// Clones "list" and the elements of "list".
+    /// </summary>
+    /// <param name="list"></param>
+    /// <returns></returns>
+    ArrayList /*LinearConstraint*/ DeeperListCopy_LC(ArrayList/*!*/ /*LinearConstraint*/ list) {
+      Contract.Requires(list != null);
+      ArrayList /*LinearConstraint*/ z = new ArrayList /*LinearConstraint*/ (list.Count);
+      foreach (LinearConstraint/*!*/ lc in list) {
+        Contract.Assert(lc != null);
+        z.Add(lc.Clone());
+      }
+      System.Diagnostics.Debug.Assert(z.Count == list.Count);
+      return z;
+    }
+
+    /// <summary>
+    /// Clones "list" and the elements of "list".
+    /// </summary>
+    /// <param name="list"></param>
+    /// <returns></returns>
+    ArrayList /*FrameElement*/ DeeperListCopy_FE(ArrayList/*!*/ /*FrameElement*/ list) {
+      Contract.Requires(list != null);
+      ArrayList /*FrameElement*/ z = new ArrayList /*FrameElement*/ (list.Count);
+      foreach (FrameElement/*!*/ fe in list) {
+        Contract.Assert(fe != null);
+        z.Add(fe.Clone());
+      }
+      System.Diagnostics.Debug.Assert(z.Count == list.Count);
+      return z;
+    }
+
+    // --------------------------------------------------------------------------------------------------------
+    // ------------------ Debugging and unit test routines ----------------------------------------------------
+    // --------------------------------------------------------------------------------------------------------
+
+    public void Dump() {
+      Console.WriteLine("  Constraints:");
+      if (Constraints == null) {
+        Console.WriteLine("    <bottom>");
+      } else {
+        foreach (LinearConstraint cc in Constraints) {
+          Console.WriteLine("    {0}", cc);
+        }
+      }
+
+      Console.WriteLine("  FrameDimensions: {0}", FrameDimensions);
+
+      Console.WriteLine("  FrameVerticies:");
+      if (FrameVertices == null) {
+        Console.WriteLine("    <null>");
+      } else {
+        foreach (FrameElement fe in FrameVertices) {
+          Console.WriteLine("    {0}", fe);
+        }
+      }
+
+      Console.WriteLine("  FrameRays:");
+      if (FrameRays == null) {
+        Console.WriteLine("    <null>");
+      } else {
+        foreach (FrameElement fe in FrameRays) {
+          Console.WriteLine("    {0}", fe);
+        }
+      }
+
+      Console.WriteLine("  FrameLines:");
+      if (FrameLines == null) {
+        Console.WriteLine("    <null>");
+      } else {
+        foreach (FrameElement fe in FrameLines) {
+          Console.WriteLine("    {0}", fe);
+        }
+      }
+    }
+
+    class TestVariable : IVariable {
+      readonly string/*!*/ name;
+      [ContractInvariantMethod]
+      void ObjectInvariant() {
+        Contract.Invariant(name != null);
+      }
+
+
+      public string/*!*/ Name {
+        get {
+          Contract.Ensures(Contract.Result<string>() != null);
+
+          return name;
+        }
+      }
+
+      public TestVariable(string/*!*/ name) {
+        Contract.Requires(name != null);
+        this.name = name;
+      }
+      [Pure]
+      public object DoVisit(ExprVisitor/*!*/ visitor) {
+        //Contract.Requires(visitor != null);
+        return visitor.VisitVariable(this);
+      }
+    }
+
+    public static void RunValidationA() {
+      IVariable/*!*/ dim1 = new TestVariable("X");
+      IVariable/*!*/ dim2 = new TestVariable("Y");
+      IVariable/*!*/ dim3 = new TestVariable("Z");
+      Contract.Assert(dim1 != null);
+      Contract.Assert(dim2 != null);
+      Contract.Assert(dim3 != null);
+
+      FrameElement s1 = new FrameElement();
+      s1.AddCoordinate(dim1, Rational.ONE);
+      s1.AddCoordinate(dim2, Rational.MINUS_ONE);
+      s1.AddCoordinate(dim3, Rational.ZERO);
+      FrameElement s2 = new FrameElement();
+      s2.AddCoordinate(dim1, Rational.MINUS_ONE);
+      s2.AddCoordinate(dim2, Rational.ONE);
+      s2.AddCoordinate(dim3, Rational.ZERO);
+      FrameElement r1 = new FrameElement();
+      r1.AddCoordinate(dim1, Rational.ZERO);
+      r1.AddCoordinate(dim2, Rational.ZERO);
+      r1.AddCoordinate(dim3, Rational.ONE);
+      FrameElement d1 = new FrameElement();
+      d1.AddCoordinate(dim1, Rational.ONE);
+      d1.AddCoordinate(dim2, Rational.ONE);
+      d1.AddCoordinate(dim3, Rational.ZERO);
+
+      // create lcs from frame -- cf. Cousot/Halbwachs 1978, section 3.3.1.1
+      LinearConstraintSystem lcs = new LinearConstraintSystem(s1);
+      lcs.Dump();
+
+      lcs.AddVertex(s2);
+      lcs.Dump();
+
+      lcs.AddRay(r1);
+      lcs.Dump();
+
+      lcs.AddLine(d1);
+      lcs.Dump();
+
+      lcs.SimplifyConstraints();
+      lcs.Dump();
+
+#if LATER
+      lcs.GenerateFrameFromConstraints(); // should give us back the original frame...
+#endif
+      Console.WriteLine("IsSubset? {0}", lcs.IsSubset(lcs.Clone()));
+      lcs.Dump();
+    }
+
+    /// <summary>
+    /// Tests the example in section 3.4.3 of Cousot and Halbwachs.
+    /// </summary>
+    public static void RunValidationB() {
+      IVariable/*!*/ X = new TestVariable("X");
+      IVariable/*!*/ Y = new TestVariable("Y");
+      IVariable/*!*/ Z = new TestVariable("Z");
+      Contract.Assert(X != null);
+      Contract.Assert(Y != null);
+      Contract.Assert(Z != null);
+      ArrayList /*LinearConstraint*/ cs = new ArrayList /*LinearConstraint*/ ();
+
+      LinearConstraint c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+      c.SetCoefficient(X, Rational.MINUS_ONE);
+      c.SetCoefficient(Y, Rational.ONE);
+      c.SetCoefficient(Z, Rational.MINUS_ONE);
+      c.rhs = Rational.ZERO;
+      cs.Add(c);
+
+      c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+      c.SetCoefficient(X, Rational.MINUS_ONE);
+      c.rhs = Rational.MINUS_ONE;
+      cs.Add(c);
+
+      c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+      c.SetCoefficient(X, Rational.MINUS_ONE);
+      c.SetCoefficient(Y, Rational.MINUS_ONE);
+      c.SetCoefficient(Z, Rational.ONE);
+      c.rhs = Rational.ZERO;
+      cs.Add(c);
+
+      c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+      c.SetCoefficient(Y, Rational.MINUS_ONE);
+      c.SetCoefficient(Z, Rational.ONE);
+      c.rhs = Rational.FromInt(3);
+      cs.Add(c);
+
+      LinearConstraintSystem lcs = new LinearConstraintSystem(cs);
+      Console.WriteLine("==================== The final linear constraint system ====================");
+      lcs.Dump();
+    }
+
+    public static void RunValidationC() {
+      // Run the example in section 3.4.3 of Cousot and Halbwachs backwards, that is, from
+      // from to constraints.
+      IVariable/*!*/ dim1 = new TestVariable("X");
+      IVariable/*!*/ dim2 = new TestVariable("Y");
+      IVariable/*!*/ dim3 = new TestVariable("Z");
+      Contract.Assert(dim1 != null);
+      Contract.Assert(dim2 != null);
+      Contract.Assert(dim3 != null);
+
+      FrameElement s0 = new FrameElement();
+      s0.AddCoordinate(dim1, Rational.ONE);
+      s0.AddCoordinate(dim2, Rational.FromInts(1, 2));
+      s0.AddCoordinate(dim3, Rational.FromInts(-1, 2));
+
+      FrameElement s1 = new FrameElement();
+      s1.AddCoordinate(dim1, Rational.ONE);
+      s1.AddCoordinate(dim2, Rational.FromInts(-1, 2));
+      s1.AddCoordinate(dim3, Rational.FromInts(1, 2));
+
+      FrameElement s2 = new FrameElement();
+      s2.AddCoordinate(dim1, Rational.FromInt(3));
+      s2.AddCoordinate(dim2, Rational.FromInts(-3, 2));
+      s2.AddCoordinate(dim3, Rational.FromInts(3, 2));
+
+      FrameElement r0 = new FrameElement();
+      r0.AddCoordinate(dim1, Rational.ONE);
+      r0.AddCoordinate(dim2, Rational.FromInts(1, 2));
+      r0.AddCoordinate(dim3, Rational.FromInts(-1, 2));
+
+      FrameElement r1 = new FrameElement();
+      r1.AddCoordinate(dim1, Rational.ONE);
+      r1.AddCoordinate(dim2, Rational.ZERO);
+      r1.AddCoordinate(dim3, Rational.ZERO);
+
+      FrameElement d0 = new FrameElement();
+      d0.AddCoordinate(dim1, Rational.ZERO);
+      d0.AddCoordinate(dim2, Rational.ONE);
+      d0.AddCoordinate(dim3, Rational.ONE);
+
+      LinearConstraintSystem lcs = new LinearConstraintSystem(s0);
+      lcs.Dump();
+
+      lcs.AddVertex(s1);
+      lcs.Dump();
+
+      lcs.AddVertex(s2);
+      lcs.Dump();
+
+      lcs.AddRay(r0);
+      lcs.Dump();
+
+      lcs.AddRay(r1);
+      lcs.Dump();
+
+      lcs.AddLine(d0);
+      lcs.Dump();
+
+      lcs.SimplifyConstraints();
+      lcs.Dump();
+
+#if LATER
+      lcs.GenerateFrameFromConstraints(); // should give us back the original frame...
+#endif
+    }
+  }
 }
 \ No newline at end of file
diff --git a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs
index 06c0f483..6c914a54 100644
--- a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs
+++ b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs
@@ -1,762 +1,762 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework {
-  using System;
-  using System.Collections;
-  using System.Collections.Generic;
-  using System.Diagnostics;
-  using System.Diagnostics.Contracts;
-  using Microsoft.Basetypes;
-
-  using ISet = Microsoft.Boogie.GSet<object>;
-  using HashSet = Microsoft.Boogie.GSet<object>;
-
-  /// <summary>
-  /// Represents an invariant over linear variable constraints, represented by a polyhedron.
-  /// </summary>
-  public class PolyhedraLattice : Lattice {
-    private static readonly Logger/*!*/ log = new Logger("Polyhedra");
-
-    private class PolyhedraLatticeElement : Element {
-
-      public LinearConstraintSystem/*!*/ lcs;
-      [ContractInvariantMethod]
-      void ObjectInvariant() {
-        Contract.Invariant(lcs != null);
-      }
-
-
-      /// <summary>
-      /// Creates a top or bottom elements, according to parameter "top".
-      /// </summary>
-      public PolyhedraLatticeElement(bool top) {
-        if (top) {
-          lcs = new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ());
-        } else {
-          lcs = new LinearConstraintSystem();
-        }
-      }
-
-      [Pure]
-      public override string/*!*/ ToString() {
-        Contract.Ensures(Contract.Result<string>() != null);
-        return lcs.ToString();
-      }
-
-      public override void Dump(string/*!*/ msg) {
-        //Contract.Requires(msg != null);
-        System.Console.WriteLine("PolyhedraLatticeElement.Dump({0}):", msg);
-        lcs.Dump();
-      }
-
-      [Pure]
-      public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-        Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
-        return lcs.FreeVariables();
-      }
-
-      public PolyhedraLatticeElement(LinearConstraintSystem/*!*/ lcs) {
-        Contract.Requires(lcs != null);
-        this.lcs = lcs;
-      }
-
-      public override Element/*!*/ Clone() {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new PolyhedraLatticeElement(cce.NonNull(lcs.Clone()));
-      }
-
-    } // class
-
-    readonly ILinearExprFactory/*!*/ factory;
-    readonly IPropExprFactory/*!*/ propFactory;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(log != null);
-      Contract.Invariant(factory != null);
-      Contract.Invariant(propFactory != null);
-    }
-
-
-    public PolyhedraLattice(ILinearExprFactory/*!*/ linearFactory, IPropExprFactory/*!*/ propFactory)
-      : base(linearFactory) {
-      Contract.Requires(propFactory != null);
-      Contract.Requires(linearFactory != null);
-      log.Enabled = Lattice.LogSwitch;
-      this.factory = linearFactory;
-      this.propFactory = propFactory;
-      // base(linearFactory);
-    }
-
-    public override Element/*!*/ Top {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-        return new PolyhedraLatticeElement(true);
-      }
-    }
-
-    public override Element/*!*/ Bottom {
-      get {
-        Contract.Ensures(Contract.Result<Element>() != null);
-
-        return new PolyhedraLatticeElement(false);
-      }
-    }
-
-    public override bool IsBottom(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
-      return e.lcs.IsBottom();
-    }
-
-    public override bool IsTop(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
-      return e.lcs.IsTop();
-    }
-
-
-    /// <summary>
-    /// Returns true iff a is a subset of this.
-    /// </summary>
-    /// <param name="a"></param>
-    /// <returns></returns>
-    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second)  // this <= that
-    {
-      //Contract.Requires(first != null);
-      //Contract.Requires(second != null);
-      PolyhedraLatticeElement a = (PolyhedraLatticeElement)first;
-      PolyhedraLatticeElement b = (PolyhedraLatticeElement)second;
-      return b.lcs.IsSubset(a.lcs);
-    }
-
-
-    public override string/*!*/ ToString(Element/*!*/ e) {
-      //Contract.Requires(e != null);
-      Contract.Ensures(Contract.Result<string>() != null);
-      return ((PolyhedraLatticeElement)e).lcs.ToString();
-    }
-
-    public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
-      //Contract.Requires(element != null);
-      Contract.Ensures(Contract.Result<IExpr>() != null);
-      PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
-      return e.lcs.ConvertToExpression(factory);
-    }
-
-
-
-    public override Lattice.Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
-      log.DbgMsg("Joining ...");
-      log.DbgMsgIndent();
-      PolyhedraLatticeElement aa = (PolyhedraLatticeElement)first;
-      PolyhedraLatticeElement bb = (PolyhedraLatticeElement)second;
-      PolyhedraLatticeElement result = new PolyhedraLatticeElement(aa.lcs.Join(bb.lcs));
-      log.DbgMsg(string.Format("{0} |_| {1} --> {2}", this.ToString(first), this.ToString(second), this.ToString(result)));
-      log.DbgMsgUnindent();
-      return result;
-    }
-
-
-    public override Lattice.Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
-      PolyhedraLatticeElement aa = (PolyhedraLatticeElement)first;
-      PolyhedraLatticeElement bb = (PolyhedraLatticeElement)second;
-      return new PolyhedraLatticeElement(aa.lcs.Meet(bb.lcs));
-    }
-
-
-    public override Lattice.Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
-      //Contract.Requires(second != null);
-      //Contract.Requires(first != null);
-      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
-      log.DbgMsg("Widening ...");
-      log.DbgMsgIndent();
-      PolyhedraLatticeElement aa = (PolyhedraLatticeElement)first;
-      PolyhedraLatticeElement bb = (PolyhedraLatticeElement)second;
-
-      LinearConstraintSystem lcs = aa.lcs.Widen(bb.lcs);
-      PolyhedraLatticeElement result = new PolyhedraLatticeElement(lcs);
-      log.DbgMsg(string.Format("{0} |_| {1} --> {2}", this.ToString(first), this.ToString(second), this.ToString(result)));
-      log.DbgMsgUnindent();
-      return result;
-    }
-
-
-    public override Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable) {
-      //Contract.Requires(variable != null);
-      //Contract.Requires(e != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      log.DbgMsg(string.Format("Eliminating {0} ...", variable));
-
-      PolyhedraLatticeElement ple = (PolyhedraLatticeElement)e;
-      if (ple.lcs.IsBottom()) {
-        return ple;
-      }
-      return new PolyhedraLatticeElement(ple.lcs.Project(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);
-      log.DbgMsg(string.Format("Renaming {0} to {1} in {2} ...", oldName, newName, this.ToString(e)));
-
-      PolyhedraLatticeElement ple = (PolyhedraLatticeElement)e;
-      if (ple.lcs.IsBottom()) {
-        return ple;
-      }
-      return new PolyhedraLatticeElement(ple.lcs.Rename(oldName, newName));
-    }
-
-    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
-      //Contract.Requires(args != null);
-      //Contract.Requires(f != null);
-      return f is IntSymbol ||
-          f.Equals(Int.Add) ||
-          f.Equals(Int.Sub) ||
-          f.Equals(Int.Negate) ||
-          f.Equals(Int.Mul) ||
-          f.Equals(Int.Eq) ||
-          f.Equals(Int.Neq) ||
-          f.Equals(Prop.Not) ||
-          f.Equals(Int.AtMost) ||
-          f.Equals(Int.Less) ||
-          f.Equals(Int.Greater) ||
-          f.Equals(Int.AtLeast);
-    }
-
-    public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
-      //Contract.Requires(var2 != null);
-      //Contract.Requires(var1 != null);
-      //Contract.Requires(e != null);
-      PolyhedraLatticeElement/*!*/ ple = (PolyhedraLatticeElement)cce.NonNull(e);
-      Contract.Assume(ple.lcs.Constraints != null);
-      ArrayList /*LinearConstraint!*//*!*/ clist = (ArrayList /*LinearConstraint!*/)cce.NonNull(ple.lcs.Constraints.Clone());
-      LinearConstraint/*!*/ lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
-      Contract.Assert(lc != null);
-      lc.SetCoefficient(var1, Rational.ONE);
-      lc.SetCoefficient(var2, Rational.MINUS_ONE);
-      clist.Add(lc);
-      LinearConstraintSystem newLcs = new LinearConstraintSystem(clist);
-      if (newLcs.IsBottom()) {
-        return Answer.Yes;
-      } else {
-        return Answer.Maybe;
-      }
-    }
-
-    public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
-      //Contract.Requires(pred != null);
-      //Contract.Requires(e != null);
-      PolyhedraLatticeElement/*!*/ ple = (PolyhedraLatticeElement)Constrain(e, pred);
-      Contract.Assert(ple != null);
-      if (ple.lcs.IsBottom()) {
-        return Answer.No;
-      }
-
-      // Note, "pred" may contain expressions that are not understood by the propFactory (in
-      // particular, this may happen because--currently, and perhaps is a design we'll want
-      // to change in the future--propFactory deals with BoogiePL expressions whereas "pred"
-      // may also refer to Equivalences.UninterpFun expressions).  Thus, we cannot just
-      // call propFactory.Not(pred) to get the negation of "pred".
-      pred = new PolyhedraLatticeNegation(pred);
-      ple = (PolyhedraLatticeElement)Constrain(e, pred);
-      if (ple.lcs.IsBottom()) {
-        return Answer.Yes;
-      } else {
-        return Answer.Maybe;
-      }
-    }
-
-    class PolyhedraLatticeNegation : IFunApp {
-      IExpr/*!*/ arg;
-      [ContractInvariantMethod]
-      void ObjectInvariant() {
-        Contract.Invariant(arg != null);
-      }
-
-
-      public PolyhedraLatticeNegation(IExpr/*!*/ arg) {
-        Contract.Requires(arg != null);
-        this.arg = arg;
-        // base();
-      }
-
-      [Pure]
-      public object DoVisit(ExprVisitor/*!*/ visitor) {
-        //Contract.Requires(visitor != null);
-        return visitor.VisitFunApp(this);
-      }
-
-      public IFunctionSymbol/*!*/ FunctionSymbol {
-        get {
-          Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
-          return Prop.Not;
-        }
-      }
-
-      public IList/*<IExpr!>*//*!*/ Arguments {
-        get {
-          Contract.Ensures(Contract.Result<IList>() != null);
-
-          IExpr[] args = new IExpr[] { arg };
-          return ArrayList.ReadOnly(args);
-        }
-      }
-
-      public IFunApp/*!*/ CloneWithArguments(IList/*<IExpr!>*//*!*/ args) {
-        //Contract.Requires(args != null);
-        Contract.Ensures(Contract.Result<IFunApp>() != null);
-        Contract.Assert(args.Count == 1);
-        return new PolyhedraLatticeNegation((IExpr/*!*/)cce.NonNull(args[0]));
-      }
-    }
-
-    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);
-      // BUGBUG: TODO: this method can be implemented in a more precise way
-      return null;
-    }
-
-
-    public override Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr) {
-      //Contract.Requires(expr != null);
-      //Contract.Requires(e != null);
-      Contract.Ensures(Contract.Result<Element>() != null);
-      log.DbgMsg(string.Format("Constraining with {0} into {1} ...", expr, this.ToString(e)));
-
-      PolyhedraLatticeElement ple = (PolyhedraLatticeElement)e;
-      if (ple.lcs.IsBottom()) {
-        return ple;
-      }
-      LinearCondition le = LinearExpressionBuilder.AsCondition(expr);
-      if (le != null) {
-        // update the polyhedron according to the linear expression
-        Contract.Assume(ple.lcs.Constraints != null);
-        ArrayList /*LinearConstraint*/ clist = (ArrayList/*!*/ /*LinearConstraint*/)cce.NonNull(ple.lcs.Constraints.Clone());
-        le.AddToConstraintSystem(clist);
-        LinearConstraintSystem newLcs = new LinearConstraintSystem(clist);
-
-        return new PolyhedraLatticeElement(newLcs);
-      }
-      return ple;
-    }
-
-  } // class
-
-
-  /// <summary>
-  /// A LinearCondition follows this grammar:
-  ///     LinearCondition ::=  unsatisfiable
-  ///                       |  LinearConstraint
-  ///                       |  ! LinearConstraint
-  /// Note that negations are distributed to the leaves.
-  /// </summary>
-  /// 
-  [ContractClass(typeof(LinearConditionContracts))]
-  abstract class LinearCondition {
-    /// <summary>
-    /// Adds constraints to the list "clist".  If "this"
-    /// entails some disjunctive constraints, they may not be added.
-    /// </summary>
-    /// <param name="clist"></param>
-    public abstract void AddToConstraintSystem(ArrayList/*!*/ /*LinearConstraint*/ clist);
-  }
-  [ContractClassFor(typeof(LinearCondition))]
-  abstract class LinearConditionContracts : LinearCondition {
-    public override void AddToConstraintSystem(ArrayList clist) {
-      Contract.Requires(clist != null);
-      throw new NotImplementedException();
-    }
-  }
-
-  class LCBottom : LinearCondition {
-    public override void AddToConstraintSystem(ArrayList/*!*/ /*LinearConstraint*/ clist) {
-      //Contract.Requires(clist != null);
-      // make an unsatisfiable constraint
-      LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
-      lc.rhs = Rational.FromInt(1);
-      clist.Add(lc);
-    }
-  }
-
-  class LinearConditionLiteral : LinearCondition {
-    public readonly bool positive;
-    public readonly LinearConstraint/*!*/ constraint;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(constraint != null);
-    }
-
-    /// <summary>
-    /// Precondition:  positive || constraint.Relation == LinearConstraint.ConstraintRelation.EQ
-    /// </summary>
-    /// <param name="positive"></param>
-    /// <param name="constraint"></param>
-    public LinearConditionLiteral(bool positive, LinearConstraint/*!*/ constraint) {
-      Contract.Requires(constraint != null);
-      Contract.Requires(positive || constraint.Relation == LinearConstraint.ConstraintRelation.EQ);
-      this.positive = positive;
-      this.constraint = constraint;
-    }
-    public override void AddToConstraintSystem(ArrayList/*!*/ /*LinearConstraint*/ clist) {
-      //Contract.Requires(clist != null);
-      if (positive) {
-        clist.Add(constraint);
-      } else {
-        Contract.Assert(constraint.Relation == LinearConstraint.ConstraintRelation.EQ);
-        // the constraint is disjunctive, so just ignore it
-      }
-    }
-  }
-
-  class LinearExpressionBuilder {
-    /// <summary>
-    /// Builds a linear condition from "e", if possible; returns null if not possible.
-    /// </summary>
-    /// <param name="e"></param>
-    /// <returns></returns>
-    public static /*maybe null*/ LinearCondition AsCondition(IExpr e) /* throws ArithmeticException */
-    {
-      return GetCond(e, true);
-    }
-
-    static /*maybe null*/ LinearCondition GetCond(IExpr e, bool positive) /* throws ArithmeticException */
-    {
-      IFunApp funapp = e as IFunApp;
-      if (funapp == null) {
-        return null;
-      }
-      IFunctionSymbol/*!*/ s = funapp.FunctionSymbol;
-      Contract.Assert(s != null);
-      if ((positive && s.Equals(Prop.False)) ||
-          (!positive && s.Equals(Prop.True))) {
-        return new LCBottom();
-      } else if (s.Equals(Prop.Not)) {
-        Contract.Assert(funapp.Arguments.Count == 1);
-        return GetCond((IExpr/*!*/)cce.NonNull(funapp.Arguments[0]), !positive);
-      } else if (funapp.Arguments.Count == 2) {
-        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(funapp.Arguments[0]);
-        IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(funapp.Arguments[1]);
-        LinearExpr le0 = AsExpr(arg0);
-        if (le0 == null) {
-          return null;
-        }
-        LinearExpr le1 = AsExpr(arg1);
-        if (le1 == null) {
-          return null;
-        }
-
-        LinearConstraint constraint = null;
-        bool sense = true;
-        if ((positive && s.Equals(Int.Less)) || (!positive && s.Equals(Int.AtLeast))) {
-          constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.LE, BigNum.ONE);
-        } else if ((positive && s.Equals(Int.AtMost)) || (!positive && s.Equals(Int.Greater))) {
-          constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.LE, BigNum.ZERO);
-        } else if ((positive && s.Equals(Int.AtLeast)) || (!positive && s.Equals(Int.Less))) {
-          constraint = MakeConstraint(le1, le0, LinearConstraint.ConstraintRelation.LE, BigNum.ZERO);
-        } else if ((positive && s.Equals(Int.Greater)) || (!positive && s.Equals(Int.AtMost))) {
-          constraint = MakeConstraint(le1, le0, LinearConstraint.ConstraintRelation.LE, BigNum.ONE);
-        } else if (s.Equals(Int.Eq)) {
-          constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.EQ, BigNum.ZERO);
-          sense = positive;
-        } else if (s.Equals(Int.Neq)) {
-          constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.EQ, BigNum.ZERO);
-          sense = !positive;
-        }
-        if (constraint != null) {
-          if (constraint.coefficients.Count != 0) {
-            return new LinearConditionLiteral(sense, constraint);
-          } else if (constraint.IsConstantSatisfiable()) {
-            return null;
-          } else {
-            return new LCBottom();
-          }
-        }
-      }
-      return null;
-    }
-
-    public static LinearConstraint MakeConstraint(LinearExpr/*!*/ le0, LinearExpr/*!*/ le1,
-        LinearConstraint.ConstraintRelation rel, BigNum constantOffset) /* throws ArithmeticException */
-    {
-      Contract.Requires(le0 != null);
-      Contract.Requires(le1 != null);
-      le1.Negate();
-      le0.Add(le1);
-      le0.AddConstant(constantOffset);
-      return le0.ToConstraint(rel);
-    }
-
-    /// <summary>
-    /// Builds a linear expression from "e", if possible; returns null if not possible.
-    /// </summary>
-    /// <param name="e"></param>
-    /// <returns></returns>
-    public static /*maybe null*/ LinearExpr AsExpr(IExpr/*!*/ e) /* throws ArithmeticException */
-    {
-      Contract.Requires(e != null);
-      if (e is IVariable) {
-        // Note, without a type for the variable, we don't know if the identifier is intended to hold an integer value.
-        // However, it seems that no harm can be caused by here treating the identifier as if it held an
-        // integer value, because other parts of this method will reject the expression as a linear expression
-        // if non-numeric operations other than equality are applied to the identifier.
-        return new LinearExpr((IVariable)e);
-      } else if (e is IFunApp) {
-        IFunApp/*!*/ funapp = (IFunApp)e;
-        Contract.Assert(funapp != null);
-        IFunctionSymbol/*!*/ s = funapp.FunctionSymbol;
-        Contract.Assert(s != null);
-
-        if (s is IntSymbol) {
-          return new LinearExpr(((IntSymbol)s).Value);
-        } else if (s.Equals(Int.Negate)) {
-          Contract.Assert(funapp.Arguments.Count == 1);
-          LinearExpr le = AsExpr((IExpr/*!*/)cce.NonNull(funapp.Arguments[0]));
-          if (le != null) {
-            le.Negate();
-            return le;
-          }
-        } else if (s.Equals(Int.Add) || s.Equals(Int.Sub) || s.Equals(Int.Mul)) {
-          Contract.Assert(funapp.Arguments.Count == 2);
-          IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(funapp.Arguments[0]);
-          IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(funapp.Arguments[1]);
-          LinearExpr le0 = AsExpr(arg0);
-          if (le0 == null) {
-            return null;
-          }
-          LinearExpr le1 = AsExpr(arg1);
-          if (le1 == null) {
-            return null;
-          }
-
-          if (s.Equals(Int.Add)) {
-            le0.Add(le1);
-            return le0;
-          } else if (s.Equals(Int.Sub)) {
-            le1.Negate();
-            le0.Add(le1);
-            return le0;
-          } else if (s.Equals(Int.Mul)) {
-            BigNum x;
-            if (le0.AsConstant(out x)) {
-              le1.Multiply(x);
-              return le1;
-            } else if (le1.AsConstant(out x)) {
-              le0.Multiply(x);
-              return le0;
-            }
-          }
-        }
-      }
-      return null;
-    }
-  }
-
-  class LinearExpr {
-    BigNum constant;
-    Term terms;
-
-    class Term {
-      public BigNum coeff;  // non-0, if the node is used
-      public IVariable/*!*/ var;
-      public Term next;
-      [ContractInvariantMethod]
-      void ObjectInvariant() {
-        Contract.Invariant(var != null);
-      }
-
-      public Term(BigNum coeff, IVariable/*!*/ var) {
-        Contract.Requires(var != null);
-        this.coeff = coeff;
-        this.var = var;
-        // base();
-      }
-    }
-
-    public LinearExpr(BigNum x) {
-      constant = x;
-    }
-
-    public LinearExpr(IVariable/*!*/ var) {
-      Contract.Requires(var != null);
-      constant = BigNum.ZERO;
-      terms = new Term(BigNum.ONE, var);
-    }
-
-    public ISet /*IVariable!*/ GetDefinedDimensions() {
-      HashSet /*IVariable!*//*!*/ dims = new HashSet /*IVariable!*/ ();
-      for (Term current = terms; current != null; current = current.next) {
-        dims.Add(current.var);
-      }
-      return dims;
-    }
-
-    public BigNum TermCoefficient(/*MayBeNull*/ IVariable/*!*/ var) {
-      Contract.Requires(var != null);
-      BigNum z = BigNum.ZERO;
-      if (var == null) {
-        z = this.constant;
-      } else if (terms != null) {
-        Term current = terms;
-        while (current != null) {
-          if (current.var == var) {
-            break;
-          }
-          current = current.next;
-        }
-        if (current != null) {
-          z = current.coeff;
-        }
-      }
-      return z;
-    }
-
-    public bool AsConstant(out BigNum x) {
-      if (terms == null) {
-        x = constant;
-        return true;
-      } else {
-        x = BigNum.FromInt(-70022);  // to please complier
-        return false;
-      }
-    }
-
-    public void Negate() /* throws ArithmeticException */
-    {
-      checked {
-        constant = -constant;
-      }
-
-      for (Term t = terms; t != null; t = t.next) {
-        checked {
-          t.coeff = -t.coeff;
-        }
-      }
-    }
-
-    /// <summary>
-    /// Adds "x" to "this".
-    /// </summary>
-    /// <param name="x"></param>
-    public void AddConstant(BigNum x) /* throws ArithmeticException */
-    {
-      checked {
-        constant += x;
-      }
-    }
-
-    /// <summary>
-    /// Adds "le" to "this".  Afterwards, "le" should not be used, because it will have been destroyed.
-    /// </summary>
-    /// <param name="le"></param>
-    public void Add(LinearExpr/*!*/ le) /* throws ArithmeticException */
-        {
-      Contract.Requires(le != null);
-      Contract.Requires(le != this);
-      checked {
-        constant += le.constant;
-      }
-      le.constant = BigNum.FromInt(-70029);  // "le" should no longer be used; assign it a strange value so that misuse is perhaps more easily detected
-
-      // optimization:
-      if (le.terms == null) {
-        return;
-      } else if (terms == null) {
-        terms = le.terms;
-        le.terms = null;
-        return;
-      }
-
-      // merge the two term lists
-      // Use a nested loop, which is quadratic in time complexity, but we hope the lists will be small
-      Term newTerms = null;
-      while (le.terms != null) {
-        // take off next term from "le"
-        Term t = le.terms;
-        le.terms = t.next;
-        t.next = null;
-
-        for (Term u = terms; u != null; u = u.next) {
-          if (u.var == t.var) {
-            checked {
-              u.coeff += t.coeff;
-            }
-            goto NextOuter;
-          }
-        }
-        t.next = newTerms;
-        newTerms = t;
-
-      NextOuter:
-        ;
-      }
-
-      // finally, include all non-0 terms
-      while (terms != null) {
-        // take off next term from "this"
-        Term t = terms;
-        terms = t.next;
-
-        if (!t.coeff.IsZero) {
-          t.next = newTerms;
-          newTerms = t;
-        }
-      }
-      terms = newTerms;
-    }
-
-    public void Multiply(BigNum x) /* throws ArithmeticException */
-    {
-      if (x.IsZero) {
-        constant = BigNum.ZERO;
-        terms = null;
-      } else {
-        for (Term t = terms; t != null; t = t.next) {
-          checked {
-            t.coeff *= x;
-          }
-        }
-        checked {
-          constant *= x;
-        }
-      }
-    }
-
-    public bool IsInvertible(IVariable/*!*/ var) {
-      Contract.Requires(var != null);
-      for (Term t = terms; t != null; t = t.next) {
-        if (t.var == var) {
-          System.Diagnostics.Debug.Assert(!t.coeff.IsZero);
-          return true;
-        }
-      }
-      return false;
-    }
-
-    public LinearConstraint ToConstraint(LinearConstraint.ConstraintRelation rel) /* throws ArithmeticException */
-    {
-      LinearConstraint constraint = new LinearConstraint(rel);
-      for (Term t = terms; t != null; t = t.next) {
-        constraint.SetCoefficient(t.var, t.coeff.ToRational);
-      }
-      BigNum rhs = -constant;
-      constraint.rhs = rhs.ToRational;
-      return constraint;
-    }
-  }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.AbstractInterpretationFramework {
+  using System;
+  using System.Collections;
+  using System.Collections.Generic;
+  using System.Diagnostics;
+  using System.Diagnostics.Contracts;
+  using Microsoft.Basetypes;
+
+  using ISet = Microsoft.Boogie.GSet<object>;
+  using HashSet = Microsoft.Boogie.GSet<object>;
+
+  /// <summary>
+  /// Represents an invariant over linear variable constraints, represented by a polyhedron.
+  /// </summary>
+  public class PolyhedraLattice : Lattice {
+    private static readonly Logger/*!*/ log = new Logger("Polyhedra");
+
+    private class PolyhedraLatticeElement : Element {
+
+      public LinearConstraintSystem/*!*/ lcs;
+      [ContractInvariantMethod]
+      void ObjectInvariant() {
+        Contract.Invariant(lcs != null);
+      }
+
+
+      /// <summary>
+      /// Creates a top or bottom elements, according to parameter "top".
+      /// </summary>
+      public PolyhedraLatticeElement(bool top) {
+        if (top) {
+          lcs = new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ());
+        } else {
+          lcs = new LinearConstraintSystem();
+        }
+      }
+
+      [Pure]
+      public override string/*!*/ ToString() {
+        Contract.Ensures(Contract.Result<string>() != null);
+        return lcs.ToString();
+      }
+
+      public override void Dump(string/*!*/ msg) {
+        //Contract.Requires(msg != null);
+        System.Console.WriteLine("PolyhedraLatticeElement.Dump({0}):", msg);
+        lcs.Dump();
+      }
+
+      [Pure]
+      public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
+        return lcs.FreeVariables();
+      }
+
+      public PolyhedraLatticeElement(LinearConstraintSystem/*!*/ lcs) {
+        Contract.Requires(lcs != null);
+        this.lcs = lcs;
+      }
+
+      public override Element/*!*/ Clone() {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new PolyhedraLatticeElement(cce.NonNull(lcs.Clone()));
+      }
+
+    } // class
+
+    readonly ILinearExprFactory/*!*/ factory;
+    readonly IPropExprFactory/*!*/ propFactory;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(log != null);
+      Contract.Invariant(factory != null);
+      Contract.Invariant(propFactory != null);
+    }
+
+
+    public PolyhedraLattice(ILinearExprFactory/*!*/ linearFactory, IPropExprFactory/*!*/ propFactory)
+      : base(linearFactory) {
+      Contract.Requires(propFactory != null);
+      Contract.Requires(linearFactory != null);
+      log.Enabled = Lattice.LogSwitch;
+      this.factory = linearFactory;
+      this.propFactory = propFactory;
+      // base(linearFactory);
+    }
+
+    public override Element/*!*/ Top {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+        return new PolyhedraLatticeElement(true);
+      }
+    }
+
+    public override Element/*!*/ Bottom {
+      get {
+        Contract.Ensures(Contract.Result<Element>() != null);
+
+        return new PolyhedraLatticeElement(false);
+      }
+    }
+
+    public override bool IsBottom(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
+      return e.lcs.IsBottom();
+    }
+
+    public override bool IsTop(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
+      return e.lcs.IsTop();
+    }
+
+
+    /// <summary>
+    /// Returns true iff a is a subset of this.
+    /// </summary>
+    /// <param name="a"></param>
+    /// <returns></returns>
+    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second)  // this <= that
+    {
+      //Contract.Requires(first != null);
+      //Contract.Requires(second != null);
+      PolyhedraLatticeElement a = (PolyhedraLatticeElement)first;
+      PolyhedraLatticeElement b = (PolyhedraLatticeElement)second;
+      return b.lcs.IsSubset(a.lcs);
+    }
+
+
+    public override string/*!*/ ToString(Element/*!*/ e) {
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<string>() != null);
+      return ((PolyhedraLatticeElement)e).lcs.ToString();
+    }
+
+    public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
+      //Contract.Requires(element != null);
+      Contract.Ensures(Contract.Result<IExpr>() != null);
+      PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
+      return e.lcs.ConvertToExpression(factory);
+    }
+
+
+
+    public override Lattice.Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
+      log.DbgMsg("Joining ...");
+      log.DbgMsgIndent();
+      PolyhedraLatticeElement aa = (PolyhedraLatticeElement)first;
+      PolyhedraLatticeElement bb = (PolyhedraLatticeElement)second;
+      PolyhedraLatticeElement result = new PolyhedraLatticeElement(aa.lcs.Join(bb.lcs));
+      log.DbgMsg(string.Format("{0} |_| {1} --> {2}", this.ToString(first), this.ToString(second), this.ToString(result)));
+      log.DbgMsgUnindent();
+      return result;
+    }
+
+
+    public override Lattice.Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
+      PolyhedraLatticeElement aa = (PolyhedraLatticeElement)first;
+      PolyhedraLatticeElement bb = (PolyhedraLatticeElement)second;
+      return new PolyhedraLatticeElement(aa.lcs.Meet(bb.lcs));
+    }
+
+
+    public override Lattice.Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+      //Contract.Requires(second != null);
+      //Contract.Requires(first != null);
+      Contract.Ensures(Contract.Result<Lattice.Element>() != null);
+      log.DbgMsg("Widening ...");
+      log.DbgMsgIndent();
+      PolyhedraLatticeElement aa = (PolyhedraLatticeElement)first;
+      PolyhedraLatticeElement bb = (PolyhedraLatticeElement)second;
+
+      LinearConstraintSystem lcs = aa.lcs.Widen(bb.lcs);
+      PolyhedraLatticeElement result = new PolyhedraLatticeElement(lcs);
+      log.DbgMsg(string.Format("{0} |_| {1} --> {2}", this.ToString(first), this.ToString(second), this.ToString(result)));
+      log.DbgMsgUnindent();
+      return result;
+    }
+
+
+    public override Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable) {
+      //Contract.Requires(variable != null);
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      log.DbgMsg(string.Format("Eliminating {0} ...", variable));
+
+      PolyhedraLatticeElement ple = (PolyhedraLatticeElement)e;
+      if (ple.lcs.IsBottom()) {
+        return ple;
+      }
+      return new PolyhedraLatticeElement(ple.lcs.Project(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);
+      log.DbgMsg(string.Format("Renaming {0} to {1} in {2} ...", oldName, newName, this.ToString(e)));
+
+      PolyhedraLatticeElement ple = (PolyhedraLatticeElement)e;
+      if (ple.lcs.IsBottom()) {
+        return ple;
+      }
+      return new PolyhedraLatticeElement(ple.lcs.Rename(oldName, newName));
+    }
+
+    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
+      //Contract.Requires(args != null);
+      //Contract.Requires(f != null);
+      return f is IntSymbol ||
+          f.Equals(Int.Add) ||
+          f.Equals(Int.Sub) ||
+          f.Equals(Int.Negate) ||
+          f.Equals(Int.Mul) ||
+          f.Equals(Int.Eq) ||
+          f.Equals(Int.Neq) ||
+          f.Equals(Prop.Not) ||
+          f.Equals(Int.AtMost) ||
+          f.Equals(Int.Less) ||
+          f.Equals(Int.Greater) ||
+          f.Equals(Int.AtLeast);
+    }
+
+    public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
+      //Contract.Requires(var2 != null);
+      //Contract.Requires(var1 != null);
+      //Contract.Requires(e != null);
+      PolyhedraLatticeElement/*!*/ ple = (PolyhedraLatticeElement)cce.NonNull(e);
+      Contract.Assume(ple.lcs.Constraints != null);
+      ArrayList /*LinearConstraint!*//*!*/ clist = (ArrayList /*LinearConstraint!*/)cce.NonNull(ple.lcs.Constraints.Clone());
+      LinearConstraint/*!*/ lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
+      Contract.Assert(lc != null);
+      lc.SetCoefficient(var1, Rational.ONE);
+      lc.SetCoefficient(var2, Rational.MINUS_ONE);
+      clist.Add(lc);
+      LinearConstraintSystem newLcs = new LinearConstraintSystem(clist);
+      if (newLcs.IsBottom()) {
+        return Answer.Yes;
+      } else {
+        return Answer.Maybe;
+      }
+    }
+
+    public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
+      //Contract.Requires(pred != null);
+      //Contract.Requires(e != null);
+      PolyhedraLatticeElement/*!*/ ple = (PolyhedraLatticeElement)Constrain(e, pred);
+      Contract.Assert(ple != null);
+      if (ple.lcs.IsBottom()) {
+        return Answer.No;
+      }
+
+      // Note, "pred" may contain expressions that are not understood by the propFactory (in
+      // particular, this may happen because--currently, and perhaps is a design we'll want
+      // to change in the future--propFactory deals with BoogiePL expressions whereas "pred"
+      // may also refer to Equivalences.UninterpFun expressions).  Thus, we cannot just
+      // call propFactory.Not(pred) to get the negation of "pred".
+      pred = new PolyhedraLatticeNegation(pred);
+      ple = (PolyhedraLatticeElement)Constrain(e, pred);
+      if (ple.lcs.IsBottom()) {
+        return Answer.Yes;
+      } else {
+        return Answer.Maybe;
+      }
+    }
+
+    class PolyhedraLatticeNegation : IFunApp {
+      IExpr/*!*/ arg;
+      [ContractInvariantMethod]
+      void ObjectInvariant() {
+        Contract.Invariant(arg != null);
+      }
+
+
+      public PolyhedraLatticeNegation(IExpr/*!*/ arg) {
+        Contract.Requires(arg != null);
+        this.arg = arg;
+        // base();
+      }
+
+      [Pure]
+      public object DoVisit(ExprVisitor/*!*/ visitor) {
+        //Contract.Requires(visitor != null);
+        return visitor.VisitFunApp(this);
+      }
+
+      public IFunctionSymbol/*!*/ FunctionSymbol {
+        get {
+          Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+          return Prop.Not;
+        }
+      }
+
+      public IList/*<IExpr!>*//*!*/ Arguments {
+        get {
+          Contract.Ensures(Contract.Result<IList>() != null);
+
+          IExpr[] args = new IExpr[] { arg };
+          return ArrayList.ReadOnly(args);
+        }
+      }
+
+      public IFunApp/*!*/ CloneWithArguments(IList/*<IExpr!>*//*!*/ args) {
+        //Contract.Requires(args != null);
+        Contract.Ensures(Contract.Result<IFunApp>() != null);
+        Contract.Assert(args.Count == 1);
+        return new PolyhedraLatticeNegation((IExpr/*!*/)cce.NonNull(args[0]));
+      }
+    }
+
+    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);
+      // BUGBUG: TODO: this method can be implemented in a more precise way
+      return null;
+    }
+
+
+    public override Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr) {
+      //Contract.Requires(expr != null);
+      //Contract.Requires(e != null);
+      Contract.Ensures(Contract.Result<Element>() != null);
+      log.DbgMsg(string.Format("Constraining with {0} into {1} ...", expr, this.ToString(e)));
+
+      PolyhedraLatticeElement ple = (PolyhedraLatticeElement)e;
+      if (ple.lcs.IsBottom()) {
+        return ple;
+      }
+      LinearCondition le = LinearExpressionBuilder.AsCondition(expr);
+      if (le != null) {
+        // update the polyhedron according to the linear expression
+        Contract.Assume(ple.lcs.Constraints != null);
+        ArrayList /*LinearConstraint*/ clist = (ArrayList/*!*/ /*LinearConstraint*/)cce.NonNull(ple.lcs.Constraints.Clone());
+        le.AddToConstraintSystem(clist);
+        LinearConstraintSystem newLcs = new LinearConstraintSystem(clist);
+
+        return new PolyhedraLatticeElement(newLcs);
+      }
+      return ple;
+    }
+
+  } // class
+
+
+  /// <summary>
+  /// A LinearCondition follows this grammar:
+  ///     LinearCondition ::=  unsatisfiable
+  ///                       |  LinearConstraint
+  ///                       |  ! LinearConstraint
+  /// Note that negations are distributed to the leaves.
+  /// </summary>
+  /// 
+  [ContractClass(typeof(LinearConditionContracts))]
+  abstract class LinearCondition {
+    /// <summary>
+    /// Adds constraints to the list "clist".  If "this"
+    /// entails some disjunctive constraints, they may not be added.
+    /// </summary>
+    /// <param name="clist"></param>
+    public abstract void AddToConstraintSystem(ArrayList/*!*/ /*LinearConstraint*/ clist);
+  }
+  [ContractClassFor(typeof(LinearCondition))]
+  abstract class LinearConditionContracts : LinearCondition {
+    public override void AddToConstraintSystem(ArrayList clist) {
+      Contract.Requires(clist != null);
+      throw new NotImplementedException();
+    }
+  }
+
+  class LCBottom : LinearCondition {
+    public override void AddToConstraintSystem(ArrayList/*!*/ /*LinearConstraint*/ clist) {
+      //Contract.Requires(clist != null);
+      // make an unsatisfiable constraint
+      LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
+      lc.rhs = Rational.FromInt(1);
+      clist.Add(lc);
+    }
+  }
+
+  class LinearConditionLiteral : LinearCondition {
+    public readonly bool positive;
+    public readonly LinearConstraint/*!*/ constraint;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(constraint != null);
+    }
+
+    /// <summary>
+    /// Precondition:  positive || constraint.Relation == LinearConstraint.ConstraintRelation.EQ
+    /// </summary>
+    /// <param name="positive"></param>
+    /// <param name="constraint"></param>
+    public LinearConditionLiteral(bool positive, LinearConstraint/*!*/ constraint) {
+      Contract.Requires(constraint != null);
+      Contract.Requires(positive || constraint.Relation == LinearConstraint.ConstraintRelation.EQ);
+      this.positive = positive;
+      this.constraint = constraint;
+    }
+    public override void AddToConstraintSystem(ArrayList/*!*/ /*LinearConstraint*/ clist) {
+      //Contract.Requires(clist != null);
+      if (positive) {
+        clist.Add(constraint);
+      } else {
+        Contract.Assert(constraint.Relation == LinearConstraint.ConstraintRelation.EQ);
+        // the constraint is disjunctive, so just ignore it
+      }
+    }
+  }
+
+  class LinearExpressionBuilder {
+    /// <summary>
+    /// Builds a linear condition from "e", if possible; returns null if not possible.
+    /// </summary>
+    /// <param name="e"></param>
+    /// <returns></returns>
+    public static /*maybe null*/ LinearCondition AsCondition(IExpr e) /* throws ArithmeticException */
+    {
+      return GetCond(e, true);
+    }
+
+    static /*maybe null*/ LinearCondition GetCond(IExpr e, bool positive) /* throws ArithmeticException */
+    {
+      IFunApp funapp = e as IFunApp;
+      if (funapp == null) {
+        return null;
+      }
+      IFunctionSymbol/*!*/ s = funapp.FunctionSymbol;
+      Contract.Assert(s != null);
+      if ((positive && s.Equals(Prop.False)) ||
+          (!positive && s.Equals(Prop.True))) {
+        return new LCBottom();
+      } else if (s.Equals(Prop.Not)) {
+        Contract.Assert(funapp.Arguments.Count == 1);
+        return GetCond((IExpr/*!*/)cce.NonNull(funapp.Arguments[0]), !positive);
+      } else if (funapp.Arguments.Count == 2) {
+        IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(funapp.Arguments[0]);
+        IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(funapp.Arguments[1]);
+        LinearExpr le0 = AsExpr(arg0);
+        if (le0 == null) {
+          return null;
+        }
+        LinearExpr le1 = AsExpr(arg1);
+        if (le1 == null) {
+          return null;
+        }
+
+        LinearConstraint constraint = null;
+        bool sense = true;
+        if ((positive && s.Equals(Int.Less)) || (!positive && s.Equals(Int.AtLeast))) {
+          constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.LE, BigNum.ONE);
+        } else if ((positive && s.Equals(Int.AtMost)) || (!positive && s.Equals(Int.Greater))) {
+          constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.LE, BigNum.ZERO);
+        } else if ((positive && s.Equals(Int.AtLeast)) || (!positive && s.Equals(Int.Less))) {
+          constraint = MakeConstraint(le1, le0, LinearConstraint.ConstraintRelation.LE, BigNum.ZERO);
+        } else if ((positive && s.Equals(Int.Greater)) || (!positive && s.Equals(Int.AtMost))) {
+          constraint = MakeConstraint(le1, le0, LinearConstraint.ConstraintRelation.LE, BigNum.ONE);
+        } else if (s.Equals(Int.Eq)) {
+          constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.EQ, BigNum.ZERO);
+          sense = positive;
+        } else if (s.Equals(Int.Neq)) {
+          constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.EQ, BigNum.ZERO);
+          sense = !positive;
+        }
+        if (constraint != null) {
+          if (constraint.coefficients.Count != 0) {
+            return new LinearConditionLiteral(sense, constraint);
+          } else if (constraint.IsConstantSatisfiable()) {
+            return null;
+          } else {
+            return new LCBottom();
+          }
+        }
+      }
+      return null;
+    }
+
+    public static LinearConstraint MakeConstraint(LinearExpr/*!*/ le0, LinearExpr/*!*/ le1,
+        LinearConstraint.ConstraintRelation rel, BigNum constantOffset) /* throws ArithmeticException */
+    {
+      Contract.Requires(le0 != null);
+      Contract.Requires(le1 != null);
+      le1.Negate();
+      le0.Add(le1);
+      le0.AddConstant(constantOffset);
+      return le0.ToConstraint(rel);
+    }
+
+    /// <summary>
+    /// Builds a linear expression from "e", if possible; returns null if not possible.
+    /// </summary>
+    /// <param name="e"></param>
+    /// <returns></returns>
+    public static /*maybe null*/ LinearExpr AsExpr(IExpr/*!*/ e) /* throws ArithmeticException */
+    {
+      Contract.Requires(e != null);
+      if (e is IVariable) {
+        // Note, without a type for the variable, we don't know if the identifier is intended to hold an integer value.
+        // However, it seems that no harm can be caused by here treating the identifier as if it held an
+        // integer value, because other parts of this method will reject the expression as a linear expression
+        // if non-numeric operations other than equality are applied to the identifier.
+        return new LinearExpr((IVariable)e);
+      } else if (e is IFunApp) {
+        IFunApp/*!*/ funapp = (IFunApp)e;
+        Contract.Assert(funapp != null);
+        IFunctionSymbol/*!*/ s = funapp.FunctionSymbol;
+        Contract.Assert(s != null);
+
+        if (s is IntSymbol) {
+          return new LinearExpr(((IntSymbol)s).Value);
+        } else if (s.Equals(Int.Negate)) {
+          Contract.Assert(funapp.Arguments.Count == 1);
+          LinearExpr le = AsExpr((IExpr/*!*/)cce.NonNull(funapp.Arguments[0]));
+          if (le != null) {
+            le.Negate();
+            return le;
+          }
+        } else if (s.Equals(Int.Add) || s.Equals(Int.Sub) || s.Equals(Int.Mul)) {
+          Contract.Assert(funapp.Arguments.Count == 2);
+          IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(funapp.Arguments[0]);
+          IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(funapp.Arguments[1]);
+          LinearExpr le0 = AsExpr(arg0);
+          if (le0 == null) {
+            return null;
+          }
+          LinearExpr le1 = AsExpr(arg1);
+          if (le1 == null) {
+            return null;
+          }
+
+          if (s.Equals(Int.Add)) {
+            le0.Add(le1);
+            return le0;
+          } else if (s.Equals(Int.Sub)) {
+            le1.Negate();
+            le0.Add(le1);
+            return le0;
+          } else if (s.Equals(Int.Mul)) {
+            BigNum x;
+            if (le0.AsConstant(out x)) {
+              le1.Multiply(x);
+              return le1;
+            } else if (le1.AsConstant(out x)) {
+              le0.Multiply(x);
+              return le0;
+            }
+          }
+        }
+      }
+      return null;
+    }
+  }
+
+  class LinearExpr {
+    BigNum constant;
+    Term terms;
+
+    class Term {
+      public BigNum coeff;  // non-0, if the node is used
+      public IVariable/*!*/ var;
+      public Term next;
+      [ContractInvariantMethod]
+      void ObjectInvariant() {
+        Contract.Invariant(var != null);
+      }
+
+      public Term(BigNum coeff, IVariable/*!*/ var) {
+        Contract.Requires(var != null);
+        this.coeff = coeff;
+        this.var = var;
+        // base();
+      }
+    }
+
+    public LinearExpr(BigNum x) {
+      constant = x;
+    }
+
+    public LinearExpr(IVariable/*!*/ var) {
+      Contract.Requires(var != null);
+      constant = BigNum.ZERO;
+      terms = new Term(BigNum.ONE, var);
+    }
+
+    public ISet /*IVariable!*/ GetDefinedDimensions() {
+      HashSet /*IVariable!*//*!*/ dims = new HashSet /*IVariable!*/ ();
+      for (Term current = terms; current != null; current = current.next) {
+        dims.Add(current.var);
+      }
+      return dims;
+    }
+
+    public BigNum TermCoefficient(/*MayBeNull*/ IVariable/*!*/ var) {
+      Contract.Requires(var != null);
+      BigNum z = BigNum.ZERO;
+      if (var == null) {
+        z = this.constant;
+      } else if (terms != null) {
+        Term current = terms;
+        while (current != null) {
+          if (current.var == var) {
+            break;
+          }
+          current = current.next;
+        }
+        if (current != null) {
+          z = current.coeff;
+        }
+      }
+      return z;
+    }
+
+    public bool AsConstant(out BigNum x) {
+      if (terms == null) {
+        x = constant;
+        return true;
+      } else {
+        x = BigNum.FromInt(-70022);  // to please complier
+        return false;
+      }
+    }
+
+    public void Negate() /* throws ArithmeticException */
+    {
+      checked {
+        constant = -constant;
+      }
+
+      for (Term t = terms; t != null; t = t.next) {
+        checked {
+          t.coeff = -t.coeff;
+        }
+      }
+    }
+
+    /// <summary>
+    /// Adds "x" to "this".
+    /// </summary>
+    /// <param name="x"></param>
+    public void AddConstant(BigNum x) /* throws ArithmeticException */
+    {
+      checked {
+        constant += x;
+      }
+    }
+
+    /// <summary>
+    /// Adds "le" to "this".  Afterwards, "le" should not be used, because it will have been destroyed.
+    /// </summary>
+    /// <param name="le"></param>
+    public void Add(LinearExpr/*!*/ le) /* throws ArithmeticException */
+        {
+      Contract.Requires(le != null);
+      Contract.Requires(le != this);
+      checked {
+        constant += le.constant;
+      }
+      le.constant = BigNum.FromInt(-70029);  // "le" should no longer be used; assign it a strange value so that misuse is perhaps more easily detected
+
+      // optimization:
+      if (le.terms == null) {
+        return;
+      } else if (terms == null) {
+        terms = le.terms;
+        le.terms = null;
+        return;
+      }
+
+      // merge the two term lists
+      // Use a nested loop, which is quadratic in time complexity, but we hope the lists will be small
+      Term newTerms = null;
+      while (le.terms != null) {
+        // take off next term from "le"
+        Term t = le.terms;
+        le.terms = t.next;
+        t.next = null;
+
+        for (Term u = terms; u != null; u = u.next) {
+          if (u.var == t.var) {
+            checked {
+              u.coeff += t.coeff;
+            }
+            goto NextOuter;
+          }
+        }
+        t.next = newTerms;
+        newTerms = t;
+
+      NextOuter:
+        ;
+      }
+
+      // finally, include all non-0 terms
+      while (terms != null) {
+        // take off next term from "this"
+        Term t = terms;
+        terms = t.next;
+
+        if (!t.coeff.IsZero) {
+          t.next = newTerms;
+          newTerms = t;
+        }
+      }
+      terms = newTerms;
+    }
+
+    public void Multiply(BigNum x) /* throws ArithmeticException */
+    {
+      if (x.IsZero) {
+        constant = BigNum.ZERO;
+        terms = null;
+      } else {
+        for (Term t = terms; t != null; t = t.next) {
+          checked {
+            t.coeff *= x;
+          }
+        }
+        checked {
+          constant *= x;
+        }
+      }
+    }
+
+    public bool IsInvertible(IVariable/*!*/ var) {
+      Contract.Requires(var != null);
+      for (Term t = terms; t != null; t = t.next) {
+        if (t.var == var) {
+          System.Diagnostics.Debug.Assert(!t.coeff.IsZero);
+          return true;
+        }
+      }
+      return false;
+    }
+
+    public LinearConstraint ToConstraint(LinearConstraint.ConstraintRelation rel) /* throws ArithmeticException */
+    {
+      LinearConstraint constraint = new LinearConstraint(rel);
+      for (Term t = terms; t != null; t = t.next) {
+        constraint.SetCoefficient(t.var, t.coeff.ToRational);
+      }
+      BigNum rhs = -constant;
+      constraint.rhs = rhs.ToRational;
+      return constraint;
+    }
+  }
+}
diff --git a/Source/AIFramework/Polyhedra/SimplexTableau.cs b/Source/AIFramework/Polyhedra/SimplexTableau.cs
index 4d734c27..347c7c45 100644
--- a/Source/AIFramework/Polyhedra/SimplexTableau.cs
+++ b/Source/AIFramework/Polyhedra/SimplexTableau.cs
@@ -1,630 +1,630 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework {
-  using System.Collections;
-  using System;
-  using System.Diagnostics.Contracts;
-  using Microsoft.Basetypes;
-  using IMutableSet = Microsoft.Boogie.GSet<object>;
-  using HashSet = Microsoft.Boogie.GSet<object>;
-
-
-  /// <summary>
-  /// Used by LinearConstraintSystem.GenerateFrameFromConstraints.
-  /// </summary>
-  public class SimplexTableau {
-    readonly int rows;
-    readonly int columns;
-    readonly Rational[,]/*!*/ m;
-
-    readonly int numInitialVars;
-    readonly int numSlackVars;
-    readonly int rhsColumn;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(m != null);
-      Contract.Invariant(inBasis != null);
-      Contract.Invariant(basisColumns != null);
-    }
-
-    readonly ArrayList /*IVariable!*//*!*/ dims;
-    readonly int[]/*!*/ basisColumns;
-    readonly int[]/*!*/ inBasis;
-    bool constructionDone = false;
-
-    void CheckInvariant() {
-      Contract.Assert(rows == m.GetLength(0));
-      Contract.Assert(1 <= columns && columns == m.GetLength(1));
-      Contract.Assert(0 <= numInitialVars);
-      Contract.Assert(0 <= numSlackVars && numSlackVars <= rows);
-      Contract.Assert(numInitialVars + numSlackVars + 1 == columns);
-      Contract.Assert(rhsColumn == columns - 1);
-      Contract.Assert(dims.Count == numInitialVars);
-      Contract.Assert(basisColumns.Length == rows);
-      Contract.Assert(inBasis.Length == numInitialVars + numSlackVars);
-
-      bool[] b = new bool[numInitialVars + numSlackVars];
-      int numColumnsInBasis = 0;
-      int numUninitializedRowInfo = 0;
-      for (int i = 0; i < rows; i++) {
-        int c = basisColumns[i];
-        if (c == rhsColumn) {
-          // all coefficients in this row are 0 (but the right-hand side may be non-0)
-          for (int j = 0; j < rhsColumn; j++) {
-            Contract.Assert(m[i, j].IsZero);
-          }
-          numColumnsInBasis++;
-        } else if (c == -1) {
-          Contract.Assert(!constructionDone);
-          numUninitializedRowInfo++;
-        } else {
-          // basis column is a column
-          Contract.Assert(0 <= c && c < numInitialVars + numSlackVars);
-          // basis column is unique
-          Contract.Assert(!b[c]);
-          b[c] = true;
-          // column is marked as being in basis
-          Contract.Assert(inBasis[c] == i);
-          // basis column really is a basis column
-          for (int j = 0; j < rows; j++) {
-            if (j == i) {
-              Contract.Assert(m[j, c].HasValue(1));// == (Rational)new Rational(1)));
-            } else {
-              Contract.Assert(m[j, c].IsZero);
-            }
-          }
-        }
-      }
-      // no other columns are marked as being in basis
-      foreach (int i in inBasis) {
-        if (0 <= i) {
-          Contract.Assert(i < rows);
-          numColumnsInBasis++;
-        } else {
-          Contract.Assert(i == -1);
-        }
-      }
-      Contract.Assert(rows - numUninitializedRowInfo <= numColumnsInBasis && numColumnsInBasis <= rows);
-      Contract.Assert(!constructionDone || numUninitializedRowInfo == 0);
-    }
-
-    /// <summary>
-    /// Constructs a matrix that represents the constraints "constraints", adding slack
-    /// variables for the inequalities among "constraints".  Puts the matrix in canonical
-    /// form.
-    /// </summary>
-    /// <param name="constraints"></param>
-    [NotDelayed]
-    public SimplexTableau(ArrayList /*LinearConstraint*//*!*/ constraints) {
-      Contract.Requires(constraints != null);
-#if DEBUG_PRINT
-            Console.WriteLine("DEBUG: SimplexTableau constructor called with:");
-            foreach (LinearConstraint lc in constraints)
-            {
-              Console.WriteLine("  {0}", lc);
-            }
-#endif
-      // Note:  This implementation is not particularly efficient, but it'll do for now.
-
-      ArrayList dims = this.dims = new ArrayList /*IVariable!*/ ();
-      int slacks = 0;
-      foreach (LinearConstraint/*!*/ cc in constraints) {
-        Contract.Assert(cc != null);
-        foreach (IVariable/*!*/ dim in cc.coefficients.Keys) {
-          Contract.Assert(dim != null);
-          if (!dims.Contains(dim)) {
-            dims.Add(dim);
-          }
-        }
-        if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
-          slacks++;
-        }
-      }
-
-      int numInitialVars = this.numInitialVars = dims.Count;
-      int numSlackVars = this.numSlackVars = slacks;
-      int rows = this.rows = constraints.Count;
-      int columns = this.columns = numInitialVars + numSlackVars + 1;
-      this.m = new Rational[rows, columns];
-      this.rhsColumn = columns - 1;
-      this.basisColumns = new int[rows];
-      this.inBasis = new int[columns - 1];
-
-      //:base();
-
-      for (int i = 0; i < inBasis.Length; i++) {
-        inBasis[i] = -1;
-      }
-
-      // Fill in the matrix
-      int r = 0;
-      int iSlack = 0;
-      foreach (LinearConstraint/*!*/ cc in constraints) {
-        Contract.Assert(cc != null);
-        for (int i = 0; i < dims.Count; i++) {
-          m[r, i] = cc[(IVariable)cce.NonNull(dims[i])];
-        }
-        if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
-          m[r, numInitialVars + iSlack] = Rational.ONE;
-          basisColumns[r] = numInitialVars + iSlack;
-          inBasis[numInitialVars + iSlack] = r;
-          iSlack++;
-        } else {
-          basisColumns[r] = -1;  // special value to communicate to Pivot that basis column i hasn't been set up yet
-        }
-        m[r, rhsColumn] = cc.rhs;
-        r++;
-      }
-      Contract.Assert(r == constraints.Count);
-      Contract.Assert(iSlack == numSlackVars);
-#if DEBUG_PRINT
-            Console.WriteLine("DEBUG: Intermediate tableau state in SimplexTableau constructor:");
-            Dump();
-#endif
-
-      // Go through the rows with uninitialized basis columns.  These correspond to equality constraints.
-      // For each one, find an initial variable (non-slack variable) whose column we can make the basis
-      // column of the row.
-      for (int i = 0; i < rows; i++) {
-        if (basisColumns[i] != -1) {
-          continue;
-        }
-        // Find a non-0 column in row i that we can make a basis column.  Since rows corresponding
-        // to equality constraints don't have slack variables and since the pivot operations performed
-        // by iterations of this loop don't introduce any non-0 coefficients in the slack-variable
-        // columns of these rows, we only need to look through the columns corresponding to initial
-        // variables.
-        for (int j = 0; j < numInitialVars; j++) {
-          if (m[i, j].IsNonZero) {
-#if DEBUG_PRINT
-                            Console.WriteLine("-- About to Pivot({0},{1})", i, j);
-#endif
-            Contract.Assert(inBasis[j] == -1);
-            Pivot(i, j);
-#if DEBUG_PRINT
-                            Console.WriteLine("Tableau after Pivot:");
-                            Dump();
-#endif
-            goto SET_UP_NEXT_INBASIS_COLUMN;
-          }
-        }
-        // Check the assertion in the comment above, that is, that columns corresponding to slack variables
-        // are 0 in this row.
-        for (int j = numInitialVars; j < rhsColumn; j++) {
-          Contract.Assert(m[i, j].IsZero);
-        }
-        // There is no column in this row that we can put into basis.
-        basisColumns[i] = rhsColumn;
-      SET_UP_NEXT_INBASIS_COLUMN: {
-        }
-      }
-
-      constructionDone = true;
-      CheckInvariant();
-    }
-
-    public IMutableSet/*!*/ /*IVariable!*/ GetDimensions() {
-      Contract.Ensures(Contract.Result<IMutableSet>() != null);
-      HashSet /*IVariable!*/ z = new HashSet /*IVariable!*/ ();
-      foreach (IVariable/*!*/ dim in dims) {
-        Contract.Assert(dim != null);
-        z.Add(dim);
-      }
-      return z;
-    }
-
-    public Rational this[int r, int c] {
-      get {
-        return m[r, c];
-      }
-      set {
-        m[r, c] = value;
-      }
-    }
-
-    /// <summary>
-    /// Applies the Pivot Operation on row "r" and column "c".
-    /// 
-    /// This method can be called when !constructionDone, that is, at a time when not all basis
-    /// columns have been set up (indicated by -1 in basisColumns).  This method helps set up
-    /// those basis columns.
-    /// 
-    /// The return value is an undo record that can be used with UnPivot.
-    /// </summary>
-    /// <param name="r"></param>
-    /// <param name="c"></param>
-    public Rational[]/*!*/ Pivot(int r, int c) {
-      Contract.Ensures(Contract.Result<Rational[]>() != null);
-      Contract.Assert(0 <= r && r < rows);
-      Contract.Assert(0 <= c && c < columns - 1);
-      Contract.Assert(m[r, c].IsNonZero);
-      Contract.Assert(inBasis[c] == -1);  // follows from invariant and m[r,c] != 0
-      Contract.Assert(basisColumns[r] != rhsColumn);  // follows from invariant and m[r,c] != 0
-
-      Rational[] undo = new Rational[rows + 1];
-      for (int i = 0; i < rows; i++) {
-        undo[i] = m[i, c];
-      }
-
-      // scale the pivot row
-      Rational q = m[r, c];
-      if (q != Rational.ONE) {
-        for (int j = 0; j < columns; j++) {
-          m[r, j] /= q;
-        }
-      }
-
-      // subtract a multiple of the pivot row from all other rows
-      for (int i = 0; i < rows; i++) {
-        if (i != r) {
-          q = m[i, c];
-          if (q.IsNonZero) {
-            for (int j = 0; j < columns; j++) {
-              m[i, j] -= q * m[r, j];
-            }
-          }
-        }
-      }
-
-      // update basis information
-      int prevCol = basisColumns[r];
-      undo[rows] = Rational.FromInt(prevCol);
-      basisColumns[r] = c;
-      if (prevCol != -1) {
-        inBasis[prevCol] = -1;
-      }
-      inBasis[c] = r;
-
-      return undo;
-    }
-
-    /// <summary>
-    /// If the last operation applied to the tableau was:
-    ///   undo = Pivot(i,j);
-    /// then UnPivot(i, j, undo) undoes the pivot operation.
-    /// Note:  This operation is not supported for any call to Pivot before constructionDone
-    /// is set to true.
-    /// </summary>
-    /// <param name="r"></param>
-    /// <param name="c"></param>
-    /// <param name="undo"></param>
-    void UnPivot(int r, int c, Rational[]/*!*/ undo) {
-      Contract.Requires(undo != null);
-      Contract.Assert(0 <= r && r < rows);
-      Contract.Assert(0 <= c && c < columns - 1);
-      Contract.Assert(m[r, c].HasValue(1));
-      Contract.Assert(undo.Length == rows + 1);
-
-      // add a multiple of the pivot row to all other rows
-      for (int i = 0; i < rows; i++) {
-        if (i != r) {
-          Rational q = undo[i];
-          if (q.IsNonZero) {
-            for (int j = 0; j < columns; j++) {
-              m[i, j] += q * m[r, j];
-            }
-          }
-        }
-      }
-
-      // scale the pivot row
-      Rational p = undo[r];
-      for (int j = 0; j < columns; j++) {
-        m[r, j] *= p;
-      }
-
-      // update basis information
-      int prevCol = undo[rows].AsInteger;
-      Contract.Assert(prevCol != -1);
-      basisColumns[r] = prevCol;
-      inBasis[c] = -1;
-      inBasis[prevCol] = r;
-    }
-
-    /// <summary>
-    /// Returns true iff the current basis of the system of constraints modeled by the simplex tableau
-    /// is feasible.  May have a side effect of performing a number of pivot operations on the tableau,
-    /// but any such pivot operation will be in the columns of slack variables (that is, this routine
-    /// does not change the set of initial-variable columns in basis).
-    /// 
-    /// CAVEAT: I have no particular reason to believe that the algorithm used here will terminate. --KRML
-    /// </summary>
-    /// <returns></returns>
-    public bool IsFeasibleBasis {
-      get {
-        // while there is a slack variable in basis whose row has a negative right-hand side
-        while (true) {
-          bool feasibleBasis = true;
-          for (int c = numInitialVars; c < rhsColumn; c++) {
-            int k = inBasis[c];
-            if (0 <= k && k < rhsColumn && m[k, rhsColumn].IsNegative) {
-              Contract.Assert(m[k, c].HasValue(1));  // c is in basis
-              // Try to pivot on a different slack variable in this row
-              for (int i = numInitialVars; i < rhsColumn; i++) {
-                if (m[k, i].IsNegative) {
-                  Contract.Assert(c != i);  // c is in basis, so m[k,c]==1, which is not negative
-                  Pivot(k, i);
-#if DEBUG_PRINT
-                  Console.WriteLine("Tableau after Pivot operation on ({0},{1}) in IsFeasibleBasis:", k, i);
-                  Dump();
-#endif
-                  Contract.Assert(inBasis[c] == -1);
-                  Contract.Assert(inBasis[i] == k);
-                  Contract.Assert(m[k, rhsColumn].IsNonNegative);
-                  goto START_ANEW;
-                }
-              }
-              feasibleBasis = false;
-            }
-          }
-          return feasibleBasis;
-        START_ANEW:
-          ;
-        }
-      }
-    }
-
-    /// <summary>
-    /// Whether or not all initial variables (the non-slack variables) are in basis)
-    /// </summary>
-    public bool AllInitialVarsInBasis {
-      get {
-        for (int i = 0; i < numInitialVars; i++) {
-          if (inBasis[i] == -1) {
-            return false;
-          }
-        }
-        return true;
-      }
-    }
-
-    /// <summary>
-    /// Adds as many initial variables as possible to the basis.
-    /// </summary>
-    /// <returns></returns>
-    public void AddInitialVarsToBasis() {
-      // while there exists an initial variable not in the basis and not satisfying
-      // condition 3.4.2.2 in Cousot and Halbwachs, perform a pivot operation
-      while (true) {
-        for (int i = 0; i < numInitialVars; i++) {
-          if (inBasis[i] == -1) {
-            // initial variable i is not in the basis
-            for (int j = 0; j < rows; j++) {
-              if (m[j, i].IsNonZero) {
-                int k = basisColumns[j];
-                if (numInitialVars <= k && k < rhsColumn) {
-                  // slack variable k is in basis for row j
-                  Pivot(j, i);
-                  Contract.Assert(inBasis[k] == -1);
-                  Contract.Assert(inBasis[i] == j && basisColumns[j] == i);
-                  goto START_ANEW;
-                }
-              }
-            }
-          }
-        }
-        // No more initial variables can be moved into basis.
-        return;
-      START_ANEW: {
-        }
-      }
-    }
-
-    /// <summary>
-    /// Adds to "lines" the lines implied by initial-variable columns not in basis
-    /// (see section 3.4.2 of Cousot and Halbwachs), and adds to "constraints" the
-    /// constraints to exclude those lines (see step 4.2 of section 3.4.3 of
-    /// Cousot and Halbwachs).
-    /// </summary>
-    /// <param name="lines"></param>
-    /// <param name="constraints"></param>
-    public void ProduceLines(ArrayList /*FrameElement*//*!*/ lines, ArrayList /*LinearConstraint*//*!*/ constraints) {
-      Contract.Requires(constraints != null);
-      Contract.Requires(lines != null);
-      // for every initial variable not in basis
-      for (int i0 = 0; i0 < numInitialVars; i0++) {
-        if (inBasis[i0] == -1) {
-          FrameElement fe = new FrameElement();
-          LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
-          for (int i = 0; i < numInitialVars; i++) {
-            if (i == i0) {
-              fe.AddCoordinate((IVariable)cce.NonNull(dims[i]), Rational.ONE);
-              lc.SetCoefficient((IVariable)cce.NonNull(dims[i]), Rational.ONE);
-            } else if (inBasis[i] != -1) {
-              // i is a basis column
-              Contract.Assert(m[inBasis[i], i].HasValue(1));
-              Rational val = -m[inBasis[i], i0];
-              fe.AddCoordinate((IVariable)cce.NonNull(dims[i]), val);
-              lc.SetCoefficient((IVariable)cce.NonNull(dims[i]), val);
-            }
-          }
-          lines.Add(fe);
-          constraints.Add(lc);
-        }
-      }
-    }
-
-    /// <summary>
-    /// From a feasible point where all initial variables are in the basis, traverses
-    /// all feasible bases containing all initial variables.  For each such basis, adds
-    /// the vertices to "vertices" and adds to "rays" the extreme rays.  See step 4.2
-    /// in section 3.4.3 of Cousot and Halbwachs.
-    /// A more efficient algorithm is found in the paper "An algorithm for
-    /// determining all extreme points of a convex polytope" by N. E. Dyer and L. G. Proll,
-    /// Mathematical Programming, 12, 1977.
-    /// Assumes that the tableau is in a state where all initial variables are in the basis.
-    /// This method has no net effect on the tableau.
-    /// Note: Duplicate vertices and rays may be added.
-    /// </summary>
-    /// <param name="vertices"></param>
-    /// <param name="rays"></param>
-    public void TraverseVertices(ArrayList/*!*/ /*FrameElement*/ vertices, ArrayList/*!*/ /*FrameElement*/ rays) {
-      Contract.Requires(vertices != null);
-      Contract.Requires(rays != null);
-      ArrayList /*bool[]*/ basesSeenSoFar = new ArrayList /*bool[]*/ ();
-      TraverseBases(basesSeenSoFar, vertices, rays);
-    }
-
-    /// <summary>
-    /// Worker method of TraverseVertices.
-    /// This method has no net effect on the tableau.
-    /// </summary>
-    /// <param name="basesSeenSoFar"></param>
-    /// <param name="vertices"></param>
-    /// <param name="rays"></param>
-    void TraverseBases(ArrayList /*bool[]*//*!*/ basesSeenSoFar, ArrayList /*FrameElement*//*!*/ vertices, ArrayList /*FrameElement*//*!*/ rays) {
-      Contract.Requires(rays != null);
-      Contract.Requires(vertices != null);
-      Contract.Requires(basesSeenSoFar != null);
-      CheckInvariant();
-
-      bool[] thisBasis = new bool[numSlackVars];
-      for (int i = numInitialVars; i < rhsColumn; i++) {
-        if (inBasis[i] != -1) {
-          thisBasis[i - numInitialVars] = true;
-        }
-      }
-      foreach (bool[]/*!*/ basis in basesSeenSoFar) {
-        Contract.Assert(basis != null);
-        Contract.Assert(basis.Length == numSlackVars);
-        for (int i = 0; i < numSlackVars; i++) {
-          if (basis[i] != thisBasis[i]) {
-            goto COMPARE_WITH_NEXT_BASIS;
-          }
-        }
-        // thisBasis and basis are the same--that is, basisColumns has been visited before--so
-        // we don't traverse anything from here
-        return;
-      COMPARE_WITH_NEXT_BASIS: {
-        }
-      }
-      // basisColumns has not been seen before; record thisBasis and continue with the traversal here
-      basesSeenSoFar.Add(thisBasis);
-
-#if DEBUG_PRINT
-      Console.Write("TraverseBases, new basis:  ");
-      foreach (bool t in thisBasis) {
-        Console.Write("{0}", t ? "*" : ".");
-      }
-      Console.WriteLine();
-      Dump();
-#endif
-      // Add vertex
-      FrameElement v = new FrameElement();
-      for (int i = 0; i < rows; i++) {
-        int j = basisColumns[i];
-        if (j < numInitialVars) {
-          v.AddCoordinate((IVariable)cce.NonNull(dims[j]), m[i, rhsColumn]);
-        }
-      }
-#if DEBUG_PRINT
-      Console.WriteLine("  Adding vertex: {0}", v);
-#endif
-      vertices.Add(v);
-
-      // Add rays.  Traverse all columns corresponding to slack variables that
-      // are not in basis (see second bullet of section 3.4.2 of Cousot and Halbwachs).
-      for (int i0 = numInitialVars; i0 < rhsColumn; i0++) {
-        if (inBasis[i0] != -1) {
-          // skip those slack-variable columns that are in basis
-          continue;
-        }
-        // check if slack-variable, non-basis column i corresponds to an extreme ray
-        for (int row = 0; row < rows; row++) {
-          if (m[row, i0].IsPositive) {
-            for (int k = numInitialVars; k < rhsColumn; k++) {
-              if (inBasis[k] != -1 && m[row, k].IsNonZero) {
-                // does not correspond to an extreme ray
-                goto CHECK_NEXT_SLACK_VAR;
-              }
-            }
-          }
-        }
-        // corresponds to an extreme ray
-        FrameElement ray = new FrameElement();
-        for (int i = 0; i < numInitialVars; i++) {
-          int j0 = inBasis[i];
-          Rational val = -m[j0, i0];
-          ray.AddCoordinate((IVariable)cce.NonNull(dims[i]), val);
-        }
-#if DEBUG_PRINT
-        Console.WriteLine("  Adding ray: {0}", ray);
-#endif
-        rays.Add(ray);
-      CHECK_NEXT_SLACK_VAR: {
-        }
-      }
-
-      // Continue traversal
-      for (int i = numInitialVars; i < rhsColumn; i++) {
-        int j = inBasis[i];
-        if (j != -1) {
-          // try moving i out of basis and some other slack-variable column into basis
-          for (int k = numInitialVars; k < rhsColumn; k++) {
-            if (inBasis[k] == -1 && m[j, k].IsPositive) {
-              Rational[] undo = Pivot(j, k);
-              // check if the new basis is feasible
-              for (int p = 0; p < rows; p++) {
-                int c = basisColumns[p];
-                if (numInitialVars <= c && c < rhsColumn && m[p, rhsColumn].IsNegative) {
-                  // not feasible
-                  goto AFTER_TRAVERSE;
-                }
-              }
-              TraverseBases(basesSeenSoFar, vertices, rays);
-            AFTER_TRAVERSE:
-              UnPivot(j, k, undo);
-            }
-          }
-        }
-      }
-    }
-
-    public void Dump() {
-      // names
-      Console.Write("      ");
-      for (int i = 0; i < numInitialVars; i++) {
-        Console.Write("  {0,4}   ", dims[i]);
-      }
-      Console.WriteLine();
-      // numbers
-      Console.Write("      ");
-      for (int i = 0; i < columns; i++) {
-        if (i == numInitialVars || i == rhsColumn) {
-          Console.Write("|");
-        }
-        Console.Write("  {0,4}", i);
-        if (i < rhsColumn && inBasis[i] != -1) {
-          Console.Write("*  ");
-          Contract.Assert(basisColumns[inBasis[i]] == i);
-        } else {
-          Console.Write("   ");
-        }
-      }
-      Console.WriteLine();
-      // line
-      Console.Write("      ");
-      for (int i = 0; i < columns; i++) {
-        if (i == numInitialVars || i == rhsColumn) {
-          Console.Write("+");
-        }
-        Console.Write("---------");
-      }
-      Console.WriteLine();
-
-      for (int j = 0; j < rows; j++) {
-        Console.Write("{0,4}: ", basisColumns[j]);
-        for (int i = 0; i < columns; i++) {
-          if (i == numInitialVars || i == rhsColumn) {
-            Console.Write("|");
-          }
-          Console.Write("  {0,4:n1}   ", m[j, i]);
-        }
-        Console.WriteLine();
-      }
-    }
-  }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.AbstractInterpretationFramework {
+  using System.Collections;
+  using System;
+  using System.Diagnostics.Contracts;
+  using Microsoft.Basetypes;
+  using IMutableSet = Microsoft.Boogie.GSet<object>;
+  using HashSet = Microsoft.Boogie.GSet<object>;
+
+
+  /// <summary>
+  /// Used by LinearConstraintSystem.GenerateFrameFromConstraints.
+  /// </summary>
+  public class SimplexTableau {
+    readonly int rows;
+    readonly int columns;
+    readonly Rational[,]/*!*/ m;
+
+    readonly int numInitialVars;
+    readonly int numSlackVars;
+    readonly int rhsColumn;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(m != null);
+      Contract.Invariant(inBasis != null);
+      Contract.Invariant(basisColumns != null);
+    }
+
+    readonly ArrayList /*IVariable!*//*!*/ dims;
+    readonly int[]/*!*/ basisColumns;
+    readonly int[]/*!*/ inBasis;
+    bool constructionDone = false;
+
+    void CheckInvariant() {
+      Contract.Assert(rows == m.GetLength(0));
+      Contract.Assert(1 <= columns && columns == m.GetLength(1));
+      Contract.Assert(0 <= numInitialVars);
+      Contract.Assert(0 <= numSlackVars && numSlackVars <= rows);
+      Contract.Assert(numInitialVars + numSlackVars + 1 == columns);
+      Contract.Assert(rhsColumn == columns - 1);
+      Contract.Assert(dims.Count == numInitialVars);
+      Contract.Assert(basisColumns.Length == rows);
+      Contract.Assert(inBasis.Length == numInitialVars + numSlackVars);
+
+      bool[] b = new bool[numInitialVars + numSlackVars];
+      int numColumnsInBasis = 0;
+      int numUninitializedRowInfo = 0;
+      for (int i = 0; i < rows; i++) {
+        int c = basisColumns[i];
+        if (c == rhsColumn) {
+          // all coefficients in this row are 0 (but the right-hand side may be non-0)
+          for (int j = 0; j < rhsColumn; j++) {
+            Contract.Assert(m[i, j].IsZero);
+          }
+          numColumnsInBasis++;
+        } else if (c == -1) {
+          Contract.Assert(!constructionDone);
+          numUninitializedRowInfo++;
+        } else {
+          // basis column is a column
+          Contract.Assert(0 <= c && c < numInitialVars + numSlackVars);
+          // basis column is unique
+          Contract.Assert(!b[c]);
+          b[c] = true;
+          // column is marked as being in basis
+          Contract.Assert(inBasis[c] == i);
+          // basis column really is a basis column
+          for (int j = 0; j < rows; j++) {
+            if (j == i) {
+              Contract.Assert(m[j, c].HasValue(1));// == (Rational)new Rational(1)));
+            } else {
+              Contract.Assert(m[j, c].IsZero);
+            }
+          }
+        }
+      }
+      // no other columns are marked as being in basis
+      foreach (int i in inBasis) {
+        if (0 <= i) {
+          Contract.Assert(i < rows);
+          numColumnsInBasis++;
+        } else {
+          Contract.Assert(i == -1);
+        }
+      }
+      Contract.Assert(rows - numUninitializedRowInfo <= numColumnsInBasis && numColumnsInBasis <= rows);
+      Contract.Assert(!constructionDone || numUninitializedRowInfo == 0);
+    }
+
+    /// <summary>
+    /// Constructs a matrix that represents the constraints "constraints", adding slack
+    /// variables for the inequalities among "constraints".  Puts the matrix in canonical
+    /// form.
+    /// </summary>
+    /// <param name="constraints"></param>
+    [NotDelayed]
+    public SimplexTableau(ArrayList /*LinearConstraint*//*!*/ constraints) {
+      Contract.Requires(constraints != null);
+#if DEBUG_PRINT
+            Console.WriteLine("DEBUG: SimplexTableau constructor called with:");
+            foreach (LinearConstraint lc in constraints)
+            {
+              Console.WriteLine("  {0}", lc);
+            }
+#endif
+      // Note:  This implementation is not particularly efficient, but it'll do for now.
+
+      ArrayList dims = this.dims = new ArrayList /*IVariable!*/ ();
+      int slacks = 0;
+      foreach (LinearConstraint/*!*/ cc in constraints) {
+        Contract.Assert(cc != null);
+        foreach (IVariable/*!*/ dim in cc.coefficients.Keys) {
+          Contract.Assert(dim != null);
+          if (!dims.Contains(dim)) {
+            dims.Add(dim);
+          }
+        }
+        if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
+          slacks++;
+        }
+      }
+
+      int numInitialVars = this.numInitialVars = dims.Count;
+      int numSlackVars = this.numSlackVars = slacks;
+      int rows = this.rows = constraints.Count;
+      int columns = this.columns = numInitialVars + numSlackVars + 1;
+      this.m = new Rational[rows, columns];
+      this.rhsColumn = columns - 1;
+      this.basisColumns = new int[rows];
+      this.inBasis = new int[columns - 1];
+
+      //:base();
+
+      for (int i = 0; i < inBasis.Length; i++) {
+        inBasis[i] = -1;
+      }
+
+      // Fill in the matrix
+      int r = 0;
+      int iSlack = 0;
+      foreach (LinearConstraint/*!*/ cc in constraints) {
+        Contract.Assert(cc != null);
+        for (int i = 0; i < dims.Count; i++) {
+          m[r, i] = cc[(IVariable)cce.NonNull(dims[i])];
+        }
+        if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
+          m[r, numInitialVars + iSlack] = Rational.ONE;
+          basisColumns[r] = numInitialVars + iSlack;
+          inBasis[numInitialVars + iSlack] = r;
+          iSlack++;
+        } else {
+          basisColumns[r] = -1;  // special value to communicate to Pivot that basis column i hasn't been set up yet
+        }
+        m[r, rhsColumn] = cc.rhs;
+        r++;
+      }
+      Contract.Assert(r == constraints.Count);
+      Contract.Assert(iSlack == numSlackVars);
+#if DEBUG_PRINT
+            Console.WriteLine("DEBUG: Intermediate tableau state in SimplexTableau constructor:");
+            Dump();
+#endif
+
+      // Go through the rows with uninitialized basis columns.  These correspond to equality constraints.
+      // For each one, find an initial variable (non-slack variable) whose column we can make the basis
+      // column of the row.
+      for (int i = 0; i < rows; i++) {
+        if (basisColumns[i] != -1) {
+          continue;
+        }
+        // Find a non-0 column in row i that we can make a basis column.  Since rows corresponding
+        // to equality constraints don't have slack variables and since the pivot operations performed
+        // by iterations of this loop don't introduce any non-0 coefficients in the slack-variable
+        // columns of these rows, we only need to look through the columns corresponding to initial
+        // variables.
+        for (int j = 0; j < numInitialVars; j++) {
+          if (m[i, j].IsNonZero) {
+#if DEBUG_PRINT
+                            Console.WriteLine("-- About to Pivot({0},{1})", i, j);
+#endif
+            Contract.Assert(inBasis[j] == -1);
+            Pivot(i, j);
+#if DEBUG_PRINT
+                            Console.WriteLine("Tableau after Pivot:");
+                            Dump();
+#endif
+            goto SET_UP_NEXT_INBASIS_COLUMN;
+          }
+        }
+        // Check the assertion in the comment above, that is, that columns corresponding to slack variables
+        // are 0 in this row.
+        for (int j = numInitialVars; j < rhsColumn; j++) {
+          Contract.Assert(m[i, j].IsZero);
+        }
+        // There is no column in this row that we can put into basis.
+        basisColumns[i] = rhsColumn;
+      SET_UP_NEXT_INBASIS_COLUMN: {
+        }
+      }
+
+      constructionDone = true;
+      CheckInvariant();
+    }
+
+    public IMutableSet/*!*/ /*IVariable!*/ GetDimensions() {
+      Contract.Ensures(Contract.Result<IMutableSet>() != null);
+      HashSet /*IVariable!*/ z = new HashSet /*IVariable!*/ ();
+      foreach (IVariable/*!*/ dim in dims) {
+        Contract.Assert(dim != null);
+        z.Add(dim);
+      }
+      return z;
+    }
+
+    public Rational this[int r, int c] {
+      get {
+        return m[r, c];
+      }
+      set {
+        m[r, c] = value;
+      }
+    }
+
+    /// <summary>
+    /// Applies the Pivot Operation on row "r" and column "c".
+    /// 
+    /// This method can be called when !constructionDone, that is, at a time when not all basis
+    /// columns have been set up (indicated by -1 in basisColumns).  This method helps set up
+    /// those basis columns.
+    /// 
+    /// The return value is an undo record that can be used with UnPivot.
+    /// </summary>
+    /// <param name="r"></param>
+    /// <param name="c"></param>
+    public Rational[]/*!*/ Pivot(int r, int c) {
+      Contract.Ensures(Contract.Result<Rational[]>() != null);
+      Contract.Assert(0 <= r && r < rows);
+      Contract.Assert(0 <= c && c < columns - 1);
+      Contract.Assert(m[r, c].IsNonZero);
+      Contract.Assert(inBasis[c] == -1);  // follows from invariant and m[r,c] != 0
+      Contract.Assert(basisColumns[r] != rhsColumn);  // follows from invariant and m[r,c] != 0
+
+      Rational[] undo = new Rational[rows + 1];
+      for (int i = 0; i < rows; i++) {
+        undo[i] = m[i, c];
+      }
+
+      // scale the pivot row
+      Rational q = m[r, c];
+      if (q != Rational.ONE) {
+        for (int j = 0; j < columns; j++) {
+          m[r, j] /= q;
+        }
+      }
+
+      // subtract a multiple of the pivot row from all other rows
+      for (int i = 0; i < rows; i++) {
+        if (i != r) {
+          q = m[i, c];
+          if (q.IsNonZero) {
+            for (int j = 0; j < columns; j++) {
+              m[i, j] -= q * m[r, j];
+            }
+          }
+        }
+      }
+
+      // update basis information
+      int prevCol = basisColumns[r];
+      undo[rows] = Rational.FromInt(prevCol);
+      basisColumns[r] = c;
+      if (prevCol != -1) {
+        inBasis[prevCol] = -1;
+      }
+      inBasis[c] = r;
+
+      return undo;
+    }
+
+    /// <summary>
+    /// If the last operation applied to the tableau was:
+    ///   undo = Pivot(i,j);
+    /// then UnPivot(i, j, undo) undoes the pivot operation.
+    /// Note:  This operation is not supported for any call to Pivot before constructionDone
+    /// is set to true.
+    /// </summary>
+    /// <param name="r"></param>
+    /// <param name="c"></param>
+    /// <param name="undo"></param>
+    void UnPivot(int r, int c, Rational[]/*!*/ undo) {
+      Contract.Requires(undo != null);
+      Contract.Assert(0 <= r && r < rows);
+      Contract.Assert(0 <= c && c < columns - 1);
+      Contract.Assert(m[r, c].HasValue(1));
+      Contract.Assert(undo.Length == rows + 1);
+
+      // add a multiple of the pivot row to all other rows
+      for (int i = 0; i < rows; i++) {
+        if (i != r) {
+          Rational q = undo[i];
+          if (q.IsNonZero) {
+            for (int j = 0; j < columns; j++) {
+              m[i, j] += q * m[r, j];
+            }
+          }
+        }
+      }
+
+      // scale the pivot row
+      Rational p = undo[r];
+      for (int j = 0; j < columns; j++) {
+        m[r, j] *= p;
+      }
+
+      // update basis information
+      int prevCol = undo[rows].AsInteger;
+      Contract.Assert(prevCol != -1);
+      basisColumns[r] = prevCol;
+      inBasis[c] = -1;
+      inBasis[prevCol] = r;
+    }
+
+    /// <summary>
+    /// Returns true iff the current basis of the system of constraints modeled by the simplex tableau
+    /// is feasible.  May have a side effect of performing a number of pivot operations on the tableau,
+    /// but any such pivot operation will be in the columns of slack variables (that is, this routine
+    /// does not change the set of initial-variable columns in basis).
+    /// 
+    /// CAVEAT: I have no particular reason to believe that the algorithm used here will terminate. --KRML
+    /// </summary>
+    /// <returns></returns>
+    public bool IsFeasibleBasis {
+      get {
+        // while there is a slack variable in basis whose row has a negative right-hand side
+        while (true) {
+          bool feasibleBasis = true;
+          for (int c = numInitialVars; c < rhsColumn; c++) {
+            int k = inBasis[c];
+            if (0 <= k && k < rhsColumn && m[k, rhsColumn].IsNegative) {
+              Contract.Assert(m[k, c].HasValue(1));  // c is in basis
+              // Try to pivot on a different slack variable in this row
+              for (int i = numInitialVars; i < rhsColumn; i++) {
+                if (m[k, i].IsNegative) {
+                  Contract.Assert(c != i);  // c is in basis, so m[k,c]==1, which is not negative
+                  Pivot(k, i);
+#if DEBUG_PRINT
+                  Console.WriteLine("Tableau after Pivot operation on ({0},{1}) in IsFeasibleBasis:", k, i);
+                  Dump();
+#endif
+                  Contract.Assert(inBasis[c] == -1);
+                  Contract.Assert(inBasis[i] == k);
+                  Contract.Assert(m[k, rhsColumn].IsNonNegative);
+                  goto START_ANEW;
+                }
+              }
+              feasibleBasis = false;
+            }
+          }
+          return feasibleBasis;
+        START_ANEW:
+          ;
+        }
+      }
+    }
+
+    /// <summary>
+    /// Whether or not all initial variables (the non-slack variables) are in basis)
+    /// </summary>
+    public bool AllInitialVarsInBasis {
+      get {
+        for (int i = 0; i < numInitialVars; i++) {
+          if (inBasis[i] == -1) {
+            return false;
+          }
+        }
+        return true;
+      }
+    }
+
+    /// <summary>
+    /// Adds as many initial variables as possible to the basis.
+    /// </summary>
+    /// <returns></returns>
+    public void AddInitialVarsToBasis() {
+      // while there exists an initial variable not in the basis and not satisfying
+      // condition 3.4.2.2 in Cousot and Halbwachs, perform a pivot operation
+      while (true) {
+        for (int i = 0; i < numInitialVars; i++) {
+          if (inBasis[i] == -1) {
+            // initial variable i is not in the basis
+            for (int j = 0; j < rows; j++) {
+              if (m[j, i].IsNonZero) {
+                int k = basisColumns[j];
+                if (numInitialVars <= k && k < rhsColumn) {
+                  // slack variable k is in basis for row j
+                  Pivot(j, i);
+                  Contract.Assert(inBasis[k] == -1);
+                  Contract.Assert(inBasis[i] == j && basisColumns[j] == i);
+                  goto START_ANEW;
+                }
+              }
+            }
+          }
+        }
+        // No more initial variables can be moved into basis.
+        return;
+      START_ANEW: {
+        }
+      }
+    }
+
+    /// <summary>
+    /// Adds to "lines" the lines implied by initial-variable columns not in basis
+    /// (see section 3.4.2 of Cousot and Halbwachs), and adds to "constraints" the
+    /// constraints to exclude those lines (see step 4.2 of section 3.4.3 of
+    /// Cousot and Halbwachs).
+    /// </summary>
+    /// <param name="lines"></param>
+    /// <param name="constraints"></param>
+    public void ProduceLines(ArrayList /*FrameElement*//*!*/ lines, ArrayList /*LinearConstraint*//*!*/ constraints) {
+      Contract.Requires(constraints != null);
+      Contract.Requires(lines != null);
+      // for every initial variable not in basis
+      for (int i0 = 0; i0 < numInitialVars; i0++) {
+        if (inBasis[i0] == -1) {
+          FrameElement fe = new FrameElement();
+          LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
+          for (int i = 0; i < numInitialVars; i++) {
+            if (i == i0) {
+              fe.AddCoordinate((IVariable)cce.NonNull(dims[i]), Rational.ONE);
+              lc.SetCoefficient((IVariable)cce.NonNull(dims[i]), Rational.ONE);
+            } else if (inBasis[i] != -1) {
+              // i is a basis column
+              Contract.Assert(m[inBasis[i], i].HasValue(1));
+              Rational val = -m[inBasis[i], i0];
+              fe.AddCoordinate((IVariable)cce.NonNull(dims[i]), val);
+              lc.SetCoefficient((IVariable)cce.NonNull(dims[i]), val);
+            }
+          }
+          lines.Add(fe);
+          constraints.Add(lc);
+        }
+      }
+    }
+
+    /// <summary>
+    /// From a feasible point where all initial variables are in the basis, traverses
+    /// all feasible bases containing all initial variables.  For each such basis, adds
+    /// the vertices to "vertices" and adds to "rays" the extreme rays.  See step 4.2
+    /// in section 3.4.3 of Cousot and Halbwachs.
+    /// A more efficient algorithm is found in the paper "An algorithm for
+    /// determining all extreme points of a convex polytope" by N. E. Dyer and L. G. Proll,
+    /// Mathematical Programming, 12, 1977.
+    /// Assumes that the tableau is in a state where all initial variables are in the basis.
+    /// This method has no net effect on the tableau.
+    /// Note: Duplicate vertices and rays may be added.
+    /// </summary>
+    /// <param name="vertices"></param>
+    /// <param name="rays"></param>
+    public void TraverseVertices(ArrayList/*!*/ /*FrameElement*/ vertices, ArrayList/*!*/ /*FrameElement*/ rays) {
+      Contract.Requires(vertices != null);
+      Contract.Requires(rays != null);
+      ArrayList /*bool[]*/ basesSeenSoFar = new ArrayList /*bool[]*/ ();
+      TraverseBases(basesSeenSoFar, vertices, rays);
+    }
+
+    /// <summary>
+    /// Worker method of TraverseVertices.
+    /// This method has no net effect on the tableau.
+    /// </summary>
+    /// <param name="basesSeenSoFar"></param>
+    /// <param name="vertices"></param>
+    /// <param name="rays"></param>
+    void TraverseBases(ArrayList /*bool[]*//*!*/ basesSeenSoFar, ArrayList /*FrameElement*//*!*/ vertices, ArrayList /*FrameElement*//*!*/ rays) {
+      Contract.Requires(rays != null);
+      Contract.Requires(vertices != null);
+      Contract.Requires(basesSeenSoFar != null);
+      CheckInvariant();
+
+      bool[] thisBasis = new bool[numSlackVars];
+      for (int i = numInitialVars; i < rhsColumn; i++) {
+        if (inBasis[i] != -1) {
+          thisBasis[i - numInitialVars] = true;
+        }
+      }
+      foreach (bool[]/*!*/ basis in basesSeenSoFar) {
+        Contract.Assert(basis != null);
+        Contract.Assert(basis.Length == numSlackVars);
+        for (int i = 0; i < numSlackVars; i++) {
+          if (basis[i] != thisBasis[i]) {
+            goto COMPARE_WITH_NEXT_BASIS;
+          }
+        }
+        // thisBasis and basis are the same--that is, basisColumns has been visited before--so
+        // we don't traverse anything from here
+        return;
+      COMPARE_WITH_NEXT_BASIS: {
+        }
+      }
+      // basisColumns has not been seen before; record thisBasis and continue with the traversal here
+      basesSeenSoFar.Add(thisBasis);
+
+#if DEBUG_PRINT
+      Console.Write("TraverseBases, new basis:  ");
+      foreach (bool t in thisBasis) {
+        Console.Write("{0}", t ? "*" : ".");
+      }
+      Console.WriteLine();
+      Dump();
+#endif
+      // Add vertex
+      FrameElement v = new FrameElement();
+      for (int i = 0; i < rows; i++) {
+        int j = basisColumns[i];
+        if (j < numInitialVars) {
+          v.AddCoordinate((IVariable)cce.NonNull(dims[j]), m[i, rhsColumn]);
+        }
+      }
+#if DEBUG_PRINT
+      Console.WriteLine("  Adding vertex: {0}", v);
+#endif
+      vertices.Add(v);
+
+      // Add rays.  Traverse all columns corresponding to slack variables that
+      // are not in basis (see second bullet of section 3.4.2 of Cousot and Halbwachs).
+      for (int i0 = numInitialVars; i0 < rhsColumn; i0++) {
+        if (inBasis[i0] != -1) {
+          // skip those slack-variable columns that are in basis
+          continue;
+        }
+        // check if slack-variable, non-basis column i corresponds to an extreme ray
+        for (int row = 0; row < rows; row++) {
+          if (m[row, i0].IsPositive) {
+            for (int k = numInitialVars; k < rhsColumn; k++) {
+              if (inBasis[k] != -1 && m[row, k].IsNonZero) {
+                // does not correspond to an extreme ray
+                goto CHECK_NEXT_SLACK_VAR;
+              }
+            }
+          }
+        }
+        // corresponds to an extreme ray
+        FrameElement ray = new FrameElement();
+        for (int i = 0; i < numInitialVars; i++) {
+          int j0 = inBasis[i];
+          Rational val = -m[j0, i0];
+          ray.AddCoordinate((IVariable)cce.NonNull(dims[i]), val);
+        }
+#if DEBUG_PRINT
+        Console.WriteLine("  Adding ray: {0}", ray);
+#endif
+        rays.Add(ray);
+      CHECK_NEXT_SLACK_VAR: {
+        }
+      }
+
+      // Continue traversal
+      for (int i = numInitialVars; i < rhsColumn; i++) {
+        int j = inBasis[i];
+        if (j != -1) {
+          // try moving i out of basis and some other slack-variable column into basis
+          for (int k = numInitialVars; k < rhsColumn; k++) {
+            if (inBasis[k] == -1 && m[j, k].IsPositive) {
+              Rational[] undo = Pivot(j, k);
+              // check if the new basis is feasible
+              for (int p = 0; p < rows; p++) {
+                int c = basisColumns[p];
+                if (numInitialVars <= c && c < rhsColumn && m[p, rhsColumn].IsNegative) {
+                  // not feasible
+                  goto AFTER_TRAVERSE;
+                }
+              }
+              TraverseBases(basesSeenSoFar, vertices, rays);
+            AFTER_TRAVERSE:
+              UnPivot(j, k, undo);
+            }
+          }
+        }
+      }
+    }
+
+    public void Dump() {
+      // names
+      Console.Write("      ");
+      for (int i = 0; i < numInitialVars; i++) {
+        Console.Write("  {0,4}   ", dims[i]);
+      }
+      Console.WriteLine();
+      // numbers
+      Console.Write("      ");
+      for (int i = 0; i < columns; i++) {
+        if (i == numInitialVars || i == rhsColumn) {
+          Console.Write("|");
+        }
+        Console.Write("  {0,4}", i);
+        if (i < rhsColumn && inBasis[i] != -1) {
+          Console.Write("*  ");
+          Contract.Assert(basisColumns[inBasis[i]] == i);
+        } else {
+          Console.Write("   ");
+        }
+      }
+      Console.WriteLine();
+      // line
+      Console.Write("      ");
+      for (int i = 0; i < columns; i++) {
+        if (i == numInitialVars || i == rhsColumn) {
+          Console.Write("+");
+        }
+        Console.Write("---------");
+      }
+      Console.WriteLine();
+
+      for (int j = 0; j < rows; j++) {
+        Console.Write("{0,4}: ", basisColumns[j]);
+        for (int i = 0; i < columns; i++) {
+          if (i == numInitialVars || i == rhsColumn) {
+            Console.Write("|");
+          }
+          Console.Write("  {0,4:n1}   ", m[j, i]);
+        }
+        Console.WriteLine();
+      }
+    }
+  }
+}