//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using Microsoft.Contracts;
namespace Microsoft.AbstractInterpretationFramework
{
    using System;
    using System.Compiler;
    using System.Collections;
    using Microsoft.Basetypes;
    using IMutableSet = Microsoft.Boogie.Set;
    using HashSet = Microsoft.Boogie.Set;
    using ISet = Microsoft.Boogie.Set;


    /// <summary>
    /// Represents a single linear constraint, coefficients are stored as Rationals.
    /// </summary>
    public class LinearConstraint 
    {

        public enum ConstraintRelation 
        {
            EQ,    // equal
            LE,    // less-than or equal
        }

        public readonly ConstraintRelation Relation;
        internal Hashtable /*IVariable->Rational*/! coefficients = new Hashtable /*IVariable->Rational*/ ();
        internal Rational rhs;

        public LinearConstraint (ConstraintRelation rel) 
        {
            Relation = rel;
        }

        [Pure]
        public override string! ToString() 
        {
            string s = null;
            foreach (DictionaryEntry /*IVariable->Rational*/ entry in coefficients) 
            {
                if (s == null) 
                {
                    s = "";
                } 
                else 
                {
                    s += " + ";
                }
                s += String.Format("{0}*{1}", entry.Value, entry.Key);
            }
            System.Diagnostics.Debug.Assert(s != null, "malformed LinearConstraint: no variables");
            s += String.Format(" {0} {1}", Relation == ConstraintRelation.EQ ? "==" : "<=", rhs);
            return s;
        }


#if DONT_KNOW_HOW_TO_TAKE_THE_TYPE_OF_AN_IVARIABLE_YET
        public bool IsOverIntegers 
        {
            get
            {
                foreach (DictionaryEntry /*IVariable->Rational*/ entry in coefficients) 
                {
                    IVariable var = (IVariable)entry.Key;
                    if ( ! var.TypedIdent.Type.IsInt) { return false; }
                }
                return true;
            }
        }
#endif


    /// <summary>
    /// Note: This method requires that all dimensions are of type Variable, something that's
    /// not required elsewhere in this class.
    /// </summary>
    /// <returns></returns>
    public IExpr! ConvertToExpression(ILinearExprFactory! factory)
    {
      IExpr leftSum = null;
      IExpr rightSum = null;
      foreach (DictionaryEntry /*object->Rational*/ entry in coefficients) 
      {
        IVariable var = (IVariable)entry.Key;
        Rational coeff = (Rational) ((!)entry.Value);
        if (coeff.IsPositive)
        {
          leftSum = AddTerm(factory, leftSum, coeff, var);
        }
        else if (coeff.IsNegative)
        {
          rightSum = AddTerm(factory, rightSum, -coeff, var);
        }
        else
        {
          // ignore the term is coeff==0
        }
      }

      if (leftSum == null && rightSum == null)
      {
        // there are no variables in this constraint
        if (Relation == ConstraintRelation.EQ ? rhs.IsZero : rhs.IsNonNegative) {
            return factory.True;
        } else {
            return factory.False;
        }
      }

      if (leftSum == null || (rightSum != null && rhs.IsNegative))
      {
        // show the constant on the left side
        leftSum = AddTerm(factory, leftSum, -rhs, null);
      } 
      else if (rightSum == null || rhs.IsPositive)
      {
        // show the constant on the right side
        rightSum = AddTerm(factory, rightSum, rhs, null);
      }

      assert leftSum != null;
      assert rightSum != null;
      return Relation == ConstraintRelation.EQ ? factory.Eq(leftSum, rightSum) : factory.AtMost(leftSum, rightSum);
    }

    /// <summary>
    /// Returns an expression that denotes sum + r*x.
    /// If sum==null, drops the "sum +".
    /// If x==null, drops the "*x".
    /// if x!=null and r==1, drops the "r*".
    /// </summary>
    /// <param name="factory"></param>
    /// <param name="sum"></param>
    /// <param name="r"></param>
    /// <param name="x"></param>
    static IExpr! AddTerm(ILinearExprFactory! factory, /*MayBeNull*/ IExpr sum, Rational r, /*MayBeNull*/ IVariable x)
    {
      IExpr! product = factory.Term(r, x);
      if (sum == null) {
        return product;
      } else {
        return factory.Add(sum, product);
      }
    }

        public ISet /*IVariable!*/! GetDefinedDimensions() 
        {
            HashSet /*IVariable!*/ dims = new HashSet /*IVariable!*/ (coefficients.Count);
            int j = 0;
            foreach (IVariable! dim in coefficients.Keys) 
            {
                dims.Add(dim);
                j++;
            }
            System.Diagnostics.Debug.Assert(j == coefficients.Count);
            return dims;
        }

        /// <summary>
        /// Returns true iff all of the coefficients in the constraint are 0.  In that
        /// case, the constraint has the form 0 &lt;= C for some constant C; hence, the
        /// constraint is either unsatisfiable or trivially satisfiable.
        /// </summary>
        /// <returns></returns>
        public bool IsConstant() 
        {
            foreach (Rational coeff in coefficients.Values) 
            {
                if (coeff.IsNonZero) 
                {
                    return false;
                }
            }
            return true;
        }

    /// <summary>
    /// For an equality constraint, returns 0 == rhs.
    /// For an inequality constraint, returns 0 &lt;= rhs.
    /// </summary>
    public bool IsConstantSatisfiable()
    {
      if (Relation == ConstraintRelation.EQ)
      {
        return rhs.IsZero;
      }
      else
      {
        return rhs.IsNonNegative;
      }
    }

        /// <summary>
        /// Returns 0 if "this" and "c" are not equivalent constraints.  If "this" and "c"
        /// are equivalent constraints, the non-0 return value "m" satisfies "this == m*c".
        /// </summary>
        /// <param name="c"></param>
        /// <returns></returns>
        public Rational IsEquivalent(LinearConstraint! c) 
        {
            // "m" is the scale factor.  If it is 0, it hasn't been used yet.  If it
            // is non-0, it will remain that value throughout, and it then says that
            // for every dimension "d", "this[d] == m * c[d]".
            Rational m = Rational.ZERO;

            ArrayList /*IVariable*/ dd = new ArrayList /*IVariable*/ ();
            foreach (IVariable! d in this.GetDefinedDimensions()) 
            {
                if (!dd.Contains(d)) { dd.Add(d); }
            }
            foreach (IVariable! d in c.GetDefinedDimensions()) 
            {
                if (!dd.Contains(d)) { dd.Add(d); }
            }

            foreach (IVariable! d in dd) 
            {
                Rational a = this[d];
                Rational b = c[d];

                if (a.IsZero || b.IsZero) 
                {
                    if (a.IsNonZero || b.IsNonZero) 
                    {
                        return Rational.ZERO;  // not equivalent
                    }
                } 
                else if (m.IsZero) 
                {
                    m = a / b;
                } 
                else if (a != m * b) 
                {
                    return Rational.ZERO;  // not equivalent
                }
            }

            // we expect there to have been some non-zero coefficient, so "m" should have been used by now
            System.Diagnostics.Debug.Assert(m.IsNonZero);

            // finally, check the rhs
            if (this.rhs == m * c.rhs) 
            {
                return m;  // equivalent
            } 
            else 
            {
                return Rational.ZERO;  // not equivalent
            }
        }

        /// <summary>
        /// Splits an equality constraint into two inequality constraints, the conjunction of
        /// which equals the equality constraint.  Assumes "this" is a equality constraint.
        /// </summary>
        /// <param name="a"></param>
        /// <param name="b"></param>
        public void GenerateInequalityConstraints(out LinearConstraint a, out LinearConstraint b) 
        {
            System.Diagnostics.Debug.Assert(this.Relation == ConstraintRelation.EQ);

            a = new LinearConstraint(ConstraintRelation.LE);
            a.coefficients = (Hashtable)this.coefficients.Clone();
            a.rhs = this.rhs;

            b = new LinearConstraint(ConstraintRelation.LE);
            b.coefficients = new Hashtable /*IVariable->Rational*/ ();
            foreach (DictionaryEntry entry in this.coefficients) 
            {
                b.coefficients[entry.Key] = -(Rational) ((!)entry.Value);
            }
            b.rhs = -this.rhs;
        }

        public void SetCoefficient(IVariable! dimension, Rational coefficient) 
        {
            coefficients[dimension] = coefficient;
        }

        /// <summary>
        /// Removes dimension "dim" from the constraint.  Only dimensions with coefficient 0 can
        /// be removed.
        /// </summary>
        /// <param name="dim"></param>
        public void RemoveDimension(IVariable! dim) 
        {
            object val = coefficients[dim];
            if (val != null) 
            {
#if FIXED_SERIALIZER            
                assert ((Rational)val).IsZero;
#endif                
                coefficients.Remove(dim);
            }
        }

        /// <summary>
        /// The getter returns 0 if the dimension is not present.
        /// </summary>
        public Rational this [IVariable! dimension] 
        {
            get 
            {
                object z = coefficients[dimension];
                if (z == null) 
                {
                    return Rational.ZERO;
                } 
                else 
                {
                    return (Rational)z;
                }
            }
            set { SetCoefficient(dimension, value); }
        }

    public LinearConstraint Rename(IVariable! oldName, IVariable! newName)
    {
      object /*Rational*/ z = coefficients[oldName];
      if (z == null)
      {
        return this;
      }
      else
      {
        System.Diagnostics.Debug.Assert(z is Rational);
        Hashtable /*IVariable->Rational*/ newCoeffs = (Hashtable! /*IVariable->Rational*/)coefficients.Clone();
        newCoeffs.Remove(oldName);
        newCoeffs.Add(newName, z);

        LinearConstraint lc = new LinearConstraint(this.Relation);
        lc.coefficients = newCoeffs;
        lc.rhs = this.rhs;
        return lc;
      }
    }

        public LinearConstraint Clone() 
        {
            LinearConstraint z = new LinearConstraint(Relation);
            z.coefficients = (Hashtable /*IVariable->Rational*/)this.coefficients.Clone();
            z.rhs = this.rhs;
            return z;
        }

    /// <summary>
    /// Returns a constraint like "this", but with the given relation "r".
    /// </summary>
    /// <returns></returns>
    public LinearConstraint! ChangeRelation(ConstraintRelation rel) 
    {
      if (Relation == rel)
      {
        return this;
      }
      else
      {
        LinearConstraint z = new LinearConstraint(rel);
        z.coefficients = (Hashtable)this.coefficients.Clone();
        z.rhs = this.rhs;
        return z;
      }
    }

    /// <summary>
    /// Returns a constraint like "this", but, conceptually, with the inequality relation >=.
    /// </summary>
    /// <returns></returns>
    public LinearConstraint! ChangeRelationToAtLeast()
    {
      LinearConstraint z = new LinearConstraint(ConstraintRelation.LE);
      foreach (DictionaryEntry /*IVariable->Rational*/ entry in this.coefficients)
      {
        z.coefficients.Add(entry.Key, -(Rational) ((!)entry.Value));
      }
      z.rhs = -this.rhs;
      return z;
    }

    /// <summary>
        /// Returns the left-hand side of the constraint evaluated at the point "v".
        /// Any coordinate not present in "v" is treated as if it were 0.
        /// Stated differently, this routine treats the left-hand side of the constraint
        /// as a row vector and "v" as a column vector, and then returns the dot-product
        /// of the two.
        /// </summary>
        /// <param name="v"></param>
        /// <returns></returns>
        public Rational EvaluateLhs(FrameElement! v) 
        {
            Rational q = Rational.ZERO;
            foreach (DictionaryEntry /*IVariable,Rational*/ term in coefficients) 
            {
                IVariable dim = (IVariable!)term.Key;
                Rational a = (Rational) ((!)term.Value);
                Rational x = v[dim];
                q += a * x;
            }
            return q;
        }

    /// <summary>
    /// Determines whether or not a given vertex or ray saturates the constraint.
    /// </summary>
    /// <param name="fe"></param>
    /// <param name="vertex">true if "fe" is a vertex; false if "fe" is a ray</param>
    /// <returns></returns>
    public bool IsSaturatedBy(FrameElement! fe, bool vertex)
    {
      Rational lhs = EvaluateLhs(fe);
      Rational rhs = vertex ? this.rhs : Rational.ZERO;
      return lhs == rhs;
    }

        /// <summary>
        /// Changes the current constraint A*X &lt;= B into (A + m*aa)*X &lt;= B + m*bb,
        /// where "cc" is the constraint aa*X &lt;= bb.
        /// </summary>
        /// <param name="m"></param>
        /// <param name="cc"></param>
        /// <returns></returns>
        public void AddMultiple(Rational m, LinearConstraint! cc) 
        {
            foreach (DictionaryEntry /*IVariable->Rational*/ entry in cc.coefficients) 
            {
                IVariable dim = (IVariable)entry.Key;
                Rational d = m * (Rational) ((!)entry.Value);
                if (d.IsNonZero) 
                {
                    object prev = coefficients[dim];
                    if (prev == null) 
                    {
                        coefficients[dim] = d;
                    } 
                    else 
                    {
                        coefficients[dim] = (Rational)prev + d;
                    }
                }
            }
            rhs += m * cc.rhs;
        }
        
        /// <summary>
        /// Try to reduce the magnitude of the coefficients used.
        /// Has a side effect on the coefficients, but leaves the meaning of the linear constraint
        /// unchanged.
        /// </summary>
        public void Normalize() {
            // compute the gcd of the numerators and the gcd of the denominators
            Rational gcd = rhs;
            foreach (Rational r in coefficients.Values) {
                gcd = Rational.Gcd(gcd, r);
            }
            // Change all coefficients, to divide their numerators with gcdNum and to
            // divide their denominators with gcdDen.
            Hashtable /*IVariable->Rational*/ newCoefficients = new Hashtable /*IVariable->Rational*/ (coefficients.Count);
            foreach (DictionaryEntry /*IVarianble->Rational*/ e in coefficients) {
                Rational r = (Rational) ((!)e.Value);
                if (r.IsNonZero) {
                    newCoefficients.Add(e.Key, new Rational(r.Numerator / gcd.Numerator, r.Denominator / gcd.Denominator));
                } else {
                    newCoefficients.Add(e.Key, r);
                }
            }

            coefficients = newCoefficients;
            rhs = rhs.IsNonZero ? (Rational)new Rational(rhs.Numerator / gcd.Numerator, rhs.Denominator / gcd.Denominator) : rhs;
        }
    }

    /// <summary>
    /// Represents a frame element (vector of dimension/value tuples).  Used only
    /// internally in class LinearConstraintSystem and its communication with class
    /// LinearConstraint.
    /// </summary>
    public class FrameElement 
    {

        Hashtable /*IVariable->Rational*/! terms = new Hashtable /*IVariable->Rational*/ ();

        /// <summary>
        /// Constructs an empty FrameElement.  To add dimensions, call AddCoordinate after construction.
        /// </summary>
        public FrameElement() 
        {
        }

        /// <summary>
        /// This method is to be thought of as being part of the FrameElement object's construction process.
        /// Assumes "dimension" is not already in FrameElement.
        /// </summary>
        /// <param name="dimension"></param>
        /// <param name="value"></param>
        public void AddCoordinate(IVariable! dimension, Rational value) 
        {
            terms.Add(dimension, value);
        }

        [Pure]
        public override string! ToString() 
        {
            string s = null;
            foreach (DictionaryEntry item in terms) 
            {
                if (s == null) 
                {
                    s = "(";
                } 
                else 
                {
                    s += ", ";
                }
                s += String.Format("<{0},{1}>", item.Key, (Rational) ((!)item.Value));
            }
            if (s == null) 
            {
                s = "(";
            }
            return s + ")";
        }

        public IMutableSet /*IVariable!*/! GetDefinedDimensions() 
        {
            HashSet /*IVariable!*/! dims = new HashSet /*IVariable!*/ (terms.Count);
            foreach (IVariable! dim in terms.Keys) 
            {
                dims.Add(dim);
            }
            System.Diagnostics.Debug.Assert(dims.Count == terms.Count);
            return dims;
        }

        /// <summary>
        /// The getter returns the value at the given dimension, or 0 if that dimension is not defined.
        /// </summary>
        public Rational this [IVariable! dimension] 
        {
            get 
            {
                object z = terms[dimension];
                if (z == null) 
                {
                    return Rational.ZERO;
                } 
                else 
                {
                    return (Rational)z;
                }
            }
            set 
            {
                terms[dimension] = value;
            }
        }

    public FrameElement Rename(IVariable! oldName, IVariable! newName)
    {
      object /*Rational*/ z = terms[oldName];
      if (z == null)
      {
        return this;
      }
      else
      {
        System.Diagnostics.Debug.Assert(z is Rational);
        Hashtable /*IVariable->Rational*/ newTerms = (Hashtable! /*IVariable->Rational*/)terms.Clone();
        newTerms.Remove(oldName);
        newTerms.Add(newName, z);

        FrameElement fe = new FrameElement();
        fe.terms = newTerms;
        return fe;
      }
    }

        public FrameElement Clone() 
        {
            FrameElement z = new FrameElement();
            z.terms = (Hashtable /*IVariable->Rational*/)this.terms.Clone();
            return z;
        }
    }
}