//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework {
  using System.Diagnostics.Contracts;
  using System.Collections;
  using System.Collections.Generic;
  using System.Diagnostics;

  using Microsoft.AbstractInterpretationFramework;
  using Microsoft.AbstractInterpretationFramework.Collections;

  using Microsoft.Boogie;

  using IMutableSet = Microsoft.Boogie.GSet<object>;
  using ISet = Microsoft.Boogie.GSet<object>;
  using Set = Microsoft.Boogie.GSet<object>;
  using HashSet = Microsoft.Boogie.GSet<object>;

  /// <summary>
  ///  Creates a lattice that works for several variables given a MicroLattice.  Assumes
  ///  if one variable is bottom, then all variables are bottom.
  /// </summary>
  public class VariableMapLattice : Lattice {
    private class Elt : Element {
      /// <summary>
      /// IsBottom(e)  iff  e.constraints == null
      /// </summary>
      /*MayBeNull*/
      private IFunctionalMap constraints;  // of type IVariable -> LATTICE_ELEMENT
      public IFunctionalMap Constraints {
        get {
          return this.constraints;
        }
      }

      private Elt(bool top) {
        if (top) {
          this.constraints = FunctionalHashtable.Empty;
        } else {
          this.constraints = null;
        }
      }

      public override Element/*!*/ Clone() {
        Contract.Ensures(Contract.Result<Element>() != null);
        return new Elt(this.constraints);
      }

      [Pure]
      public override string/*!*/ ToString() {
        Contract.Ensures(Contract.Result<string>() != null);
        if (constraints == null) {
          return "<bottom>";
        }
        string s = "[";
        string sep = "";
        foreach (IVariable/*!*/ v in cce.NonNull(constraints.Keys)) {
          Contract.Assert(v != null);
          Element m = (Element)constraints[v];
          s += sep + v.Name + " -> " + m;
          sep = ", ";
        }
        return s + "]";
      }

      public static readonly Elt/*!*/ Top = new Elt(true);
      public static readonly Elt/*!*/ Bottom = new Elt(false);


      public Elt(IFunctionalMap constraints) {
        this.constraints = constraints;
      }

      public bool IsBottom {
        get {
          return this.constraints == null;
        }
      }

      public int Count {
        get {
          return this.constraints == null ? 0 : this.constraints.Count;
        }
      }

      public IEnumerable/*<IVariable>*//*!*/ Variables {
        get {
          Contract.Requires(!this.IsBottom);
          Contract.Ensures(Contract.Result<IEnumerable>() != null);
          Contract.Assume(this.constraints != null);
          return cce.NonNull(this.constraints.Keys);
        }
      }

      public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
        Contract.Ensures(Contract.Result<IEnumerable>() != null);
        if (variableComparer == null) {
          return Variables;
        } else {
          ArrayList /*IVariable*/ vars = new ArrayList /*IVariable*/ (Count);
          foreach (IVariable variable in Variables) {
            vars.Add(variable);
          }
          vars.Sort(variableComparer);
          return vars;
        }
      }

      public Element Lookup(IVariable v) {
        if ((v == null) || (this.constraints == null)) {
          return null;
        }
        return (Element)this.constraints[v];
      }

      public Element this[IVariable/*!*/ key] {
        get {
          Contract.Requires(!this.IsBottom);
          Contract.Requires(key != null);
          Contract.Assume(this.constraints != null);
          return (Element)constraints[key];
        }
      }

      /// <summary>
      /// Add a new entry in the functional map: var --> value.
      /// If the variable is already there, throws an exception
      /// </summary>
      public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) {
        Contract.Requires(microLattice != null);
        Contract.Requires(value != null);
        Contract.Requires(var != null);
        Contract.Requires((!this.IsBottom));
        Contract.Ensures(Contract.Result<Elt>() != null);
        Contract.Assume(this.constraints != null);
        Contract.Assert(!this.constraints.Contains(var));

        if (microLattice.IsBottom(value)) {
          return Bottom;
        }
        if (microLattice.IsTop(value)) {
          return this.Remove(var, microLattice);
        }

        return new Elt(this.constraints.Add(var, value));
      }

      /// <summary>
      /// Set the value of the variable in the functional map
      /// If the variable is not already there, throws an exception
      /// </summary>
      public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) {
        Contract.Requires(microLattice != null);
        Contract.Requires(value != null);
        Contract.Requires(var != null);
        Contract.Ensures(Contract.Result<Elt>() != null);
        if (microLattice.IsBottom(value)) {
          return Bottom;
        }
        if (microLattice.IsTop(value)) {
          return this.Remove(var, microLattice);
        }

        Contract.Assume(this.constraints != null);
        Contract.Assert(this.constraints.Contains(var));

        // this.constraints[var] = value;
        IFunctionalMap newMap = this.constraints.Set(var, value);

        return new Elt(newMap);
      }

      public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice) {
        Contract.Requires(var != null);
        Contract.Ensures(Contract.Result<Elt>() != null);
        if (this.IsBottom) {
          return this;
        }
        Contract.Assume(this.constraints != null);
        return new Elt(this.constraints.Remove(var));
      }

      public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice) {
        Contract.Requires(microLattice != null);
        Contract.Requires(newName != null);
        Contract.Requires(oldName != null);
        Contract.Requires((!this.IsBottom));
        Contract.Ensures(Contract.Result<Elt>() != null);
        Element value = this[oldName];
        if (value == null) {
          return this;
        } // 'oldName' isn't in the map, so neither will be 'newName'
        Contract.Assume(this.constraints != null);
        IFunctionalMap newMap = this.constraints.Remove(oldName);
        newMap = newMap.Add(newName, value);
        return new Elt(newMap);
      }

      [Pure]
      public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
        Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
        throw new System.NotImplementedException();
      }

    } // class

    private readonly MicroLattice/*!*/ microLattice;

    private readonly IPropExprFactory/*!*/ propExprFactory;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(microLattice != null);
      Contract.Invariant(propExprFactory != null);
    }


    private readonly /*maybe null*/IComparer variableComparer;

    public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer)
      : base(valueExprFactory) {
      Contract.Requires(microLattice != null);
      Contract.Requires(valueExprFactory != null);
      Contract.Requires(propExprFactory != null);
      this.propExprFactory = propExprFactory;
      this.microLattice = microLattice;
      this.variableComparer = variableComparer;
      // base(valueExprFactory);
    }

    protected override object/*!*/ UniqueId {
      get {
        Contract.Ensures(Contract.Result<object>() != null);
        return this.microLattice.GetType();
      }
    }

    public override Element/*!*/ Top {
      get {
        Contract.Ensures(Contract.Result<Element>() != null);
        return Elt.Top;
      }
    }

    public override Element Bottom {
      get {
        Contract.Ensures(Contract.Result<Element>() != null);
        return Elt.Bottom;
      }
    }

    public override bool IsTop(Element/*!*/ element) {
      //Contract.Requires(element != null);
      Elt e = (Elt)element;
      return !e.IsBottom && e.Count == 0;
    }

    public override bool IsBottom(Element/*!*/ element) {
      //Contract.Requires(element != null);
      return ((Elt)element).IsBottom;
    }

    protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) {
      //Contract.Requires(second != null);
      //Contract.Requires(first != null);
      Elt a = (Elt)first;
      Elt b = (Elt)second;

      // return true iff every constraint in "this" is no weaker than the corresponding
      // constraint in "that" and there are no additional constraints in "that"
      foreach (IVariable/*!*/ var in a.Variables) {
        Contract.Assert(var != null);
        Element thisValue = cce.NonNull(a[var]);

        Element thatValue = b[var];
        if (thatValue == null) {
          continue;
        } // it's okay for "a" to know something "b" doesn't

        if (this.microLattice.LowerThan(thisValue, thatValue)) {
          continue;
        } // constraint for "var" satisfies AtMost relation

        return false;
      }
      foreach (IVariable/*!*/ var in b.Variables) {
        Contract.Assert(var != null);
        if (a.Lookup(var) != null) {
          continue;
        } // we checked this case in the loop above

        Element thatValue = cce.NonNull(b[var]);
        if (this.microLattice.IsTop(thatValue)) {
          continue;
        } // this is a trivial constraint

        return false;
      }
      return true;
    }

    private Elt/*!*/ AddConstraint(Element/*!*/ element, IVariable/*!*/ var, /*MicroLattice*/Element/*!*/ newValue) {
      Contract.Requires((newValue != null));
      Contract.Requires((var != null));
      Contract.Requires((element != null));
      Contract.Ensures(Contract.Result<Elt>() != null);
      Elt e = (Elt)element;

      if (!e.IsBottom && !this.microLattice.IsBottom(newValue)) // if we're not at bottom
            {
        /*MicroLattice*/
        Element currentValue = e[var];

        if (currentValue == null) {
          // No information currently, so we just add the new info.
          return e.Add(var, newValue, this.microLattice);
        } else {
          // Otherwise, take the meet of the new and current info.
          //return e.Add(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
          return e.Set(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
        }
      }
      return e;
    }

    public override string/*!*/ ToString(Element/*!*/ element) {
      //Contract.Requires(element != null);
      Contract.Ensures(Contract.Result<string>() != null);
      Elt e = (Elt)element;

      if (IsTop(e)) {
        return "<top>";
      }
      if (IsBottom(e)) {
        return "<bottom>";
      }

      int k = 0;
      System.Text.StringBuilder buffer = new System.Text.StringBuilder();
      foreach (IVariable/*!*/ key in e.SortedVariables(variableComparer)) {
        Contract.Assert(key != null);
        if (k++ > 0) {
          buffer.Append("; ");
        }
        buffer.AppendFormat("{0} = {1}", key, e[key]);
      }
      return buffer.ToString();
    }

    public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
      //Contract.Requires(second != null);
      //Contract.Requires(first != null);
      Contract.Ensures(Contract.Result<Element>() != null);
      Elt a = (Elt)first;
      Elt b = (Elt)second;

      IFunctionalMap newMap = FunctionalHashtable.Empty;
      foreach (IVariable/*!*/ key in a.Variables) {
        Contract.Assert(key != null);
        Element aValue = a[key];
        Element bValue = b[key];

        if (aValue != null && bValue != null) {
          // Keep only the variables known to both elements.
          Element newValue = this.microLattice.Join(aValue, bValue);
          newMap = newMap.Add(key, newValue);
        }
      }
      Elt/*!*/ join = new Elt(newMap);
      Contract.Assert(join != null);

      // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));

      return join;
    }

    public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
      //Contract.Requires(second != null);
      //Contract.Requires(first != null);
      Contract.Ensures(Contract.Result<Element>() != null);
      Elt a = (Elt)first;
      Elt b = (Elt)second;

      IFunctionalMap newMap = FunctionalHashtable.Empty;
      foreach (IVariable/*!*/ key in a.Variables) {
        Contract.Assert(key != null);
        Element/*!*/ aValue = cce.NonNull(a[key]);
        Element bValue = b[key];

        Element newValue =
          bValue == null ? aValue :
          this.microLattice.Meet(aValue, bValue);

        newMap = newMap.Add(key, newValue);
      }
      foreach (IVariable/*!*/ key in b.Variables) {
        Contract.Assert(key != null);
        Element aValue = a[key];
        Element bValue = b[key];
        Debug.Assert(bValue != null);

        if (aValue == null) {
          // It's a variable we didn't cover in the last loop.
          newMap = newMap.Add(key, bValue);
        }
      }
      return new Elt(newMap);
    }

    /// <summary>
    /// Perform the pointwise widening of the elements in the map
    /// </summary>
    public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
      //Contract.Requires((second != null));
      //Contract.Requires((first != null));
      Contract.Ensures(Contract.Result<Element>() != null);
      Elt a = (Elt)first;
      Elt b = (Elt)second;

      // Note we have to add those cases as we do not have a "NonTrivialWiden" method
      if (a.IsBottom)
        return new Elt(b.Constraints);
      if (b.IsBottom)
        return new Elt(a.Constraints);

      IFunctionalMap newMap = FunctionalHashtable.Empty;
      foreach (IVariable/*!*/ key in a.Variables) {
        Contract.Assert(key != null);
        Element aValue = a[key];
        Element bValue = b[key];

        if (aValue != null && bValue != null) {
          // Keep only the variables known to both elements.
          Element newValue = this.microLattice.Widen(aValue, bValue);
          newMap = newMap.Add(key, newValue);
        }
      }
      Element/*!*/ widen = new Elt(newMap);
      Contract.Assert(widen != null);
      // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));

      return widen;
    }

    internal static ISet/*<IVariable!>*//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/*<IVariable!>*//*!*/ ignoreVars) {
      Contract.Requires(ignoreVars != null);
      Contract.Requires(e != null);
      Contract.Ensures(Contract.Result<ISet>() != null);
      HashSet s = new HashSet();

      IFunApp f = e as IFunApp;
      IFunction lambda = e as IFunction;

      if (e is IVariable) {
        if (!ignoreVars.Contains(e))
          s.Add(e);
      } else if (f != null) // e is IFunApp
            {
        foreach (IExpr/*!*/ arg in f.Arguments) {
          Contract.Assert(arg != null);
          s.AddAll(VariablesInExpression(arg, ignoreVars));
        }
      } else if (lambda != null) {
        IMutableSet x = new HashSet(1);
        x.Add(lambda.Param);

        // Ignore the bound variable
        s.AddAll(VariablesInExpression(lambda.Body, cce.NonNull(Set.Union(ignoreVars, x))));
      } else if (e is IUnknown) {
        // skip (actually, it would be appropriate to return the universal set of all variables)
      } else {
        Debug.Assert(false, "case not handled: " + e);
      }
      return s;
    }


    private static ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e) {
      Contract.Ensures(Contract.Result<ArrayList>() != null);
      ArrayList result = new ArrayList();

      IFunApp f = e as IFunApp;
      if (f != null) {
        if (f.FunctionSymbol.Equals(Prop.And)) {
          foreach (IExpr arg in f.Arguments) {
            result.AddRange(FindConjuncts(arg));
          }
        } else if (f.FunctionSymbol.Equals(Prop.Or)
                 || f.FunctionSymbol.Equals(Prop.Implies)) {
          // Do nothing.
        } else {
          result.Add(e);
        }
      } else {
        result.Add(e);
      }

      return result;
    }

    private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right) {
      Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out right) != null);
      left = null;
      right = null;

      // See if we have an equality
      IFunApp nary = expr as IFunApp;
      if (nary == null || !nary.FunctionSymbol.Equals(Value.Eq)) {
        return false;
      }

      // See if it is an equality of two variables
      IVariable idLeft = nary.Arguments[0] as IVariable;
      IVariable idRight = nary.Arguments[1] as IVariable;
      if (idLeft == null || idRight == null) {
        return false;
      }

      left = idLeft;
      right = idRight;
      return true;
    }

    /// <summary>
    /// Returns true iff the expression is in the form var == arithmeticExpr
    /// </summary>
    private static bool IsArithmeticExpr(IExpr/*!*/ expr) {
      Contract.Requires(expr != null);
      // System.Console.WriteLine("\t\tIsArithmetic called with {0} of type {1}", expr, expr.GetType().ToString());

      if (expr is IVariable)   // expr is a variable
        return true;
      else if (expr is IFunApp)     // may be ==, +, -, /, % or an integer
        {
        IFunApp fun = (IFunApp)expr;

        if (fun.FunctionSymbol is IntSymbol)     // it is an integer
          return true;
        else if (fun.FunctionSymbol.Equals(Int.Negate))  // it is an unary minus
          return IsArithmeticExpr((IExpr/*!*/)cce.NonNull(fun.Arguments[0]));
        else if (fun.Arguments.Count != 2)       // A function of two or more operands is not arithmetic
          return false;
        else {
          IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
          IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);

          if (!(left is IVariable || right is IVariable))    // At least one of the two operands must be a variable
            return false;

          if (fun.FunctionSymbol.Equals(Value.Eq)
              || fun.FunctionSymbol.Equals(Int.Add)
              || fun.FunctionSymbol.Equals(Int.Sub)
              || fun.FunctionSymbol.Equals(Int.Mul)
              || fun.FunctionSymbol.Equals(Int.Div)
              || fun.FunctionSymbol.Equals(Int.Mod))
            return IsArithmeticExpr(left) && IsArithmeticExpr(right);
          else
            return false;
        }
      } else {
        return false;
      }
    }

    public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
      //Contract.Requires(element != null);
      Contract.Ensures(Contract.Result<IExpr>() != null);
      if (IsTop(element)) {
        return propExprFactory.True;
      }
      if (IsBottom(element)) {
        return propExprFactory.False;
      }

      Elt e = (Elt)element;
      IExpr truth = propExprFactory.True;
      IExpr result = truth;

      foreach (IVariable/*!*/ variable in e.SortedVariables(variableComparer)) {
        Contract.Assert(variable != null);
        Element value = (Element)e[variable];

        if (value == null || this.microLattice.IsTop(value)) {
          continue;
        } // Skip variables about which we know nothing.
        if (this.microLattice.IsBottom(value)) {
          return propExprFactory.False;
        }

        IExpr conjunct = this.microLattice.ToPredicate(variable, value);

        result = (result == truth) ? (IExpr)conjunct : (IExpr)propExprFactory.And(result, conjunct);
      }
      return result;
    }


    public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable) {
      //Contract.Requires(variable != null);
      //Contract.Requires(element != null);
      Contract.Ensures(Contract.Result<Element>() != null);
      return cce.NonNull((Elt)element).Remove(variable, this.microLattice);
    }

    private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var);
    private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var) {
      //Contract.Requires(var != null);
      Contract.Ensures(Contract.Result<IExpr>() != null);
      return var;
    }

    /// <summary>
    /// Return a new expression in which each variable has been 
    /// replaced by an expression representing what is known about
    /// that variable.
    /// </summary>
    private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/*<IVariable!>*//*!*/ notInlineable,
        OnUnableToInline/*!*/ unableToInline) {
      Contract.Requires(unableToInline != null);
      Contract.Requires(notInlineable != null);
      Contract.Requires(expr != null);
      Contract.Requires(element != null);
      Contract.Ensures(Contract.Result<IExpr>() != null);
      IVariable var = expr as IVariable;
      if (var != null) {
        /*MicroLattice*/
        Element value = element[var];
        if (notInlineable.Contains(var) || value == null || this.microLattice.IsTop(value)) {
          return unableToInline(var); // We don't know anything about this variable.
        } else {
          // GetFoldExpr returns null when it can yield an expression that
          // can be substituted for the variable.
          IExpr valueExpr = this.microLattice.GetFoldExpr(value);
          return (valueExpr == null) ? var : valueExpr;
        }
      }

      // else

      IFunApp fun = expr as IFunApp;
      if (fun != null) {
        IList newargs = new ArrayList();
        foreach (IExpr/*!*/ arg in fun.Arguments) {
          Contract.Assert(arg != null);
          newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
        }
        return fun.CloneWithArguments(newargs);
      }

      // else

      IFunction lambda = expr as IFunction;
      if (lambda != null) {
        IMutableSet x = new HashSet(1);
        x.Add(lambda.Param);

        // Don't inline the bound variable
        return lambda.CloneWithBody(
                   InlineVariables(element, lambda.Body,
                                    cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
               );
      }

      // else

      if (expr is IUnknown) {
        return expr;
      } else {
        throw
          new System.NotImplementedException("cannot inline identifies in expression " + expr);
      }
    }


    public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr) {
      //Contract.Requires(expr != null);
      //Contract.Requires(element != null);
      //Contract.Ensures(Contract.Result<Element>() != null);
      Elt/*!*/ result = (Elt)element;
      Contract.Assert(result != null);

      if (IsBottom(element)) {
        return result; // == element 
      }

      expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));

      foreach (IExpr/*!*/ conjunct in FindConjuncts(expr)) {
        Contract.Assert(conjunct != null);
        IVariable left, right;

        if (IsSimpleEquality(conjunct, out left, out right)) {
          #region The conjunct is a simple equality


          Contract.Assert(left != null && right != null);

          Element leftValue = result[left], rightValue = result[right];
          if (leftValue == null) {
            leftValue = this.microLattice.Top;
          }
          if (rightValue == null) {
            rightValue = this.microLattice.Top;
          }
          Element newValue = this.microLattice.Meet(leftValue, rightValue);
          result = AddConstraint(result, left, newValue);
          result = AddConstraint(result, right, newValue);

          #endregion
        } else {
          ISet/*<IVariable>*/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty);

          if (variablesInvolved.Count == 1) {
            #region We have just one variable

            IVariable var = null;
            foreach (IVariable/*!*/ v in variablesInvolved) {
              Contract.Assert(v != null);
              var = v;
            } // why is there no better way to get the elements?
            Contract.Assert(var != null);
            Element/*!*/ value = this.microLattice.EvaluatePredicate(conjunct);
            result = AddConstraint(result, var, value);

            #endregion
          } else if (IsArithmeticExpr(conjunct) && this.microLattice.UnderstandsBasicArithmetics) {
            #region We evalaute an arithmetic expression

            IFunApp fun = (IFunApp)conjunct;
            if (fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
                       {
              // get the variable to be assigned
              IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
              IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
              IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg;

              Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
              Contract.Assert(value != null);
              result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value);
            }
            #endregion
          }
        }
      }
      return result;
    }


    public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
      //Contract.Requires(newName != null);
      //Contract.Requires(oldName != null);
      //Contract.Requires(element != null);
      //Contract.Ensures(Contract.Result<Element>() != null);
      if (IsBottom(element)) {
        return element;
      } else {
        return ((Elt)element).Rename(oldName, newName, this.microLattice);
      }
    }


    public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
      //Contract.Requires(args != null);
      //Contract.Requires(f != null);
      return f.Equals(Prop.And) ||
             f.Equals(Value.Eq) ||
             microLattice.Understands(f, args);
    }

    private sealed class EquivalentExprException : CheckedException {
    }
    private sealed class EquivalentExprInlineCallback {
      private readonly IVariable/*!*/ var;
      [ContractInvariantMethod]
      void ObjectInvariant() {
        Contract.Invariant(var != null);
      }

      public EquivalentExprInlineCallback(IVariable/*!*/ var) {
        Contract.Requires(var != null);
        this.var = var;
        // base();
      }

      public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar)
        //throws EquivalentExprException;
      {
        Contract.Requires(othervar != null);
        Contract.Ensures(Contract.Result<IExpr>() != null);
        Contract.EnsuresOnThrow<EquivalentExprException>(true);
        if (othervar.Equals(var))
          throw new EquivalentExprException();
        else
          return othervar;
      }
    }

    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);
      try {
        EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var);
        return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty),
                               new OnUnableToInline(closure.ThrowOnUnableToInline));
      } catch (EquivalentExprException) {
        return null;
      }
    }


    /// <summary>
    /// Check to see if the given predicate holds in the given lattice element.
    /// 
    /// TODO:  We leave this unimplemented for now and just return maybe.
    /// </summary>
    /// <param name="e">The lattice element.</param>
    /// <param name="pred">The predicate.</param>
    /// <returns>Yes, No, or Maybe</returns>
    public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
      //Contract.Requires(pred != null);
      //Contract.Requires(e != null);
      return Answer.Maybe;
    }

    /// <summary>
    ///  Answers a disequality about two variables.  The same information could be obtained
    ///  by asking CheckPredicate, but a different implementation may be simpler and more
    ///  efficient.
    /// 
    ///  TODO: We leave this unimplemented for now and just return maybe.
    /// </summary>
    /// <param name="e">The lattice element.</param>
    /// <param name="var1">The first variable.</param>
    /// <param name="var2">The second variable.</param>
    /// <returns>Yes, No, or Maybe.</returns>
    public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
      //Contract.Requires(var2 != null);
      //Contract.Requires(var1 != null);
      //Contract.Requires(e != null);
      return Answer.Maybe;
    }

    public override void Validate() {
      base.Validate();
      microLattice.Validate();
    }

  }
}