diff options
Diffstat (limited to 'Source/AIFramework/Polyhedra/LinearConstraint.cs')
| -rw-r--r-- | Source/AIFramework/Polyhedra/LinearConstraint.cs | 788 |
1 files changed, 372 insertions, 416 deletions
diff --git a/Source/AIFramework/Polyhedra/LinearConstraint.cs b/Source/AIFramework/Polyhedra/LinearConstraint.cs index 087c3696..ce5c23a2 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraint.cs +++ b/Source/AIFramework/Polyhedra/LinearConstraint.cs @@ -3,59 +3,55 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-using Microsoft.Contracts;
-namespace Microsoft.AbstractInterpretationFramework
-{
- using System;
- using System.Compiler;
- using System.Collections;
- using Microsoft.Basetypes;
- using IMutableSet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
- using ISet = Microsoft.Boogie.Set;
-
-
- /// <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
- }
+using System.Diagnostics.Contracts;
+namespace Microsoft.AbstractInterpretationFramework {
+ using System;
+ //using System.Compiler;
+ using System.Collections;
+ using Microsoft.Basetypes;
+ using IMutableSet = Microsoft.Boogie.Set;
+ using HashSet = Microsoft.Boogie.Set;
+ using ISet = Microsoft.Boogie.Set;
+
+
+ /// <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 readonly ConstraintRelation Relation;
+ internal Hashtable /*IVariable->Rational*//*!*/ coefficients = new Hashtable /*IVariable->Rational*/ ();
+ internal Rational rhs;
- public LinearConstraint (ConstraintRelation rel)
- {
- Relation = rel;
- }
+ public LinearConstraint(ConstraintRelation rel) {
+ Relation = rel;
+ }
- [Pure]
- public override string! ToString()
- {
- 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;
+ [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
@@ -79,51 +75,42 @@ namespace Microsoft.AbstractInterpretationFramework /// not required elsewhere in this class.
/// </summary>
/// <returns></returns>
- public IExpr! ConvertToExpression(ILinearExprFactory! factory)
- {
+ 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)
- {
+ foreach (DictionaryEntry /*object->Rational*/ entry in coefficients) {
IVariable var = (IVariable)entry.Key;
- Rational coeff = (Rational) ((!)entry.Value);
- if (coeff.IsPositive)
- {
+ Rational coeff = (Rational)(cce.NonNull(entry.Value));
+ if (coeff.IsPositive) {
leftSum = AddTerm(factory, leftSum, coeff, var);
- }
- else if (coeff.IsNegative)
- {
+ } else if (coeff.IsNegative) {
rightSum = AddTerm(factory, rightSum, -coeff, var);
- }
- else
- {
+ } else {
// ignore the term is coeff==0
}
}
- if (leftSum == null && rightSum == null)
- {
+ if (leftSum == null && rightSum == null) {
// there are no variables in this constraint
if (Relation == ConstraintRelation.EQ ? rhs.IsZero : rhs.IsNonNegative) {
- return factory.True;
+ return factory.True;
} else {
- return factory.False;
+ return factory.False;
}
}
- if (leftSum == null || (rightSum != null && rhs.IsNegative))
- {
+ 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)
- {
+ } else if (rightSum == null || rhs.IsPositive) {
// show the constant on the right side
rightSum = AddTerm(factory, rightSum, rhs, null);
}
- assert leftSum != null;
- assert rightSum != null;
+ Contract.Assert(leftSum != null);
+ Contract.Assert(rightSum != null);
return Relation == ConstraintRelation.EQ ? factory.Eq(leftSum, rightSum) : factory.AtMost(leftSum, rightSum);
}
@@ -137,198 +124,189 @@ namespace Microsoft.AbstractInterpretationFramework /// <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)
- {
- IExpr! product = factory.Term(r, x);
+ 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;
+ }
- public ISet /*IVariable!*/! GetDefinedDimensions()
- {
- HashSet /*IVariable!*/ dims = new HashSet /*IVariable!*/ (coefficients.Count);
- int j = 0;
- foreach (IVariable! dim in coefficients.Keys)
- {
- 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 <= 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>
+ /// Returns true iff all of the coefficients in the constraint are 0. In that
+ /// case, the constraint has the form 0 <= 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 <= rhs.
/// </summary>
- public bool IsConstantSatisfiable()
- {
- if (Relation == ConstraintRelation.EQ)
- {
+ public bool IsConstantSatisfiable() {
+ if (Relation == ConstraintRelation.EQ) {
return rhs.IsZero;
- }
- else
- {
+ } 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)
- {
- // "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())
- {
- if (!dd.Contains(d)) { dd.Add(d); }
- }
- foreach (IVariable! d in c.GetDefinedDimensions())
- {
- if (!dd.Contains(d)) { dd.Add(d); }
- }
-
- foreach (IVariable! d in dd)
- {
- 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);
+ /// <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);
+ }
+ }
- // finally, check the rhs
- if (this.rhs == m * c.rhs)
- {
- return m; // equivalent
- }
- else
- {
- return Rational.ZERO; // not equivalent
- }
+ 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
}
+ }
- /// <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);
+ // we expect there to have been some non-zero coefficient, so "m" should have been used by now
+ System.Diagnostics.Debug.Assert(m.IsNonZero);
- a = new LinearConstraint(ConstraintRelation.LE);
- a.coefficients = (Hashtable)this.coefficients.Clone();
- a.rhs = this.rhs;
+ // finally, check the rhs
+ if (this.rhs == m * c.rhs) {
+ return m; // equivalent
+ } else {
+ return Rational.ZERO; // not equivalent
+ }
+ }
- b = new LinearConstraint(ConstraintRelation.LE);
- b.coefficients = new Hashtable /*IVariable->Rational*/ ();
- foreach (DictionaryEntry entry in this.coefficients)
- {
- b.coefficients[entry.Key] = -(Rational) ((!)entry.Value);
- }
- b.rhs = -this.rhs;
- }
+ /// <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)
- {
- coefficients[dimension] = coefficient;
- }
+ 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)
- {
- object val = coefficients[dim];
- if (val != null)
- {
+ /// <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
- assert ((Rational)val).IsZero;
-#endif
- coefficients.Remove(dim);
- }
- }
+ 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
- {
- object z = coefficients[dimension];
- if (z == null)
- {
- return Rational.ZERO;
- }
- else
- {
- return (Rational)z;
- }
- }
- set { SetCoefficient(dimension, value); }
+ /// <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)
- {
+ public LinearConstraint Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+ Contract.Requires(newName != null);
+ Contract.Requires(oldName != null);
object /*Rational*/ z = coefficients[oldName];
- if (z == null)
- {
+ if (z == null) {
return this;
- }
- else
- {
+ } else {
System.Diagnostics.Debug.Assert(z is Rational);
- Hashtable /*IVariable->Rational*/ newCoeffs = (Hashtable! /*IVariable->Rational*/)coefficients.Clone();
+ Hashtable /*IVariable->Rational*/ newCoeffs = (Hashtable/*!*/ /*IVariable->Rational*/)cce.NonNull(coefficients.Clone());
newCoeffs.Remove(oldName);
newCoeffs.Add(newName, z);
@@ -339,26 +317,22 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- public LinearConstraint Clone()
- {
- LinearConstraint z = new LinearConstraint(Relation);
- z.coefficients = (Hashtable /*IVariable->Rational*/)this.coefficients.Clone();
- z.rhs = this.rhs;
- return z;
- }
+ 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)
- {
- if (Relation == rel)
- {
+ public LinearConstraint/*!*/ ChangeRelation(ConstraintRelation rel) {
+ Contract.Ensures(Contract.Result<LinearConstraint>() != null);
+ if (Relation == rel) {
return this;
- }
- else
- {
+ } else {
LinearConstraint z = new LinearConstraint(rel);
z.coefficients = (Hashtable)this.coefficients.Clone();
z.rhs = this.rhs;
@@ -370,38 +344,36 @@ namespace Microsoft.AbstractInterpretationFramework /// Returns a constraint like "this", but, conceptually, with the inequality relation >=.
/// </summary>
/// <returns></returns>
- public LinearConstraint! ChangeRelationToAtLeast()
- {
+ 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) ((!)entry.Value));
+ 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)
- {
- Rational q = Rational.ZERO;
- foreach (DictionaryEntry /*IVariable,Rational*/ term in coefficients)
- {
- IVariable dim = (IVariable!)term.Key;
- Rational a = (Rational) ((!)term.Value);
- Rational x = v[dim];
- q += a * x;
- }
- return q;
- }
+ /// 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.
@@ -409,166 +381,151 @@ namespace Microsoft.AbstractInterpretationFramework /// <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)
- {
+ 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 <= B into (A + m*aa)*X <= B + m*bb,
- /// where "cc" is the constraint aa*X <= bb.
- /// </summary>
- /// <param name="m"></param>
- /// <param name="cc"></param>
- /// <returns></returns>
- public void AddMultiple(Rational m, LinearConstraint! cc)
- {
- foreach (DictionaryEntry /*IVariable->Rational*/ entry in cc.coefficients)
- {
- IVariable dim = (IVariable)entry.Key;
- Rational d = m * (Rational) ((!)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) ((!)e.Value);
- if (r.IsNonZero) {
- newCoefficients.Add(e.Key, new Rational(r.Numerator / gcd.Numerator, r.Denominator / gcd.Denominator));
- } else {
- newCoefficients.Add(e.Key, r);
- }
- }
-
- coefficients = newCoefficients;
- rhs = rhs.IsNonZero ? (Rational)new Rational(rhs.Numerator / gcd.Numerator, rhs.Denominator / gcd.Denominator) : rhs;
+ /// <summary>
+ /// Changes the current constraint A*X <= B into (A + m*aa)*X <= B + m*bb,
+ /// where "cc" is the constraint aa*X <= 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>
- /// Represents a frame element (vector of dimension/value tuples). Used only
- /// internally in class LinearConstraintSystem and its communication with class
- /// LinearConstraint.
+ /// 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 class FrameElement
- {
+ 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, new Rational(r.Numerator / gcd.Numerator, r.Denominator / gcd.Denominator));
+ } else {
+ newCoefficients.Add(e.Key, r);
+ }
+ }
- Hashtable /*IVariable->Rational*/! terms = new Hashtable /*IVariable->Rational*/ ();
+ coefficients = newCoefficients;
+ rhs = rhs.IsNonZero ? (Rational)new Rational(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);
+ }
- /// <summary>
- /// Constructs an empty FrameElement. To add dimensions, call AddCoordinate after construction.
- /// </summary>
- public FrameElement()
- {
- }
+ Hashtable /*IVariable->Rational*//*!*/ terms = new Hashtable /*IVariable->Rational*/ ();
- /// <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)
- {
- terms.Add(dimension, value);
- }
+ /// <summary>
+ /// Constructs an empty FrameElement. To add dimensions, call AddCoordinate after construction.
+ /// </summary>
+ public FrameElement() {
+ }
- [Pure]
- public override string! ToString()
- {
- string s = null;
- foreach (DictionaryEntry item in terms)
- {
- if (s == null)
- {
- s = "(";
- }
- else
- {
- s += ", ";
- }
- s += String.Format("<{0},{1}>", item.Key, (Rational) ((!)item.Value));
- }
- if (s == null)
- {
- s = "(";
- }
- return s + ")";
- }
+ /// <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);
+ }
- public IMutableSet /*IVariable!*/! GetDefinedDimensions()
- {
- HashSet /*IVariable!*/! dims = new HashSet /*IVariable!*/ (terms.Count);
- foreach (IVariable! dim in terms.Keys)
- {
- dims.Add(dim);
- }
- System.Diagnostics.Debug.Assert(dims.Count == terms.Count);
- return dims;
+ [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 + ")";
+ }
- /// <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
- {
- object z = terms[dimension];
- if (z == null)
- {
- return Rational.ZERO;
- }
- else
- {
- return (Rational)z;
- }
- }
- set
- {
- terms[dimension] = value;
- }
+ 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)
- {
+ public FrameElement Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+ Contract.Requires(newName != null);
+ Contract.Requires(oldName != null);
object /*Rational*/ z = terms[oldName];
- if (z == null)
- {
+ if (z == null) {
return this;
- }
- else
- {
+ } else {
System.Diagnostics.Debug.Assert(z is Rational);
- Hashtable /*IVariable->Rational*/ newTerms = (Hashtable! /*IVariable->Rational*/)terms.Clone();
+ Hashtable /*IVariable->Rational*/ newTerms = (Hashtable/*!*/ /*IVariable->Rational*/)cce.NonNull(terms.Clone());
newTerms.Remove(oldName);
newTerms.Add(newName, z);
@@ -578,11 +535,10 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- public FrameElement Clone()
- {
- FrameElement z = new FrameElement();
- z.terms = (Hashtable /*IVariable->Rational*/)this.terms.Clone();
- return z;
- }
+ public FrameElement Clone() {
+ FrameElement z = new FrameElement();
+ z.terms = (Hashtable /*IVariable->Rational*/)this.terms.Clone();
+ return z;
}
+ }
}
|