summaryrefslogtreecommitdiff
path: root/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs')
-rw-r--r--Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs1524
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;
+ }
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 06:19:13 +0000