path: root/Source/VCExpr/VCExprAST.cs

//-----------------------------------------------------------------------------
//
// 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;

// Prover-independent syntax trees for representing verification conditions
// The language can be seen as a simple polymorphically typed first-order logic,
// very similar to the expression language of Boogie

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

  public class VCExpressionGenerator {
    public static readonly VCExpr False = new VCExprLiteral(Type.Bool);
    public static readonly VCExpr True = new VCExprLiteral(Type.Bool);

    private Function ControlFlowFunction = null;
    public VCExpr ControlFlowFunctionApplication(VCExpr e1, VCExpr e2) {
      Contract.Requires(e1 != null);
      Contract.Requires(e2 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      if (ControlFlowFunction == null) {
        Formal/*!*/ first = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);
        Formal/*!*/ second = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);
        List<Variable> inputs = new List<Variable>();
        inputs.Add(first);
        inputs.Add(second);
        Formal/*!*/ returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), false);
        ControlFlowFunction = new Function(Token.NoToken, "ControlFlow", inputs, returnVar);
      }
      List<VCExpr/*!*/> args = new List<VCExpr/*!*/>();
      args.Add(e1);
      args.Add(e2);
      return Function(BoogieFunctionOp(ControlFlowFunction), args);
    }

    public VCExpr/*!*/ Integer(BigNum x) {
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      return new VCExprIntLit(x);
    }

    public VCExpr/*!*/ Real(BigDec x) {
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      return new VCExprRealLit(x);
    }

    public VCExpr/*!*/ Function(VCExprOp/*!*/ op,
                            List<VCExpr/*!*/>/*!*/ arguments,
                            List<Type/*!*/>/*!*/ typeArguments) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(arguments));
      Contract.Requires(cce.NonNullElements(typeArguments));
      if (typeArguments.Count > 0)
        return new VCExprMultiAry(op, arguments, typeArguments);

      switch (arguments.Count) {
        case 0:
          return new VCExprNullary(op);
        case 1:
          return new VCExprUnary(op, arguments);
        case 2:
          return new VCExprBinary(op, arguments);
        default:
          return new VCExprMultiAry(op, arguments);
      }
    }

    public VCExpr/*!*/ Function(VCExprOp/*!*/ op, List<VCExpr/*!*/>/*!*/ arguments) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(arguments));
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      return Function(op, arguments, VCExprNAry.EMPTY_TYPE_LIST);
    }

    public VCExpr/*!*/ Function(VCExprOp/*!*/ op, params VCExpr[]/*!*/ arguments) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(arguments));

      return Function(op,
                      HelperFuns.ToNonNullList(arguments),
                      VCExprNAry.EMPTY_TYPE_LIST);
    }

    public VCExpr/*!*/ Function(VCExprOp/*!*/ op, VCExpr[]/*!*/ arguments, Type[]/*!*/ typeArguments) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(arguments));
      Contract.Requires(cce.NonNullElements(typeArguments));
      Contract.Ensures(Contract.Result<VCExpr>() != null);


      return Function(op,
                      HelperFuns.ToNonNullList(arguments),
                      HelperFuns.ToNonNullList(typeArguments));
    }

    public VCExpr/*!*/ Function(Function/*!*/ op, List<VCExpr/*!*/>/*!*/ arguments) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(arguments));
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      return Function(BoogieFunctionOp(op), arguments, VCExprNAry.EMPTY_TYPE_LIST);
    }

    public VCExpr/*!*/ Function(Function/*!*/ op, params VCExpr[]/*!*/ arguments) {
      Contract.Requires(cce.NonNullElements(arguments));
      Contract.Requires(op != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      return Function(BoogieFunctionOp(op), arguments);
    }


    // The following method should really be called "ReduceLeft". It must
    // only be used for the binary operators "and" and "or"
    public VCExpr/*!*/ NAry(VCExprOp/*!*/ op, List<VCExpr/*!*/>/*!*/ args) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      return NAry(op, args.ToArray());
    }

    public VCExpr/*!*/ NAry(VCExprOp/*!*/ op, params VCExpr[]/*!*/ args) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(args));
      Contract.Requires(op == AndOp || op == OrOp);
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      bool and = (op == AndOp);

      VCExpr/*!*/ e = and ? True : False;
      foreach (VCExpr a in args) {
        e = and ? AndSimp(e, cce.NonNull(a)) : OrSimp(e, cce.NonNull(a));
      }
      return e;
    }

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

    public static readonly VCExprOp NotOp = new VCExprNAryOp(1, Type.Bool);
    public static readonly VCExprOp EqOp = new VCExprNAryOp(2, Type.Bool);
    public static readonly VCExprOp NeqOp = new VCExprNAryOp(2, Type.Bool);
    public static readonly VCExprOp AndOp = new VCExprNAryOp(2, Type.Bool);
    public static readonly VCExprOp OrOp = new VCExprNAryOp(2, Type.Bool);
    public static readonly VCExprOp ImpliesOp = new VCExprNAryOp(2, Type.Bool);

    public VCExprDistinctOp DistinctOp(int arity) {
      Contract.Ensures(Contract.Result<VCExprDistinctOp>() != null);

      return new VCExprDistinctOp(arity);
    }

    public VCExpr/*!*/ Not(List<VCExpr/*!*/>/*!*/ args) {
      Contract.Requires(args != null);
      Contract.Requires(args.Count == 1);
      Contract.Requires(args[0] != null);
      return Function(NotOp, args);
    }

    public VCExpr/*!*/ Not(VCExpr/*!*/ e0) {
      Contract.Requires(e0 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      return Function(NotOp, e0);
    }
    public VCExpr/*!*/ Eq(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
      return Function(EqOp, e0, e1);
    }
    public VCExpr/*!*/ Neq(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
      Contract.Requires(e0 != null);
      Contract.Requires(e1 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      return Function(NeqOp, e0, e1);
    }
    public VCExpr/*!*/ And(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
      Contract.Requires(e0 != null);
      Contract.Requires(e1 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(AndOp, e0, e1);
    }
    public VCExpr/*!*/ Gt(VCExpr/*!*/ e0, VCExpr/*!*/ e1)
    {
        Contract.Requires(e0 != null);
        Contract.Requires(e1 != null);
        Contract.Ensures(Contract.Result<VCExpr>() != null);

        return Function(GtOp, e0, e1);
    }
    public VCExpr/*!*/ Add(VCExpr/*!*/ e0, VCExpr/*!*/ e1)
    {
        Contract.Requires(e0 != null);
        Contract.Requires(e1 != null);
        Contract.Ensures(Contract.Result<VCExpr>() != null);

        VCExprOp op = cce.NonNull(cce.NonNull(e0).Type).IsInt ? AddIOp : AddROp;
        return Function(op, e0, e1);
    }
    public VCExpr/*!*/ Or(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
      Contract.Requires(e0 != null);
      Contract.Requires(e1 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(OrOp, e0, e1);
    }
    public VCExpr/*!*/ Implies(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
      Contract.Requires(e0 != null);
      Contract.Requires(e1 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(ImpliesOp, e0, e1);
    }
    public VCExpr/*!*/ Distinct(List<VCExpr/*!*/>/*!*/ args) {
      Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<VCExpr>() != null);

      if (args.Count <= 1)
        // trivial case
        return True;
      return Function(DistinctOp(args.Count), args);
    }

    ///////////////////////////////////////////////////////////////////////////
    // Versions of the propositional operators that automatically simplify in
    // certain cases (for example, if one of the operators is True or False)

    public VCExpr NotSimp(VCExpr e0) {
      Contract.Requires(e0 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      if (e0.Equals(True))
        return False;
      if (e0.Equals(False))
        return True;
      return Not(e0);
    }
    public VCExpr AndSimp(VCExpr e0, VCExpr e1) {
      Contract.Requires(e1 != null);
      Contract.Requires(e0 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      if (e0.Equals(True))
        return e1;
      if (e1.Equals(True))
        return e0;
      if (e0.Equals(False) || e1.Equals(False))
        return False;
      return And(e0, e1);
    }
    public VCExpr OrSimp(VCExpr e0, VCExpr e1) {
      Contract.Requires(e1 != null);
      Contract.Requires(e0 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      if (e0.Equals(False))
        return e1;
      if (e1.Equals(False))
        return e0;
      if (e0.Equals(True) || e1.Equals(True))
        return True;
      return Or(e0, e1);
    }
    public VCExpr ImpliesSimp(VCExpr e0, VCExpr e1, bool aggressive = true) {
      Contract.Requires(e1 != null);
      Contract.Requires(e0 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      if (e0.Equals(True))
        return e1;
      if (e1.Equals(False))
        return NotSimp(e0);
      if (e0.Equals(False) || e1.Equals(True))
        return True;
      // attempt to save on the depth of expressions (to reduce chances of stack overflows)
      while (aggressive && e1 is VCExprBinary) {
        VCExprBinary n = (VCExprBinary)e1;
        if (n.Op == ImpliesOp) {
          if (AndSize(n[0]) <= AndSize(e0)) {
            // combine the antecedents
            e0 = And(e0, n[0]);
            e1 = n[1];
            continue;
          }
        }
        break;
      }
      return Implies(e0, e1);
    }

    ///<summary>
    /// Returns some measure of the number of conjuncts in e.  This could be the total number of conjuncts in all
    /// top-most layers of the expression, or it can simply be the length of the left-prong of this and-tree.  The
    /// important thing is that: AndSize(e0) >= AndSize(31) ==> AndSize(And(e0,e1)) > AndSize(e0).
    ///</summary>
    int AndSize(VCExpr e) {
      Contract.Requires(e != null);
      int n = 1;
      while (true) {
        VCExprNAry nary = e as VCExprNAry;
        if (nary != null && nary.Op == AndOp && 2 <= nary.Arity) {
          e = nary[0];
          n++;
        } else {
          return n;
        }
      }
    }

    ////////////////////////////////////////////////////////////////////////////////
    // Further operators

    public static readonly VCExprOp AddIOp = new VCExprNAryOp(2, Type.Int);
    public static readonly VCExprOp AddROp = new VCExprNAryOp(2, Type.Real);
    public static readonly VCExprOp SubIOp = new VCExprNAryOp(2, Type.Int);
    public static readonly VCExprOp SubROp = new VCExprNAryOp(2, Type.Real);
    public static readonly VCExprOp MulIOp = new VCExprNAryOp(2, Type.Int);
    public static readonly VCExprOp MulROp = new VCExprNAryOp(2, Type.Real);
    public static readonly VCExprOp DivIOp = new VCExprNAryOp(2, Type.Int);
    public static readonly VCExprOp DivROp = new VCExprNAryOp(2, Type.Real);
    public static readonly VCExprOp ModOp = new VCExprNAryOp(2, Type.Int);
    public static readonly VCExprOp PowOp = new VCExprNAryOp(2, Type.Real);
    public static readonly VCExprOp LtOp = new VCExprNAryOp(2, Type.Bool);
    public static readonly VCExprOp LeOp = new VCExprNAryOp(2, Type.Bool);
    public static readonly VCExprOp GtOp = new VCExprNAryOp(2, Type.Bool);
    public static readonly VCExprOp GeOp = new VCExprNAryOp(2, Type.Bool);
    public static readonly VCExprOp SubtypeOp = new VCExprNAryOp(2, Type.Bool);
    // ternary version of the subtype operator, the first argument of which gives
    // the type of the compared terms
    public static readonly VCExprOp Subtype3Op = new VCExprNAryOp(3, Type.Bool);
    public static readonly VCExprOp IfThenElseOp = new VCExprIfThenElseOp();
    public static readonly VCExprOp ToIntOp = new VCExprNAryOp(1, Type.Int);
    public static readonly VCExprOp ToRealOp = new VCExprNAryOp(1, Type.Real);

    public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);

    public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool);

    public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool);
    public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool);

    public VCExprOp BoogieFunctionOp(Function func) {
      Contract.Requires(func != null);
      Contract.Ensures(Contract.Result<VCExprOp>() != null);
      return new VCExprBoogieFunctionOp(func);
    }

    // Bitvector nodes

    public VCExpr Bitvector(BvConst bv) {
      Contract.Requires(bv != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(new VCExprBvOp(bv.Bits), Integer(bv.Value));
    }

    public VCExpr BvExtract(VCExpr bv, int bits, int start, int end) {
      Contract.Requires(bv != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(new VCExprBvExtractOp(start, end, bits), bv);
    }

    public VCExpr BvConcat(VCExpr bv1, VCExpr bv2) {
      Contract.Requires(bv2 != null);
      Contract.Requires(bv1 != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(new VCExprBvConcatOp(bv1.Type.BvBits, bv2.Type.BvBits), bv1, bv2);
    }

    public VCExpr AtMost(VCExpr smaller, VCExpr greater) {
      Contract.Requires(greater != null);
      Contract.Requires(smaller != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(SubtypeOp, smaller, greater);
    }


    ////////////////////////////////////////////////////////////////////////////////
    // Dispatcher for the visitor

    // the declared singleton operators
    internal enum SingletonOp {
      NotOp,
      EqOp,
      NeqOp,
      AndOp,
      OrOp,
      ImpliesOp,
      AddOp,
      SubOp,
      MulOp,
      DivOp,
      ModOp,
      RealDivOp,
      PowOp,
      LtOp,
      LeOp,
      GtOp,
      GeOp,
      SubtypeOp,
      Subtype3Op,
      BvConcatOp,
      ToIntOp,
      ToRealOp
    };
    internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict;
    [ContractInvariantMethod]
    void MiscInvariant() {
      Contract.Invariant(SingletonOpDict != null);
    }


    static VCExpressionGenerator() {
      SingletonOpDict = new Dictionary<VCExprOp/*!*/, SingletonOp>();
      SingletonOpDict.Add(NotOp, SingletonOp.NotOp);
      SingletonOpDict.Add(EqOp, SingletonOp.EqOp);
      SingletonOpDict.Add(NeqOp, SingletonOp.NeqOp);
      SingletonOpDict.Add(AndOp, SingletonOp.AndOp);
      SingletonOpDict.Add(OrOp, SingletonOp.OrOp);
      SingletonOpDict.Add(ImpliesOp, SingletonOp.ImpliesOp);
      SingletonOpDict.Add(AddIOp, SingletonOp.AddOp);
      SingletonOpDict.Add(AddROp, SingletonOp.AddOp);
      SingletonOpDict.Add(SubIOp, SingletonOp.SubOp);
      SingletonOpDict.Add(SubROp, SingletonOp.SubOp);
      SingletonOpDict.Add(MulIOp, SingletonOp.MulOp);
      SingletonOpDict.Add(MulROp, SingletonOp.MulOp);
      SingletonOpDict.Add(DivIOp, SingletonOp.DivOp);
      SingletonOpDict.Add(DivROp, SingletonOp.RealDivOp);
      SingletonOpDict.Add(ModOp, SingletonOp.ModOp);
      SingletonOpDict.Add(PowOp, SingletonOp.PowOp);
      SingletonOpDict.Add(LtOp, SingletonOp.LtOp);
      SingletonOpDict.Add(LeOp, SingletonOp.LeOp);
      SingletonOpDict.Add(GtOp, SingletonOp.GtOp);
      SingletonOpDict.Add(GeOp, SingletonOp.GeOp);
      SingletonOpDict.Add(SubtypeOp, SingletonOp.SubtypeOp);
      SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op);
      SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp);
      SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp);
    }

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


    // Let-bindings

    public VCExprLetBinding LetBinding(VCExprVar v, VCExpr e) {
      Contract.Requires(e != null);
      Contract.Requires(v != null);
      Contract.Ensures(Contract.Result<VCExprLetBinding>() != null);
      return new VCExprLetBinding(v, e);
    }

    // A "real" let expression. All let-bindings happen simultaneously, i.e.,
    // at this level the order of the bindings does not matter. It is possible to
    // create expressions like   "let x = y, y = 5 in ...". All bound variables are
    // bound in all bound terms/formulas and can occur there, but the dependencies
    // have to be acyclic
    public VCExpr Let(List<VCExprLetBinding> bindings, VCExpr body) {
      Contract.Requires(body != null);
      Contract.Requires(cce.NonNullElements(bindings));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      if (bindings.Count == 0)
        // no empty let-bindings
        return body;
      return new VCExprLet(bindings, body);
    }

    public VCExpr Let(VCExpr body, params VCExprLetBinding[] bindings) {
      Contract.Requires(body != null);
      Contract.Requires((cce.NonNullElements(bindings)));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Let(HelperFuns.ToNonNullList(bindings), body);
    }


    /// <summary>
    /// In contrast to the previous method, the following methods are not a general LET.
    ///  Instead, it
    /// is a boolean "LET b = P in Q", where P and Q are predicates, that is allowed to be
    /// encoded as "(b == P) ==> Q" or even as "(P ==> b) ==> Q"
    /// (or "(P ==> b) and Q" in negative positions).
    /// The method assumes that the variables in the bindings are unique in the entire formula
    /// to be produced, which allows the implementation to ignore scope issues in the event that
    /// it needs to generate an alternate expression for LET.
    /// </summary>


    // Turn let-bindings let v = E in ... into implications E ==> v
    public VCExpr AsImplications(List<VCExprLetBinding> bindings) {
      Contract.Requires(cce.NonNullElements(bindings));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      VCExpr/*!*/ antecedents = True;
      foreach (VCExprLetBinding b in bindings)
        // turn "LET_binding v = E" into "v <== E"
        antecedents = AndSimp(antecedents, Implies(b.E, b.V));
      return antecedents;
    }

    // Turn let-bindings let v = E in ... into equations v == E
    public VCExpr AsEquations(List<VCExprLetBinding> bindings) {
      Contract.Requires(cce.NonNullElements(bindings));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      VCExpr/*!*/ antecedents = True;
      foreach (VCExprLetBinding b in bindings)
        // turn "LET_binding v = E" into "v <== E"
        antecedents = AndSimp(antecedents, Eq(b.E, b.V));
      return antecedents;
    }



    // Maps

    public VCExpr Select(params VCExpr[] allArgs) {
      Contract.Requires(allArgs != null);
      Contract.Requires((cce.NonNullElements(allArgs)));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(new VCExprSelectOp(allArgs.Length - 1, 0),
                      HelperFuns.ToNonNullList(allArgs),
                      VCExprNAry.EMPTY_TYPE_LIST);
    }

    public VCExpr Select(VCExpr[] allArgs, Type[] typeArgs) {
      Contract.Requires(1 <= allArgs.Length);
      Contract.Requires(cce.NonNullElements(allArgs));
      Contract.Requires(cce.NonNullElements(typeArgs));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(new VCExprSelectOp(allArgs.Length - 1, typeArgs.Length),
                      allArgs, typeArgs);
    }

    public VCExpr Select(List<VCExpr> allArgs, List<Type> typeArgs) {
      Contract.Requires(cce.NonNullElements(typeArgs));
      Contract.Requires(cce.NonNullElements(allArgs));
      Contract.Requires((1 <= allArgs.Count));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(new VCExprSelectOp(allArgs.Count - 1, typeArgs.Count),
                      allArgs, typeArgs);
    }

    public VCExpr Store(params VCExpr[] allArgs) {
      Contract.Requires(allArgs != null);
      Contract.Requires(cce.NonNullElements(allArgs));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(new VCExprStoreOp(allArgs.Length - 2, 0),
                      HelperFuns.ToNonNullList(allArgs),
                      VCExprNAry.EMPTY_TYPE_LIST);
    }

    public VCExpr Store(VCExpr[] allArgs, Type[] typeArgs) {
      Contract.Requires(typeArgs != null);
      Contract.Requires(allArgs != null);
      Contract.Requires((2 <= allArgs.Length));
      Contract.Requires(cce.NonNullElements(allArgs));
      Contract.Requires(cce.NonNullElements(typeArgs));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(new VCExprStoreOp(allArgs.Length - 2, typeArgs.Length),
                      allArgs, typeArgs);
    }

    public VCExpr Store(List<VCExpr> allArgs, List<Type/*!*/>/*!*/ typeArgs) {
      Contract.Requires(cce.NonNullElements(typeArgs));
      Contract.Requires(cce.NonNullElements(allArgs));
      Contract.Requires((2 <= allArgs.Count));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(new VCExprStoreOp(allArgs.Count - 2, typeArgs.Count),
                      allArgs, typeArgs);
    }


    // Labels

    public VCExprLabelOp LabelOp(bool pos, string l) {
      Contract.Requires(l != null);
      Contract.Ensures(Contract.Result<VCExprLabelOp>() != null);
      return new VCExprLabelOp(pos, l);
    }

    public VCExpr LabelNeg(string label, VCExpr e) {
      Contract.Requires(e != null);
      Contract.Requires(label != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      if (e.Equals(True)) {
        return e;  // don't bother putting negative labels around True (which will expose the True to further peephole optimizations)
      }
      return Function(LabelOp(false, label), e);
    }
    public VCExpr LabelPos(string label, VCExpr e) {
      Contract.Requires(e != null);
      Contract.Requires(label != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Function(LabelOp(true, label), e);
    }

    // Quantifiers

    public VCExpr Quantify(Quantifier quan, List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) {
      Contract.Requires(body != null);
      Contract.Requires(infos != null);
      Contract.Requires(cce.NonNullElements(triggers));
      Contract.Requires(cce.NonNullElements(vars));
      Contract.Requires(cce.NonNullElements(typeParams));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return new VCExprQuantifier(quan, typeParams, vars, triggers, infos, body);
    }

    public VCExpr Forall(List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) {
      Contract.Requires(body != null);
      Contract.Requires(infos != null);
      Contract.Requires(cce.NonNullElements(triggers));
      Contract.Requires(cce.NonNullElements(vars));
      Contract.Requires(cce.NonNullElements(typeParams));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Quantify(Quantifier.ALL, typeParams, vars, triggers, infos, body);
    }
    public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, int weight, VCExpr body) {
      Contract.Requires(body != null);
      Contract.Requires(qid != null);
      Contract.Requires(cce.NonNullElements(triggers));
      Contract.Requires(cce.NonNullElements(vars));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      QKeyValue kv = null;
      if (0 <= weight) {
        kv = new QKeyValue(Token.NoToken, "weight", new List<object>() { new LiteralExpr(Token.NoToken, BigNum.FromInt(0)) }, null);
      }
      return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
                            triggers, new VCQuantifierInfos(qid, -1, false, kv), body);
    }
    public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body) {
      Contract.Requires(body != null);
      Contract.Requires(cce.NonNullElements(triggers));
      Contract.Requires(cce.NonNullElements(vars));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
                            triggers, new VCQuantifierInfos(null, -1, false, null), body);
    }
    public VCExpr Forall(VCExprVar var, VCTrigger trigger, VCExpr body) {
      Contract.Requires(body != null);
      Contract.Requires(trigger != null);
      Contract.Requires(var != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Forall(HelperFuns.ToNonNullList(var), HelperFuns.ToNonNullList(trigger), body);
    }
    public VCExpr Exists(List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) {
      Contract.Requires(body != null);
      Contract.Requires(infos != null);
      Contract.Requires(cce.NonNullElements(triggers));
      Contract.Requires(cce.NonNullElements(vars));
      Contract.Requires(cce.NonNullElements(typeParams));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Quantify(Quantifier.EX, typeParams, vars, triggers, infos, body);
    }
    public VCExpr Exists(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body) {
      Contract.Requires(body != null);
      Contract.Requires(cce.NonNullElements(triggers));
      Contract.Requires(cce.NonNullElements(vars));
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Quantify(Quantifier.EX, new List<TypeVariable/*!*/>(), vars,
                      triggers, new VCQuantifierInfos(null, -1, false, null), body);
    }
    public VCExpr Exists(VCExprVar var, VCTrigger trigger, VCExpr body) {
      Contract.Requires(body != null);
      Contract.Requires(trigger != null);
      Contract.Requires(var != null);
      Contract.Ensures(Contract.Result<VCExpr>() != null);
      return Exists(HelperFuns.ToNonNullList(var), HelperFuns.ToNonNullList(trigger), body);
    }

    public VCTrigger Trigger(bool pos, List<VCExpr> exprs) {
      Contract.Requires(cce.NonNullElements(exprs));
      Contract.Ensures(Contract.Result<VCTrigger>() != null);
      return new VCTrigger(pos, exprs);
    }

    public VCTrigger Trigger(bool pos, params VCExpr[] exprs) {
      Contract.Requires(exprs != null);
      Contract.Requires((Contract.ForAll(0, exprs.Length, i => exprs[i] != null)));
      Contract.Ensures(Contract.Result<VCTrigger>() != null);
      return Trigger(pos, HelperFuns.ToNonNullList(exprs));
    }

    // Reference to a bound or free variable

    public VCExprVar Variable(string name, Type type) {
      Contract.Requires(type != null);
      Contract.Requires(name != null);
      Contract.Ensures(Contract.Result<VCExprVar>() != null);
      return new VCExprVar(name, type);
    }
  }
}

namespace Microsoft.Boogie.VCExprAST {

  public class HelperFuns {
    public static bool SameElements(IEnumerable a, IEnumerable b) {
      Contract.Requires(b != null);
      Contract.Requires(a != null);
      IEnumerator ia = a.GetEnumerator();
      IEnumerator ib = b.GetEnumerator();
      while (true) {
        if (ia.MoveNext()) {
          if (ib.MoveNext()) {
            if (!cce.NonNull(ia.Current).Equals(ib.Current))
              return false;
          } else {
            return false;
          }
        } else {
          return !ib.MoveNext();
        }
      }
    }

    public static int PolyHash(int init, int factor, IEnumerable a) {
      Contract.Requires(a != null);
      int res = init;
      foreach (object x in a)
        res = res * factor + (cce.NonNull(x)).GetHashCode();
      return res;
    }

    public static List<T> ToList<T>(IEnumerable<T> l) {
      Contract.Requires(l != null);
      Contract.Ensures(Contract.Result<List<T>>() != null);
      List<T>/*!*/ res = new List<T>();
      foreach (T x in l)
        res.Add(x);
      return res;
    }

    public static List<Type> ToTypeSeq(VCExpr[] exprs, int startIndex) {
      Contract.Requires(exprs != null);
      Contract.Requires((Contract.ForAll(0, exprs.Length, i => exprs[i] != null)));
      Contract.Ensures(Contract.Result<List<Type>>() != null);
      List<Type>/*!*/ res = new List<Type>();
      for (int i = startIndex; i < exprs.Length; ++i)
        res.Add(cce.NonNull(exprs[i]).Type);
      return res;
    }

    public static List<T/*!*/>/*!*/ ToNonNullList<T>(params T[] args) where T : class {
      Contract.Requires(args != null);
      List<T/*!*/>/*!*/ res = new List<T>(args.Length);
      foreach (T t in args)
        res.Add(cce.NonNull(t));
      return res;
    }

    public static IDictionary<A, B> Clone<A, B>(IDictionary<A, B> dict) {
      Contract.Requires(dict != null);
      Contract.Ensures(Contract.Result<IDictionary<A, B>>() != null);
      IDictionary<A, B> res = new Dictionary<A, B>(dict.Count);
      foreach (KeyValuePair<A, B> pair in dict)
        res.Add(pair);
      return res;
    }
  }

  [ContractClassFor(typeof(VCExpr))]
  public abstract class VCExprContracts : VCExpr {
    public override Type Type {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);
        throw new NotImplementedException();
      }

    }
    public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
      Contract.Requires(visitor != null);
      throw new NotImplementedException();
    }
  }

  [ContractClass(typeof(VCExprContracts))]
  public abstract class VCExpr {
    public abstract Type Type {
      get;
    }

    public abstract Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg);

    [Pure]
    public override string ToString() {
      Contract.Ensures(Contract.Result<string>() != null);
      StringWriter sw = new StringWriter();
      VCExprPrinter printer = new VCExprPrinter();
      printer.Print(this, sw);
      return cce.NonNull(sw.ToString());
    }
  }

  /////////////////////////////////////////////////////////////////////////////////
  // Literal expressions

  public class VCExprLiteral : VCExpr {
    private readonly Type LitType;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(LitType != null);
    }

    public override Type Type {
      get {
        return LitType;
      }
    }
    internal VCExprLiteral(Type type) {
      Contract.Requires(type != null);
      this.LitType = type;
    }
    public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      return visitor.Visit(this, arg);
    }
  }

  public class VCExprIntLit : VCExprLiteral {
    public readonly BigNum Val;
    internal VCExprIntLit(BigNum val)
      : base(Type.Int) {
      this.Val = val;
    }
    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprIntLit)
        return Val == ((VCExprIntLit)that).Val;
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return Val.GetHashCode() * 72321;
    }
  }

  public class VCExprRealLit : VCExprLiteral {
    public readonly BigDec Val;
    internal VCExprRealLit(BigDec val)
      : base(Type.Real) {
      this.Val = val;
    }
    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprRealLit)
        return Val == ((VCExprRealLit)that).Val;
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return Val.GetHashCode() * 72321;
    }
  }

  /////////////////////////////////////////////////////////////////////////////////
  // Operator expressions with fixed arity
  [ContractClassFor(typeof(VCExprNAry))]
  public abstract class VCExprNAryContracts : VCExprNAry {
    public VCExprNAryContracts()
      : base(null) {
    }
    public override VCExpr this[int index] {
      get {
        Contract.Ensures(Contract.Result<VCExpr>() != null);
        throw new NotImplementedException();
      }
    }
  }

  [ContractClass(typeof(VCExprNAryContracts))]
  public abstract class VCExprNAry : VCExpr, IEnumerable<VCExpr/*!*/> {
    public readonly VCExprOp Op;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Op != null);
      Contract.Invariant(cce.NonNullElements(EMPTY_TYPE_LIST));
      Contract.Invariant(cce.NonNullElements(EMPTY_VCEXPR_LIST));
    }

    public int Arity {
      get {
        return Op.Arity;
      }
    }
    public int TypeParamArity {
      get {
        return Op.TypeParamArity;
      }
    }
    public int Length {
      get {
        return Arity;
      }
    }
    // the sub-expressions of the expression
    public abstract VCExpr/*!*/ this[int index] {
      get;
    }

    // the type arguments
    public abstract List<Type/*!*/>/*!*/ TypeArguments {
      get;
    }

    [Pure]
    [GlobalAccess(false)]
    [Escapes(true, false)]
    public IEnumerator<VCExpr/*!*/>/*!*/ GetEnumerator() {
      Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerator<VCExpr>>()));
      for (int i = 0; i < Arity; ++i)
        yield return this[i];
    }
    [Pure]
    [GlobalAccess(false)]
    [Escapes(true, false)]
    IEnumerator System.Collections.IEnumerable.GetEnumerator() {
      Contract.Ensures(Contract.Result<IEnumerator>() != null);
      for (int i = 0; i < Arity; ++i)
        yield return this[i];
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprNAry) {
        // we compare the subterms iteratively (not recursively)
        // to avoid stack overflows

        VCExprNAryEnumerator enum0 = new VCExprNAryEnumerator(this);
        VCExprNAryEnumerator enum1 = new VCExprNAryEnumerator((VCExprNAry)that);

        while (true) {
          bool next0 = enum0.MoveNext();
          bool next1 = enum1.MoveNext();
          if (next0 != next1)
            return false;
          if (!next0)
            return true;

          VCExprNAry nextExprNAry0 = enum0.Current as VCExprNAry;
          VCExprNAry nextExprNAry1 = enum1.Current as VCExprNAry;

          if ((nextExprNAry0 == null) != (nextExprNAry1 == null))
            return false;
          if (nextExprNAry0 != null && nextExprNAry1 != null) {
            if (!nextExprNAry0.Op.Equals(nextExprNAry1.Op))
              return false;
          } else {
            if (!cce.NonNull(enum0.Current).Equals(enum1.Current))
              return false;
          }
        }
      }
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return HelperFuns.PolyHash(Op.GetHashCode() * 123 + Arity * 61521,
                                 3, this);
    }

    internal VCExprNAry(VCExprOp op) {
      Contract.Requires(op != null);
      this.Op = op;
    }
    public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      return visitor.Visit(this, arg);
    }
    public Result Accept<Result, Arg>(IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      Contract.Requires(visitor != null);
      return Op.Accept(this, visitor, arg);
    }

    internal static readonly List<Type/*!*/>/*!*/ EMPTY_TYPE_LIST = new List<Type/*!*/>();
    internal static readonly List<VCExpr/*!*/>/*!*/ EMPTY_VCEXPR_LIST = new List<VCExpr/*!*/>();

    public IEnumerable<VCExpr> UniformArguments
    {
      get
      {
        var enumerator = new VCExprNAryUniformOpEnumerator(this);
        while (enumerator.MoveNext()) {
          VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
          if (naryExpr == null || !naryExpr.Op.Equals(this.Op)) {
            yield return (VCExpr)enumerator.Current;
          }
        }
      }
    }
  }

  // We give specialised implementations for nullary, unary and binary expressions

  internal class VCExprNullary : VCExprNAry {
    private readonly Type ExprType;
    [ContractInvariantMethod]
    void loneinvariant() {
      Contract.Invariant(ExprType != null);
    }

    public override Type Type {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);
        return ExprType;
      }
    }
    public override VCExpr this[int index] {
      get {
        Contract.Ensures(Contract.Result<VCExpr>() != null);

        Contract.Assert(false);
        throw new cce.UnreachableException(); // no arguments
      }
    }

    // the type arguments
    public override List<Type/*!*/>/*!*/ TypeArguments {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
        return EMPTY_TYPE_LIST;
      }
    }

    internal VCExprNullary(VCExprOp op)
      : base(op) {
      Contract.Requires(op != null);
      Contract.Requires(op.Arity == 0 && op.TypeParamArity == 0);
      this.ExprType = op.InferType(EMPTY_VCEXPR_LIST, EMPTY_TYPE_LIST);
    }
  }

  internal class VCExprUnary : VCExprNAry {
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Argument != null);
      Contract.Invariant(ExprType != null);

    }

    private readonly VCExpr/*!*/ Argument;
    private readonly Type/*!*/ ExprType;
    public override Type/*!*/ Type {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);
        return ExprType;
      }
    }
    public override VCExpr/*!*/ this[int index] {
      get {
        Contract.Ensures(Contract.Result<VCExpr>() != null);

        Contract.Assume(index == 0);
        return Argument;
      }
    }

    // the type arguments
    public override List<Type/*!*/>/*!*/ TypeArguments {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
        return EMPTY_TYPE_LIST;
      }
    }

    internal VCExprUnary(VCExprOp op, List<VCExpr> arguments)
      : base(op) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(arguments));
      Contract.Requires(op.Arity == 1 && op.TypeParamArity == 0 && arguments.Count == 1);

      this.Argument = arguments[0];
      this.ExprType =
        op.InferType(arguments, EMPTY_TYPE_LIST);
    }

    internal VCExprUnary(VCExprOp op, VCExpr argument)
      : base(op) {
      Contract.Requires(argument != null);
      Contract.Requires(op != null);
      Contract.Requires(op.Arity == 1 && op.TypeParamArity == 0);

      this.Argument = argument;
      // PR: could be optimised so that the argument does
      // not have to be boxed in an array each time
      this.ExprType =
        op.InferType(HelperFuns.ToNonNullList(argument), EMPTY_TYPE_LIST);
    }
  }

  internal class VCExprBinary : VCExprNAry {
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Argument0 != null);
      Contract.Invariant(Argument1 != null);
      Contract.Invariant(ExprType != null);
    }

    private readonly VCExpr Argument0;
    private readonly VCExpr Argument1;
    private readonly Type ExprType;
    public override Type Type {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);
        return ExprType;
      }
    }
    public override VCExpr this[int index] {
      get {
        Contract.Ensures(Contract.Result<VCExpr>() != null);

        switch (index) {
          case 0:
            return Argument0;
          case 1:
            return Argument1;
          default: {
              Contract.Assert(false);
              throw new cce.UnreachableException();
            }
        }
      }
    }

    // the type arguments
    public override List<Type/*!*/>/*!*/ TypeArguments {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
        return EMPTY_TYPE_LIST;
      }
    }

    internal VCExprBinary(VCExprOp op, List<VCExpr> arguments)
      : base(op) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(arguments));
      Contract.Requires(op.Arity == 2 && op.TypeParamArity == 0 && arguments.Count == 2);

      this.Argument0 = arguments[0];
      this.Argument1 = arguments[1];
      this.ExprType = op.InferType(arguments, EMPTY_TYPE_LIST);
    }

    internal VCExprBinary(VCExprOp op, VCExpr argument0, VCExpr argument1)
      : base(op) {
      Contract.Requires(argument1 != null);
      Contract.Requires(argument0 != null);
      Contract.Requires(op != null);
      Contract.Requires(op.Arity == 2 && op.TypeParamArity == 0);
      this.Argument0 = argument0;
      this.Argument1 = argument1;
      // PR: could be optimised so that the arguments do
      // not have to be boxed in an array each time
      this.ExprType =
        op.InferType(HelperFuns.ToNonNullList(argument0, argument1),
                     EMPTY_TYPE_LIST);
    }
  }

  internal class VCExprMultiAry : VCExprNAry {
    private readonly List<VCExpr/*!*/>/*!*/ Arguments;
    private readonly List<Type/*!*/>/*!*/ TypeArgumentsAttr;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(cce.NonNullElements(Arguments));
      Contract.Invariant(cce.NonNullElements(TypeArgumentsAttr));
      Contract.Invariant(ExprType != null);
    }


    private readonly Type/*!*/ ExprType;
    public override Type/*!*/ Type {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);
        return ExprType;
      }
    }
    public override VCExpr/*!*/ this[int index] {
      get {
        Contract.Ensures(Contract.Result<VCExpr>() != null);

        Contract.Assume(index >= 0 && index < Arity);
        return cce.NonNull(Arguments)[index];
      }
    }

    // the type arguments
    public override List<Type/*!*/>/*!*/ TypeArguments {
      get {
        Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
        return TypeArgumentsAttr;
      }
    }

    internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments)
      : base(op) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(arguments));
      this.Arguments = arguments;
      this.TypeArgumentsAttr = EMPTY_TYPE_LIST;
      this.ExprType = op.InferType(arguments, TypeArgumentsAttr);
    }
    internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments, List<Type/*!*/>/*!*/ typeArguments)
      : base(op) {
      Contract.Requires(op != null);
      Contract.Requires(cce.NonNullElements(typeArguments));
      Contract.Requires(cce.NonNullElements(arguments));
      Contract.Requires(arguments.Count > 2 || typeArguments.Count > 0);
      Contract.Requires(op.Arity == arguments.Count);
      Contract.Requires(op.TypeParamArity == typeArguments.Count);
      this.Arguments = arguments;
      this.TypeArgumentsAttr = typeArguments;
      this.ExprType = op.InferType(arguments, typeArguments);
    }
  }

  /////////////////////////////////////////////////////////////////////////////////
  // The various operators available
  [ContractClass(typeof(VCExprOpContracts))]
  public abstract class VCExprOp {
    // the number of value parameters
    public abstract int Arity {
      get;
    }
    // the number of type parameters
    public abstract int TypeParamArity {
      get;
    }

    public abstract Type/*!*/ InferType(List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs);

    public virtual Result Accept<Result, Arg>(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      Contract.Requires(visitor != null);
      Contract.Requires(expr != null);
      VCExpressionGenerator.SingletonOp op;
      if (VCExpressionGenerator.SingletonOpDict.TryGetValue(this, out op)) {
        switch (op) {
          case VCExpressionGenerator.SingletonOp.NotOp:
            return visitor.VisitNotOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.EqOp:
            return visitor.VisitEqOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.NeqOp:
            return visitor.VisitNeqOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.AndOp:
            return visitor.VisitAndOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.OrOp:
            return visitor.VisitOrOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.ImpliesOp:
            return visitor.VisitImpliesOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.AddOp:
            return visitor.VisitAddOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.SubOp:
            return visitor.VisitSubOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.MulOp:
            return visitor.VisitMulOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.DivOp:
            return visitor.VisitDivOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.ModOp:
            return visitor.VisitModOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.RealDivOp:
            return visitor.VisitRealDivOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.PowOp:
            return visitor.VisitPowOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.LtOp:
            return visitor.VisitLtOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.LeOp:
            return visitor.VisitLeOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.GtOp:
            return visitor.VisitGtOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.GeOp:
            return visitor.VisitGeOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.SubtypeOp:
            return visitor.VisitSubtypeOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.Subtype3Op:
            return visitor.VisitSubtype3Op(expr, arg);
          case VCExpressionGenerator.SingletonOp.BvConcatOp:
            return visitor.VisitBvConcatOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.ToIntOp:
            return visitor.VisitToIntOp(expr, arg);
          case VCExpressionGenerator.SingletonOp.ToRealOp:
            return visitor.VisitToRealOp(expr, arg);
          default:
            Contract.Assert(false);
            throw new cce.UnreachableException();
        }
      } else {
        Contract.Assert(false);
        throw new cce.UnreachableException();
      }
    }
  }
  [ContractClassFor(typeof(VCExprOp))]
  abstract class VCExprOpContracts : VCExprOp {
    public override Type InferType(List<VCExpr> args, List<Type> typeArgs) {
      Contract.Requires(cce.NonNullElements(args));
      Contract.Requires(cce.NonNullElements(typeArgs));
      Contract.Ensures(Contract.Result<Type>() != null);

      throw new NotImplementedException();
    }
  }

  public class VCExprNAryOp : VCExprOp {
    private readonly Type OpType;
    private readonly int OpArity;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(OpType != null);
    }

    public override int Arity {
      get {
        return OpArity;
      }
    }
    public override int TypeParamArity {
      get {
        return 0;
      }
    }
    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
      //Contract.Requires(cce.NonNullElements(typeArgs));
      //Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<Type>() != null);
      return OpType;
    }

    internal VCExprNAryOp(int arity, Type type) {
      Contract.Requires(type != null);
      this.OpArity = arity;
      this.OpType = type;
    }
  }

  public class VCExprDistinctOp : VCExprNAryOp {
    internal VCExprDistinctOp(int arity)
      : base(arity, Type.Bool) {
    }
    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprDistinctOp)
        return Arity == ((VCExprDistinctOp)that).Arity;
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return Arity * 917632481;
    }
    public override Result Accept<Result, Arg>
           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      //Contract.Requires(expr != null);
      return visitor.VisitDistinctOp(expr, arg);
    }
  }

  public class VCExprLabelOp : VCExprOp {
    public override int Arity {
      get {
        return 1;
      }
    }
    public override int TypeParamArity {
      get {
        return 0;
      }
    }
    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
      //Contract.Requires(cce.NonNullElements(typeArgs));
      //Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<Type>() != null);
      return args[0].Type;
    }

    public readonly bool pos;
    public readonly string label;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(label != null);
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprLabelOp) {
        VCExprLabelOp/*!*/ thatOp = (VCExprLabelOp)that;
        return this.pos == thatOp.pos && this.label.Equals(thatOp.label);
      }
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return (pos ? 9817231 : 7198639) + label.GetHashCode();
    }

    internal VCExprLabelOp(bool pos, string l) {
      Contract.Requires(l != null);
      this.pos = pos;
      this.label = pos ? "+" + l : "@" + l;
    }
    public override Result Accept<Result, Arg>
           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      //Contract.Requires(expr != null);
      return visitor.VisitLabelOp(expr, arg);
    }
  }

  public class VCExprSelectOp : VCExprOp {
    private readonly int MapArity;
    private readonly int MapTypeParamArity;
    public override int Arity {
      get {
        return MapArity + 1;
      }
    }
    public override int TypeParamArity {
      get {
        return MapTypeParamArity;
      }
    }

    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
      //Contract.Requires(cce.NonNullElements(typeArgs));
      //Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<Type>() != null);
      MapType/*!*/ mapType = args[0].Type.AsMap;
      Contract.Assert(TypeParamArity == mapType.TypeParameters.Count);
      IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
      for (int i = 0; i < TypeParamArity; ++i)
        subst.Add(mapType.TypeParameters[i], typeArgs[i]);
      return mapType.Result.Substitute(subst);
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprSelectOp)
        return Arity == ((VCExprSelectOp)that).Arity &&
          TypeParamArity == ((VCExprSelectOp)that).TypeParamArity;
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return Arity * 1212481 + TypeParamArity * 298741;
    }

    internal VCExprSelectOp(int arity, int typeParamArity) {
      Contract.Requires(0 <= arity && 0 <= typeParamArity);
      this.MapArity = arity;
      this.MapTypeParamArity = typeParamArity;
    }
    public override Result Accept<Result, Arg>
           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      //Contract.Requires(expr != null);
      return visitor.VisitSelectOp(expr, arg);
    }
  }

  public class VCExprStoreOp : VCExprOp {
    private readonly int MapArity;
    private readonly int MapTypeParamArity;
    public override int Arity {
      get {
        return MapArity + 2;
      }
    }
    // stores never need explicit type parameters, because also the
    // rhs is a value argument
    public override int TypeParamArity {
      get {
        return MapTypeParamArity;
      }
    }

    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
      //Contract.Requires(cce.NonNullElements(typeArgs));
      //Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<Type>() != null);
      return args[0].Type;
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprStoreOp)
        return Arity == ((VCExprStoreOp)that).Arity;
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return Arity * 91361821;
    }

    internal VCExprStoreOp(int arity, int typeParamArity) {
      Contract.Requires(0 <= arity && 0 <= typeParamArity);
      this.MapArity = arity;
      this.MapTypeParamArity = typeParamArity;
    }
    public override Result Accept<Result, Arg>
           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      //Contract.Requires(expr != null);
      return visitor.VisitStoreOp(expr, arg);
    }
  }

  public class VCExprIfThenElseOp : VCExprOp {
    public override int Arity {
      get {
        return 3;
      }
    }
    public override int TypeParamArity {
      get {
        return 0;
      }
    }
    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
      //Contract.Requires(cce.NonNullElements(typeArgs));
      //Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<Type>() != null);
      return args[1].Type;
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprIfThenElseOp)
        return true;
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return 1;
    }

    internal VCExprIfThenElseOp() {
    }
    public override Result Accept<Result, Arg>
           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      //Contract.Requires(expr != null);
      return visitor.VisitIfThenElseOp(expr, arg);
    }
  }

  public class VCExprCustomOp : VCExprOp {
    public readonly string/*!*/ Name;
    int arity;
    public readonly Type/*!*/ Type;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Name != null);
      Contract.Invariant(Type != null);
    }

    public VCExprCustomOp(string/*!*/ name, int arity, Type/*!*/ type) {
      Contract.Requires(name != null);
      Contract.Requires(type != null);
      this.Name = name;
      this.arity = arity;
      this.Type = type;
    }
    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      VCExprCustomOp t = that as VCExprCustomOp;
      if (t == null)
        return false;
      return this.Name == t.Name && this.arity == t.arity && this.Type == t.Type;
    }
    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override int GetHashCode() {
      int h = Name.GetHashCode();
      h = 7823 * h + arity;
      h = 7823 * h + Type.GetHashCode();
      return h;
    }
    public override int Arity {
      get {
        return arity;
      }
    }
    public override int TypeParamArity {
      get {
        return 0;
      }
    }
    public override Type/*!*/ InferType(List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {
      //Contract.Requires((cce.NonNullElements(args)));
      //Contract.Requires((cce.NonNullElements(typeArgs)));
      Contract.Ensures(Contract.Result<Type>() != null);
      return Type;
    }
    public override Result Accept<Result, Arg>
           (VCExprNAry/*!*/ expr, IVCExprOpVisitor<Result, Arg>/*!*/ visitor, Arg arg) {
      //Contract.Requires(expr != null);
      //Contract.Requires(visitor != null);
      return visitor.VisitCustomOp(expr, arg);
    }
  }

  /////////////////////////////////////////////////////////////////////////////////
  // Bitvector operators

  public class VCExprBvOp : VCExprOp {
    public readonly int Bits;

    public override int Arity {
      get {
        return 1;
      }
    }
    public override int TypeParamArity {
      get {
        return 0;
      }
    }
    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
      //Contract.Requires(cce.NonNullElements(typeArgs));
      //Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<Type>() != null);
      return Type.GetBvType(Bits);
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprBvOp)
        return this.Bits == ((VCExprBvOp)that).Bits;
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return Bits * 81748912;
    }

    internal VCExprBvOp(int bits) {
      this.Bits = bits;
    }
    public override Result Accept<Result, Arg>
           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      //Contract.Requires(expr != null);
      return visitor.VisitBvOp(expr, arg);
    }
  }

  public class VCExprBvExtractOp : VCExprOp {
    public readonly int Start;
    public readonly int End;
    public readonly int Total;  // the number of bits from which the End-Start bits are extracted

    public override int Arity {
      get {
        return 1;
      }
    }
    public override int TypeParamArity {
      get {
        return 0;
      }
    }
    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
      //Contract.Requires(cce.NonNullElements(typeArgs));
      //Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<Type>() != null);
      return Type.GetBvType(End - Start);
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprBvExtractOp) {
        VCExprBvExtractOp/*!*/ thatExtract = (VCExprBvExtractOp)that;
        return this.Start == thatExtract.Start && this.End == thatExtract.End && this.Total == thatExtract.Total;
      }
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return Start * 81912 + End * 978132 + Total * 571289;
    }

    internal VCExprBvExtractOp(int start, int end, int total) {
      Contract.Requires(0 <= start && start <= end && end <= total);
      this.Start = start;
      this.End = end;
      this.Total = total;
    }
    public override Result Accept<Result, Arg>
           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      //Contract.Requires(expr != null);
      return visitor.VisitBvExtractOp(expr, arg);
    }
  }

  public class VCExprBvConcatOp : VCExprOp {
    public readonly int LeftSize;
    public readonly int RightSize;

    public override int Arity {
      get {
        return 2;
      }
    }
    public override int TypeParamArity {
      get {
        return 0;
      }
    }
    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
      //Contract.Requires(cce.NonNullElements(typeArgs));
      //Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<Type>() != null);
      return Type.GetBvType(args[0].Type.BvBits + args[1].Type.BvBits);
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprBvConcatOp) {
        VCExprBvConcatOp thatConcat = (VCExprBvConcatOp)that;
        return this.LeftSize == thatConcat.LeftSize && this.RightSize == thatConcat.RightSize;
      }
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return LeftSize * 81912 + RightSize * 978132;
    }

    internal VCExprBvConcatOp(int leftSize, int rightSize) {
      Contract.Requires(0 <= leftSize && 0 <= rightSize);
      this.LeftSize = leftSize;
      this.RightSize = rightSize;
    }
    public override Result Accept<Result, Arg>
           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      //Contract.Requires(expr != null);
      return visitor.VisitBvConcatOp(expr, arg);
    }
  }

  /////////////////////////////////////////////////////////////////////////////////
  // References to user-defined Boogie functions

  public class VCExprBoogieFunctionOp : VCExprOp {
    public readonly Function Func;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Func != null);
    }


    public override int Arity {
      get {
        return Func.InParams.Count;
      }
    }
    public override int TypeParamArity {
      get {
        return Func.TypeParameters.Count;
      }
    }
    public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
      //Contract.Requires(cce.NonNullElements(typeArgs));
      //Contract.Requires(cce.NonNullElements(args));
      Contract.Ensures(Contract.Result<Type>() != null);
      Contract.Assert(TypeParamArity == Func.TypeParameters.Count);
      if (TypeParamArity == 0)
        return cce.NonNull(Func.OutParams[0]).TypedIdent.Type;
      IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>(TypeParamArity);
      for (int i = 0; i < TypeParamArity; ++i)
        subst.Add(Func.TypeParameters[i], typeArgs[i]);
      return cce.NonNull(Func.OutParams[0]).TypedIdent.Type.Substitute(subst);
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprBoogieFunctionOp)
        return this.Func.Equals(((VCExprBoogieFunctionOp)that).Func);
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return Func.GetHashCode() + 18731;
    }

    // we require that the result type of the expression is specified, because we
    // do not want to perform full type inference at this point
    internal VCExprBoogieFunctionOp(Function func) {
      Contract.Requires(func != null);
      this.Func = func;
    }
    public override Result Accept<Result, Arg>
           (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      //Contract.Requires(expr != null);
      return visitor.VisitBoogieFunctionOp(expr, arg);
    }
  }

  /////////////////////////////////////////////////////////////////////////////////
  // Binders (quantifiers and let-expressions). We introduce our own class for
  // term variables, but use the Boogie-AST class for type variables

  public class VCExprVar : VCExpr {
    // the name of the variable. Note that the name is not used for comparison,
    // i.e., there can be two distinct variables with the same name
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Name != null);
      Contract.Invariant(VarType != null);
    }

    public readonly string/*!*/ Name;
    private readonly Type/*!*/ VarType;
    public override Type/*!*/ Type {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);
        return VarType;
      }
    }

    internal VCExprVar(string name, Type type) {
      Contract.Requires(type != null);
      Contract.Requires(name != null);
      this.Name = name;
      this.VarType = type;
    }
    public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      return visitor.Visit(this, arg);
    }
  }

  public class VCExprConstant : VCExprVar
  {
      internal VCExprConstant(string name, Type type) : base(name,type) {
      Contract.Requires(type != null);
      Contract.Requires(name != null);
    }
  }

  public abstract class VCExprBinder : VCExpr {
    public readonly VCExpr/*!*/ Body;
    public readonly List<TypeVariable/*!*/>/*!*/ TypeParameters;
    public readonly List<VCExprVar/*!*/>/*!*/ BoundVars;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Body != null);
      Contract.Invariant(cce.NonNullElements(TypeParameters));
      Contract.Invariant(cce.NonNullElements(BoundVars));
    }


    public override Type/*!*/ Type {
      get {
        Contract.Ensures(Contract.Result<Type>() != null);

        return Body.Type;
      }
    }

    internal VCExprBinder(List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ boundVars, VCExpr body) {
      Contract.Requires(body != null);
      Contract.Requires(cce.NonNullElements(boundVars));
      Contract.Requires(cce.NonNullElements(typeParams));
      Contract.Requires(boundVars.Count + typeParams.Count > 0);     // only nontrivial binders ...
      this.TypeParameters = typeParams;
      this.BoundVars = boundVars;
      this.Body = body;
    }
  }

  public class VCTrigger {
    public readonly bool Pos;
    public readonly List<VCExpr/*!*/>/*!*/ Exprs;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Exprs != null);
    }


    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCTrigger) {
        VCTrigger/*!*/ thatTrigger = (VCTrigger)that;
        return this.Pos == thatTrigger.Pos &&
          HelperFuns.SameElements(this.Exprs, thatTrigger.Exprs);
      }
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return (Pos ? 913821 : 871334) +
             HelperFuns.PolyHash(123, 7, this.Exprs);
    }

    public VCTrigger(bool pos, List<VCExpr> exprs) {
      Contract.Requires(cce.NonNullElements(exprs));
      this.Pos = pos;
      this.Exprs = exprs;
    }
  }

  public class VCQuantifierInfos {
    public readonly string qid;
    public readonly int uniqueId;
    public readonly bool bvZ3Native;
    public QKeyValue attributes;

    public VCQuantifierInfos(string qid, int uniqueId, bool bvZ3Native, QKeyValue attributes) {
      this.qid = qid;
      this.uniqueId = uniqueId;
      this.bvZ3Native = bvZ3Native;
      this.attributes = attributes;
    }
  }

  public enum Quantifier {
    ALL,
    EX
  };

  public class VCExprQuantifier : VCExprBinder {
    public readonly Quantifier Quan;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(Infos != null);
      Contract.Invariant(cce.NonNullElements(Triggers));
    }


    public readonly List<VCTrigger/*!*/>/*!*/ Triggers;
    public readonly VCQuantifierInfos Infos;

    // Equality is /not/ modulo bound renaming at this point
    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprQuantifier) {
        VCExprQuantifier/*!*/ thatQuan = (VCExprQuantifier)that;
        return this.Quan == thatQuan.Quan &&
               HelperFuns.SameElements(this.Triggers, thatQuan.Triggers) &&
               HelperFuns.SameElements(this.TypeParameters, thatQuan.TypeParameters) &&
               HelperFuns.SameElements(this.BoundVars, thatQuan.BoundVars) &&
               this.Body.Equals(thatQuan.Body);
      }
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return Quan.GetHashCode() +
        HelperFuns.PolyHash(973219, 7, TypeParameters) +
        HelperFuns.PolyHash(998431, 9, BoundVars) +
        HelperFuns.PolyHash(123, 11, Triggers);
    }

    internal VCExprQuantifier(Quantifier kind, List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ boundVars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body)
      : base(typeParams, boundVars, body) {
      Contract.Requires(body != null);
      Contract.Requires(infos != null);
      Contract.Requires(cce.NonNullElements(triggers));
      Contract.Requires(cce.NonNullElements(boundVars));
      Contract.Requires(cce.NonNullElements(typeParams));

      this.Quan = kind;
      this.Triggers = triggers;
      this.Infos = infos;
    }
    public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      return visitor.Visit(this, arg);
    }
  }

  /////////////////////////////////////////////////////////////////////////////////
  // Let-Bindings

  public class VCExprLetBinding {
    public readonly VCExprVar V;
    public readonly VCExpr E;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(V != null);
      Contract.Invariant(E != null);
    }


    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprLetBinding) {
        VCExprLetBinding/*!*/ thatB = (VCExprLetBinding)that;
        return this.V.Equals(thatB.V) && this.E.Equals(thatB.E);
      }
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return V.GetHashCode() * 71261 + E.GetHashCode();
    }

    internal VCExprLetBinding(VCExprVar v, VCExpr e) {
      Contract.Requires(e != null);
      Contract.Requires(v != null);
      this.V = v;
      this.E = e;
      Contract.Assert(v.Type.Equals(e.Type));
    }
  }

  public class VCExprLet : VCExprBinder, IEnumerable<VCExprLetBinding/*!*/> {
    private readonly List<VCExprLetBinding/*!*/>/*!*/ Bindings;
    [ContractInvariantMethod]
    void ObjectInvariant() {
      Contract.Invariant(cce.NonNullElements(Bindings));

    }


    public int Length {
      get {
        return Bindings.Count;
      }
    }
    public VCExprLetBinding this[int index] {
      get {
        Contract.Ensures(Contract.Result<VCExprLetBinding>() != null);
        return Bindings[index];
      }
    }

    [Pure]
    [Reads(ReadsAttribute.Reads.Nothing)]
    public override bool Equals(object that) {
      if (Object.ReferenceEquals(this, that))
        return true;
      if (that is VCExprLet) {
        VCExprLet/*!*/ thatLet = (VCExprLet)that;
        return this.Body.Equals(thatLet.Body) &&
               HelperFuns.SameElements(this, (VCExprLet)that);
      }
      return false;
    }
    [Pure]
    public override int GetHashCode() {
      return HelperFuns.PolyHash(Body.GetHashCode(), 9, Bindings);
    }

    [Pure]
    [GlobalAccess(false)]
    [Escapes(true, false)]
    public IEnumerator<VCExprLetBinding/*!*/>/*!*/ GetEnumerator() {
      Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerator<VCExprLetBinding>>()));
      return Bindings.GetEnumerator();
    }
    [Pure]
    [GlobalAccess(false)]
    [Escapes(true, false)]
    IEnumerator System.Collections.IEnumerable.GetEnumerator() {
      Contract.Ensures(Contract.Result<IEnumerator>() != null);
      return Bindings.GetEnumerator();
    }

    private static List<VCExprVar/*!*/>/*!*/ toSeq(List<VCExprLetBinding/*!*/>/*!*/ bindings) {
      Contract.Requires(cce.NonNullElements(bindings));
      Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
      List<VCExprVar> res = new List<VCExprVar>();
      foreach (VCExprLetBinding/*!*/ b in bindings)
        res.Add(b.V);
      return res;
    }

    internal VCExprLet(List<VCExprLetBinding/*!*/>/*!*/ bindings, VCExpr/*!*/ body)
      : base(new List<TypeVariable/*!*/>(), toSeq(bindings), body) {
      Contract.Requires(cce.NonNullElements(bindings));
      Contract.Requires(body != null);
      this.Bindings = bindings;
    }
    public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
      //Contract.Requires(visitor != null);
      return visitor.Visit(this, arg);
    }
  }
}