diff options
Diffstat (limited to 'Source/AIFramework/Polyhedra/LinearConstraint.cs')
| -rw-r--r-- | Source/AIFramework/Polyhedra/LinearConstraint.cs | 1088 |
1 files changed, 544 insertions, 544 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 <= 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) {
- 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 <= 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>
- /// 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 <= 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) { + 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 <= 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> + /// 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; + } + } +} |