diff options
Diffstat (limited to 'Source/AIFramework/Polyhedra/LinearConstraint.ssc')
| -rw-r--r-- | Source/AIFramework/Polyhedra/LinearConstraint.ssc | 588 |
1 files changed, 588 insertions, 0 deletions
diff --git a/Source/AIFramework/Polyhedra/LinearConstraint.ssc b/Source/AIFramework/Polyhedra/LinearConstraint.ssc new file mode 100644 index 00000000..9ce1552b --- /dev/null +++ b/Source/AIFramework/Polyhedra/LinearConstraint.ssc @@ -0,0 +1,588 @@ +//-----------------------------------------------------------------------------
+//
+// 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
+ }
+
+ public readonly ConstraintRelation Relation;
+ internal Hashtable /*IVariable->Rational*/! coefficients = new Hashtable /*IVariable->Rational*/ ();
+ internal Rational rhs;
+
+ public LinearConstraint (ConstraintRelation rel)
+ {
+ Relation = rel;
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ 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;
+ }
+
+
+#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)
+ {
+ IExpr leftSum = null;
+ IExpr rightSum = null;
+ foreach (DictionaryEntry /*object->Rational*/ entry in coefficients)
+ {
+ IVariable var = (IVariable)entry.Key;
+ Rational coeff = (Rational) ((!)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);
+ }
+
+ assert leftSum != null;
+ 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)
+ {
+ IExpr! product = factory.Term(r, x);
+ if (sum == null) {
+ return product;
+ } else {
+ return factory.Add(sum, product);
+ }
+ }
+
+ 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>
+ /// 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)
+ {
+ // "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);
+
+ // 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) ((!)entry.Value);
+ }
+ b.rhs = -this.rhs;
+ }
+
+ public void SetCoefficient(IVariable! dimension, Rational coefficient)
+ {
+ 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)
+ {
+#if FIXED_SERIALIZER
+ 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); }
+ }
+
+ public LinearConstraint Rename(IVariable! oldName, IVariable! newName)
+ {
+ 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*/)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)
+ {
+ 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()
+ {
+ LinearConstraint z = new LinearConstraint(ConstraintRelation.LE);
+ foreach (DictionaryEntry /*IVariable->Rational*/ entry in this.coefficients)
+ {
+ z.coefficients.Add(entry.Key, -(Rational) ((!)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;
+ }
+
+ /// <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)
+ {
+ 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>
+ /// 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
+ {
+
+ 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)
+ {
+ terms.Add(dimension, value);
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ 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 + ")";
+ }
+
+ 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;
+ }
+
+ /// <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 FrameElement Rename(IVariable! oldName, IVariable! newName)
+ {
+ 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*/)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;
+ }
+ }
+}
|