From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- .../AIFramework/Polyhedra/PolyhedraAbstraction.cs | 1524 ++++++++++---------- 1 file changed, 762 insertions(+), 762 deletions(-) (limited to 'Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs') 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; - using HashSet = Microsoft.Boogie.GSet; - - /// - /// Represents an invariant over linear variable constraints, represented by a polyhedron. - /// - 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); - } - - - /// - /// Creates a top or bottom elements, according to parameter "top". - /// - 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() != 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/*!*/ FreeVariables() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return lcs.FreeVariables(); - } - - public PolyhedraLatticeElement(LinearConstraintSystem/*!*/ lcs) { - Contract.Requires(lcs != null); - this.lcs = lcs; - } - - public override Element/*!*/ Clone() { - Contract.Ensures(Contract.Result() != 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() != null); - return new PolyhedraLatticeElement(true); - } - } - - public override Element/*!*/ Bottom { - get { - Contract.Ensures(Contract.Result() != 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(); - } - - - /// - /// Returns true iff a is a subset of this. - /// - /// - /// - 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() != null); - return ((PolyhedraLatticeElement)e).lcs.ToString(); - } - - public override IExpr/*!*/ ToPredicate(Element/*!*/ element) { - //Contract.Requires(element != null); - Contract.Ensures(Contract.Result() != 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() != 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() != 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() != 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() != 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() != 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/**//*!*/ 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() != null); - return Prop.Not; - } - } - - public IList/**//*!*/ Arguments { - get { - Contract.Ensures(Contract.Result() != null); - - IExpr[] args = new IExpr[] { arg }; - return ArrayList.ReadOnly(args); - } - } - - public IFunApp/*!*/ CloneWithArguments(IList/**//*!*/ args) { - //Contract.Requires(args != null); - Contract.Ensures(Contract.Result() != 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/**//*!*/ 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() != 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 - - - /// - /// A LinearCondition follows this grammar: - /// LinearCondition ::= unsatisfiable - /// | LinearConstraint - /// | ! LinearConstraint - /// Note that negations are distributed to the leaves. - /// - /// - [ContractClass(typeof(LinearConditionContracts))] - abstract class LinearCondition { - /// - /// Adds constraints to the list "clist". If "this" - /// entails some disjunctive constraints, they may not be added. - /// - /// - 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); - } - - /// - /// Precondition: positive || constraint.Relation == LinearConstraint.ConstraintRelation.EQ - /// - /// - /// - 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 { - /// - /// Builds a linear condition from "e", if possible; returns null if not possible. - /// - /// - /// - 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); - } - - /// - /// Builds a linear expression from "e", if possible; returns null if not possible. - /// - /// - /// - 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; - } - } - } - - /// - /// Adds "x" to "this". - /// - /// - public void AddConstant(BigNum x) /* throws ArithmeticException */ - { - checked { - constant += x; - } - } - - /// - /// Adds "le" to "this". Afterwards, "le" should not be used, because it will have been destroyed. - /// - /// - 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; + using HashSet = Microsoft.Boogie.GSet; + + /// + /// Represents an invariant over linear variable constraints, represented by a polyhedron. + /// + 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); + } + + + /// + /// Creates a top or bottom elements, according to parameter "top". + /// + 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() != 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/*!*/ FreeVariables() { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return lcs.FreeVariables(); + } + + public PolyhedraLatticeElement(LinearConstraintSystem/*!*/ lcs) { + Contract.Requires(lcs != null); + this.lcs = lcs; + } + + public override Element/*!*/ Clone() { + Contract.Ensures(Contract.Result() != 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() != null); + return new PolyhedraLatticeElement(true); + } + } + + public override Element/*!*/ Bottom { + get { + Contract.Ensures(Contract.Result() != 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(); + } + + + /// + /// Returns true iff a is a subset of this. + /// + /// + /// + 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() != null); + return ((PolyhedraLatticeElement)e).lcs.ToString(); + } + + public override IExpr/*!*/ ToPredicate(Element/*!*/ element) { + //Contract.Requires(element != null); + Contract.Ensures(Contract.Result() != 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() != 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() != 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() != 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() != 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() != 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/**//*!*/ 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() != null); + return Prop.Not; + } + } + + public IList/**//*!*/ Arguments { + get { + Contract.Ensures(Contract.Result() != null); + + IExpr[] args = new IExpr[] { arg }; + return ArrayList.ReadOnly(args); + } + } + + public IFunApp/*!*/ CloneWithArguments(IList/**//*!*/ args) { + //Contract.Requires(args != null); + Contract.Ensures(Contract.Result() != 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/**//*!*/ 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() != 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 + + + /// + /// A LinearCondition follows this grammar: + /// LinearCondition ::= unsatisfiable + /// | LinearConstraint + /// | ! LinearConstraint + /// Note that negations are distributed to the leaves. + /// + /// + [ContractClass(typeof(LinearConditionContracts))] + abstract class LinearCondition { + /// + /// Adds constraints to the list "clist". If "this" + /// entails some disjunctive constraints, they may not be added. + /// + /// + 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); + } + + /// + /// Precondition: positive || constraint.Relation == LinearConstraint.ConstraintRelation.EQ + /// + /// + /// + 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 { + /// + /// Builds a linear condition from "e", if possible; returns null if not possible. + /// + /// + /// + 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); + } + + /// + /// Builds a linear expression from "e", if possible; returns null if not possible. + /// + /// + /// + 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; + } + } + } + + /// + /// Adds "x" to "this". + /// + /// + public void AddConstant(BigNum x) /* throws ArithmeticException */ + { + checked { + constant += x; + } + } + + /// + /// Adds "le" to "this". Afterwards, "le" should not be used, because it will have been destroyed. + /// + /// + 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; + } + } +} -- cgit v1.2.3