//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Text;
using System.IO;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;

// different classes for erasing complex types in VCExprs, replacing them
// with axioms that can be handled by theorem provers and SMT solvers

namespace Microsoft.Boogie.TypeErasure {
  using Microsoft.Boogie.VCExprAST;

  // some functionality that is needed in many places (and that should
  // really be provided by the Spec# container classes; maybe one
  // could integrate the functions in a nicer way?)
  public class HelperFuns {

    public static Function BoogieFunction(string name, List<TypeVariable/*!*/>/*!*/ typeParams, params Type[] types) {
      Contract.Requires(types != null);
      Contract.Requires(name != null);
      Contract.Requires(cce.NonNullElements(typeParams));
      Contract.Requires(types.Length > 0);
      Contract.Requires(Contract.ForAll(0, types.Length, i => types[i] != null));
      Contract.Ensures(Contract.Result<Function>() != null);

      VariableSeq args = new VariableSeq();
      for (int i = 0; i < types.Length - 1; ++i)
        args.Add(new Formal(Token.NoToken,
                             new TypedIdent(Token.NoToken, "arg" + i, cce.NonNull(types[i])),
                             true));
      Formal result = new Formal(Token.NoToken,
                                   new TypedIdent(Token.NoToken, "res",
                                                   cce.NonNull(types)[types.Length - 1]),
                                   false);
      return new Function(Token.NoToken, name, ToSeq(typeParams), args, result);
    }

    public static Function BoogieFunction(string name, params Type[] types) {
      Contract.Requires(types != null);
      Contract.Requires(name != null);
      Contract.Ensures(Contract.Result<Function>() != null);
      return BoogieFunction(name, new List<TypeVariable/*!*/>(), types);
    }

    // boogie function where all arguments and the result have the same type U
    public static Function UniformBoogieFunction(string name, int arity, Type U) {
      Contract.Requires(U != null);
      Contract.Requires(name != null);
      Contract.Ensures(Contract.Result<Function>() != null);
      Type[]/*!*/ types = new Type[arity + 1];
      for (int i = 0; i < arity + 1; ++i)
        types[i] = U;
      return BoogieFunction(name, types);
    }

    public static List<VCExprVar/*!*/>/*!*/ GenVarsForInParams(Function fun, VCExpressionGenerator gen) {
      Contract.Requires(gen != null);
      Contract.Requires(fun != null);
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
      List<VCExprVar/*!*/>/*!*/ arguments = new List<VCExprVar/*!*/>(fun.InParams.Length);
      foreach (Formal/*!*/ f in fun.InParams) {
        Contract.Assert(f != null);
        VCExprVar/*!*/ var = gen.Variable(f.Name, f.TypedIdent.Type);
        arguments.Add(var);
      }
      return arguments;
    }

    public static List<T/*!*/>/*!*/ ToList<T>(params T[] args) where T : class{
      Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<T>>()));
      return new List<T>(args);
    }

    public static List<TypeVariable/*!*/>/*!*/ ToList(TypeVariableSeq seq) {
      Contract.Requires(seq != null);
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
      List<TypeVariable/*!*/>/*!*/ res = new List<TypeVariable/*!*/>(seq.Length);
      foreach (TypeVariable/*!*/ var in seq) {
        Contract.Assert(var != null);
        res.Add(var);
      }
      return res;
    }

    public static TypeVariableSeq ToSeq(List<TypeVariable/*!*/>/*!*/ list) {
      Contract.Requires(cce.NonNullElements(list));
      Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
      TypeVariableSeq/*!*/ res = new TypeVariableSeq();
      foreach (TypeVariable/*!*/ var in list) {
        Contract.Assert(var != null);
        res.Add(var);
      }
      return res;
    }

    public static List<T>/*!*/ Intersect<T>(List<T> a, List<T> b) {
      Contract.Requires(b != null);
      Contract.Requires(a != null);
      Contract.Ensures(Contract.Result<List<T>>() != null);

      List<T>/*!*/ res = new List<T>(Math.Min(a.Count, b.Count));
      foreach (T x in a)
        if (b.Contains(x))
          res.Add(x);
      res.TrimExcess();
      return res;
    }

    public static List<KeyValuePair<T1, T2>>/*!*/ ToPairList<T1, T2>(IDictionary<T1, T2> dict) {
      Contract.Requires((dict != null));
      Contract.Ensures(Contract.Result<List<KeyValuePair<T1, T2>>>() != null);
      List<KeyValuePair<T1, T2>>/*!*/ res = new List<KeyValuePair<T1, T2>>(dict);
      return res;
    }

    public static void AddRangeWithoutDups<T>(IEnumerable<T> fromList, List<T> toList) {
      Contract.Requires(toList != null);
      Contract.Requires(fromList != null);
      foreach (T t in fromList)
        if (!toList.Contains(t))
          toList.Add(t);
    }

    public static void AddFreeVariablesWithoutDups(Type type, List<TypeVariable/*!*/>/*!*/ toList) {
      Contract.Requires(type != null);
      Contract.Requires(cce.NonNullElements(toList));
      foreach (TypeVariable var in type.FreeVariables) {
        Contract.Assert(var != null);
        if (!toList.Contains(var))
          toList.Add(var);
      }
    }

    public static List<VCExpr/*!*/>/*!*/ ToVCExprList(List<VCExprVar/*!*/>/*!*/ list) {
      Contract.Requires(cce.NonNullElements(list));
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
      List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>(list.Count);
      foreach (VCExprVar/*!*/ var in list) {
        Contract.Assert(var != null);
        res.Add(var);
      }
      return res;
    }

    public static List<VCExprVar/*!*/>/*!*/ VarVector(string baseName, int num, Type type, VCExpressionGenerator gen) {
      Contract.Requires(gen != null);
      Contract.Requires(type != null);
      Contract.Requires(baseName != null);
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
      List<VCExprVar/*!*/>/*!*/ res = new List<VCExprVar/*!*/>(num);
      for (int i = 0; i < num; ++i)
        res.Add(gen.Variable(baseName + i, type));
      return res;
    }

    public static List<VCExprVar/*!*/>/*!*/ VarVector(string baseName, List<Type/*!*/>/*!*/ types, VCExpressionGenerator gen) {
      Contract.Requires(gen != null);
      Contract.Requires(baseName != null);
      Contract.Requires(cce.NonNullElements(types));
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
      List<VCExprVar/*!*/>/*!*/ res = new List<VCExprVar/*!*/>(types.Count);
      for (int i = 0; i < types.Count; ++i)
        res.Add(gen.Variable(baseName + i, types[i]));
      return res;
    }
  }

  //////////////////////////////////////////////////////////////////////////////

  internal struct TypeCtorRepr {
    // function that represents the application of the type constructor
    // to smaller types
    public readonly Function/*!*/ Ctor;
    // left-inverse functions that extract the subtypes of a compound type
    public readonly List<Function/*!*/>/*!*/ Dtors;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Ctor != null);
      Contract.Invariant(cce.NonNullElements(Dtors));
    }


    public TypeCtorRepr(Function ctor, List<Function/*!*/>/*!*/ dtors) {
      Contract.Requires(ctor != null);
      Contract.Requires(cce.NonNullElements(dtors));
      Contract.Requires(ctor.InParams.Length == dtors.Count);
      this.Ctor = ctor;
      this.Dtors = dtors;
    }
  }

  //////////////////////////////////////////////////////////////////////////////

  // The class responsible for creating and keeping track of all
  // axioms related to the type system. This abstract class is made
  // concrete in two subclasses, one for type erasure with type
  // premisses in quantifiers (the semantic approach), and one for
  // type erasure with explicit type arguments of polymorphic
  // functions (the syntacted approach).
  [ContractClass(typeof(TypeAxiomBuilderContracts))]
  public abstract class TypeAxiomBuilder : ICloneable {

    protected readonly VCExpressionGenerator/*!*/ Gen;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Gen != null);
      Contract.Invariant(Ctor != null);

    }


    internal abstract MapTypeAbstractionBuilder/*!*/ MapTypeAbstracter {
      get;
    }

    ///////////////////////////////////////////////////////////////////////////
    // Type Axioms

    // list in which all typed axioms are collected
    private readonly List<VCExpr/*!*/>/*!*/ AllTypeAxioms;
    [ContractInvariantMethod]
    void AllTypeAxiomsInvariantMethod() {
      Contract.Invariant(cce.NonNullElements(AllTypeAxioms));
    }

    // list in which type axioms are incrementally collected
    private readonly List<VCExpr/*!*/>/*!*/ IncTypeAxioms;
    [ContractInvariantMethod]
    void IncTypeAxiomsInvariantMethod() {
      Contract.Invariant(cce.NonNullElements(IncTypeAxioms));
    }

    internal void AddTypeAxiom(VCExpr axiom) {
      Contract.Requires(axiom != null);
      AllTypeAxioms.Add(axiom);
      IncTypeAxioms.Add(axiom);
    }

    // Return all axioms that were added since the last time NewAxioms
    // was called
    public VCExpr GetNewAxioms() {
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      VCExpr/*!*/ res = Gen.NAry(VCExpressionGenerator.AndOp, IncTypeAxioms);
      IncTypeAxioms.Clear();
      return res;
    }

    // mapping from a type to its constructor number/index
    private readonly Function/*!*/ Ctor;
    private BigNum CurrentCtorNum;

    private VCExpr GenCtorAssignment(VCExpr typeRepr) {
      Contract.Requires(typeRepr != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      if (CommandLineOptions.Clo.TypeEncodingMethod
                == CommandLineOptions.TypeEncoding.None)
        return VCExpressionGenerator.True;

      VCExpr res = Gen.Eq(Gen.Function(Ctor, typeRepr),
                           Gen.Integer(CurrentCtorNum));
      CurrentCtorNum = CurrentCtorNum + BigNum.ONE;
      return res;
    }

    private VCExpr GenCtorAssignment(Function typeRepr) {
      Contract.Requires(typeRepr != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      if (CommandLineOptions.Clo.TypeEncodingMethod
                == CommandLineOptions.TypeEncoding.None)
        return VCExpressionGenerator.True;

      List<VCExprVar/*!*/>/*!*/ quantifiedVars = HelperFuns.GenVarsForInParams(typeRepr, Gen);
      VCExpr/*!*/ eq =
        GenCtorAssignment(Gen.Function(typeRepr,
                                       HelperFuns.ToVCExprList(quantifiedVars)));

      if (typeRepr.InParams.Length == 0)
        return eq;

      return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(),
                        "ctor:" + typeRepr.Name, -1, eq);
    }

    // generate an axiom (forall x0, x1, ... :: invFun(fun(x0, x1, ...) == xi)
    protected VCExpr GenLeftInverseAxiom(Function fun, Function invFun, int dtorNum) {
      Contract.Requires(invFun != null);
      Contract.Requires(fun != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      List<VCExprVar/*!*/>/*!*/ quantifiedVars = HelperFuns.GenVarsForInParams(fun, Gen);
      Contract.Assert(cce.NonNullElements(quantifiedVars));

      VCExpr/*!*/ funApp = Gen.Function(fun, HelperFuns.ToVCExprList(quantifiedVars));
      VCExpr/*!*/ lhs = Gen.Function(invFun, funApp);
      VCExpr/*!*/ rhs = quantifiedVars[dtorNum];
      VCExpr/*!*/ eq = Gen.Eq(lhs, rhs);

      List<VCTrigger/*!*/>/*!*/ triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));
      Contract.Assert(cce.NonNullElements(triggers));
      return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, -1, eq);
    }

    ///////////////////////////////////////////////////////////////////////////

    // the type of everything that is not int, bool, or a type
    [ContractInvariantMethod]
    void ObjectInvariant2() {
      Contract.Invariant(UDecl != null);
      Contract.Invariant(TDecl != null);
      Contract.Invariant(U != null);
      Contract.Invariant(T != null);
    }

    private readonly TypeCtorDecl/*!*/ UDecl;
    public readonly Type/*!*/ U;

    // the type of types
    private readonly TypeCtorDecl/*!*/ TDecl;
    public readonly Type/*!*/ T;

    public abstract Type/*!*/ TypeAfterErasure(Type/*!*/ type);
    [Pure]
    public abstract bool UnchangedType(Type/*!*/ type);

    ///////////////////////////////////////////////////////////////////////////
    // Symbols for representing types

    private readonly IDictionary<Type/*!*/, VCExpr/*!*/>/*!*/ BasicTypeReprs;
    [ContractInvariantMethod]
    void BasicTypeReprsInvariantMethod() {
      Contract.Invariant(cce.NonNullDictionaryAndValues(BasicTypeReprs));
    }

    private VCExpr GetBasicTypeRepr(Type type) {
      Contract.Requires(type != null);
      Contract.Requires(type.IsBasic || type.IsBv);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      VCExpr res;
      if (!BasicTypeReprs.TryGetValue(type, out res)) {
        res = Gen.Function(HelperFuns.BoogieFunction(type.ToString() + "Type", T));
        AddTypeAxiom(GenCtorAssignment(res));
        BasicTypeReprs.Add(type, res);
      }
      return cce.NonNull(res);
    }

    private readonly IDictionary<TypeCtorDecl/*!*/, TypeCtorRepr/*!*/>/*!*/ TypeCtorReprs;
    [ContractInvariantMethod]
    void TypeCtorReprsInvariantMethod() {
      Contract.Invariant(TypeCtorReprs != null);
    }

    internal TypeCtorRepr GetTypeCtorReprStruct(TypeCtorDecl decl) {
      Contract.Requires(decl != null);
      TypeCtorRepr reprSet;
      if (!TypeCtorReprs.TryGetValue(decl, out reprSet)) {
        Function/*!*/ ctor = HelperFuns.UniformBoogieFunction(decl.Name + "Type", decl.Arity, T);
        Contract.Assert(ctor != null);
        AddTypeAxiom(GenCtorAssignment(ctor));

        List<Function/*!*/>/*!*/ dtors = new List<Function/*!*/>(decl.Arity);
        for (int i = 0; i < decl.Arity; ++i) {
          Function/*!*/ dtor = HelperFuns.UniformBoogieFunction(decl.Name + "TypeInv" + i, 1, T);
          dtors.Add(dtor);
          AddTypeAxiom(GenLeftInverseAxiom(ctor, dtor, i));
        }

        reprSet = new TypeCtorRepr(ctor, dtors);
        TypeCtorReprs.Add(decl, reprSet);
      }

      return reprSet;
    }

    public Function GetTypeCtorRepr(TypeCtorDecl decl) {
      Contract.Requires(decl != null);
      Contract.Ensures(Contract.Result<Function>() != null);
      return GetTypeCtorReprStruct(decl).Ctor;
    }

    public Function GetTypeDtor(TypeCtorDecl decl, int num) {
      Contract.Requires(decl != null);
      Contract.Ensures(Contract.Result<Function>() != null);
      return GetTypeCtorReprStruct(decl).Dtors[num];
    }

    // mapping from free type variables to VCExpr variables
    private readonly IDictionary<TypeVariable/*!*/, VCExprVar/*!*/>/*!*/ TypeVariableMapping;
    [ContractInvariantMethod]
    void TypeVariableMappingInvariantMethod() {
      Contract.Invariant(cce.NonNullDictionaryAndValues(TypeVariableMapping));
    }

    public VCExprVar Typed2Untyped(TypeVariable var) {
      Contract.Requires(var != null);
      Contract.Ensures(Contract.Result<VCExprVar>() != null);
      VCExprVar res;
      if (!TypeVariableMapping.TryGetValue(var, out res)) {
        res = new VCExprVar(var.Name, T);
        TypeVariableMapping.Add(var, res);
      }
      return cce.NonNull(res);
    }


    ////////////////////////////////////////////////////////////////////////////
    // Symbols for representing variables and constants

    // Globally defined variables
    private readonly IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ Typed2UntypedVariables;
    [ContractInvariantMethod]
    void Typed2UntypedVariablesInvariantMethod() {
      Contract.Invariant(cce.NonNullDictionaryAndValues(Typed2UntypedVariables));
    }

    // This method must only be used for free (unbound) variables
    public VCExprVar Typed2Untyped(VCExprVar var) {
      Contract.Requires(var != null);
      Contract.Ensures(Contract.Result<VCExprVar>() != null);
      VCExprVar res = TryTyped2Untyped(var);
      if (res == null) {
        res = Gen.Variable(var.Name, TypeAfterErasure(var.Type));
        Typed2UntypedVariables.Add(var, res);
        AddVarTypeAxiom(res, var.Type);
      }
      return cce.NonNull(res);
    }

    /// <summary>
    ///  This method is like Typed2Untyped, except in the case where the given variables
    ///  doesn't exist in the mapping.  For that case, this method returns null whereas
    ///  Typed2Untyped creates a new variable that it adds to the mapping.
    /// </summary>
    /// <param name="var"></param>
    /// <returns></returns>
    public VCExprVar TryTyped2Untyped(VCExprVar var) {
      Contract.Requires(var != null);
      VCExprVar res;
      if (Typed2UntypedVariables.TryGetValue(var, out res)) {
        return res;
      } else {
        return null;
      }
    }

    protected abstract void AddVarTypeAxiom(VCExprVar/*!*/ var, Type/*!*/ originalType);

    ///////////////////////////////////////////////////////////////////////////
    // Translation function from types to their term representation

    public VCExpr Type2Term(Type type, IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ varMapping) {
      Contract.Requires(type != null);
      Contract.Requires(cce.NonNullDictionaryAndValues(varMapping));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      //
      if (type.IsBasic || type.IsBv) {
        //
        return GetBasicTypeRepr(type);
        //
      } else if (type.IsCtor) {
        //
        CtorType ctype = type.AsCtor;
        Function/*!*/ repr = GetTypeCtorRepr(ctype.Decl);
        List<VCExpr/*!*/>/*!*/ args = new List<VCExpr/*!*/>(ctype.Arguments.Length);
        foreach (Type/*!*/ t in ctype.Arguments) {
          Contract.Assert(t != null);
          args.Add(Type2Term(t, varMapping));
        }
        return Gen.Function(repr, args);
        //
      } else if (type.IsVariable) {
        //
        VCExpr res;
        if (!varMapping.TryGetValue(type.AsVariable, out res))
          // then the variable is free and we bind it at this point to a term
          // variable
          res = Typed2Untyped(type.AsVariable);
        return cce.NonNull(res);
        //
      } else if (type.IsMap) {
        //
        return Type2Term(MapTypeAbstracter.AbstractMapType(type.AsMap), varMapping);
        //
      } else {
        System.Diagnostics.Debug.Fail("Don't know how to handle this type: " + type);
        Contract.Assert(false);
        throw new cce.UnreachableException();  // please the compiler
      }
    }

    ////////////////////////////////////////////////////////////////////////////

    public TypeAxiomBuilder(VCExpressionGenerator gen) {
      Contract.Requires(gen != null);
      this.Gen = gen;
      AllTypeAxioms = new List<VCExpr/*!*/>();
      IncTypeAxioms = new List<VCExpr/*!*/>();
      BasicTypeReprs = new Dictionary<Type/*!*/, VCExpr/*!*/>();
      CurrentCtorNum = BigNum.ZERO;
      TypeCtorReprs = new Dictionary<TypeCtorDecl/*!*/, TypeCtorRepr>();
      TypeVariableMapping = new Dictionary<TypeVariable/*!*/, VCExprVar/*!*/>();
      Typed2UntypedVariables = new Dictionary<VCExprVar/*!*/, VCExprVar/*!*/>();

      TypeCtorDecl/*!*/ uDecl = new TypeCtorDecl(Token.NoToken, "U", 0);
      UDecl = uDecl;
      Type/*!*/ u = new CtorType(Token.NoToken, uDecl, new TypeSeq());
      U = u;

      TypeCtorDecl/*!*/ tDecl = new TypeCtorDecl(Token.NoToken, "T", 0);
      TDecl = tDecl;
      Type/*!*/ t = new CtorType(Token.NoToken, tDecl, new TypeSeq());
      T = t;

      Ctor = HelperFuns.BoogieFunction("Ctor", t, Type.Int);
    }

    public virtual void Setup() {
      GetBasicTypeRepr(Type.Int);
      GetBasicTypeRepr(Type.Bool);
    }

    // constructor to allow cloning
    internal TypeAxiomBuilder(TypeAxiomBuilder builder) {
      Contract.Requires(builder != null);
      Gen = builder.Gen;
      AllTypeAxioms = new List<VCExpr/*!*/>(builder.AllTypeAxioms);
      IncTypeAxioms = new List<VCExpr/*!*/>(builder.IncTypeAxioms);

      UDecl = builder.UDecl;
      U = builder.U;

      TDecl = builder.TDecl;
      T = builder.T;

      Ctor = builder.Ctor;
      CurrentCtorNum = builder.CurrentCtorNum;

      BasicTypeReprs = new Dictionary<Type/*!*/, VCExpr/*!*/>(builder.BasicTypeReprs);
      TypeCtorReprs = new Dictionary<TypeCtorDecl/*!*/, TypeCtorRepr>(builder.TypeCtorReprs);

      TypeVariableMapping =
        new Dictionary<TypeVariable/*!*/, VCExprVar/*!*/>(builder.TypeVariableMapping);
      Typed2UntypedVariables =
        new Dictionary<VCExprVar/*!*/, VCExprVar/*!*/>(builder.Typed2UntypedVariables);
    }

    public abstract Object/*!*/ Clone();
  }

  [ContractClassFor(typeof(TypeAxiomBuilder))]
  public abstract class TypeAxiomBuilderContracts : TypeAxiomBuilder {
    public TypeAxiomBuilderContracts()
      : base((VCExpressionGenerator)null) {
    }
    internal override MapTypeAbstractionBuilder MapTypeAbstracter {
      get {
        Contract.Ensures(Contract.Result<MapTypeAbstractionBuilder>() != null);
        throw new NotImplementedException();
      }
    }

    public override Type TypeAfterErasure(Type type) {
      Contract.Requires(type != null);
      Contract.Ensures(Contract.Result<Type>() != null);

      throw new NotImplementedException();
    }

    public override bool UnchangedType(Type type) {
      Contract.Requires(type != null);
      throw new NotImplementedException();
    }

    protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) {
      Contract.Requires(var != null);
      Contract.Requires(originalType != null);
      throw new NotImplementedException();
    }

    public override object Clone() {
      Contract.Ensures(Contract.Result<object>() != null);

      throw new NotImplementedException();
    }
  }

  //////////////////////////////////////////////////////////////////////////////

  // Subclass of the TypeAxiomBuilder that provides all functionality
  // to deal with native sorts of a theorem prover (that are the only
  // types left after erasing all other types). Currently, these are:
  //
  //  U ... sort of all individuals/objects/values
  //  T ... sort of all types
  //  int ... integers
  //  bool ... booleans

  [ContractClass(typeof(TypeAxiomBuilderIntBoolUContracts))]
  public abstract class TypeAxiomBuilderIntBoolU : TypeAxiomBuilder {

    public TypeAxiomBuilderIntBoolU(VCExpressionGenerator gen)
      : base(gen) {
      Contract.Requires(gen != null);

      TypeCasts = new Dictionary<Type/*!*/, TypeCastSet>();
    }

    // constructor to allow cloning
    internal TypeAxiomBuilderIntBoolU(TypeAxiomBuilderIntBoolU builder)
      : base(builder) {
      Contract.Requires(builder != null);

      TypeCasts = new Dictionary<Type/*!*/, TypeCastSet>(builder.TypeCasts);
    }

    public override void Setup() {
      base.Setup();

      GetTypeCasts(Type.Int);
      GetTypeCasts(Type.Bool);
    }

    // generate inverse axioms for casts (castToU(castFromU(x)) = x, under certain premisses)
    protected abstract VCExpr/*!*/ GenReverseCastAxiom(Function/*!*/ castToU, Function/*!*/ castFromU);

    protected VCExpr GenReverseCastEq(Function castToU, Function castFromU, out VCExprVar var, out List<VCTrigger/*!*/>/*!*/ triggers) {
      Contract.Requires((castFromU != null));
      Contract.Requires((castToU != null));
      Contract.Ensures((cce.NonNullElements(Contract.ValueAtReturn(out triggers))));
      Contract.Ensures(Contract.ValueAtReturn(out var) != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      var = Gen.Variable("x", U);

      VCExpr inner = Gen.Function(castFromU, var);
      VCExpr lhs = Gen.Function(castToU, inner);
      triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(inner)));

      return Gen.Eq(lhs, var);
    }

    protected abstract VCExpr/*!*/ GenCastTypeAxioms(Function/*!*/ castToU, Function/*!*/ castFromU);

    ///////////////////////////////////////////////////////////////////////////
    // storage of type casts for types that are supposed to be left over in the
    // VCs (like int, bool, bitvectors)

    private readonly IDictionary<Type/*!*/, TypeCastSet/*!*/>/*!*/ TypeCasts;
    [ContractInvariantMethod]
    void TypeCastsInvariantMethod() {
      Contract.Invariant(TypeCasts != null);
    }

    private TypeCastSet GetTypeCasts(Type type) {
      Contract.Requires(type != null);
      TypeCastSet res;
      if (!TypeCasts.TryGetValue(type, out res)) {
        Function/*!*/ castToU = HelperFuns.BoogieFunction(type.ToString() + "_2_U", type, U);
        Function/*!*/ castFromU = HelperFuns.BoogieFunction("U_2_" + type.ToString(), U, type);

        AddTypeAxiom(GenLeftInverseAxiom(castToU, castFromU, 0));
        AddTypeAxiom(GenReverseCastAxiom(castToU, castFromU));
        AddTypeAxiom(GenCastTypeAxioms(castToU, castFromU));

        res = new TypeCastSet(castToU, castFromU);
        TypeCasts.Add(type, res);
      }
      return res;
    }
    [Pure]
    public Function CastTo(Type type) {
      Contract.Requires(type != null);
      Contract.Requires(UnchangedType(type));
      Contract.Ensures(Contract.Result<Function>() != null);
      return GetTypeCasts(type).CastFromU;
    }

    public Function CastFrom(Type type) {
      Contract.Requires(type != null);
      Contract.Requires((UnchangedType(type)));
      Contract.Ensures(Contract.Result<Function>() != null);
      return GetTypeCasts(type).CastToU;
    }

    private struct TypeCastSet {
      public readonly Function/*!*/ CastToU;
      public readonly Function/*!*/ CastFromU;
      [ContractInvariantMethod]
      void ObjectInvariant() {
        Contract.Invariant(CastToU != null);
        Contract.Invariant(CastFromU != null);
      }


      public TypeCastSet(Function castToU, Function castFromU) {
        Contract.Requires(castFromU != null);
        Contract.Requires(castToU != null);
        CastToU = castToU;
        CastFromU = castFromU;
      }
    }

    public bool IsCast(Function fun) {
      Contract.Requires(fun != null);
      if (fun.InParams.Length != 1)
        return false;
      Type/*!*/ inType = cce.NonNull(fun.InParams[0]).TypedIdent.Type;
      if (inType.Equals(U)) {
        Type/*!*/ outType = cce.NonNull(fun.OutParams[0]).TypedIdent.Type;
        if (!TypeCasts.ContainsKey(outType))
          return false;
        return fun.Equals(CastTo(outType));
      } else {
        if (!TypeCasts.ContainsKey(inType))
          return false;
        Type/*!*/ outType = cce.NonNull(fun.OutParams[0]).TypedIdent.Type;
        if (!outType.Equals(U))
          return false;
        return fun.Equals(CastFrom(inType));
      }
    }

    ////////////////////////////////////////////////////////////////////////////

    // the only types that we allow in "untyped" expressions are U,
    // Type.Int, and Type.Bool

    public override Type TypeAfterErasure(Type type) {
      //Contract.Requires(type != null);
      Contract.Ensures(Contract.Result<Type>() != null);
      if (UnchangedType(type))
        // these types are kept
        return type;
      else
        // all other types are replaced by U
        return U;
    }

    [Pure]
    public override bool UnchangedType(Type type) {
      //Contract.Requires(type != null);
      return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);
    }

    public VCExpr Cast(VCExpr expr, Type toType) {
      Contract.Requires(toType != null);
      Contract.Requires(expr != null);
      Contract.Requires((expr.Type.Equals(U) || UnchangedType(expr.Type)));
      Contract.Requires((toType.Equals(U) || UnchangedType(toType)));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      if (expr.Type.Equals(toType))
        return expr;

      if (toType.Equals(U)) {
        return Gen.Function(CastFrom(expr.Type), expr);
      } else {
        Contract.Assert(expr.Type.Equals(U));
        return Gen.Function(CastTo(toType), expr);
      }
    }

    public List<VCExpr/*!*/>/*!*/ CastSeq(List<VCExpr/*!*/>/*!*/ exprs, Type toType) {
      Contract.Requires(toType != null);
      Contract.Requires(cce.NonNullElements(exprs));
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
      List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>(exprs.Count);
      foreach (VCExpr/*!*/ expr in exprs) {
        Contract.Assert(expr != null);
        res.Add(Cast(expr, toType));
      }
      return res;
    }


  }

  [ContractClassFor(typeof(TypeAxiomBuilderIntBoolU))]
  public abstract class TypeAxiomBuilderIntBoolUContracts : TypeAxiomBuilderIntBoolU {
    public TypeAxiomBuilderIntBoolUContracts()
      : base((TypeAxiomBuilderIntBoolU)null) {
    }
    protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFromU) {
      Contract.Requires(castToU != null);
      Contract.Requires(castFromU != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      throw new NotImplementedException();
    }

    protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) {
      Contract.Requires(castFromU != null);
      Contract.Requires(castToU != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      throw new NotImplementedException();
    }

    internal override MapTypeAbstractionBuilder MapTypeAbstracter {
      get {
        throw new NotImplementedException();
      }
    }

    protected override void AddVarTypeAxiom(VCExprVar var, Type originalType) {
      throw new NotImplementedException();
    }

    public override object Clone() {
      throw new NotImplementedException();
    }
  }

  //////////////////////////////////////////////////////////////////////////////
  // Class for computing most general abstractions of map types. An abstraction
  // of a map type t is a maptype t' in which closed proper subtypes have been replaced
  // with type variables. E.g., an abstraction of <a>[C a, int]a would be <a>[C a, b]a.
  // We subsequently consider most general abstractions as ordinary parametrised types,
  // i.e., "<a>[C a, b]a" would be considered as a type "M b" with polymorphically typed
  // access functions
  //
  //            select<a,b>(M b, C a, b) returns (a)
  //            store<a,b>(M b, C a, b, a) returns (M b)
  [ContractClass(typeof(MapTypeAbstractionBuilderContracts))]
  internal abstract class MapTypeAbstractionBuilder {

    protected readonly TypeAxiomBuilder/*!*/ AxBuilder;
    protected readonly VCExpressionGenerator/*!*/ Gen;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(AxBuilder != null);
      Contract.Invariant(Gen != null);
    }


    internal MapTypeAbstractionBuilder(TypeAxiomBuilder axBuilder, VCExpressionGenerator gen) {
      Contract.Requires(gen != null);
      Contract.Requires(axBuilder != null);
      this.AxBuilder = axBuilder;
      this.Gen = gen;
      AbstractionVariables = new List<TypeVariable/*!*/>();
      ClassRepresentations = new Dictionary<MapType/*!*/, MapTypeClassRepresentation>();
    }

    // constructor for cloning
    internal MapTypeAbstractionBuilder(TypeAxiomBuilder axBuilder, VCExpressionGenerator gen, MapTypeAbstractionBuilder builder) {
      Contract.Requires(builder != null);
      Contract.Requires(gen != null);
      Contract.Requires(axBuilder != null);
      this.AxBuilder = axBuilder;
      this.Gen = gen;
      AbstractionVariables =
        new List<TypeVariable/*!*/>(builder.AbstractionVariables);
      ClassRepresentations =
        new Dictionary<MapType/*!*/, MapTypeClassRepresentation>(builder.ClassRepresentations);
    }

    ///////////////////////////////////////////////////////////////////////////
    // Type variables used in the abstractions. We use the same variables in the
    // same order in all abstractions in order to obtain comparable abstractions
    // (equals, hashcode)

    private readonly List<TypeVariable/*!*/>/*!*/ AbstractionVariables;
    [ContractInvariantMethod]
    void AbstractionVariablesInvariantMethod() {
      Contract.Invariant(cce.NonNullElements(AbstractionVariables));
    }

    private TypeVariable AbstractionVariable(int num) {
      Contract.Requires((num >= 0));
      Contract.Ensures(Contract.Result<TypeVariable>() != null);
      while (AbstractionVariables.Count <= num)
        AbstractionVariables.Add(new TypeVariable(Token.NoToken,
                                                   "aVar" + AbstractionVariables.Count));
      return AbstractionVariables[num];
    }

    ///////////////////////////////////////////////////////////////////////////
    // The untyped representation of a class of map types, i.e., of a map type
    // <a0, a1, ...>[A0, A1, ...] R, where the argument types and the result type
    // possibly contain free type variables. For each such class, a separate type
    // constructor and separate select/store functions are introduced.

    protected struct MapTypeClassRepresentation {
      public readonly TypeCtorDecl/*!*/ RepresentingType;
      public readonly Function/*!*/ Select;
      public readonly Function/*!*/ Store;
      [ContractInvariantMethod]
      void ObjectInvariant() {
        Contract.Invariant(RepresentingType != null);
        Contract.Invariant(Select != null);
        Contract.Invariant(Store != null);
      }


      public MapTypeClassRepresentation(TypeCtorDecl representingType, Function select, Function store) {
        Contract.Requires(store != null);
        Contract.Requires(select != null);
        Contract.Requires(representingType != null);
        this.RepresentingType = representingType;
        this.Select = select;
        this.Store = store;
      }
    }

    private readonly IDictionary<MapType/*!*/, MapTypeClassRepresentation/*!*/>/*!*/ ClassRepresentations;
    [ContractInvariantMethod]
    void ClassRepresentationsInvariantMethod() {
      Contract.Invariant(ClassRepresentations != null);
    }

    protected MapTypeClassRepresentation GetClassRepresentation(MapType abstractedType) {
      Contract.Requires(abstractedType != null);
      MapTypeClassRepresentation res;
      if (!ClassRepresentations.TryGetValue(abstractedType, out res)) {
        int num = ClassRepresentations.Count;
        TypeCtorDecl/*!*/ synonym =
          new TypeCtorDecl(Token.NoToken, "MapType" + num, abstractedType.FreeVariables.Length);

        Function/*!*/ select, store;
        GenSelectStoreFunctions(abstractedType, synonym, out select, out store);

        res = new MapTypeClassRepresentation(synonym, select, store);
        ClassRepresentations.Add(abstractedType, res);
      }
      return res;
    }

    // the actual select and store functions are generated by the
    // concrete subclasses of this class
    protected abstract void GenSelectStoreFunctions(MapType/*!*/ abstractedType, TypeCtorDecl/*!*/ synonymDecl, out Function/*!*/ select, out Function/*!*/ store);

    ///////////////////////////////////////////////////////////////////////////

    public Function Select(MapType rawType, out TypeSeq instantiations) {
      Contract.Requires((rawType != null));
      Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
      Contract.Ensures(Contract.Result<Function>() != null);
      return AbstractAndGetRepresentation(rawType, out instantiations).Select;
    }

    public Function Store(MapType rawType, out TypeSeq instantiations) {
      Contract.Requires((rawType != null));
      Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
      Contract.Ensures(Contract.Result<Function>() != null);
      return AbstractAndGetRepresentation(rawType, out instantiations).Store;
    }

    private MapTypeClassRepresentation
            AbstractAndGetRepresentation(MapType rawType, out TypeSeq instantiations) {
      Contract.Requires((rawType != null));
      Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
      instantiations = new TypeSeq();
      MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations);
      return GetClassRepresentation(abstraction);
    }

    public CtorType AbstractMapType(MapType rawType) {
      Contract.Requires(rawType != null);
      Contract.Ensures(Contract.Result<CtorType>() != null);
      TypeSeq/*!*/ instantiations = new TypeSeq();
      MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations);

      MapTypeClassRepresentation repr = GetClassRepresentation(abstraction);
      Contract.Assume(repr.RepresentingType.Arity == instantiations.Length);
      return new CtorType(Token.NoToken, repr.RepresentingType, instantiations);
    }

    // TODO: cache the result of this operation
    protected MapType ThinOutMapType(MapType rawType, TypeSeq instantiations) {
      Contract.Requires(instantiations != null);
      Contract.Requires(rawType != null);
      Contract.Ensures(Contract.Result<MapType>() != null);
      TypeSeq/*!*/ newArguments = new TypeSeq();
      foreach (Type/*!*/ subtype in rawType.Arguments) {
        Contract.Assert(subtype != null);
        newArguments.Add(ThinOutType(subtype, rawType.TypeParameters,
                                     instantiations));
      }
      Type/*!*/ newResult = ThinOutType(rawType.Result, rawType.TypeParameters,
                                    instantiations);
      return new MapType(Token.NoToken, rawType.TypeParameters, newArguments, newResult);
    }

    // the instantiations of inserted type variables, the order corresponds to the order in which "AbstractionVariable(int)" delivers variables
    private Type/*!*/ ThinOutType(Type rawType, TypeVariableSeq boundTypeParams, TypeSeq instantiations) {
      Contract.Requires(instantiations != null);
      Contract.Requires(boundTypeParams != null);
      Contract.Requires(rawType != null);
      Contract.Ensures(Contract.Result<Type>() != null);

      if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))
        return rawType;

      if (Contract.ForAll(0, rawType.FreeVariables.Length, var => !boundTypeParams.Has(rawType.FreeVariables[var]))) {
        // Bingo!
        // if the type does not contain any bound variables, we can simply
        // replace it with a type variable
        TypeVariable/*!*/ abstractionVar = AbstractionVariable(instantiations.Length);
        Contract.Assume(!boundTypeParams.Has(abstractionVar));
        instantiations.Add(rawType);
        return abstractionVar;
      }

      if (rawType.IsVariable) {
        //
        // then the variable has to be bound, we cannot do anything
        TypeVariable/*!*/ rawVar = rawType.AsVariable;
        Contract.Assume(boundTypeParams.Has(rawVar));
        return rawVar;
        //
      } else if (rawType.IsMap) {
        //
        // recursively abstract this map type and continue abstracting
        CtorType/*!*/ abstraction = AbstractMapType(rawType.AsMap);
        return ThinOutType(abstraction, boundTypeParams, instantiations);
        //
      } else if (rawType.IsCtor) {
        //
        // traverse the subtypes
        CtorType/*!*/ rawCtorType = rawType.AsCtor;
        TypeSeq/*!*/ newArguments = new TypeSeq();
        foreach (Type/*!*/ subtype in rawCtorType.Arguments) {
          Contract.Assert(subtype != null);
          newArguments.Add(ThinOutType(subtype, boundTypeParams,
                                       instantiations));
        }
        return new CtorType(Token.NoToken, rawCtorType.Decl, newArguments);
        //
      } else {
        System.Diagnostics.Debug.Fail("Don't know how to handle this type: " + rawType);
        return rawType;   // compiler appeasement policy
      }
    }

  }
  [ContractClassFor(typeof(MapTypeAbstractionBuilder))]
  internal abstract class MapTypeAbstractionBuilderContracts : MapTypeAbstractionBuilder {
    public MapTypeAbstractionBuilderContracts()
      : base(null, null) {
    }
    protected override void GenSelectStoreFunctions(MapType abstractedType, TypeCtorDecl synonymDecl, out Function select, out Function store) {
      Contract.Requires(abstractedType != null);
      Contract.Requires(synonymDecl != null);
      Contract.Ensures(Contract.ValueAtReturn(out select) != null);
      Contract.Ensures(Contract.ValueAtReturn(out store) != null);

      throw new NotImplementedException();
    }
  }


  //////////////////////////////////////////////////////////////////////////////

  public class VariableBindings {
    public readonly IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ VCExprVarBindings;
    public readonly IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ TypeVariableBindings;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(cce.NonNullDictionaryAndValues(VCExprVarBindings));
      Contract.Invariant(cce.NonNullDictionaryAndValues(TypeVariableBindings));
    }


    public VariableBindings(IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ vcExprVarBindings,
                            IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ typeVariableBindings) {
      Contract.Requires(cce.NonNullDictionaryAndValues(vcExprVarBindings));
      Contract.Requires(cce.NonNullDictionaryAndValues(typeVariableBindings));
      this.VCExprVarBindings = vcExprVarBindings;
      this.TypeVariableBindings = typeVariableBindings;
    }

    public VariableBindings() :
      this(new Dictionary<VCExprVar/*!*/, VCExprVar/*!*/>(),
            new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>()) {
    }

    public VariableBindings Clone() {
      Contract.Ensures(Contract.Result<VariableBindings>() != null);
      IDictionary<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ newVCExprVarBindings =
        new Dictionary<VCExprVar/*!*/, VCExprVar/*!*/>();
      foreach (KeyValuePair<VCExprVar/*!*/, VCExprVar/*!*/> pair in VCExprVarBindings) {
        Contract.Assert(cce.NonNullElements(pair));
        newVCExprVarBindings.Add(pair);
      }
      IDictionary<TypeVariable/*!*/, VCExpr/*!*/>/*!*/ newTypeVariableBindings =
        new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>();
      foreach (KeyValuePair<TypeVariable/*!*/, VCExpr/*!*/> pair in TypeVariableBindings) {
        Contract.Assert(cce.NonNullElements(pair));
        newTypeVariableBindings.Add(pair);
      }
      return new VariableBindings(newVCExprVarBindings, newTypeVariableBindings);
    }
  }

  //////////////////////////////////////////////////////////////////////////////

  // The central class for turning types VCExprs into untyped
  // VCExprs. This class makes use of the type axiom builder to manage
  // the available types and symbols.
  [ContractClass(typeof(TypeEraserContracts))]
  public abstract class TypeEraser : MutatingVCExprVisitor<VariableBindings/*!*/> {

    protected readonly TypeAxiomBuilderIntBoolU/*!*/ AxBuilder;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(AxBuilder != null);
    }


    protected abstract OpTypeEraser/*!*/ OpEraser {
      get;
    }

    ////////////////////////////////////////////////////////////////////////////

    public TypeEraser(TypeAxiomBuilderIntBoolU axBuilder, VCExpressionGenerator gen)
      : base(gen) {
      Contract.Requires(gen != null);
      Contract.Requires(axBuilder != null);
      AxBuilder = axBuilder;
    }

    public VCExpr Erase(VCExpr expr, int polarity) {
      Contract.Requires(expr != null);
      Contract.Requires((polarity >= -1 && polarity <= 1));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      this.Polarity = polarity;
      return Mutate(expr, new VariableBindings());
    }

    internal int Polarity = 1;  // 1 for positive, -1 for negative, 0 for both

    ////////////////////////////////////////////////////////////////////////////

    public override VCExpr Visit(VCExprLiteral node, VariableBindings bindings) {
      Contract.Requires(bindings != null);
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int);
      return node;
    }

    ////////////////////////////////////////////////////////////////////////////

    public override VCExpr Visit(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires(bindings != null);
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      VCExprOp/*!*/ op = node.Op;
      if (op == VCExpressionGenerator.AndOp || op == VCExpressionGenerator.OrOp)
        // more efficient on large conjunctions/disjunctions
        return base.Visit(node, bindings);

      // the visitor that handles all other operators
      return node.Accept<VCExpr/*!*/, VariableBindings/*!*/>(OpEraser, bindings);
    }

    // this method is called by MutatingVCExprVisitor.Visit(VCExprNAry, ...)
    protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, bool changed, VariableBindings/*!*/ bindings) {
      //Contract.Requires(originalNode != null);
      //Contract.Requires(cce.NonNullElements(newSubExprs));
      //Contract.Requires(bindings != null);
      Contract.Assume(originalNode.Op == VCExpressionGenerator.AndOp ||
             originalNode.Op == VCExpressionGenerator.OrOp);
      return Gen.Function(originalNode.Op,
                          AxBuilder.Cast(newSubExprs[0], Type.Bool),
                          AxBuilder.Cast(newSubExprs[1], Type.Bool));
    }

    ////////////////////////////////////////////////////////////////////////////

    public override VCExpr Visit(VCExprVar node, VariableBindings bindings) {
      Contract.Requires(bindings != null);
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      VCExprVar res;
      if (!bindings.VCExprVarBindings.TryGetValue(node, out res))
        return AxBuilder.Typed2Untyped(node);
      return cce.NonNull(res);
    }

    ////////////////////////////////////////////////////////////////////////////

    protected bool IsUniversalQuantifier(VCExprQuantifier node) {
      Contract.Requires(node != null);
      return Polarity == 1 && node.Quan == Quantifier.EX ||
             Polarity == -1 && node.Quan == Quantifier.ALL;
    }

    protected List<VCExprVar/*!*/>/*!*/ BoundVarsAfterErasure(List<VCExprVar/*!*/>/*!*/ oldBoundVars,
      // the mapping between old and new variables
      // is added to this bindings-object
                                                      VariableBindings/*!*/ bindings) {
      Contract.Requires(bindings != null);
      Contract.Requires(cce.NonNullElements(oldBoundVars));
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));

      List<VCExprVar/*!*/>/*!*/ newBoundVars = new List<VCExprVar/*!*/>(oldBoundVars.Count);
      foreach (VCExprVar/*!*/ var in oldBoundVars) {
        Type/*!*/ newType = AxBuilder.TypeAfterErasure(var.Type);
        VCExprVar/*!*/ newVar = Gen.Variable(var.Name, newType);
        newBoundVars.Add(newVar);
        bindings.VCExprVarBindings.Add(var, newVar);
      }
      return newBoundVars;
    }

    // We check whether casts Int2U or Bool2U on the bound variables
    // occur in triggers. In case a trigger like f(Int2U(x)) occurs,
    // it may be better to give variable x the type U and remove the
    // cast. The following method returns true if the quantifier
    // should be translated again with a different typing
    protected bool RedoQuantifier(VCExprQuantifier/*!*/ node,
                                  VCExprQuantifier/*!*/ newNode,
      // the bound vars that actually occur in the body or
      // in any of the triggers
                                  List<VCExprVar/*!*/>/*!*/ occurringVars,
                                  VariableBindings/*!*/ oldBindings,
                                  out VariableBindings/*!*/ newBindings,
                                  out List<VCExprVar/*!*/>/*!*/ newBoundVars) {
      Contract.Requires(node != null);
      Contract.Requires(newNode != null);
      Contract.Requires(cce.NonNullElements(occurringVars));
      Contract.Requires(oldBindings != null);
      Contract.Ensures(Contract.ValueAtReturn(out newBindings) != null);
      Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out newBoundVars)));
      List<VCExprVar/*!*/> castVariables =
        VariableCastCollector.FindCastVariables(node, newNode, AxBuilder);
      if (castVariables.Count == 0) {
        newBindings = oldBindings;         // to make the compiler happy
        newBoundVars = newNode.BoundVars;  // to make the compiler happy
        return false;
      }

      // redo everything with a different typing ...

      newBindings = oldBindings.Clone();
      newBoundVars = new List<VCExprVar/*!*/>(node.BoundVars.Count);
      foreach (VCExprVar/*!*/ var in node.BoundVars) {
        Contract.Assert(var != null);
        Type/*!*/ newType =
          castVariables.Contains(var) ? AxBuilder.U
                                      : AxBuilder.TypeAfterErasure(var.Type);
        Contract.Assert(newType != null);
        VCExprVar/*!*/ newVar = Gen.Variable(var.Name, newType);
        Contract.Assert(newVar != null);
        newBoundVars.Add(newVar);
        newBindings.VCExprVarBindings.Add(var, newVar);
      }

      return true;
    }

    ////////////////////////////////////////////////////////////////////////////

    public override VCExpr Visit(VCExprLet node, VariableBindings bindings) {
      Contract.Requires(bindings != null);
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      VariableBindings/*!*/ newVarBindings = bindings.Clone();

      List<VCExprVar/*!*/>/*!*/ newBoundVars = new List<VCExprVar/*!*/>(node.BoundVars.Count);
      foreach (VCExprVar/*!*/ var in node.BoundVars) {
        Type/*!*/ newType = AxBuilder.TypeAfterErasure(var.Type);
        VCExprVar/*!*/ newVar = Gen.Variable(var.Name, newType);
        newBoundVars.Add(newVar);
        newVarBindings.VCExprVarBindings.Add(var, newVar);
      }

      List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/>(node.Length);
      for (int i = 0; i < node.Length; ++i) {
        VCExprLetBinding/*!*/ binding = node[i];
        Contract.Assert(binding != null);
        VCExprVar/*!*/ newVar = newBoundVars[i];
        Type/*!*/ newType = newVar.Type;

        VCExpr/*!*/ newE = AxBuilder.Cast(Mutate(binding.E, newVarBindings), newType);
        newbindings.Add(Gen.LetBinding(newVar, newE));
      }

      VCExpr/*!*/ newbody = Mutate(node.Body, newVarBindings);
      return Gen.Let(newbindings, newbody);
    }
  }

  [ContractClassFor(typeof(TypeEraser))]
  public abstract class TypeEraserContracts : TypeEraser {
    public TypeEraserContracts()
      : base(null, null) {
    }
    protected override OpTypeEraser OpEraser {
      get {
        Contract.Ensures(Contract.Result<OpTypeEraser>() != null);
        throw new NotImplementedException();
      }
    }
  }


  //////////////////////////////////////////////////////////////////////////////

  public abstract class OpTypeEraser : StandardVCExprOpVisitor<VCExpr/*!*/, VariableBindings/*!*/> {

    protected readonly TypeAxiomBuilderIntBoolU/*!*/ AxBuilder;

    protected readonly TypeEraser/*!*/ Eraser;
    protected readonly VCExpressionGenerator/*!*/ Gen;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(AxBuilder != null);
      Contract.Invariant(Eraser != null);
      Contract.Invariant(Gen != null);
    }


    public OpTypeEraser(TypeEraser/*!*/ eraser, TypeAxiomBuilderIntBoolU/*!*/ axBuilder, VCExpressionGenerator/*!*/ gen) {
      Contract.Requires(eraser != null);
      Contract.Requires(axBuilder != null);
      Contract.Requires(gen != null);
      this.AxBuilder = axBuilder;
      this.Eraser = eraser;
      this.Gen = gen;
    }

    protected override VCExpr StandardResult(VCExprNAry node, VariableBindings bindings) {
      //Contract.Requires(bindings != null);
      //Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      System.Diagnostics.Debug.Fail("Don't know how to erase types in this expression: " + node);
      Contract.Assert(false);
      throw new cce.UnreachableException();  // to please the compiler
    }

    private List<VCExpr/*!*/>/*!*/ MutateSeq(VCExprNAry node, VariableBindings bindings, int newPolarity) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
      int oldPolarity = Eraser.Polarity;
      Eraser.Polarity = newPolarity;
      List<VCExpr/*!*/>/*!*/ newArgs = Eraser.MutateSeq(node, bindings);
      Eraser.Polarity = oldPolarity;
      return newArgs;
    }

    private VCExpr CastArguments(VCExprNAry node, Type argType, VariableBindings bindings, int newPolarity) {
      Contract.Requires(bindings != null);
      Contract.Requires(argType != null);
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Gen.Function(node.Op,
                          AxBuilder.CastSeq(MutateSeq(node, bindings, newPolarity),
                          argType));
    }

    // Cast the arguments of the node to their old type if necessary and possible; otherwise use
    // their new type (int, bool, or U)
    private VCExpr CastArgumentsToOldType(VCExprNAry node, VariableBindings bindings, int newPolarity) {
      Contract.Requires(bindings != null);
      Contract.Requires(node != null);
      Contract.Requires((node.Arity > 0));
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      List<VCExpr/*!*/>/*!*/ newArgs = MutateSeq(node, bindings, newPolarity);
      Type/*!*/ oldType = node[0].Type;
      if (AxBuilder.UnchangedType(oldType) &&
          Contract.ForAll(1, node.Arity, i => node[i].Type.Equals(oldType)))
        return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, oldType));
      else
        return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U));
    }

    ///////////////////////////////////////////////////////////////////////////

    public override VCExpr VisitNotOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, Type.Bool, bindings, -Eraser.Polarity);
    }
    public override VCExpr VisitEqOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArgumentsToOldType(node, bindings, 0);
    }
    public override VCExpr VisitNeqOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArgumentsToOldType(node, bindings, 0);
    }
    public override VCExpr VisitImpliesOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      // UGLY: the code for tracking polarities should be factored out
      List<VCExpr/*!*/>/*!*/ newArgs = new List<VCExpr/*!*/>(2);
      Eraser.Polarity = -Eraser.Polarity;
      newArgs.Add(Eraser.Mutate(node[0], bindings));
      Eraser.Polarity = -Eraser.Polarity;
      newArgs.Add(Eraser.Mutate(node[1], bindings));
      return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, Type.Bool));
    }
    public override VCExpr VisitDistinctOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArgumentsToOldType(node, bindings, 0);
    }
    public override VCExpr VisitLabelOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      // argument of the label operator should always be a formula
      // (at least for Simplify ... should this be ensured at a later point?)
      return CastArguments(node, Type.Bool, bindings, Eraser.Polarity);
    }
    public override VCExpr VisitIfThenElseOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      List<VCExpr/*!*/>/*!*/ newArgs = MutateSeq(node, bindings, 0);
      newArgs[0] = AxBuilder.Cast(newArgs[0], Type.Bool);
      Type t = node.Type;
      if (!AxBuilder.UnchangedType(t)) {
        t = AxBuilder.U;
      }
      newArgs[1] = AxBuilder.Cast(newArgs[1], t);
      newArgs[2] = AxBuilder.Cast(newArgs[2], t);
      return Gen.Function(node.Op, newArgs);
    }
    public override VCExpr/*!*/ VisitCustomOp(VCExprNAry/*!*/ node, VariableBindings/*!*/ bindings) {
      Contract.Requires(node != null);
      Contract.Requires(bindings != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      List<VCExpr/*!*/>/*!*/ newArgs = MutateSeq(node, bindings, 0);
      return Gen.Function(node.Op, newArgs);
    }
    public override VCExpr VisitAddOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, Type.Int, bindings, 0);
    }
    public override VCExpr VisitSubOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, Type.Int, bindings, 0);
    }
    public override VCExpr VisitMulOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, Type.Int, bindings, 0);
    }
    public override VCExpr VisitDivOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, Type.Int, bindings, 0);
    }
    public override VCExpr VisitModOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, Type.Int, bindings, 0);
    }
    public override VCExpr VisitLtOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, Type.Int, bindings, 0);
    }
    public override VCExpr VisitLeOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, Type.Int, bindings, 0);
    }
    public override VCExpr VisitGtOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, Type.Int, bindings, 0);
    }
    public override VCExpr VisitGeOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, Type.Int, bindings, 0);
    }
    public override VCExpr VisitSubtypeOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArguments(node, AxBuilder.U, bindings, 0);
    }
    public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArgumentsToOldType(node, bindings, 0);
    }
    public override VCExpr VisitBvExtractOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires(bindings != null);
      Contract.Requires(node != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return CastArgumentsToOldType(node, bindings, 0);
    }
    public override VCExpr VisitBvConcatOp(VCExprNAry node, VariableBindings bindings) {
      Contract.Requires((bindings != null));
      Contract.Requires((node != null));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      List<VCExpr/*!*/>/*!*/ newArgs = MutateSeq(node, bindings, 0);

      // each argument is cast to its old type
      Contract.Assert(newArgs.Count == node.Arity && newArgs.Count == 2);
      VCExpr/*!*/ arg0 = AxBuilder.Cast(newArgs[0], node[0].Type);
      Contract.Assert(arg0 != null);
      VCExpr/*!*/ arg1 = AxBuilder.Cast(newArgs[1], node[1].Type);
      Contract.Assert(arg1 != null);
      return Gen.Function(node.Op, arg0, arg1);
    }

  }

  //////////////////////////////////////////////////////////////////////////////

  /// <summary>
  /// Collect all variables x occurring in expressions of the form Int2U(x) or Bool2U(x), and
  /// collect all variables x occurring outside such forms.
  /// </summary>
  internal class VariableCastCollector : TraversingVCExprVisitor<bool, bool> {
    /// <summary>
    /// Determine those bound variables in "oldNode" <em>all</em> of whose relevant uses
    /// have to be cast in potential triggers in "newNode".  It is assume that
    /// the bound variables of "oldNode" correspond to the first bound
    /// variables of "newNode".
    /// </summary>
    public static List<VCExprVar/*!*/>/*!*/ FindCastVariables(VCExprQuantifier oldNode, VCExprQuantifier newNode, TypeAxiomBuilderIntBoolU axBuilder) {
      Contract.Requires((axBuilder != null));
      Contract.Requires((newNode != null));
      Contract.Requires((oldNode != null));
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
      VariableCastCollector/*!*/ collector = new VariableCastCollector(axBuilder);
      Contract.Assert(collector != null);
      if (Contract.Exists(newNode.Triggers, trigger => trigger.Pos)) {
        // look in the given triggers
        foreach (VCTrigger/*!*/ trigger in newNode.Triggers) {
          Contract.Assert(trigger != null);
          if (trigger.Pos) {
            foreach (VCExpr/*!*/ expr in trigger.Exprs) {
              Contract.Assert(expr != null);
              collector.Traverse(expr, true);
            }
          }
        }
      } else {
        // look in the body of the quantifier
        collector.Traverse(newNode.Body, true);
      }

      List<VCExprVar/*!*/>/*!*/ castVariables = new List<VCExprVar/*!*/>(collector.varsInCasts.Count);
      foreach (VCExprVar/*!*/ castVar in collector.varsInCasts) {
        Contract.Assert(castVar != null);
        int i = newNode.BoundVars.IndexOf(castVar);
        if (0 <= i && i < oldNode.BoundVars.Count && !collector.varsOutsideCasts.ContainsKey(castVar))
          castVariables.Add(oldNode.BoundVars[i]);
      }
      return castVariables;
    }

    public VariableCastCollector(TypeAxiomBuilderIntBoolU axBuilder) {
      Contract.Requires(axBuilder != null);
      this.AxBuilder = axBuilder;
    }

    readonly List<VCExprVar/*!*/>/*!*/ varsInCasts = new List<VCExprVar/*!*/>();
    readonly Dictionary<VCExprVar/*!*/, object>/*!*/ varsOutsideCasts = new Dictionary<VCExprVar/*!*/, object>();
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(cce.NonNullElements(varsInCasts));
      Contract.Invariant(varsOutsideCasts != null && Contract.ForAll(varsOutsideCasts, voc => voc.Key != null));
      Contract.Invariant(AxBuilder != null);

    }


    readonly TypeAxiomBuilderIntBoolU/*!*/ AxBuilder;

    protected override bool StandardResult(VCExpr node, bool arg) {
      //Contract.Requires(node != null);
      return true; // not used
    }

    public override bool Visit(VCExprNAry node, bool arg) {
      Contract.Requires(node != null);
      if (node.Op is VCExprBoogieFunctionOp) {
        Function func = ((VCExprBoogieFunctionOp)node.Op).Func;
        Contract.Assert(func != null);
        if ((AxBuilder.IsCast(func)) && node[0] is VCExprVar) {
          VCExprVar castVar = (VCExprVar)node[0];
          if (!varsInCasts.Contains(castVar))
            varsInCasts.Add(castVar);
          return true;
        }
      } else if (node.Op is VCExprNAryOp) {
        VCExpressionGenerator.SingletonOp op = VCExpressionGenerator.SingletonOpDict[node.Op];
        switch (op) {
          // the following operators cannot be used in triggers, so disregard any uses of variables as direct arguments
          case VCExpressionGenerator.SingletonOp.NotOp:
          case VCExpressionGenerator.SingletonOp.EqOp:
          case VCExpressionGenerator.SingletonOp.NeqOp:
          case VCExpressionGenerator.SingletonOp.AndOp:
          case VCExpressionGenerator.SingletonOp.OrOp:
          case VCExpressionGenerator.SingletonOp.ImpliesOp:
          case VCExpressionGenerator.SingletonOp.LtOp:
          case VCExpressionGenerator.SingletonOp.LeOp:
          case VCExpressionGenerator.SingletonOp.GtOp:
          case VCExpressionGenerator.SingletonOp.GeOp:
            foreach (VCExpr n in node) {
              if (!(n is VCExprVar)) {  // don't recurse on VCExprVar argument
                n.Accept<bool, bool>(this, arg);
              }
            }
            return true;
          default:
            break;
        }
      }
      return base.Visit(node, arg);
    }

    public override bool Visit(VCExprVar node, bool arg) {
      Contract.Requires(node != null);
      if (!varsOutsideCasts.ContainsKey(node))
        varsOutsideCasts.Add(node, null);
      return true;
    }
  }

}