diff options
author | 2015-06-28 01:44:30 +0100 | |
---|---|---|
committer | 2015-06-28 01:44:30 +0100 | |
commit | 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch) | |
tree | 27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs | |
parent | e11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff) |
Normalise line endings using a .gitattributes file. Unfortunately
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
Diffstat (limited to 'Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs')
-rw-r--r-- | Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs | 1524 |
1 files changed, 762 insertions, 762 deletions
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; + } + } +} |